Martin-Löf型理論
Martin-Löf型理論(マーティン=レーフかたりろん、Martin-Löf's type theory)
あらゆる数学的対象は型(type)を持つ。数学的対象$ a が型$ A を持つことを $ a: A
と書き、$ a は型$ A の要素(element)であるともいう。
数学的対象は変数(variable)に依存する場合もあり、$ a が変数$ x に依存するかもしれないことを強調するときは$ a を$ a[x] と書く。
$ a[x] 中$ x に数学的対象 $ b を代入して得られる数学的対象を $ a[b] と書く。
二つの数学的対象が等しいことを $ a \equiv b で表す。
数学的対象$ a に名前 $ f を付けるときには$ f:\equiv a と書き、$ f を$ a と定義するなどと言う。
型A, Bに対し、AからBへの関数型(function type)を$ A → B と書く。
変数$ x:A と要素$ b[x] :B に対し、λ-抽象(λ-abstraction) $ λ(x : A):b[x] : A → B
帰納的型
1. 構成規則 (formation rule)
2. 構成子 (constructor)
3. 除去子 (eliminator)
4. 計算規則 (computation rule)
1. 構成規則 (formation rule)
構成規則 はその型がとるパラメータなどを指定
2. 構成子 (constructor)
その型の要素を作るための定数や関数
3. 除去子 (eliminator)
その型から他の型への関数を作るもの
帰納法原理 (induction principle) とも呼ばれる
4. 計算規則 (computation rule)
除去子に構成子を適用したときにどのように簡略されるかという規則
============================
依存型理論を学習する
確認用
参考・出典
依存型理論をどうやって学べばいいか
関連