类型论中文术语翻译表(过时)
更新: 现在我认为应该使用香蕉空间的翻译,它对范畴论名词提供了系统性的翻译策略, 而我在这些基础上加入了类型论的术语。
下表已经过时且不再维护,但由于我有一些老文章使用了这个术语表,因此我不会删除它。
截止 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 | 良类型的 |