型理論のお勉強

型理論で良く出てくるのが、依存型である。これは、ある型が別の型に依存して いたり、ある型の値に依存して決まったりできるような型のこと。

これにはdependent sum(Σ)というのとdependent product(Π)というのがある。 何となく説明を読んだりして分かった気になるのだけれど、人に説明できる ほどではないような気がするので、Programming in Martin-Löf's Type Theory を元に勉強してまとめる。

CoqとかAgdaを使えるようになるには、このあたりの最低限の理解が必要だと思う。


2章の導入をまず読んでみる。

大切な考え方は、命題を集合と同一視するということ。普通の数学でするように、命題は 必ず真か偽かどちらか一方である、という考え方ではなく、命題が真であるのは、それを証明できるとき だけである、とする考え方に基づいている。

A∨¬Aという命題は、Aが真か偽かのどちらかなので、いずれにせよ真である、と考えることも出来る。 一方、論理和の一方が証明できたときに、上記命題が真である、とする立場もある。 これが型理論が元とする考え方となる。

この考え方を進めて、

A⊃Bの証明とは、Aの証明を与えたときに ...

more…