花了非常大的力气才搞明白第一个等式怎么理解。

αx ⊢ β
———————
⊢ Ξα(λx.β)

这个表达式的前提里已经没有项M了，所以它只能是在类型里，是马丁洛夫Π类型的形成规则。

至此，柯里的类型系统三大定律：

Ξα(KβM)对应纯粹的Π类型形成规则，注意这里的语义是完全对应的。

FαβM ≡ Ξα(BβM)，对应非依赖类型的项引入规则

αx ⊢ βM
———————
⊢ Fαβ(λx.M)

GαβM ≡ Ξα(SβM)，对应依赖类型的项引入规则

αx ⊢ βM
———————
⊢ Gα(λx.β)(λx.M)

++++++

这里的元变量符号包括αβ，是类型，M，是项。剩下的常量符号只有

Ξ 形式蕴含，包含全称，λ抽象，和蕴含！
KBS 三个纯计算组合子；

就这么点东西，把马丁洛夫类型论的核心概念，展示出来了。柯里真特么是狠人啊。

http://t.cn/AXGfusai