柯里-霍华德同构

点击量:139 来源:www.baijia520.com

相继式演算

希尔伯特式证明是很难构造的。证明逻辑定理的更加直觉的方式是根岑的相继式演算。相继式演算以同希尔伯特式证明对应于组合子表达式一样的方式对应于λ-表达式程序。

直觉逻辑的蕴涵片段的相继式演算规则是:

Γ , α α {\displaystyle {{} \over \Gamma ,\alpha \vdash \alpha }} (公理)
Γ , α β Γ α β {\displaystyle {\Gamma ,\alpha \vdash \beta \over \Gamma \vdash \alpha \rightarrow \beta }} (Right →)
Γ α Σ , β γ Γ , Σ , α β γ {\displaystyle {\Gamma \vdash \alpha \qquad \qquad \Sigma ,\beta \vdash \gamma \over \Gamma ,\Sigma ,\alpha \rightarrow \beta \vdash \gamma }} (Left →)

Γ表示上下文,它是假设的集合。 Γ a {\displaystyle \Gamma \vdash a} 指示假定上下文Γ我们可以证明a。逻辑定理完全由其证明不需要假设的那些公式t组成的;就是说,t是一个定理,当且仅当我们可以证明 t {\displaystyle \vdash t} 。详情请参见相继式演算。

在相继式演算中的证明是树,它的根是我们要证明的定理,而它的叶子是公理模式实例;每个内部节点必须标记为要么Right →要么Left →,并且必须包含依据指定规则从子节点推出的一个公式。

相继式演算证明紧密的对应于λ-演算表达式。断言 Γ a {\displaystyle \Gamma \vdash a} 可以被解释为意味着,给定带有在Γ中列出类型的值,我们可以制造带有类型a的一个值。公理对应于带有新的无约束的类型的新变量介入。

Right →规则对应于函数抽象:

Γ , α β Γ α β {\displaystyle {\Gamma ,\alpha \vdash \beta \over \Gamma \vdash \alpha \rightarrow \beta }} (Right →)

什么时候我们能结论出某个程序Γ包含类型α→β的函数?在Γ加上类型α的一个值的时候,包含了足够的机械来允许我们制造类型β的一个值。

Left →规则对应于函数应用:

Γ α Σ , β γ Γ , Σ , α β γ {\displaystyle {\Gamma \vdash \alpha \qquad \Sigma ,\beta \vdash \gamma \over \Gamma ,\Sigma ,\alpha \rightarrow \beta \vdash \gamma }} (Left →)

如果我们可以制造类型α的一个值,并且如果给出类型β的一个值,我们还可以制造类型γ的一个值,则类型α→β的一个函数将允许我们制造类型γ的一个值:首先我们可以制造α,接着应用α→β函数于它,并接着使用结果的β值来制造类型γ的一个值。

例子

例如,(β→α)→(γ→β)→γ→α的相继式演算如下:

γ γ β β α α β , β α α L e f t γ , β α , γ β α β α , γ β γ α β α ( γ β ) γ α ( β α ) ( γ β ) γ α R i g h t R i g h t R i g h t L e f t {\displaystyle {\cfrac {\gamma \vdash \gamma \qquad {\cfrac {\beta \vdash \beta \qquad \alpha \vdash \alpha }{\beta ,\beta \rightarrow \alpha \vdash \alpha }}Left\rightarrow }{\qquad {\cfrac {\gamma ,\beta \rightarrow \alpha ,\gamma \rightarrow \beta \vdash \alpha }{\qquad {\cfrac {\beta \rightarrow \alpha ,\gamma \rightarrow \beta \vdash \gamma \rightarrow \alpha }{\qquad {\cfrac {\beta \rightarrow \alpha \vdash (\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }{\vdash (\beta \rightarrow \alpha )\rightarrow (\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }}Right\rightarrow }}Right\rightarrow }}Right\rightarrow }}Left\rightarrow }

(β→α)→(γ→β)→γ→α的证明告诉我们如何制造带有这个类型的一个λ-表达式。首先,介入分别带有类型α和β的变量a和b。Left →规则声称制造程序 (λb.a b),它构造类型α的一个值。我们再次使用Left →来构造(λb.a (λg.b g)),它仍有类型α。

原文链接: http://www.baijia520.com/c520/4oh30.html