合成コンビネータと (β → α) → (γ → β) → γ → α のヒルベルト流の証明
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/07 20:51 UTC 版)
「カリー＝ハワード同型対応」の記事における「合成コンビネータと (β → α) → (γ → β) → γ → α のヒルベルト流の証明」の解説
もっと複雑な例として、 B {\displaystyle B} コンビネータに対応する定理を示そう。 B {\displaystyle B} の型は ( β → α ) → ( ( γ → β ) → ( γ → α ) ) {\displaystyle (\beta \to \alpha )\to ((\gamma \to \beta )\to (\gamma \to \alpha ))} である。 B {\displaystyle B} は S ( K S ) K {\displaystyle S(KS)K} に対応する（この事実は抽象除去などを用いて得られる）。これは目的の定理の証明の道筋を与えている。 まず K S {\displaystyle KS} を構成する。公理 K {\displaystyle K} の前にまず公理 S {\displaystyle S} の形を見る。そして公理 K {\displaystyle K} の α {\displaystyle \alpha } に公理 S {\displaystyle S} の論理式を代入する。すると次が得られる： K : α → β → α {\displaystyle K:\alpha \to \beta \to \alpha } K : ( ( α → β → γ ) → ( α → β ) → α → γ ) → δ → ( α → β → γ ) → ( α → β ) → α → γ {\displaystyle K:((\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma )\to \delta \to (\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma } ここで S : ( α → β → γ ) → ( α → β ) → α → γ {\displaystyle S:(\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma } とモーダス・ポネンスにより、 K S : δ → ( α → β → γ ) → ( α → β ) → α → γ {\displaystyle KS:\delta \to (\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma } 次にこの論理式と公理 S {\displaystyle S} の最初の部分 α → β → γ {\displaystyle \alpha \to \beta \to \gamma } とが同一になるような代入を求め（ユニフィケーション）、 S : ( δ → ( α → β → γ ) → ( α → β ) → α → γ ) → ( δ → α → β → γ ) → δ → ( α → β ) → α → γ {\displaystyle S:(\delta \to (\alpha \to \beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma )\to (\delta \to \alpha \to \beta \to \gamma )\to \delta \to (\alpha \to \beta )\to \alpha \to \gamma } を得る。これと先の論理式にモーダス・ポネンスを適用すれば、 S ( K S ) : ( δ → α → β → γ ) → δ → ( α → β ) → α → γ {\displaystyle S(KS):(\delta \to \alpha \to \beta \to \gamma )\to \delta \to (\alpha \to \beta )\to \alpha \to \gamma } この論理式の最初の部分 δ → α → β → γ {\displaystyle \delta \to \alpha \to \beta \to \gamma } と公理 K : α → β → α {\displaystyle K:\alpha \to \beta \to \alpha } とが同一になるような代入を求めれば、それは δ = β → γ {\displaystyle \delta =\beta \to \gamma } であるから、 K : ( β → γ ) → α → β → γ {\displaystyle K:(\beta \to \gamma )\to \alpha \to \beta \to \gamma } S ( K S ) : ( ( β → γ ) → α → β → γ ) → ( β → γ ) → ( α → β ) → α → γ {\displaystyle S(KS):((\beta \to \gamma )\to \alpha \to \beta \to \gamma )\to (\beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma } 最後にこれらにモーダス・ポネンスを適用すれば次を得る： S ( K S ) K : ( β → γ ) → ( α → β ) → α → γ {\displaystyle S(KS)K:(\beta \to \gamma )\to (\alpha \to \beta )\to \alpha \to \gamma } 適当に命題変数の名前を付け替えれば所望の論理式の証明が得られる。
※この「合成コンビネータと (β → α) → (γ → β) → γ → α のヒルベルト流の証明」の解説は、「カリー＝ハワード同型対応」の解説の一部です。
「合成コンビネータと (β → α) → (γ → β) → γ → α のヒルベルト流の証明」を含む「カリー＝ハワード同型対応」の記事については、「カリー＝ハワード同型対応」の概要を参照ください。
- 合成コンビネータと → → γ → α のヒルベルト流の証明のページへのリンク
