Martin-Löf型理論
Martin-Löf型理論(マーティン＝レーフかたりろん、Martin-Löf's type theory; MLTT)
値によって型が変わる依存型というものが組み込まれている型理論 $ A , $ A\ \mathrm{type}
型A
Aは型である
詳細はわからないけれど、近年は$ A\ \mathrm{type} と書く。おそらくこの方が混乱が少ないのだろう。
$ a : A
あらゆる数学的対象は型(type)を持つ。数学的対象$ a が型$ A を持つことを$ a: A と書く $ a は型$ A の要素(element)であるともいう。
$ a[x]
数学的対象は変数(variable)に依存する場合もあり、$ a が変数$ x に依存するかもしれないことを強調するときは$ a を$ a[x] と書く。
$ a[x] 中$ x に数学的対象 $ b を代入して得られる数学的対象を $ a[b] と書く。
$ a \equiv b
二つの数学的対象が等しいことを $ a \equiv b で表す。
数学的対象$ a に名前 $ f を付けるときには$ f:\equiv a と書き、$ f を$ a と定義するなどと言う。
$ a =_A b : A
二つの式a, bが、型Aの内部で等しいこと
$ α = β : \mathrm{Type}
二つの型α、βが等しいこと
$ B(x)
$ A → B
型A, Bに対し、AからBへの関数型(function type)
型A, Bに対し、AからBへの関数型(function type)を$ A → B と書く。 $ \sum_{x:A}B(x)
$ \prod_{x:A}B(x)
変数$ x:A と要素$ b[x] :B に対し、λ-抽象(λ-abstraction) $ λ(x : A):b[x] : A → B
確認用
Q. Martin-Löf型理論
Q. 依存型理論
参考・出典
メモ