术语表

读者可能注意到本文的标签中有规范二字,不必为此过于恐慌,因为我从来不期望别人遵守这些规范,我自己有时也不遵守。

这里提供一份(我所使用的)供对照的通用术语表,随博客更新而加长,按西文字母顺序排列。不确定的放到最前面并加 * 号。同一词义的不同词性,通常只列其中一个(若列动词则必定列现在时),列哪个视我当时使用到哪个词而定。

  • *circularity:循环定义、循环论证
  • *identity type:相等类型
  • *intensional type theory:内涵类型论
  • *strictly positive:严格为正
  • -ary:(运算符的)元、(数字表示方式的)进制
  • Boolean:布尔(的)
  • Cantor's theorem:康托尔定理
  • Curry-Howard correspondence:柯里-霍华德对应
  • Russell's paradox:罗素悖论
  • absurd:荒谬
  • apply/application:应用
  • argument:参数
  • arrow:箭头
  • assocative:结合(的)
  • bijection:双射
  • binary tree:二叉树
  • category:范畴
  • class:类
  • co-:余(表对偶);共(表共同)、并(表同时)
  • concatenate:串接
  • conjunction:合取
  • connective:连接词
  • constructor:构造器
  • contradiction:矛盾
  • data:数据
  • definition:定义
  • dependent:依赖(的)
  • diagonal:对角
  • disjunction:析取
  • double negation:双重否定
  • eliminate:消去
  • embed:嵌入
  • epic:上的
  • explicit:显式(的)
  • faithful:忠实(的函子)
  • function:函数
  • functor:函子
  • goal:目标
  • height:(树的)高度
  • hierarchy:等级系统
  • higher-:高阶(的)
  • homomorphism:同态
  • identity:恒等(函数、箭头等);(群的)幺元
  • implicit:隐式(的)
  • imply:蕴涵
  • index:索引
  • induction:归纳(法)
  • inductive:归纳(的)
  • injection:单射
  • insertion sort:插入排序
  • internal node:非叶子节点
  • intuitionistic:直觉(的)
  • inverse:逆
  • involution:对合
  • isomorphism:同构
  • lambda calculus:lambda 演算
  • law of excluded middle:排中律
  • leaf:叶子(节点)
  • matrix:矩阵
  • monic:单的
  • morphism:箭头(注意我不使用态射一词)
  • named:具名(的)
  • negation:否定、反命题
  • numeral:数字字面量
  • object:(范畴中的)物件;(程序中的)对象
  • operator:运算符
  • pair:对
  • parameter:参数
  • pattern matching:模式匹配
  • polymorphism:多态
  • predicate:谓词
  • projection:射影
  • proof assistant:证明助理
  • proof:证明
  • property:性质
  • proposition:命题
  • pure:纯粹
  • quantifier:量词
  • record:记录
  • reduce:归约
  • reflexivity:自反(性)
  • result type:结果类型
  • reverse:翻转
  • structural recursion:结构化递归
  • subtype:子类型
  • sum type:和类型
  • surjection:满射
  • terminate/halt:停机
  • term:项
  • theorem prover:定理证明器
  • total:完全(的)
  • tuple:元组
  • type synonym:类型别名
  • typechecker:类型检查器
  • typecheck:(通过)类型检查
  • universe:全集
  • untyped:无类型(的)
  • vector:向量
  • ZFC:策梅洛-弗兰克尔-选择公理,策-弗公理