型理論
概要
型理論（type theory）とは、すべての項が型をもち、「項 $M$ は型 $A$ をもつ」という判断を規則によって導く形式体系の総称である。基本の例である単純型付きラムダ計算では、型は簡約で保たれ（主部簡約）、型の付いた項はすべて正規形をもつ。型を論理式、項を証明と読むと、型付けの規則は含意の自然演繹の規則と一対一に対応し（Curry–Howard 対応）、正規形の存在から含意だけの最小論理の無矛盾性が従う。依存型を加えた Martin-Löf 型理論やホモトピー型理論は、集合論と並ぶ数学の基礎の言語として研究されている。
集合論では「$x$ は自然数である」は $x\in\mathbb{N}$ という命題であり、成り立つことも成り立たないこともある。これに対し、プログラムの変数には「整数型」「関数型」のような型が最初から付いており、型の合わない式（整数に関数を適用する式など）はそもそも書けない。対象がつねに型をもち、「項 $M$ は型 $A$ をもつ」という判断 $M:A$ を規則によって導く形式体系を 型理論（type theory）という。
型理論のいちばん基本的な例は 単純型付きラムダ計算 である。この体系では、型 $A\to B$ の項は「型 $A$ の入力から型 $B$ の出力を作る関数」を表し、関数の適用は簡約という計算規則で実行される。同時に、型を論理式、項をその証明と読むと、単純型付きラムダ計算は含意だけの自然演繹と正確に対応する（Curry–Howard 対応）。この記事では、単純型付きラムダ計算を定義し、型の一意性、簡約で型が保たれること（主部簡約）、Curry–Howard 対応、正規形の存在を証明し、その帰結として論理の無矛盾性を導く。最後に、依存型などを含むより大きな型理論への広がりを述べる。
定義
型と項
基本型 と呼ぶ記号の集合を 1 つ固定し、$o,o'$ などで表す。単純型（simple type）を次の規則で帰納的に定める。
- 基本型は単純型である。
- $A,B$ が単純型ならば、$(A\to B)$ は単純型である。
括弧は右に結合するものとして省き、$A\to B\to C$ は $A\to(B\to C)$ を表す。
変数の可算無限集合を 1 つ固定し、$x,y,z,f,g$ などで表す。
項（term）を次の規則で帰納的に定める。
- 変数 $x$ は項である。
- $x$ が変数、$A$ が単純型、$M$ が項ならば、$(\lambda x{:}A.\,M)$ は項である（抽象）。
- $M,N$ が項ならば、$(MN)$ は項である（適用）。
適用は左に結合するものとして括弧を省き、$MNL$ は $((MN)L)$ を表す。$\lambda x{:}A.\,M$ の $x$ は $M$ の中で 束縛 されるといい、束縛されていない変数の出現を 自由 な出現という。項 $M$ の自由変数の集合を $\mathrm{FV}(M)$ と書く。束縛変数の名前だけが違う項は同じものとみなす。
項 $M$ の自由な $x$ をすべて項 $N$ に置き換えたものを $M[N/x]$ と書く。$N$ の自由変数が $M$ の中の $\lambda$ に捕まらないように、必要なら $M$ の束縛変数の名前を先に変えておく。$M[N/x]$ は、$x[N/x]=N$、$y[N/x]=y$（$y\ne x$）、$(M_1M_2)[N/x]=M_1[N/x]\,M_2[N/x]$、$(\lambda y{:}A.\,M_1)[N/x]=\lambda y{:}A.\,M_1[N/x]$（$y\ne x$、$y\notin\mathrm{FV}(N)$）という再帰で定まる。項は帰納的に生成され、組み立て方がただ 1 通りに読める（一意可読性）ので、この再帰は矛盾なく 1 つの項を定める（構造的帰納法 の定理「構造的再帰定理」）。
型付け
文脈（context）とは、相異なる変数 $x_1,\dots,x_n$ に単純型を 1 つずつ割り当てた有限の宣言の集まり $\Gamma=\{x_1{:}A_1,\dots,x_n{:}A_n\}$ のことである。$x$ が $\Gamma$ に現れないとき、$\Gamma$ に $x{:}A$ を加えた文脈を $\Gamma,x{:}A$ と書く。
型判断 $\Gamma\vdash M:A$ を、次の 3 つの規則で導かれるものとして帰納的に定める。
$$
\dfrac{x{:}A\in\Gamma}{\Gamma\vdash x:A}\ {\scriptstyle(\mathrm{var})}\qquad
\dfrac{\Gamma,x{:}A\vdash M:B}{\Gamma\vdash\lambda x{:}A.\,M:A\to B}\ {\scriptstyle(\mathrm{abs})}\qquad
\dfrac{\Gamma\vdash M:A\to B\qquad\Gamma\vdash N:A}{\Gamma\vdash MN:B}\ {\scriptstyle(\mathrm{app})}
$$
規則 (abs) では、束縛変数の名前を変えて $x$ が $\Gamma$ に現れないようにしておく。ある $\Gamma,A$ について $\Gamma\vdash M:A$ が導かれるとき、$M$ は 型付け可能 であるという。$\emptyset\vdash M:A$ を $\vdash M:A$ と書き、自由変数をもたない項を 閉じた項 という。
$(\lambda x{:}A.\,M)N$ の形の項を β 基（redex）という。項の中の 1 つの β 基 $(\lambda x{:}A.\,M)N$ を $M[N/x]$ に置き換える操作を β 簡約 の一歩といい、$M\to_\beta M'$ と書く。$\to_\beta$ を $0$ 回以上続けることを $\to_\beta^{*}$ と書く。β 基を含まない項を 正規形 という。$M\to_\beta^{*}N$ となる正規形 $N$ を $M$ の正規形という。
$A,B,C$ を単純型とする。
- $\vdash\lambda x{:}A.\,x:A\to A$（恒等関数）。
- $\vdash\lambda x{:}A.\,\lambda y{:}B.\,x:A\to B\to A$（2 番目の引数を捨てる関数）。
- $\vdash\lambda g{:}B\to C.\,\lambda f{:}A\to B.\,\lambda x{:}A.\,g(fx):(B\to C)\to(A\to B)\to A\to C$（関数の合成）。
- $\vdash\lambda f{:}A\to B\to C.\,\lambda g{:}A\to B.\,\lambda x{:}A.\,fx(gx):(A\to B\to C)\to(A\to B)\to A\to C$。
たとえば 3 は、$\Gamma=\{g{:}B\to C,\ f{:}A\to B,\ x{:}A\}$ で (var) と (app) により $\Gamma\vdash fx:B$、$\Gamma\vdash g(fx):C$ を導き、(abs) を 3 回使って得られる。$(\lambda x{:}A.\,x)y$ は β 基で、$(\lambda x{:}A.\,x)y\to_\beta y$ である。
$xx$ はどの文脈でも型付け可能でない。$\Gamma\vdash xx:B$ が導かれたとすると、最後の規則は (app) なので、ある $A$ について $\Gamma\vdash x:A\to B$ と $\Gamma\vdash x:A$ が導かれ、どちらも (var) によるから、$\Gamma$ が $x$ に割り当てる型は $A\to B$ と $A$ の両方に等しい。ところが $A\to B$ は $A$ より真に長い記号列なので $A\ne A\to B$ であり、矛盾する。したがって、$xx$ を含む項 $\lambda x{:}A.\,xx$ も型付け可能でない。型の付かないλ計算ではこの形の項から終わらない計算が作れるが（下の反例の表の 1 行目）、型付けがそれを締め出している。
基本的な性質
型付け規則は項の形ごとにちょうど 1 つあるので、型判断の導出は項の形から逆にたどれる。
- $\Gamma\vdash x:C$ ならば $x{:}C\in\Gamma$ である。
- $\Gamma\vdash\lambda x{:}A.\,M:C$ ならば、ある $B$ について $C=A\to B$ かつ $\Gamma,x{:}A\vdash M:B$ である。
- $\Gamma\vdash MN:C$ ならば、ある $A$ について $\Gamma\vdash M:A\to C$ かつ $\Gamma\vdash N:A$ である。
型判断の導出の最後の規則は、結論の項が変数なら (var)、抽象なら (abs)、適用なら (app) でしかありえない。それぞれの規則の前提が主張の内容である。$\square$
- （型の一意性）$\Gamma\vdash M:A$ かつ $\Gamma\vdash M:B$ ならば $A=B$ である。
- （弱化）$\Gamma\vdash M:A$ で、$\Gamma'$ が $\Gamma$ を含む文脈ならば、$\Gamma'\vdash M:A$ である。
- （置換）$\Gamma,x{:}A\vdash M:B$ かつ $\Gamma\vdash N:A$ ならば、$\Gamma\vdash M[N/x]:B$ である。
要点：どれも $M$ の組み立てについての帰納法で、各段で lem-tt-generation により前提を取り出し、帰納法の仮定を当てて同じ規則で組み立て直す。
詳細
1：$M=x$ なら、lem-tt-generation の 1 により $A$ も $B$ も $\Gamma$ が $x$ に割り当てる型である。$M=\lambda x{:}C.\,M_1$ なら、生成補題の 2 により $A=C\to A_1$、$B=C\to B_1$、$\Gamma,x{:}C\vdash M_1:A_1$、$\Gamma,x{:}C\vdash M_1:B_1$ であり、帰納法の仮定で $A_1=B_1$ なので $A=B$ である。$M=M_1M_2$ なら、生成補題の 3 により $\Gamma\vdash M_1:C\to A$、$\Gamma\vdash M_1:D\to B$ となる $C,D$ があり、帰納法の仮定で $C\to A=D\to B$、よって $A=B$ である。
2：$M$ が変数なら (var) の条件は $\Gamma'$ でも成り立つ。適用なら帰納法の仮定と (app) による。$M=\lambda y{:}C.\,M_1$ なら、束縛変数の名前を変えて $y$ が $\Gamma'$ に現れないようにしておくと、$\Gamma,y{:}C\vdash M_1:B_1$ と帰納法の仮定から $\Gamma',y{:}C\vdash M_1:B_1$、(abs) で $\Gamma'\vdash M:C\to B_1$ である。
3：$M=x$ なら生成補題の 1 により $B=A$ で、$M[N/x]=N$ の型は $A$ である。$M=y\ne x$ なら $y{:}B\in\Gamma$ で、$M[N/x]=y$ である。$M=M_1M_2$ なら、生成補題の 3 と帰納法の仮定、(app) による。$M=\lambda y{:}C.\,M_1$（$y\ne x$、$y\notin\mathrm{FV}(N)$、$y$ は $\Gamma$ に現れない）なら、生成補題の 2 により $B=C\to D$、$\Gamma,x{:}A,y{:}C\vdash M_1:D$ である。2 により $\Gamma,y{:}C\vdash N:A$ なので、帰納法の仮定（文脈 $\Gamma,y{:}C$ に対して）から $\Gamma,y{:}C\vdash M_1[N/x]:D$、(abs) で $\Gamma\vdash\lambda y{:}C.\,M_1[N/x]:C\to D$ を得る。$\square$
$\Gamma\vdash M:A$ かつ $M\to_\beta M'$ ならば、$\Gamma\vdash M':A$ である。したがって $M\to_\beta^{*}M'$ でも $\Gamma\vdash M':A$ である。
$M$ の組み立てについての帰納法で示す。まず $M$ 自身が簡約される β 基 $(\lambda x{:}C.\,P)N$ で $M'=P[N/x]$ の場合を考える。lem-tt-generation の 3 により、ある $D$ について $\Gamma\vdash\lambda x{:}C.\,P:D\to A$ かつ $\Gamma\vdash N:D$ である。生成補題の 2 により $D\to A=C\to B$、$\Gamma,x{:}C\vdash P:B$ となる $B$ があり、$D=C$、$B=A$ である。よって prop-tt-uniqueness-substitution の 3 により $\Gamma\vdash P[N/x]:A$ である。
簡約される β 基が $M$ の真部分にある場合。$M=M_1M_2$ で $M_1\to_\beta M_1'$ なら、生成補題の 3 により $\Gamma\vdash M_1:D\to A$、$\Gamma\vdash M_2:D$ であり、帰納法の仮定から $\Gamma\vdash M_1':D\to A$、(app) で $\Gamma\vdash M_1'M_2:A$ である。$M_2$ の中で簡約する場合も同じである。$M=\lambda y{:}C.\,M_1$ で $M_1\to_\beta M_1'$ なら、生成補題の 2 により $A=C\to B$、$\Gamma,y{:}C\vdash M_1:B$ であり、帰納法の仮定と (abs) で $\Gamma\vdash\lambda y{:}C.\,M_1':A$ である。後半は一歩ごとに前半を使えばよい。$\square$
Curry–Howard 対応
基本型を命題変数（命題論理）と読み、型の $\to$ を論理の含意と読むと、単純型は含意 $\to$ だけからなる論理式になる。以下、論理式はこの意味の含意の論理式とし、自然演繹 の規則のうち仮定・$\to\mathrm I$・$\to\mathrm E$ の 3 つだけを使う体系（含意だけの最小論理）を考える。導出・開いた仮定の集合 $\mathrm{Open}(D)$・$\Delta\vdash A$ は 自然演繹 の定義「自然演繹の導出」を、この 3 つの規則に制限して用いる。文脈 $\Gamma$ に現れる型の集合を $\lvert\Gamma\rvert$ と書く。
- $\Gamma\vdash M:A$ ならば、含意だけの最小論理で $\lvert\Gamma\rvert\vdash A$ である。
- 部分論理式をとる操作で閉じた論理式の集合 $\Phi$ と、各 $B\in\Phi$ に変数 $x_B$ を対応させる単射を 1 つ固定する（変数は可算個なので $\Phi$ は可算とする。有限集合なら必ずとれる）。有限集合 $\Delta\subset\Phi$ に対して、文脈を $\Gamma_\Delta:=\{x_B{:}B\mid B\in\Delta\}$ とする。含意だけの最小論理で、$\mathrm{Open}(D)\subset\Delta$ で結論が $A$ の導出 $D$ であって、$D$ に現れる論理式がすべて $\Phi$ に属するものがあれば、$\Gamma_\Delta\vdash M:A$ となる項 $M$ がある。
特に、論理式 $A$ が含意だけの最小論理で証明可能であることと、$\vdash M:A$ となる項 $M$ があることは同値である。
1：型判断の導出についての帰納法で、結論が $A$ で $\mathrm{Open}(D)\subset\lvert\Gamma\rvert$ の導出 $D$ を作る。(var) なら $A\in\lvert\Gamma\rvert$ なので、$A$ だけの導出でよい。(app) なら、帰納法の仮定による $A\to B$ の導出と $A$ の導出に $\to\mathrm E$ を当てる。開いた仮定は両者の和で、$\lvert\Gamma\rvert$ に含まれる。(abs) なら、$\Gamma,x{:}A\vdash M:B$ から帰納法の仮定で $\mathrm{Open}(D_1)\subset\lvert\Gamma\rvert\cup\{A\}$ の $B$ の導出 $D_1$ があり、$\to\mathrm I$ で $A$ を外すと、開いた仮定は $\mathrm{Open}(D_1)\setminus\{A\}\subset\lvert\Gamma\rvert$ の $A\to B$ の導出になる。
2：導出 $D$ についての帰納法で、「$D$ に現れる論理式がすべて $\Phi$ に属するならば、$\mathrm{Open}(D)\subset\Delta$ を満たすすべての有限集合 $\Delta\subset\Phi$ について、$\Gamma_\Delta\vdash M:\mathrm{concl}(D)$ となる $M$ がある」ことを示す。$D$ が仮定 $A$ だけなら、$A\in\Delta$ なので $M:=x_A$ でよい。最後の規則が $\to\mathrm E$ で、前提の導出 $D_1,D_2$ の結論が $A\to B$、$A$ なら、$\mathrm{Open}(D_i)\subset\mathrm{Open}(D)\subset\Delta$ なので帰納法の仮定から $\Gamma_\Delta\vdash M_1:A\to B$、$\Gamma_\Delta\vdash M_2:A$ があり、$M:=M_1M_2$ とする。最後の規則が $\to\mathrm I$ で、前提の導出 $D_1$ の結論が $B$、$\mathrm{concl}(D)=A\to B$ なら、$\mathrm{Open}(D_1)\subset\Delta\cup\{A\}$ であり、$A$ は $A\to B\in\Phi$ の部分論理式なので $\Delta\cup\{A\}\subset\Phi$ である。よって帰納法の仮定から $\Gamma_{\Delta\cup\{A\}}\vdash M_1:B$ である。$A\notin\Delta$ なら、$B\mapsto x_B$ は単射なので $x_A$ は $\Gamma_\Delta$ に現れず、$\Gamma_{\Delta\cup\{A\}}=\Gamma_\Delta,x_A{:}A$ で、(abs) により $\Gamma_\Delta\vdash\lambda x_A{:}A.\,M_1:A\to B$ である。$A\in\Delta$ なら $\Gamma_{\Delta\cup\{A\}}=\Gamma_\Delta$ であり、$\Gamma_\Delta$ に現れない変数 $y$ をとると prop-tt-uniqueness-substitution の 2 により $\Gamma_\Delta,y{:}A\vdash M_1:B$、(abs) により $\Gamma_\Delta\vdash\lambda y{:}A.\,M_1:A\to B$ である。
最後の主張は、1 を $\Gamma=\emptyset$ に当て、2 を $\Delta=\emptyset$ と、$A$ の導出に現れる論理式の部分論理式全体（有限集合）を $\Phi$ にとって当てればよい。$\square$
この対応で、仮定は変数、$\to\mathrm I$ は抽象、$\to\mathrm E$ は適用にあたる。たとえば ex-tt-examples の 2 と 4 の項は、Hilbert 流の体系の公理 $A\to B\to A$ と $(A\to B\to C)\to(A\to B)\to A\to C$（自然演繹 の節「Hilbert 流の体系との関係」の (A1)・(A2)）の証明を表し、3 の項は含意の推移律の証明を表す。さらに、β 基 $(\lambda x{:}A.\,M)N$ は「$\to\mathrm I$ で $A\to B$ を導いた直後に $\to\mathrm E$ で $B$ を導く」遠回りの導出にあたり、β 簡約はその遠回りを、仮定 $A$ の使われる場所に $A$ の導出 $N$ を差し込む操作にあたる。直積型 $A\times B$ と連言 $\land$ を加えても同じ対応が成り立つ（GLT89 §3.1・§3.5、pp. 15, 19）。この読み方は、直観主義論理 の BHK 解釈の「$A\to B$ の証明は、$A$ の証明を $B$ の証明に変える手続きである」を形式化したものである。導出の側から見た遠回りの取り除きと部分論理式性は 正規化定理(自然演繹) で扱う。
正規化と無矛盾性
型付け可能な項はすべて正規形をもつ。
要点：型の長さを測る「次数」を β 基に付け、次数が最大の β 基のうち内側にあるものを簡約すると、新しくできる β 基の次数は真に小さく、複製される β 基の次数も小さいので、「最大の次数と、その次数の β 基の個数」の組が辞書式に減る。
詳細
型の 次数 を $\partial(o):=1$（基本型）、$\partial(A\to B):=\max(\partial(A),\partial(B))+1$ と定める。$\Gamma\vdash M:C$ とし、$M$ の中の β 基 $(\lambda x{:}A.\,P)Q$ の次数を、$\lambda x{:}A.\,P$ の型 $A\to B$ の次数 $\partial(A\to B)$ と定める（$M$ の部分項の型は、lem-tt-generation で導出を逆にたどって得られる文脈のもとで prop-tt-uniqueness-substitution の 1 により一通りに決まる）。$M$ の β 基の次数の最大値を $n(M)$（正規形なら $0$）、次数 $n(M)$ の β 基の個数を $m(M)$ とする。
$n(M)>0$ とし、次数 $n:=n(M)$ の β 基のうち、その内部に次数 $n$ の β 基を含まないもの $r=(\lambda x{:}A.\,P)Q$ を 1 つ選ぶ（内側から選べばよい）。$r$ を $P[Q/x]$ に置き換えた項を $M'$ とする。thm-tt-subject-reduction により $M'$ も型付け可能で、部分項の型は変わらない。$M'$ の β 基は次のどれかである。
(i) $r$ の外にあった β 基。$r$ を含むものも含めて、型は変わらないので次数も変わらない。(ii) $P$ や $Q$ の中にあった β 基とその複製（$Q$ は $x$ の出現の個数だけ複製される）。仮定によりどれも次数は $n$ 未満である。(iii) 置き換えで新しくできた β 基。$P$ の中に $xR$ の形の部分があり $Q$ が抽象のとき、$QR$ が β 基になり、その次数は $\partial(A)$ である。また $r$ がもともと $rR$ の形の関数の位置にあり $P[Q/x]$ が抽象のとき、$P[Q/x]R$ が β 基になり、その次数は $\partial(B)$ である。どちらも $\partial(A\to B)=n$ より真に小さい。
よって次数 $n$ の β 基は $r$ が消えた分だけ 1 つ減り、$n(M')< n$ であるか、$n(M')=n$ かつ $m(M')=m(M)-1$ である。組 $(n(M),m(M))$ についての辞書式順序の帰納法（自然数の組の辞書式順序は整礎）により、有限回の簡約で正規形に達する。$\square$
正規形の項は形が限られる。項 $N$ を、適用の左側をたどって $N=hN_1\cdots N_k$（$h$ は適用でない項、$k\ge0$）と書くと、$h$ は変数か抽象である。$h$ が抽象で $k\ge1$ なら $hN_1$ が β 基になるので、正規形の項は抽象であるか、変数 $h$ に正規形の項を並べた $hN_1\cdots N_k$ の形である（GLT89 §3.4 の補題、pp. 18–19）。
基本型 $o$ について、$\vdash M:o$ となる項 $M$ は存在しない。したがって、含意だけの最小論理で命題変数 $o$ は証明できない。
$\vdash M:o$ となる項 $M$ があったとする。thm-tt-weak-normalization により $M\to_\beta^{*}N$ となる正規形 $N$ があり、thm-tt-subject-reduction により $\vdash N:o$ である。$N$ が抽象なら、lem-tt-generation の 2 によりその型は $A\to B$ の形で、基本型 $o$ ではない。そうでなければ上の注意により $N=hN_1\cdots N_k$（$h$ は変数）である。生成補題の 3 を $k$ 回使うと、空の文脈で $\vdash h:C$ となる型 $C$ があり、生成補題の 1 により $h{:}C\in\emptyset$ となって矛盾する。よって $\vdash M:o$ となる項はない。後半は thm-tt-curry-howard の最後の主張による。$\square$
簡約の順序によらない性質も知られている。Church–Rosser の性質（$M\to_\beta^{*}N_1$、$M\to_\beta^{*}N_2$ なら $N_1,N_2\to_\beta^{*}L$ となる $L$ がある）から正規形の一意性が従い（GLT89 §4.1、pp. 22–23）、さらに 強正規化定理（型付け可能な項から始まる β 簡約の列はどれも有限で終わる）が成り立つ（GLT89 第 6 章、pp. 41–45）。どちらもこの記事では証明せず、強正規化定理 で証明する。型付け可能な項についての Church–Rosser の性質は、その記事の定理「強正規化と局所合流性からの合流性」から従う。弱正規化と Church–Rosser の性質を合わせると、型付け可能な 2 つの項が β 簡約と逆向きの簡約で移り合うかどうかは、正規形を計算して比べることで判定できる（GLT89 §4.2、p. 24）。
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 項が型付け可能（thm-tt-weak-normalization） | 型の注釈を除いた項 $\Omega=(\lambda x.\,xx)(\lambda x.\,xx)$ | 正規形の存在 |
| 型付け規則が (var)・(abs)・(app) だけ（cor-tt-consistency） | 規則 $\Gamma\vdash\mathrm{fix}_A:(A\to A)\to A$ を加え、$\mathrm{fix}_o(\lambda x{:}o.\,x)$ を作る | $\vdash M:o$ となる項がないこと |
| 抽象の束縛変数に型を書く（prop-tt-uniqueness-substitution の 1） | 規則 (abs) で $\lambda x.\,M$ に任意の $A$ で型 $A\to B$ を付ける体系での $\lambda x.\,x$ | 型の一意性 |
各行の確かめを開く
1 行目：$\Omega$ の β 基は全体だけで（$\lambda x.\,xx$ の中に β 基はない）、それを簡約すると $(xx)[\lambda x.\,xx/x]=\Omega$ に戻る。したがって $\Omega$ からの簡約の列は $\Omega$ を繰り返すだけで、正規形に達しない。型付けのない項では ex-tt-self-application の制限がないので、このような項が書ける。
2 行目：$\vdash\lambda x{:}o.\,x:o\to o$ と新しい規則から、(app) で $\vdash\mathrm{fix}_o(\lambda x{:}o.\,x):o$ となり、空の文脈で型 $o$ をもつ項ができる。$\mathrm{fix}_A$ は再帰的な定義を書くための不動点の記号で、論理の側では任意の $A$ について $(A\to A)\to A$ を公理とすることにあたり、どの命題も証明できてしまう。
3 行目：束縛変数に型を書かない体系では、(abs) は「$\Gamma,x{:}A\vdash M:B$ なら $\Gamma\vdash\lambda x.\,M:A\to B$」となり、$\vdash\lambda x.\,x:o\to o$ と $\vdash\lambda x.\,x:(o\to o)\to(o\to o)$ がどちらも導かれる。
補足
- 型理論の広がり。 単純型付きラムダ計算に、型変数 $X$ についての抽象と型 $\Pi X.\,A$ を加えた体系が System F で、含意と全称量化に基づき、整数やリストなどのデータ型を項として定義できる（GLT89 第 11 章、p. 81）。型が項に依存してよい 依存型（たとえば「長さ $n$ の列の型」）を許すと、依存積型 $\Pi$ と依存和型 $\Sigma$ が「すべての」「ある」に対応し、述語論理の量化子も型として表される（UFP13 Introduction、p. 8、§1.11、p. 44）。依存型の理論の代表が Martin-Löf型理論 であり、それに単一性公理（UFP13 Axiom 2.10.3、p. 88）を加えた ホモトピー型理論 は、集合論に代わる数学の基礎の言語として提案されている（UFP13 §1.1、p. 17）。
- 判断と命題。 集合論の $a\in A$ は証明したり否定したりできる命題だが、型理論の $a:A$ は規則で導かれる判断であり、型の付いていない対象を考えることはない（UFP13 §1.1、pp. 17–18）。命題をその証明の型と同一視する見方（命題は型、propositions as types）は、真・偽・連言・選言・含意・否定を、単位型・空型・直積型・直和型・関数型・空型への関数型に対応させる（UFP13 §1.11、pp. 41–42）。
- 一意可読性と構文。 項の置換や型付けは項の組み立て方に沿った再帰・帰納法で定義されており、項が一通りに読めること（一意可読性）を前提にしている。構文の扱いは Backus–Naur記法 の補足「抽象構文の流儀」も参照。
関連項目
- 前提: 直観主義論理, 自然演繹, 構造的帰納法
- 構文: 一意可読性, 構文解析, Backus–Naur記法
- 比較: λ計算, 数理論理学, Heyting代数
- 発展: 強正規化定理, 正規化定理(自然演繹), Martin-Löf型理論, ホモトピー型理論, トポス
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
