カリー＝ハワード＝ランベック対応
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/07 20:51 UTC 版)
「カリー＝ハワード同型対応」の記事における「カリー＝ハワード＝ランベック対応」の解説
ヨアヒム・ランベックは1970年始めに直観主義命題論理とデカルト閉圏の等式理論と対応するある種の型付きコンビネータとの対応関係の証明を示した。このカリー＝ハワード＝ランベック対応は直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる。ここではオブジェクトは型あるいは命題に、モルフィズムは項あるいは証明に解釈される。この対応は等号レベルに於いて働き、カリー＝ハワード対応にあるような構文的・構造的同等性を表現しない：すなわち、デカルト閉圏のモルフィズムの構造と、対応する判定のヒルベルト流あるいは自然演繹の証明の構造と比較することはできない。もちろん構文的に対応するような証明体系を構成することはできる。この区別を明確にするために、デカルト閉圏の構文的な構造を次のように言い換える。すなわちデカルト閉圏を型付きの等式理論として形式化する。 オブジェクト（型）は次のように帰納的に定義される： ⊤ {\displaystyle \top } はオブジェクトである、 α {\displaystyle \alpha } と β {\displaystyle \beta } がオブジェクトならば、 α × β {\displaystyle \alpha \times \beta } と α → β {\displaystyle \alpha \rightarrow \beta } はオブジェクトである。 モルフィズム（項）は次のように帰納的に定義される： i d {\displaystyle id} 、 ⋆ {\displaystyle \star } 、 eval {\displaystyle \operatorname {eval} } 、 π 1 {\displaystyle \pi _{1}} と π 2 {\displaystyle \pi _{2}} はモルフィズムである、 t {\displaystyle t} がモルフィズムならば λ t {\displaystyle \lambda t} はモルフィズムである、 t {\displaystyle t} と u {\displaystyle u} がモルフィズムならば ⟨ t , u ⟩ {\displaystyle \langle t,u\rangle } と u ∘ t {\displaystyle u\circ t} はモルフィズムである。 Well-definedなモルフィズム（型付きの項）は以下の型付け規則にしたがって構成される： 恒等射： i d : α ⟶ α {\displaystyle {\frac {}{id:\alpha \longrightarrow \alpha }}} 合成: t : α ⟶ β u : β ⟶ γ u ∘ t : α ⟶ γ {\displaystyle {\frac {t:\alpha \longrightarrow \beta \qquad u:\beta \longrightarrow \gamma }{u\circ t:\alpha \longrightarrow \gamma }}} 終対象: ⋆ : α ⟶ ⊤ {\displaystyle {\frac {}{\star :\alpha \longrightarrow \top }}} 直積: t : α ⟶ β u : α ⟶ γ ⟨ t , u ⟩ : α ⟶ β × γ {\displaystyle {\frac {t:\alpha \longrightarrow \beta \qquad u:\alpha \longrightarrow \gamma }{\langle t,u\rangle :\alpha \longrightarrow \beta \times \gamma }}} 射影: π 1 : α × β ⟶ α π 2 : α × β ⟶ β {\displaystyle {\frac {}{\pi _{1}:\alpha \times \beta \longrightarrow \alpha }}\qquad {\frac {}{\pi _{2}:\alpha \times \beta \longrightarrow \beta }}} カリー化: t : α × β ⟶ γ λ t : α ⟶ β → γ {\displaystyle {\frac {t:\alpha \times \beta \longrightarrow \gamma }{\lambda t:\alpha \longrightarrow \beta \rightarrow \gamma }}} 評価: e v a l : ( α → β ) × α ⟶ β {\displaystyle {\frac {}{eval:(\alpha \rightarrow \beta )\times \alpha \longrightarrow \beta }}} 最後に、圏の等式を次により定める： i d ∘ t = t , t ∘ i d = t , ( v ∘ u ) ∘ t = v ∘ ( u ∘ t ) , {\displaystyle id\circ t=t,t\circ id=t,(v\circ u)\circ t=v\circ (u\circ t),} ⋆ ∘ t = ⋆ , {\displaystyle \star \circ t=\star ,} π 1 ∘ ⟨ t , u ⟩ = t , π 2 ∘ ⟨ t , u ⟩ = u , ⟨ π 1 ∘ t , π 2 ∘ t ⟩ = t , {\displaystyle \pi _{1}\circ \langle t,u\rangle =t,\pi _{2}\circ \langle t,u\rangle =u,\langle \pi _{1}\circ t,\pi _{2}\circ t\rangle =t,} e v a l ∘ ⟨ λ t , i d ⟩ = t , λ e v a l = i d . {\displaystyle eval\circ \langle \lambda t,id\rangle =t,\lambda eval=id.} このとき、 t : α 1 × … × α n ⟶ β {\displaystyle t:\alpha _{1}\times \ldots \times \alpha _{n}\longrightarrow \beta } なるモルフィズム t {\displaystyle t} が存在することと、 α 1 , … , α n ⊢ β {\displaystyle \alpha _{1},\ldots ,\alpha _{n}\vdash \beta } なるシークエントが直観論理の含意論理積断片で証明可能であることとは同値である。上記のデカルト閉圏の射の等式体系として得られる計算模型はカテゴリカルコンビネータあるいは圏的コンビネータ論理として知られる。 論理圏論論理式 オブジェクト 含意 α ⊃ β {\displaystyle \alpha \supset \beta } 指数 α → β {\displaystyle \alpha \to \beta } 論理積 α ∧ β {\displaystyle \alpha \wedge \beta } 直積 α × β {\displaystyle \alpha \times \beta } 論理和 α ∨ β {\displaystyle \alpha \vee \beta } 余積 α + β {\displaystyle \alpha +\beta } 真 ⊤ {\displaystyle \top } 終対象 1 {\displaystyle 1} 偽 ⊥ {\displaystyle \bot } 始対象 0 {\displaystyle 0} 証明 モルフィズム 証明図の合成・カット モルフィズムの合成
※この「カリー＝ハワード＝ランベック対応」の解説は、「カリー＝ハワード同型対応」の解説の一部です。
「カリー＝ハワード＝ランベック対応」を含む「カリー＝ハワード同型対応」の記事については、「カリー＝ハワード同型対応」の概要を参照ください。
- カリー＝ハワード＝ランベック対応のページへのリンク
