中文译名：A-正规形式．

中文译名： 抽象语法 （见 抽象语法 ）．

中文译名： 实无穷 （见 潜无穷与实无穷 ）．

中文译名：仿射类型．

中文译名：代数数据类型．

中文译名：代数作用．

中文译名：代数作用处理器．

中文译名： 算法可靠性 （见 可靠与完备 ）．

中文译名：公理．

中文译名：Backus–Naur 表示法．

中文译名：基准情况．

中文译名： β 规约 （见 求值策略、规约策略与合流性 ）．

中文译名：双向类型检查．

中文译名：大步操作语义．

中文译名：二元关系．

中文译名：结合力．

中文译名： 底类型 （见 显式错误规则与 Kotlin 的底类型 ）．

中文译名： 绑定出现 （见 求值策略、规约策略与合流性 ）．

中文译名：按名调用．

中文译名： 按需调用 （见 求值策略、规约策略与合流性 ）．

中文译名： 按值调用 （见 求值策略、规约策略与合流性 ）．

中文译名： 典范形式 （见 典范形式 ）．

中文译名： 分类讨论 （见 确定性 ）．

中文译名： 子节点 （见 树的基本术语 ）．

中文译名： 循环论证 （见 合法的归纳假设与循环论证 ）．

中文译名： 闭项 （见 类型检查、类型推理与类型居留性 ）．

中文译名： 封闭条件 （见 词项的集合 ）．

中文译名： 余归纳 （见 什么是归纳 ）．

中文译名：编译期错误．

中文译名： 完备 （见 可靠与完备 ）．

中文译名： 完备性 （见 可靠与完备 ）．

中文译名：组合性．

中文译名：计算规则．

中文译名：结论．

中文译名： 合流性 （见 求值策略、规约策略与合流性 ）．

中文译名：同余规则．

中文译名：构造子．

中文译名： 语境 （见 类型与类型判断 ）．

中文译名：语境语义．

中文译名：续延传递风格．

中文译名：收缩规则．

中文译名： 共递归 （见 什么是归纳 ）．

中文译名：可判定．

中文译名： 演绎推理 （见 什么是归纳 ）．

中文译名：定界续延．

中文译名：指称语义．

中文译名：依值类型．

中文译名： 深度 （见 大小与深度 ）．

中文译名：推导．

中文译名：推导树．

中文译名： 后代 （见 树的基本术语 ）．

中文译名：脱糖．

中文译名： 确定性 （见 确定性 ）．

中文译名： 动态类型语言 （见 静态类型与动态类型 ）．

中文译名： 边 （见 树的基本术语 ）．

中文译名：作用．

中文译名：作用行．

中文译名：作用系统．

中文译名：求值语境．

中文译名：求值关系．

中文译名： 求值策略 （见 求值策略、规约策略与合流性 ）．

中文译名： 求值器与一步规约一致 （见 求值器与一步规约一致 ）．

中文译名： 最小性子句 （见 词项的集合 ）．

中文译名：一等续延．

中文译名：形式文法．

中文译名：形式化．

中文译名： 自由出现 （见 求值策略、规约策略与合流性 ）．

中文译名：广义代数数据类型．

中文译名：文法．

中文译名：高阶类型构造子．

中文译名：高秩多态类型．

中文译名：卫生性．

中文译名： 不良类型 （见 良类型 ）．

中文译名： 直接子项 （见 直接子项与真子项 ）．

中文译名： 归纳假设 （见 归纳假设 ）．

中文译名： 推导上的归纳 （见 规则归纳法 ）．

中文译名：归纳情况．

中文译名：归纳类型．

中文译名：推导规则．

中文译名： 居留者 （见 类型检查、类型推理与类型居留性 ）．

中文译名： 实例 （见 元变量 ）．

中文译名：中间表示．

中文译名： 内部节点 （见 树的基本术语 ）．

中文译名： 反演 （见 反演 ）．

中文译名： 判断 （见 箭头 $⟶$ 的读法与用法 ）．

中文译名： λ 演算 （见 求值策略、规约策略与合流性 ）．

中文译名： 叶子 （见 树的基本术语 ）．

中文译名： 最小 （见 词项的集合 ）．

中文译名：线性类型．

中文译名： 宽松相等 （见 JavaScript 隐式转换与相等三角图 ）．

中文译名： 元语言 （见 对象语言与元语言 ）．

中文译名： 元变量 （见 元变量 ）．

中文译名：单子．

中文译名：单态化．

中文译名： 多步规约 （见 多步规约 ）．

中文译名：自然演绎．

中文译名：自然语言．

中文译名：自然语义．

中文译名： 节点 （见 树的基本术语 ）．

中文译名：非终结符号．

