証明理論と型理論

ウィキペディア小見出し辞書

証明理論と型理論

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 09:51 UTC 版)

「自然演繹」の記事における「証明理論と型理論」の解説

ここまでの説明は、命題の性質に重きを置いており、「証明」の形式的定義をしていなかった。証明を形式的に記述するには、仮説的導出の記法を若干変える必要がある。前件に（変項の無限可算集合 V から）「証明変項; proof variables」によるラベルを付け、後件を実際の証明で装飾する。前件あるいは仮説はターンスタイル(⊢)を挟んで、後件の前に記される。このような変形を「局所化仮説; localized hypotheses」と呼ぶこともある。以上の変更を図にまとめると次のようになる。 ---- u1 ---- u2 ... ---- un J1 J2 Jn ⋮ J ⇒ u1:J1, u2:J2, ..., un:Jn ⊢ J 詳細が不要な場合、仮説群をまとめて Γ と記す。証明を正確にするには、証明不能な判断 "A true" ではなく、"π is a proof of (A true)"（πは A true の証明である）という判断を扱う。これを記号的に "π : A true" と記する。標準的手法では、証明は判断 "π proof" に構成規則を適用することで示される。最も単純な証明として、ラベル付き仮説を使ったものがある。この場合の証拠はラベル自身である。 u ∈ V------- proof-Fu proof --------------------- hypu:A true ⊢ u : A true 簡潔さを保つため、以下では判断ラベル true を省略する。従って、"Γ ⊢ π : A" となる。ここで、明確な証明でいくつかの結合子を再評価する。論理積については、論理積の証明の形式を見つけるために、その導入規則 ∧I を見てみる。それらは、2つの要素の証明の対となる。従って、次のようになる。 π1 proof π2 proof-------------------- pair-F(π1, π2) proof Γ ⊢ π1 : A Γ ⊢ π2 : B------------------------ ∧IΓ ⊢ (π1, π2) : A ∧ B 除去規則 ∧E1 と ∧E2 は論理積の右か左のいずれかの要素を選択する。従って、証明は2つの投影（第一 = fst と 第二 = snd）の対となる。 π proof----------- fst-Ffst π proof Γ ⊢ π : A ∧ B------------- ∧E1Γ ⊢ fst π : A π proof----------- snd-Fsnd π proof Γ ⊢ π : A ∧ B------------- ∧E2Γ ⊢ snd π : B 含意については、導入によって仮説の局所化（あるいは束縛）が形成され、これを λ を使って記述する。規則にある "Γ, u:A" は、仮説群 Γ に追加の仮説 u を加えることを意味する。 π proof------------ λ-Fλu. π proof Γ, u:A ⊢ π : B----------------- ⊃IΓ ⊢ λu. π : A ⊃ B π1 proof π2 proof------------------- app-Fπ1 π2 proof Γ ⊢ π1 : A ⊃ B Γ ⊢ π2 : A---------------------------- ⊃EΓ ⊢ π1 π2 : B 明確化された証明では、証明を処理し、論じることが可能となる。証明に関する重要な操作は、ある証明を別の証明の前提に置き換える操作である。これを一般に「代入定理; substitution theorem」と呼び、数学的帰納法によって証明可能である。 代入定理 Γ ⊢ π1 : A かつ Γ, u:A ⊢ π2 : B なら、 Γ ⊢ [π1/u] π2 : B である。 これまで、判断 "Γ ⊢ π : A" は、純粋に論理的な意味しかなかった。型理論では、論理的な観点からより計算的な観点へと変換が行われる。論理的には命題とされていたものが「型」となり、証明はラムダ計算におけるプログラムとなる。従って、"π : A" は、「プログラム π の型は A である」という解釈になる。論理結合子も異なった解釈となる。論理積は積（×）、含意は関数矢印（→）などとなる。ただし、これらの違いは単に表面的なものである。型理論では、構成規則、導入規則、除去規則を自然演繹的に表現する。実際、自然演繹を知っていれば、単純階型理論は容易に理解できる。 論理と型理論の違いは、焦点が型（命題）からプログラム（証明）に移っている点である。型理論は、プログラムの変換可能性や還元可能性に興味の中心がある。全ての型について、還元不可能な正規のプログラムが存在する。これを「正規形」または「値」と呼ぶ。全てのプログラムが正規形に還元可能なら、その型理論は「正規化; normalising」（あるいは弱正規化）されていると言える。正規形が唯一である場合、その理論は「強正規化; strongly normalising」されていると言える。正規化性は複雑な型理論では滅多にない特性であり、その点で論理の世界とは一線を画すことになる（多くの論理において、論理導出には等価な正規な導出があるという事実を思い出していただきたい）。再帰的定義が可能な型理論では、1つの値に還元できないプログラムを書くことが可能である。そのようなプログラムは一般にいかなる型も与えることが可能である。特に、再帰プログラムは型 ⊥ を持つこともあるが、"⊥ true" についての論理的証明は存在しない。以上から、「型としての命題、プログラムとしての証明」というパラダイムは一方向にしか働かない。もし型理論を論理に無理やり変換したとしても、一貫性のない論理しか得られない。 論理と同様、型理論には様々な拡張や変種があり、一階版も高階版もある。型理論の興味深い変種として依存型理論がある。これは、プログラム全体に量化を施せるものである。量化型は ∀ と ∃ の代わりに Π と Σ を使って記述する。構成規則は次のようになる。 Γ ⊢ A type Γ, x:A ⊢ B type----------------------------- Π-FΓ ⊢ Πx:A. B type Γ ⊢ A type Γ, x:A ⊢ B type---------------------------- Σ-FΓ ⊢ Σx:A. B type これらの型は矢印と積の型の一般化であり、導入規則と除去規則は次のようになる。 Γ, x:A ⊢ π : B-------------------- ΠIΓ ⊢ λx. π : Πx:A. B Γ ⊢ π1 : Πx:A. B Γ ⊢ π2 : A----------------------------- ΠEΓ ⊢ π1 π2 : [π2/x] B Γ ⊢ π1 : A Γ, x:A ⊢ π2 : B----------------------------- ΣIΓ ⊢ (π1, π2) : Σx:A. B Γ ⊢ π : Σx:A. B---------------- ΣE1Γ ⊢ fst π : A Γ ⊢ π : Σx:A. B------------------------ ΣE2Γ ⊢ snd π : [fst π/x] B 普遍的な依存型理論は非常に強力であり、プログラムの想像可能ないかなる属性もプログラムの型で直接表すことができる。ただし、その普遍性と引き換えに、あるプログラムがある型であるかを決定不能となっている。このため、依存型理論を実際に使う場合、任意のプログラムの量化を許さないで、特定の決定可能な領域（整数、文字列、線形プログラムなど）のみを扱うことが多い。 依存型理論では型がプログラムに依存することを許すのだが、そこから自然に生じる疑問として、プログラムが型に依存するとか他の組合せの依存は可能か、というものがある。この疑問には様々な答えがある。一般的な手法はプログラムを型に関して量化するもので、「パラメトリック・ポリモルフィズム」と呼ぶ。これは、型とプログラムを明確に区別する「断定的ポリモルフィズム」と、両者の区別があいまいな「非断定的ポリモルフィズム」に分類される。依存性とポリモルフィズムの組合せは様々なものが考えられ、Henk Barendregt の ラムダ・キューブが有名である。 論理と型理論の境界領域は、研究が盛んな分野である。新たな論理は、論理フレームワークとして型理論的設定で形式化されることが多い。そのような論理フレームワークとして、calculus of constructions や LF は高階依存型理論に基づいており、決定可能性と表現能力のトレードオフを考慮して考案されている。これらの論理フレームワーク自体は常に自然演繹体系に則っており、自然演繹手法の汎用性を示している。