Coqとのはじめての対話
【 ファースト・インプレッション 】
今回のセッションの目的は、はじめてCoqに触れる人に、Coqという言語のイメージを持ってもらうことです。当面は、Coqをインストールして実際に動かしてみなくとも、テキストでCoqの基本的な動きを説明したいと思っています。
ファースト・コンタクトでのファースト・インプレッションは大事なものです。ただ、この点では、今回の導入は少し危険な冒険をしています。
というのも、Coqは関数型言語としても使えますので、LISPの親戚のように紹介することもできるのですが、ここではそうしませんでした。Coqでの「証明」のサンプルを紹介しています。それがCoqの一番重要な働きだと考えているからです。
もちろん、「証明」のサンプルには、簡単なものを選びました。ここで「証明」していることは「すべての命題Aについて、AならばAである。」という命題です。
「「AならばA」だって？ そんなのを、同語反復という。」
「自明のことだろう。」
「そんなことに、証明が必要なわけ？」
ファースト・コンタクト、最初から悪印象を残しそうです。
僕がCoqでの「証明」の紹介を続けると、さらに悪いことが続きます。
「そんなのが証明なわけ？」
「意味わからん」
「ChatGPTなら、誰でも最初からすごいと思うよ」
確かに。
それは、ChatGPTのような大規模言語モデルにもとづく「人工知能」技術が、我々人間に、生まれつき誰にも備わっている「言葉の意味を理解する能力」に、直接、訴求しているからです。
ただ、ことばにとって「意味」が本質的に重要であるように、数学にとっては「証明」が、やはり本質的に重要なのです。我々の日常の世界は、ほとんど「ことばとその意味の世界」で満ち足りてているように見えるかもしれません。ただ、我々の認識の発展史からみれば、それは「世界」の一面です。
今回の「導入」で悪印象を与えたかもしれないことには、もう一つ理由があります。それは、今回の「Coqとのはじめての対話」が、人間とCoqとの「対話」になっていなかったことに原因があると考えています。
Coqは、機械と人間との対話で証明を進めます。それが大きな特徴です。Coqは「証明支援システム」と呼ばれるのですが、この言葉だけだと「人間の証明を支援する」システムということになります。ただ、対話を続けていくと、「機械の証明を人間が支援しているのでは？」という不思議な気持ちになることがあります。
こうした、奇妙な連帯感を説明するのは難しかったのですが、GitHubのCoPilotで開発を進めている多くの開発者も、こうした感情を共有できるのではと感じています。
-------------------------------------
ショートムービー「Coqとのはじめての対話 」を公開しました。https://youtu.be/CVnjUwUcHa8?list=PLQIrJ0f9gMcPrNFRG1sEmtCRDnemxc1Pc
資料 pdf「 Coqとのはじめての対話 」https://drive.google.com/file/d/1jqJFqKpWk6bBNXaWo52iMQmRw0wNTY0v/view?usp=sharing
コメント
コメントを投稿