型理論のお勉強
型理論で良く出てくるのが、依存型である。これは、ある型が別の型に依存して いたり、ある型の値に依存して決まったりできるような型のこと。
これにはdependent sum(Σ)というのとdependent product(Π)というのがある。 何となく説明を読んだりして分かった気になるのだけれど、人に説明できる ほどではないような気がするので、Programming in Martin-Löf's Type Theory を元に勉強してまとめる。
CoqとかAgdaを使えるようになるには、このあたりの最低限の理解が必要だと思う。
2章の導入をまず読んでみる。
大切な考え方は、命題を集合と同一視するということ。普通の数学でするように、命題は 必ず真か偽かどちらか一方である、という考え方ではなく、命題が真であるのは、それを証明できるとき だけである、とする考え方に基づいている。
A∨¬Aという命題は、Aが真か偽かのどちらかなので、いずれにせよ真である、と考えることも出来る。 一方、論理和の一方が証明できたときに、上記命題が真である、とする立場もある。 これが型理論が元とする考え方となる。
この考え方を進めて、
A⊃Bの証明とは、Aの証明を与えたときに、Bの証明を与える関数(あるいは手続き)である
と考える。この考え方だと、λx. xというのは、A⊃Aの証明と考えられる。なぜなら、与えられた 入力(A)をそのまま返すからである。同様に、
A&Bの証明とは、Aの証明とBの証明のペア(つまり直積)である
と考える。命題を、その証明の集合と同一視するというのがミソである。そのため、命題が真 であるのは、その命題に対応する集合が空集合ではないときである。
否定は次のように定義できる：
¬A ≡ A⊃⊥
⊥は矛盾、つまり空集合に対応させる。
命題論理を表現するには、多くの関数型プログラミング言語に存在する型を使うことで 足りる。でも限量子を表現するには、集合の集まりについての操作が必要になる。存在記号は 次のように解釈する。
(∃x∈A)B(x)の証明とは、集合Aの要素aとB(a)の証明とからなるペアのことである
ここで、ペア〈a, b〉ただし、a∈A, b∈B(a)からなる集合を(Σx∈A)B(x)と書くことにすると、
(∃x∈A)B(x)は、集合(Σx∈A)B(x)と同一視される
となる。同じように、全量化についても、
(∀x∈A)B(x)の証明とは、集合Aの各要素aについて、B(a)の証明を与える関数である
と考える。この「集合Aの要素aを与えると、B(a)の要素を返す関数」を要素とする 集合を(Πx∈A)B(x)と書くことにする。したがって、
(∀x∈A)B(x)は、集合(Πx∈A)B(x)と同一視される
となる。