中文译名： 正规形式 （见 正规形式与受阻 ）．

中文译名： 数值 （见 值与数值 ）．

中文译名： 对象语言 （见 对象语言与元语言 ）．

中文译名：缩进与换行规则．

中文译名： 一步规约 （见 一步规约 ）．

中文译名：操作语义．

中文译名： 有序树 （见 树的基本术语 ）．

中文译名： 父节点 （见 树的基本术语 ）．

中文译名： 解析 （见 抽象语法 ）．

中文译名：部分应用．

中文译名：部分求值．

中文译名：偏函数．

中文译名：模式匹配．

中文译名： 潜无穷 （见 潜无穷与实无穷 ）．

中文译名：前驱．

中文译名：前提．

中文译名： 保型 （见 保型 ）．

中文译名： 主类型 （见 类型检查、类型推理与类型居留性 ）．

中文译名：产生式．

中文译名： 生产性 （见 什么是归纳 ）．

中文译名：程序语言语义学．

中文译名：程序语言理论．

中文译名： 进展 （见 进展 ）．

中文译名： 真子项 （见 直接子项与真子项 ）．

中文译名：可规约项．

中文译名：可规约表达式．

中文译名： 规约 （见 一步规约 ）．

中文译名：规约规则．

中文译名：规约语义．

中文译名： 规约策略 （见 求值策略、规约策略与合流性 ）．

中文译名：精化类型．

中文译名： 自反传递闭包 （见 多步规约 ）．

中文译名： 自反性 （见 JavaScript 隐式转换与相等三角图 ）．

中文译名： 重写 （见 求值策略、规约策略与合流性 ）．

中文译名： 根 （见 树的基本术语 ）．

中文译名： 规则归纳法 （见 规则归纳法 ）．

中文译名：运行时．

中文译名：运行时错误．

中文译名：语义域．

中文译名：语义．

中文译名：附加条件．

中文译名：简单类型 λ 演算．

中文译名： 大小 （见 大小与深度 ）．

中文译名：小步操作语义．

中文译名： 可靠 （见 可靠与完备 ）．

中文译名：源到源编译．

中文译名：规格．

中文译名：多阶段编程．

中文译名：静态单赋值形式．

中文译名： 静态类型检查 （见 静态类型与动态类型 ）．

中文译名： 静态类型语言 （见 静态类型与动态类型 ）．

中文译名： 严格相等 （见 JavaScript 隐式转换与相等三角图 ）．

中文译名： 结构归纳法 （见 结构归纳原理 ）．

中文译名：结构递归．

中文译名：结构规则．

中文译名： 受阻 （见 正规形式与受阻 ）．

中文译名： 保型 （见 保型 ）．

中文译名： 子项 （见 直接子项与真子项 ）．

中文译名： 子树 （见 树的基本术语 ）．

中文译名： 子类型 （见 显式错误规则与 Kotlin 的底类型 ）．

中文译名： 子类型关系 （见 显式错误规则与 Kotlin 的底类型 ）．

中文译名：后继．

中文译名：语法．

中文译名： 语法树 （见 抽象语法 ）．

中文译名： 语法导向 （见 反演依赖语法导向 ）．

中文译名：F 系统．

中文译名： 词项 （见 词项的集合 ）．

中文译名：终结符号．

中文译名： 终止性 （见 求值策略、规约策略与合流性 ）．

中文译名：全函数．

中文译名：全函数式编程．

中文译名： 转移 （见 一步规约 ）．

中文译名： 转移关系 （见 一步规约 ）．

中文译名： 传递性 （见 JavaScript 隐式转换与相等三角图 ）．

中文译名： 树 （见 树的基本术语 ）．

中文译名： 推导符号 （见 类型与类型判断 ）．

中文译名： 类型 （见 类型与类型判断 ）．

中文译名： 类型检查 （见 类型检查、类型推理与类型居留性 ）．

中文译名：类型类．

中文译名： 类型推理 （见 类型检查、类型推理与类型居留性 ）．

中文译名： 类型居留性 （见 类型检查、类型推理与类型居留性 ）．

中文译名： 类型安全性 （见 类型安全 ）．

中文译名： 类型健全性 （见 类型安全 ）．

中文译名： 类型环境 （见 类型与类型判断 ）．

中文译名： 类型判断 （见 类型与类型判断 ）．

中文译名： 类型关系 （见 类型与类型判断 ）．

中文译名： 类型规则 （见 类型与类型判断 ）．

中文译名：未定义行为．

中文译名： 类型唯一 （见 类型唯一 ）．

中文译名：值化函数．

中文译名： 值 （见 值与数值 ）．

中文译名： 良基性 （见 归纳假设不只限于直接子项 ）．

中文译名： 良类型 （见 良类型 ）．