「型の理論」と証明支援システム

「ギョエテとは、俺のことかとゲーテいい」
「Voevodsky(僕は「ヴォヴォスキー」と呼んでいたのだが、いい加減かもしれない)」と書いたのだが、やはり、いい加減だったかも。
ウィキを見たら「ヴォエヴォドスキー」と書いてある。英文wikiには、/vɔɪˈvɒdski/ と発音記号が出ている。(ちゃんと調べろよ)
字面を見たら wiki が正しそうだ。でも、ビデオを見ていると、僕には、そう聞こえたのだが。「ヴォ[イ]ヴォ[ド]スキー」。ま、許してください。今、発音、練習中です。
数学の証明にコンピュータを使おうという彼のアイデアを、以前(2013年)、マルレクで取り上げたことがある。「「型の理論」と証明支援システム -- Coqの世界」https://goo.gl/S6u41w
話せば長い話なので、今回は、まず、そのマルレクの「はじめに」の部分を紹介する。
-----------------------
現在、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を授賞した。
型の理論と証明支援システムに対する関心が広がることを期待したい。
-----------------------
DRIVE.GOOGLE.COM

コメント

このブログの人気の投稿

マルレク・ネット「エントロピーと情報理論」公開しました。

初めにことばありき

人間は、善と悪との重ね合わせというモデルの失敗について