型理論
type theory
基礎論として見た時、集合論は公理系 + 論理だが、型理論は兩方を包含してゐる 記號
證據 (assumption。文脈 (context)。環境 (environment)。型宣言列。基底 (basis))$ \Gamma,\Delta,\dots
$ s:S,t:T,\dotsの有限な列
項 (term)$ s,t,\dots
型 (type)$ S,T,\dots
判定 (judgment。assertion)
$ \Gamma~{\rm ctx}。$ \Gammaは證據である
$ \Gamma\vdash T~{\rm type}。證據$ \Gammaの下で$ Tは型である
$ \Gamma\vdash T:{\rm Type}や$ \Gamma\vdash T\in{\cal U}とも書く
$ \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は等しい
※出現する項や型は well-defined である (well-typed)
理論により異なる
例
$ \frac{\Gamma\vdash s:S\quad\Delta\vdash S\equiv T}{\Gamma,\Delta\vdash s:T}
$ \frac{}{\vdash 0:{\rm Nat}}
よく定義する型
空型 (empty type。0 type)$ \bot,$ 0,$ \varnothing 單型 (unit type。1 type)$ \top,$ 1 Boolean 型 (Boolean type。2 type)$ \sf bool,$ \Bbb B,$ 2
函數型 (function type)$ A\to B
直積型 (product type)$ A\times B
直和型 (sum type)$ A+B
依存積 (dependent product)$ \prod_{a:A}P(a),$ \prod a:A.P(a)
依存和 (dependent sum)$ \sum_{a:A}P(a),$ \sum a:A.P(a)
型演算$ \lambda\underline\omega 型無しλ計算
分岐型理論 (ramified type thory)
依存型理論 (dependent type theory)
table:型理論:homotopy
型 A 空閒 A
要素 a:A 點 a∈A
依存和 Σ 全空閒
依存積 Π 切片の空閒
等式型 a1=a2 a1からa2への道の空閒
一價性公理 (univalence axiom)
等式型 (identity type。path type)
高階歸納的型 (higher inductive type)
樣相 homotopy 型理論
部分構造型 (substructual type system) pure type system