(β → α) → (γ → β) → γ → α の自然演繹における証明とラムダ項
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/07 20:51 UTC 版)
「カリー＝ハワード同型対応」の記事における「(β → α) → (γ → β) → γ → α の自然演繹における証明とラムダ項」の解説
次の図は ( β → α ) → ( γ → β ) → γ → α {\displaystyle (\beta \to \alpha )\to (\gamma \to \beta )\to \gamma \to \alpha } の自然演繹における証明である。簡単のため、文脈 Γ ⊢ {\displaystyle \Gamma \vdash } は省略してある。 x : β → α y : γ → β z : γ y z : β x ( y z ) : α λ z . x ( y z ) : γ → α λ y . λ z . x ( y z ) : ( γ → β ) → γ → α λ x . λ y . λ z . x ( y z ) : ( β → α ) → ( γ → β ) → γ → α {\displaystyle {\dfrac {\dfrac {{\begin{matrix}{}\\x:\beta \rightarrow \alpha \end{matrix}}\quad {\dfrac {y:\gamma \rightarrow \beta \quad z:\gamma }{yz:\beta }}}{\dfrac {x\,(yz):\alpha }{\lambda z.x\,(yz):\gamma \rightarrow \alpha }}}{\dfrac {\lambda y.\lambda z.x\,(yz):(\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }{\lambda x.\lambda y.\lambda z.x\,(yz):(\beta \rightarrow \alpha )\rightarrow (\gamma \rightarrow \beta )\rightarrow \gamma \rightarrow \alpha }}}} この証明が型付きラムダ項 λ x . λ y . λ z . x ( y z ) {\displaystyle \lambda x.\lambda y.\lambda z.x(yz)} と解釈できることは明らかである。なお、前述の ( β → α ) → ( γ → β ) → γ → α {\displaystyle (\beta \to \alpha )\to (\gamma \to \beta )\to \gamma \to \alpha } のヒルベルト流の証明は、自然演繹におけるこの証明に対して抽象の除去とη変換を何度か使用することで得られる。
※この「(β → α) → (γ → β) → γ → α の自然演繹における証明とラムダ項」の解説は、「カリー＝ハワード同型対応」の解説の一部です。
「(β → α) → (γ → β) → γ → α の自然演繹における証明とラムダ項」を含む「カリー＝ハワード同型対応」の記事については、「カリー＝ハワード同型対応」の概要を参照ください。
- → → γ → α の自然演繹における証明とラムダ項のページへのリンク
