Typeof.net

程序即证明

Curry-Howard 同构揭示出来的东西是十分深刻的。最近看了一些有关 lambda muλμ 演算的资料更加确信这一点,在设计这些扩展系统的时候首先设计的是类型与推理系统,然后才是形式语言。

比如说直觉命题逻辑的自然演绎,只用蕴含符号的系统如下:

  1. {} over {alpha vdash alpha} ~ I(/αα)I
  2. {Gamma, alpha vdash beta, Delta} over {Gamma vdash alpha -> beta, Delta} -> _ I(Γ,αβ, Δ/Γ αβ, Δ) I
  3. {Gamma vdash alpha -> beta, Delta quad Gamma' vdash alpha, Delta'} over {Gamma, Gamma' vdash beta, Delta, Delta'} -> _ E(Γ αβ, ΔΓ α,Δ /Γ,Γ β, Δ,Δ ) E

对比简单类型 Lambda 演算的类型指派:

  1. {} over {E:alpha vdash E:alpha} ~ I(/E:αE:α)I
  2. {Gamma, x:alpha vdash E:beta, Delta} over {Gamma vdash lambda x.E:alpha -> beta, Delta} -> _ I(Γ,x:αE:β, Δ/Γ λx.E:αβ, Δ) I
  3. {Gamma vdash E:alpha -> beta, Delta quad Gamma' vdash F:alpha, Delta'} over {Gamma, Gamma' vdash (E~F):beta, Delta, Delta'} -> _ E(Γ E:αβ, ΔΓ F:α,Δ /Γ,Γ (EF):β, Δ,Δ ) E

可以看出,每一条类型指派法则都对应一种 lambdaλ 演算的语言构造,而与之相对的推理法则则是构造证明的基本构造。因此,「lambdaλ 表达式」和「证明过程」也有同构关系。

比如著名的 K 组合子,其定义为

K = lambda x. lambda y. lambda z. xz(yz)K=λx.λy.λz.xz(yz)

其类型是 (alpha -> beta -> gamma) -> (alpha -> beta) -> alpha -> gamma(αβγ)(αβ)αγ

K 的类型指派过程是这样的:

{{{{} over {x : alpha -> beta -> gamma} u quad {} over {z : alpha} v} over {u, v vdash (xz) : beta -> gamma} -> _ E quad {{} over {y : alpha -> beta} w quad {} over {z : alpha} v} over {v, w vdash (yz) : beta} -> _ E} over {u, v, w vdash xz(yz):gamma} -> _ E} over {vdash lambda x. lambda y. lambda z. xz(yz) : (alpha -> beta -> gamma) -> (alpha -> beta) -> alpha -> gamma} -> _ I((((/x:αβγ)u(/z:α)v/u,v(xz):βγ) E((/y:αβ)w(/z:α)v/v,w(yz):β) E/u,v,wxz(yz):γ) E/λx.λy.λz.xz(yz):(αβγ)(αβ)αγ) I

来,让我们删掉冒号前的表达式:

{{{{} over {alpha -> beta -> gamma} u quad {} over {alpha} v} over {u, v vdash beta -> gamma} -> _ E quad {{} over {alpha -> beta} w quad {} over { alpha} v} over {v, w vdash beta} -> _ E} over {u, v, w vdash gamma} -> _ E} over {vdash (alpha -> beta -> gamma) -> (alpha -> beta) -> alpha -> gamma} -> _ I((((/αβγ)u(/α)v/u,vβγ) E((/αβ)w(/α)v/v,wβ) E/u,v,wγ) E/(αβγ)(αβ)αγ) I

这就是一条非常正常的自然演绎系统的逻辑推理,我们证明了 (alpha -> beta -> gamma) -> (alpha -> beta) -> alpha -> gamma(αβγ)(αβ)αγ 这条定理。这正是为何很多人说「程序是类型的解答」:因为你用程序证明类型。

另外,每个形式演算体系背后都对应着一套推理系统,下面就列个干净好了: