直觀主義型理論
intuitionistic type theory。構成的型理論 (constructive type theory)。Martin-Löf の型理論 (Martin-Löf's type theory)
項
變數$ x,y,\dots,$ \alpha,\beta,\dots
定數
適當に備へる
宇宙$ {\cal U}_0:{\cal U}_1:\dots
可算個の宇宙
※
$ {\cal U}_0は命題の全體、$ {\cal U}_1は集合の全體と見做せる $ {\cal U}_i:{\cal U}_{i+1}である
函數$ \lambda x.a
變數$ xが$ A型である事を明示するには$ \lambda x_{:A}.bと書く
函數適用$ a~b
項$ aが變數$ xを含む事を明示するには$ a(x)と書く
依存積 (dependent product)$ \prod_{x:A}B(x)
$ \prod x:A.B(x)とも書く
項$ Bが變數$ xを含まない場合は$ A\to Bとも書く
$ B:{\cal U}_0である場合は$ \forall x:A.Bとも書く
證據$ \Gamma,\Delta,\dots
項の有限列
大域的な環境$ E
定義濟みの定數と項の集合
判定
$ \Gamma~{\rm ctx}。$ \Gammaは證據である
$ \Gamma\vdash T~{\rm type}。證據$ \Gammaの下で$ Tは型である
$ \Gamma\vdash t:T。證據$ \Gammaの下で$ tは$ T型の項である
$ \Gamma\vdash S\equiv T。證據$ \Gammaの下で項$ Sと項$ Tは等しい
$ \Gamma\vdash s\equiv t:T。證據$ \Gammaの下で$ Tの項である$ sと$ tは等しい
推論規則
$ \frac{}{\Gamma,x:A\vdash x:A}
.
$ \frac{\Gamma\vdash y:B}{\Gamma,x:A\vdash y:B}
.
變數$ \frac{x:A\in\Gamma}{\Gamma\vdash x:A}
定數
$ \frac{\bar u.(c_{\bar u}:A)\in E\quad\forall i,n\vdash l_i~{\rm ok}}{\Gamma\vdash c_{\bar l}:A[\bar l/\bar u]}
.
$ \frac{\bar u.(c_{\bar u}:A)\in E\quad\forall i,n\vdash l_i,l_i'~{\rm ok}\land l_i\equiv l_i'}{\Gamma\vdash c_{\bar l}\equiv c_{\bar{l'}}:A[\bar l/\bar u]}
.
宇宙
$ \frac{}{{\cal U}_i:{\cal U}_{i+1}}
.
$ \frac{i\equiv j}{{\cal U}_i\equiv{\cal U}_j:{\cal U}_{i+1}}
依存積
構文$ \frac{\Gamma\vdash A:{\cal U}_i\quad\Gamma,x:A\vdash B:{\cal U}_j}{\Gamma\vdash\prod_{x:A}B:{\cal U}_{{\rm imax}(i,j)}}但し$ {\rm imax}(i,j):=\begin{cases}0 & j=0 \\ \max\{i,j\} & j\ne 0\end{cases}
.
導入 (函數)$ \frac{\Gamma\vdash A:{\cal U}_i\quad\Gamma,x:A\vdash b:B}{\Gamma\vdash\lambda x_{:A}.b:\prod_{x:A}B}
.
β變換$ \frac{\Gamma,x:A\vdash b:B\quad\Gamma\vdash a:A}{\Gamma\vdash(\lambda x_{:A}.b)~a\equiv b[a/x]:B[a/x]}
.
η變換$ \frac{\Gamma\vdash f:\prod_{y:A}B}{\Gamma\vdash\lambda x_{:A}.f~x\equiv f:\prod_{y:A}B}
.
除去 (函數適用)$ \frac{\Gamma\vdash f:\prod_{x:A}B\quad\Gamma\vdash a:A}{\Gamma\vdash f~a:B[a/x]}
.
$ \frac{\Gamma\vdash f_1\equiv f_2:\forall x:A.B\quad\Gamma\vdash a_1\equiv a_2:A}{\Gamma\vdash f_1~a_1\equiv f_2~a_2:B[a/x]}
.
等しさ$ \frac{\Gamma,x:A\vdash b:B\quad\Gamma\vdash a:A}{\Gamma\vdash(\lambda x.b)~a\equiv b[a/x]:B[a/x]}
.
外延性$ \frac{\Gamma\vdash f:\prod_{x:A}B}{\Gamma\vdash\lambda x.f~x\equiv f:\prod_{x:A}B}
.
等しさを保存する$ \frac{\Gamma\vdash A\equiv A':{\cal U}_i\quad\Gamma,x:A\vdash B\equiv B':{\cal U}_j}{\Gamma\vdash\prod_{x:A}B\equiv\prod_{x:A'}B':{\cal U}_{{\rm imax}(i,j)}}
判定にて等しい (judgment equality。定義上等しい (definitional equality))
對稱律$ \frac{\Gamma\vdash a_1\equiv a_2:A}{\Gamma\vdash a_2\equiv a_1:A} .
推移律$ \frac{\Gamma\vdash a_1\equiv a_2:A\quad\Gamma\vdash a_2\equiv a_3:A}{\Gamma\vdash a_1\equiv a_3:A} .
$ \frac{\Gamma\vdash a:A\quad\Gamma\vdash A\equiv B:{\cal U}_i}{\Gamma\vdash a:B}
.
$ \frac{\Gamma\vdash A\equiv B:{\cal U}_i\quad\Gamma\vdash a_1\equiv a_2:A}{\Gamma\vdash a_1\equiv a_2:B}
.
proof irrelevance$ \frac{\Gamma\vdash p:{\cal U}_0\quad\Gamma\vdash h:p\quad\Gamma\vdash h':p}{\Gamma\vdash h\equiv h':p}
.
extra$ \frac{\bar u.(e\equiv e':A)\in E\quad\forall i,n\vdash l_i~{\rm ok}}{\Gamma\vdash e[\bar l/\bar u]\equiv e'[\bar l/\bar u]:A[\bar l/\bar u]}
$ A:{\cal U}_iの型の族 (type family)$ B:A\to{\cal U}_i
恆等射$ {\rm id}:\equiv(\lambda X.\lambda x.x):\prod_{X:{\cal U}_i}X\to X
合成射。$ f:A\to B,$ g:B\to Cに對して$ f;g:\equiv\lambda x.g(f~x)であり、$ (\lambda(X,Y,X,g,f).f;g):\prod_{X,Y,Z:{\cal U}_i}(Y\to Z)\to(X\to Y)\to(X\to Z)
歸納的型 (inductive type)。以下の 4 つから構成される 構成規則 (formation rule)
構成子 (constructor)
除去子 (eliminator。歸納法原理 (induction principle))
計算規則 (computation rule)
構成規則$ \N:{\cal U}
構成子
$ 0:\N
$ {\rm succ}:\N\to\N
除去子$ {\rm ind}_\N:\prod_{P:\N\to{\cal U}}P(0)\to\left(\prod_{x:\N}P(x)\to P({\rm succ}(x))\right)\to\prod_{x:\N}P(x)
計算規則
$ {\rm ind}_\N(P,z,s,0)\equiv z
$ {\rm ind}_\N(P,z,s,{\rm succ}(x))\equiv s(x,{\rm ind}_\N(P,z,s,x))
自然數の倍$ {\rm double}:\N\to\N,$ {\rm double}:\equiv{\rm ind}_\N(\lambda x.\N,0,\lambda(x,n).{\rm succ}({\rm succ}(n)))
$ {\rm double}(0)\equiv 0
$ {\rm double}({\rm succ}(n))\equiv{\rm succ}({\rm succ}({\rm double}(n)))
依存和 (dependent sum)$ \sum_{x:A}B(x)
構成規則。$ A:{\cal U},$ A\to{\cal U}に對して$ \sum_{x:A}B(x):{\cal U}
構成子$ {\rm pair}:\prod_{x:A}B(x)\to\sum_{x:A}B(x)
除去子$ {\rm ind}_{\sum_{x:A}B}:\prod_{P:(\sum_{x:A}B(x))\to{\cal U}}\left(\prod_{x:A}\prod_{y:B(x)}P({\rm pair}(x,y))\right)\to\prod_{z:\sum_{x:A}B(x)}P(z)
計算規則$ {\rm ind}_{\sum_{x:A}B}(P,c,{\rm pair}(x,y))\equiv c(x,y)
存在量化に當たる
$ A,B:{\cal U}に對して$ A\times B:\equiv\sum_{x:A}B
$ {\rm pr}_1:\left(\sum_{x:A}B(x)\right)\to A,$ {\rm pr}_1({\rm pair}(x,y)):\equiv x
$ {\rm pr}_2:\prod_{z:\sum_{x:A}B(x)}B({\rm pr}_1(z)),$ {\rm pr}_2({\rm pair}(x,y)):\equiv y
直和 (coproduct)$ A+B
構成規則$ A,B:{\cal U}に對して$ A+B:{\cal U}
構成子
$ {\rm inl}:A\to A+B
$ {\rm inr}:B\to A+B
除去子$ {\rm ind}_{A+B}:\prod_{P:A+B\to{\cal U}}\left(\prod_{x:A}P({\rm inl}(x))\right)\to\left(\prod_{y:B}P({\rm inr}(y))\right)\to\prod_{z:A+B}P(z)
計算規則
$ {\rm ind}_{A+B}(P,l,r,{\rm inl}(x))\equiv l(x)
$ {\rm ind}_{A+B}(P,l,r,{\rm inr}(y))\equiv r(y)
unit type$ \bf 1
構成規則$ {\bf 1}:{\cal U}
構成子$ *:{\bf 1}
除去子$ {\rm ind}_{\bf 1}:\prod_{P:{\bf 1}\to{\cal U}}P(*)\to\prod_{x:{\bf 1}}P(x)
計算規則$ {\rm ind}_{\bf 1}(P,t,*)\equiv t
list 型。長さ$ nの型$ Aの要素の list$ {\bf Vec}(A,n)
構成要素$ A:{\cal U}に對して$ {\bf Vec}(A):\N\to{\cal U}
構成子
$ {\rm nil}:{\bf Vec}(A,0)
$ {\rm cons}:\prod_{n:\N}A\to{\bf Vec}(A,n)\to{\bf Vec}(A,{\rm succ}(n))
除去子$ {\rm ind}_{{\bf Vec}(A)}:\prod_{P:\prod_n{\bf Vec}(A,n)\to{\cal U}}P(0,{\rm nil})\to\left(\prod_{n:\N,x:A,s:{\bf Vec}(A,n)}P(n,s)\to P({\rm succ}(n),{\rm cons}(n,x,s))\right)\to\prod_{n:\N,s:{\bf Vec}(A,n)}P(n,s)
計算規則
$ {\rm ind}_{{\bf Vec}(A)}(P,z,c,0,{\rm nil})\equiv z
$ {\rm ind}_{{\bf Vec}(A)}(P,z,c,{\rm succ}(n),{\rm cons}(n,x,s))\equiv c(n,x,s,{\rm ind}_{{\bf Vec}(A)}(P,z,c,n,s))
等式型 (identity type)$ a=_A b
定義 1$ =_A
構成規則$ A:{\cal U}に對して$ \_=_A\_:A\to A\to{\cal U}
構成子$ {\rm refl}:\prod_{x:A}x=_A x反射律 除去子$ {\rm ind}_{=_A}:\prod_{P:\prod_{x,y:A}x=_A y\to{\cal U}}\left(\prod_{x:A}P(x,x,{\rm refl}(x))\right)\to\prod_{x,y:A,p:x=_A y}P(x,y,p)道歸納法 (path induction)
計算規則$ {\rm ind}_{=_A}(P,r,x,x,{\rm refl}(x))\equiv r(x)
定義 2$ a=
構成規則$ A:{\cal U},$ a:Aに對して$ a=_A\_:A\to{\cal U}
構成子$ {\rm refl}(a):a=a
除去子$ {\rm ind}_{a=}:\prod_{P:\prod_{x:A}a=x\to{\cal U}}P(a,{\rm refl}(a))\to\prod_{x:A,p:a=x}P(x,p)基點附き道歸納法 (based path induction)
計算規則$ {\rm ind}_{a=}(P,r,a,{\rm refl}(a))\equiv r