LEAN 赋型唯一性（Unique Typing）之 并行 κ 简化 （Parallel κ reduction）＞＞ₖ

        基于 κ 简化 （κ reduction） 的概念，引入了并行简化（Parallel Reduction）的概念，记 >>，而 并行K简化（Parallel K Reduction）记为 >>ₖ 。直观的意思是，如 e >>ₖ e'，意味这，表达式 e' 是由 表达式 e 中的多个部分同时通过 K 简化（K reduction）而来的。也就是说，在表达式e 中，存在多个部分是可以进行简化的，这些部分成为可简化部分（Redex），同时如果应用的简化规则是 K简化的话，即称为 可K简化部分（K - Redex）。表达式 e 中的 可K简化部分（K - Redex）通过K简化后，得到了 表达式 e'，那么，就有 表达式 e 并行K简化为 表达式 e'，记为 e >>ₖ e' ，如果所有的可K简化部分（K - Redex）都进行了K简化的话，称为完全简化（Complete Reduction），记 e >>>ₖ e' 。

        并行简化（Parallel Reduction）概念是由于 trait 和 martin lof 证明 beta 简化（β reduction）的 Church-Rosser 定理时引入的。这里，Mario 在证明 LEAN 的 Church-Rosser定理时，将并行简化概念扩展到 K 简化中，由此证明，在LEAN类型理论中，K 简化的 Church-Rosser 定理成立。即

       并行K简化（Parallel K Reduction，>>ₖ）在LEAN的定义如下：

        即，对于每一条K简化步进规则，都有一条对应的并行K简化（Parallel K Reduction，>>ₖ）规则，使得表达式的各可K简化部分都经过K简化，即为目标表达式（Target Expression）。

        如下引用：

        那么，并行K简化（Parallel K Reduction，>>ₖ）有以下属性，这是由其定义决定的，其证明过程只需通过对并行K简化的定义加以说明代入即可。

        以及，并行K简化的概念，⟫ₖ， 与 证据不区分（Proof Irrelevance）下的定义上相等（Definitional Equality），≡ₚ，所兼容。即

        其中的证明是，

        就是说，根据 证据不区分（Proof Relevance）关系，≡ₚ ，归纳分析 e₃ 的形态，同时 反推 e₃ >>ₖ e₂ 中能使 e₃ >>ₖ e₂成立的条件，以此进行归纳证明（Inductive proof）。

        详细的证明过程，原文有详细描述，这里就不赘述了。可看下图：

        同理可以证明：

        详细过程请查看原文。