0
0

程序即证明

Typeof 发表于 1970年01月01日 08:00 | Hits: 909

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:α, Δ{′}/Γ, Γ{′} ⊢ (E F):beta, Δ, Δ{′}} →{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, w ⊢ xz(yz):gamma} →{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(α → β → γ) → (α → β) → α → γ这条定理。这正是为何很多人说「程序是类型的解答」:因为你用程序证明类型。

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

  • SK 组合子演算对应Hilbert 推理系统
  • 参数多态对应forall∀符号
  • 积类型对应wedge∧符号
  • 和类型对应vee∨符号
  • call/cc 对应排中律,或者说vdash ((alpha -> beta) -> alpha) -> alpha⊢ ((α → β) → α) → α

原文链接: http://typeof.net/2014/m/programs-are-proofs.html

0     0

评价列表(0)