在注解 LEAN 对 Church-Rosser 定理证明前,为了更好地理解其证明过程,需要梳理一下,在LEAN的类型系统中,定义的各种符号,及其含义。同时,在前面章节中的证明过程,也为了证明过程的便利,定义了额外的一些符号。此篇文章,主要就是梳理目前为止,围绕着LEAN类型系统所衍生的符号定义。
一、推演规则(Inference Rule)
LEAN的类型理论,是通过自然推导(Natural Deduction)及其树形表示法(Tree-Notation),定义了一集(a collection of)推演规则(Inference Rules),用以,定义在该理论体系内,可使用的规则。即,前因后果,符合规则的前提(Premises),就有该规则的结果(Consequence)。由此,可以看作,整个LEAN类型系统,就是由这些最根本的因果关系组成的。
同时,推演规则(Inference Rules),根据其作用,分为 赋型规则,定义上相等规则,算法式定义上相等规则,等等,以此,规范系统中的不同内容。
其中,最主要的是定义了,依赖类型(Dependent Type)和 归纳类型(Inductive Type),包括其类型组成规则(Type Formation Rule),正规元素的构建规则(Introduction Rules),正规元素的使用规则(Elimination Rule),以及计算规则(Computation / Reduction / Equality Rules)。
在推演规则中,常见的符号有
1. Gamma 符号,Γ,表示(Representing)的是局部上下文(Local Context),也称假设(Assumptions),包括了一连串的变量及其类型信息,可以为空,以符号, · ,表示,也会用Delta符号,Δ,表示额外的假设。
2. Turnstile 符号,⊢,表示“蕴涵”(entail)的意思,即 该符号的左边 为 一连串的假设(Assumptions),其右边 为 基于左边的假设(Assumptions)下成立的表达式(Expression)。也就是,其 左边的假设 蕴涵了 右边的表达式(Expression)成立。即右表达式可以从左表达式推导出(The right one can be derivable from the left expressions)。
3. 冒号,:,是类型符号,表示,冒号右边表达式是左边表达式的类型,如 π1 的类型是 A ⊃ B。
4. 定义上相等(Definitional Equality)符号,≡,表示,符号两边的表达式,在定义上,是相等的。
5. 算法式定义上相等(Algorithm Defintional Equality)符号,⇔,表示,符号两边的表达式,可经过计算规则(Computation / Reduction / Equality Rules)相互转化,即计算后相等。
6. 等号,=,表示,符号两边的表达式相同。用 相等类型表达(Equality Type)。
7. 步进符号,⤳,如e ⤳ k,表示,表达式 e 使用了 一次(one step) LEAN定义了的一种(one of)转化规则,转化成表达式 k。此时,如果 k 与表达式 e' 是算法式定义上相等,那么 表达式e 和 表达式 e' 算法式定义上相等。
8. 多步进符号,⤳*,如 e ⤳* k,表示多次使用,即多步(multi-step),转换规则。
9. 小于等于符号,≤ ,出现于宇宙层次的定义上,表示,符号左边的层次低于或等于其右边。可以看作为定义在自然数上的小于等于操作符。
10. 类型等式符号,≃,用于表达符号两边的类型表达式,算法式定义上相等。
11. 定义符号,:=,用于表示,符号右边表达式是其左边名称的定义。
12. 函数符号,→,表示,符号左边为函数输入的类型,右边为函数输出的类型。
13. Lambda 符号,λ,表示,介绍新的变量(variable),即 变量binder,用于其后的表达式中。
14. Miu符号,μ,表示,介绍新的类型变量(Type variable),即 类型变量binder,用于其后的表达式中。
15. n-provability 符号,⊢ₙ ,即,表达式 e 在进行计算的过程中,赋型规则随着表达式 e 的形变,给每一步计算后的形变表达式 e‘ 进行赋型。此时,赋型规则的前提(Premises),利用归纳假设(Inductive Hypothese)提供的定义上相等关系,即 Γ ⊢ₙ α ≡ β,为其结果的赋型,即 Γ ⊢ₙ e:α,提供证明。那么就有, Γ ⊢ₙ α ≡ β => Γ ⊢ₙ e:α => Γ ⊢ₙ₊₁ α ≡ β => ... ,归纳推演的过程(Induction Proof)。
16. 表达式常态(normal form)符号,表达式上划线,表示,表达式满足 rec 常态及 lift 常态的要求。
17. K简化步进符号,⤳ₖ,表示通过K简化规则进行简化。同样的还有,其它简化规则的步进符号,以下角标来表示。以及,K简化多步进符号,⤳*ₖ 。
18. 证据不区分(Proof Relevance)的情况下,定义上相等(Definitional Equal)符号,≡ₚ ,即 对于具备证据不区分(Proof Relevance)关系的两表达式的简化规则(Reduction Rule)。
后面还有引入更多的符号,以便证明,如并行K简化符号,>>ₖ,等等。到时候介绍到对应的概念的再说。
说白了,符号是为了把对应的具体含义浓缩到一个符号来表示,以方便系统地证明或说明清楚某一事实,即符号系统。也就是,形、意,的关系。