类型论中文术语翻译表(过时)

更新: 现在我认为应该使用香蕉空间的翻译,它对范畴论名词提供了系统性的翻译策略, 而我在这些基础上加入了类型论的术语。

下表已经过时且不再维护,但由于我有一些老文章使用了这个术语表,因此我不会删除它。

截止 2020 年,类型论相关中文术语依然非常混乱。由于这个学科尚未像集合论、分析、代数等学科一样成为主流, 因此翻译尚有改进的可能。作者将从 2021 年开始自行采用这个术语翻译表进行类型论相关讨论,并尽可能地宣传这个翻译表。 本术语表除了包含类型论名词之外,也讨论相关学科的名词(如范畴论)。 统一中文翻译有诸多好处,可以避免英语世界中相同概念的不同名词导致的诸多问题。

本术语表接受任意形式的修改意见,但是不保证会采用。如果需要提意见或者需要术语表的源码,请联系作者。 本术语表将会参考『欧林猫的术语表』(被墙)。

英语 中文翻译 备注
AST (Abstract Syntax Tree) 语法树 不翻译『abstract』
Abstract rewriting system 抽象重写系统  
Bisimulation 互拟  
Boundary separation 边界分离 概念来自 XTT 类型论
Boundary 边界 概念来自立方类型论
Cartesian morphism 笛卡尔态射  
Cartesianness 笛卡尔性  
Category of contexts 语境的范畴  
Category 范畴  
Classifying category 划分范畴  
Cleavage 分裂  
Cloven fibration 裂纤维化  
Codependent type 逆依值类型  
Comprehension category 概括范畴  
Computation rule 计算规则  
Confluence 合流性  
Congruence 合同性  
Context comprehension 语境概括 参考
Context extension 语境延伸  
Context 语境 常见翻译『上下文』
Contextual category 语境范畴  
Contextuality 语境性  
Coslice category 逆切片范畴  
Democracy 民主性 来自 CwF 的讨论
Dependent type 依值类型 来自台译
Dependent product 依值积 这是范畴论的概念,不是类型论的
Display map 陈列态射 它实际上是一个态射
Dynamic scoping 动态作用域  
Elaboration 繁饰 参考
Elimination rule 消去规则  
Eliminator 消去子  
Extensionality 外延性  
Family of sets 集合族 参考日语汉字翻译
Family 参考日语汉字翻译
Fibration 纤维化  
Formation rule 形成规则  
Full subcategory 完全子范畴  
Full subcategory 完全子范畴  
Functor 函子  
Heterogeneous equality 异类型等价  
Heterogeneous unification 异类型合一化  
Higher inductive type 高阶归纳类型  
Homogeneous equality 同类型等价  
Identity type 相等类型  
Inductive type 归纳类型  
Inference rule 推理规则  
Introduction rule 构造规则 类似 Construction
John-Major equality 异类型等价 同 Heterogeneous equality
Lexical Scoping 词法作用域  
Metalanguage 元语言 不是 Meta Language
Metatheory 元理论  
Morphism 态射 也可以用「箭头」来称呼
Natural transformation 自然变换  
Naturality 自然性  
Object 对象  
Overcategory 切片范畴 同 Slice category
Polymorphism 多态  
Precategory 准范畴  
Preserve 保持  
Presheaf 准层 常见翻译『预层』
Projection 投影 从几何里征用的名词,参考
Pseudofunctor 仿函子  
Pullback 拉回  
Pushforward 推出  
Pushout 推出  
Quasicategory 拟范畴  
Reduction rule 化简规则  
Reduction 化简 其他翻译:规约
Regularity 规整性 出处
Representable presheaf 可表准层 常见翻译『可表函子』
Rewriting rule 重写规则  
Rewriting system 重写系统  
Scope 作用域  
Semantics 语义  
Sequent 相继式  
Slice category 切片范畴  
Split fibration 裂纤维化  
Subcategory 子范畴  
Substitution object (一组)替换  
Substitution (一组)替换  
Syntax 文法 又作『语法』,应该和 grammar 是可以互换的
Theory 理论  
Topos theory 意象学  
Topos 意象  
Type check 类型检查 也作 Tyck
Type constructor 类型构造器  
Type-category 类型范畴 概念来自 Andrew Pitts 的书
Undercategory 逆切片范畴 同 Coslice category
Unification 合一化  
Univalence 宇宙等价  
Universe hierarchy 宇宙层级  
Universe polymorphism 宇宙多态  
Weakening 弱化  
Well-formed 良形式的  
Well-founded 良基的 参考
Well-typed 良类型的