Personal Fabrication

音楽、勉強・読書記録、日常の感想

Coqで大学数学に入門する[2.学習の流れと現在の課題]

以前の記事では、Coqの簡単な紹介と現在の僕の課題について簡単に書きました。

Coqと共に大学数学に入門する【1.簡単な導入】 - Personal Fabrication

 

今回はもう少し整理をして、実際にCoqと数学を融合するには、どのような手順で学ぶかを書こうと思います。また、現状最大の課題についても書きます(以前の記事でも書きましたが)。

 

現在の僕の力程度であれば、“誰でも”反復練習で身に付けられます。しかし、ここまでの能力を身につけるだけでも、証明という営みがかなりクリアになるはずです。

サンプルが僕だけなので一般化することはできませんが、数学書の証明を読む際「これはどういう着想で証明を始めたのだろう?」、「どうやったら証明が終わったことになるの?」などの悩みを抱えている過去の僕のような方には、全力でオススメします。

 

少しだけ余談(経験談)です。

僕は、高校数学の初歩的な参考書白チャートの証明問題を解く際、証明をどこから手をつけて良いのか全くわかりませんでした。解答を読んでも、僅かながら理解度が上がる程度でその問題は解決しませんでした。なぜなら、解答の思考は当然のように“上から下”に向かう進んでいくのですが、実際の問題を解く際は、“上から下”に加えて“下から上”の思考を必要とすることに気付いていなかったからです。もう少し具体的にいうと、証明は、仮定と証明すべきこと(ゴール)を明確にする前処理からスタートし、「ゴールを成り立たせるにはこれが必要だな」と徐々に証明を上に展開する流れを理解すると言えば良いでしょうか。与えられた仮定やゴールを闇雲にいじっても証明は完成しません。仮にたどり着けたとして、単なる偶然でしょう。

これは高校数学の話でしたが、Coqは、まさにその問題を解決しています。基本的に“下から上”がCoqの証明の流れです。したがって、証明が苦手な人の思考を矯正するギブスとしても、Coqは役に立つと思います。

 

本題に戻ります。

僕は、直接的に学んだことはないですが、Coqを通してはじめに学ぶことは、記号論理学だと思います。*1「じゃあ記号論理学を学べば良いのでは?」と思われる方がいると思いますが、少し複雑な論理式の操作が必要な練習問題などを解く際、自分の操作の正しさを自分自身で検証しながら練習問題を解くのは簡単ではないと思います。

 

また、上に述べた通り僕は、記号論理学を学んだことがないので注意喚起程度ですが、記号論理学の教科書が、論理式が仮定に存在する場合と結論に存在する場合で取り扱い方が全く異なることを述べていないのであれば、実際の数学には不十分だと思います。

 

Coqはそれらの問題を解決してくれます。Coqは誤った操作を許してくれないので、Coqと共に自分の操作の正しさを検証しながら安心して証明を書くことができます。

 

Coqを使用する利点を理解していただいたところで、今回の本題、Coqと共に数学の証明を学ぶ流れについて書こうと思います。

まず、数学書に書かれていることが、論理記号の集まり(論理式)に直す(変換する)ことができることを知りましょう。より具体的にいうと、論理式は、->(ならば)、/\(かつ)、 \/(ならば)、~(否定)、=(イコール)、∀(forall)、∃(exists) などから構成されています。

 

まずは、Coqでこれらの記号の取り扱いに習熟することが第一ステップになります。

より細かく分けると、はじめに、->(ならば)、/\(かつ)、 \/(または)、~(否定)、=(イコール)の記号の操作に慣れましょう。

数学における証明は、仮定(証明の道具箱)と結論(ゴール)から構成されています。そして、上でも少し触れましたが、例えば、A/\B が仮定にある場合と結論にある場合で全く扱い方が異なります。/\以外の論理記号についても同様なので、論理式が仮定にある場合と結論にある場合の取り扱いを混同せず、機械的に処理できるようになりましょう。

 

第二ステップは、 forall と exists の操作に習熟することです。

量化記号と言われるこれらは、取り扱う上で少し厄介な存在ですが、慣れれば機械的に処理できるようになります。

 

第三ステップは、二重否定除去則、排中律、対偶の扱いに慣れることです。これらの規則はしばしば証明の過程で登場します。慣れてしまえば、さほど難しくはないです。

 

冒頭の繰り返しになりますが、ここまでのステップは、文字通り“誰でも”反復練習で身に付けられるので全く恐れる必要はありません。

 

次に、数学書を読むステップに入ります。

先に伝えておくと、もしかすると、ここは果てしなく続くステップかもしれません。

数学書に書かれていることをCoq語(論理式)に置き換えて、機械的な手順で証明を構成します。ここが非常に難しいところで、現在の僕の最も大きな課題です。何故かというと、数学書が、必ずしも論理式で書かれていないこと、証明すべきことの仮定と結論が明確でないことなどがあげられます。

この問題を解決する能力を獲得したいのですが、今の僕には、そうした能力を向上させる方法がわかりません。ただ、論理式の機械的な操作に習熟し、数学書に書かれた内容を論理式に置き換える能力を身につけることは、数学書を読む基礎能力そのものだと考えています。

 

正直、難しい概念を扱う数学をしている方々を羨ましく思うこともありますが、僕は先に数学書を正確に読む基礎能力を身につけようと思っています。

私の師匠曰く、

Coqを通じて数学をすることが数学書を正確に読む唯一の正しい方法だと思います

とのことで、僕もそれを信じています。僕自身、数学書の論理的ギャップを埋め、自分の証明の正しさを確認し、厳密な数学のシステムに従って数学し、基本的な式変形(対偶や量化子の否定など)でさえ証明可能な、現在の数学の学び方にとても満足しています。そして、このスタイルで、より難しい数学を学びたいと思っています。

 

もし、それを可能とする方法論を確立できたのであれば、多くの大学数学挫折者を減らせるとも考えています。三流私大卒、根っからの文系、大卒後から小学校レベルから数学を独学、計算嫌いな僕でも、今のところはそれなりに上手くいっているので大丈夫です。(この記事を読んでいる皆さんの方が、間違いなく賢いと思います)

 

ただ、上で述べたように、現状最大の課題である数学書に書かれていることをCoq語(論理式)に置き換える能力の開発方法を見つけられていません。そこで、こういう風にブログを書いて、皆さんの力を借りたり、勉強仲間を探そうと思った訳です。

 

 

とりあえず、Coqの理解度をあげることが有効と考えるに至ったので、以下のCoq'Artという本で勉強しようと思っています。

Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

 

 

 

 「一緒に勉強したい!」、「Coqに興味ある!」なんて思う奇特な方は、是非一緒に勉強しましょう! 勿論、数学学習について過去の僕と同じ悩みを共有する人も大歓迎です(むしろ、そっちの方が嬉しい)。大阪or京都であれば、カフェや図書館などで直接顔を合わせて勉強しましょう。距離がある場合は、スカイプの導入も検討します。

 

フォロー外からでもDM開放しているので、Twitterから連絡ください。

Twitterしてないよという方は、頑張ってアカウントを作るか、ブログのコメントに捨てアドを書いてください。そこから僕が連絡します。


 

*1:ただ、僕の学習方針の場合で、+の定義を書いたりする人もいると思います