「型の理論」と証明支援システム -- Coqの世界
2013年12月16日 マルレク
現在、HoTT(Homotopy Type Theory)と呼ばれる新しい型の理論とそれを基礎付けるUnivalent Theoryと呼ばれる新しい数学理論が、熱い関心を集めている。Univalent Theoryは、数学者のVladimir Voevodskyが、論理学者Per Martin-Löfの型の理論を「再発見」したことに始まる。この新しい分野は、21世紀の数学とコンピュータサイエンスの双方に、大きな影響を与えていくだろう。
「証明支援システム」は、人間の証明をコンピュータが支援するシステムである。ただ見方を変えれば、それは、コンピュータの証明を人間が支援しているシステムだと考えることも出来る。コンピュータの進化が進んでいる方向の先には知性を持つ機械の実現があると筆者は考えている。「証明支援システム」での人間と機械の、証明をめぐる双対的な「共生」は、それに至る一つの段階なのだと思う。
小論は、HoTTを直接の対象とはしていない。HoTTにいたる型の理論のオーバービューを与え、Martin-Löfの型の理論に基づいた証明支援システムCoqの初等的な紹介を行うことを目的にしている。
おりしも、Coqは、今年2013年に、ACMのSIGPLANのProgramming Languages Software Awardを授賞した。型の理論と証明支援システムに対する関心が広がることを期待したい。
