[0077] 型理論

型理論は形式体系の一種で、様々な用途がある。歴史的には数学の基礎付け(foundations of mathematics)が元々の動機である。Russell[Russell--1908-0000]が型理論を導入した当時はパラドックスの発見により数学の基礎付けが揺らいでいた時期である。Russell[Russell--1908-0000]の型理論は後にChurch[Church--1940-0000]によって単純型付きラムダ計算として整備され、元々の動機であった数学の基礎付けとは別にプログラミング言語(programming language)の理論においても活発に研究されている[Pierce--2002-0000]。型理論はさらに別の方向で圏論との関わりもあり、例えば単純型付きラムダ計算はデカルト閉圏の内部言語(internal language)である[Lambek--Scott--1986-0000]。ホモトピー型理論の直接の基盤となる型理論はMartin-Löf型理論[Martin-Loef--1975-0000]である。これはMartin-Löf[Martin-Loef--1975-0000]が構成的数学の基礎付けとして導入したもので、定理証明支援系(interactive theorem prover, proof assistant)の基礎でもある。

型理論が圏の内部言語であるという意味を説明する。圏とは、集合と写像のような、なんらかの対象とその間の射のなる構造を抽象化した概念である。単純型付きラムダ計算がデカルト閉圏の内部言語であるとは、デカルト閉圏と呼ばれる特別な構造を持つ圏は型を対象、要素を射と解釈することで単純型付きラムダ計算のモデルになるという意味である(実際にはデカルト閉圏の構造が単純型付きラムダ計算を解釈するために必要最低限のものであるというようなことも言える)。例えば集合と写像のなす圏はデカルト閉圏であり、型を集合、要素を写像と解釈することで単純型付きラムダ計算のモデルになる。他にも、群\(G\)に対して\(G\)の作用を持つ集合のなす圏、空間\(X\)に対して\(X\)上の層のなす圏などはデカルト閉圏である。したがって、単純型付きラムダ計算の中での構成は自動的にこれらの圏の中での構成に翻訳される。

定理証明支援系とは、コンピュータ上で定理を証明または証明の正しさを検証するソフトウェアで、CoqやAgdaやIsabelleなどがある。このうちはCoqとAgdaはMartin-Löf型理論(の派生)を基盤としている。

型理論はしばしば構成的(constructive)であることが強調される。構成的でない議論の例としては、排中律や二重否定の除去がある。排中律は、すべての命題は真または偽のいずれかであるという公理であるが、構成的な立場からは真か偽のどちらなのかを決定できない限りは真または偽のいずれかであるとは言えない。二重否定の除去は例えばある性質を満たす\(x\)が存在しないと仮定して矛盾を導き、よってその性質を満たす\(x\)が存在するというような議論である。実際に証拠となる\(x\)を構成しなくても\(x\)の存在を証明できてしまう場合があるので構成的ではない。型理論では、このような非構成的な公理は一般には仮定しない。

非構成的な公理を仮定しないということは当然証明力は落ちる。構成主義者でもない限りあまり構成的であることにこだわる意味はないように思うかもしれない。しかし、型理論は圏の内部言語という観点から見ると、証明力を落とすことはモデルが増えるという意味で利点でもある。実際、排中律を適切に解釈できる圏というのは特殊なもので、排中律を仮定した型理論は圏の内部言語としてはあまり使い勝手が良いものではない。このことから、構成主義者でなくとも構成的な型理論を使う価値は十分にある。

型理論が構成的であることはプログラミング言語の観点からは重要である。構成がはっきりしない部分があると計算が進まないのでプログラムとは言えない。逆に、構成的な証明からはプログラム抽出(program extraction)ができる。例えば任意の\(x\)に対してある性質を満たす\(y\)が存在するという命題を構成的に証明できたとしよう。証明が構成的であるということは、\(x\)から具体的に\(y\)が構成されたということであるが、これは\(x\)から\(y\)を計算するプログラムであると言える。このように証明から抽出されたプログラムは定義により満たすべき性質を満たしていることが保証されている。