如何理解“证明即程序、结论公式即程序类型”？

[zzz6519003]

No description provided.

[SnowOnion]

常伴随着“证明即程序、结论公式即程序类型”的 slogan 闪亮登场的 Curry-Howard Correspondence（柯里-霍华德对应、CH 对应）可以以很多种“面貌”出现。
比如，自然演绎系统里的证明 与 Lambda 演算里的程序 的对应。
比如，希尔伯特风格公理系统里的证明 与 组合子演算里的程序 的对应。
它们都属于 CH 对应。

选定一种“面貌”之后，也可以考察 CH 对应的从简单到复杂的不同情形。
可以只考虑简单的情形而不妨碍体验到 CH 对应的美妙。
以上面举例的第一种“面貌”，自然演绎-Lambda 演算 的对应为例，可以只考虑 【直觉主义命题逻辑的蕴含词片段的自然演绎（有时记作 $Ni_{\to}$）】-【只含有基本类型和函数类型 T→T 的简单赋类 Lambda 演算（有时记作 $\lambda_\to$）】这一简单情形。

理解这个简单情形的一个办法是：读 Basic Proof Theory 第二版（ https://book.douban.com/subject/2006104/ ），从头撸到第 26 页的下图所示的例子，应该就明白噜。
如果用一句话描述该例子，我会说：(A->B->C)->(A->B)->A->C 这个 formula 在自然演绎里的如图所示的证明树，可被“无损地”表示为 λuvw.uw(vw)；而如果把 λuvw.uw(vw) 当成简单赋类 Lambda 演算里的项，对它做类型推断的结果恰好是 (A->B->C)->(A->B)->A->C 这个 type。
你是逻辑，是证明；我是程序，是类型。你对应我，我对应你。这就是 CH 对应（的一个简单情形）。

（注：我假定读者熟悉“箭头是右结合的”，所以我的文字描述，比起下图书上的例子，省略了更多括号）

[zzz6519003]

看不太懂 谢谢！

[SnowOnion]

略微修改了措辞。@zzz6519003