不完全性定理の理解不完全性

大阪大学に赴任してから半年たったぐらいの2019年2月頃に、離散数学と計算の理論という題目の講義を4月から担当することに決まった。その理由は、その講義を元々担当していた当時研究室の准教授だった先生が、他大学の教授へとご栄転されることが決まったからである。

自分はネットワークシステム、分散・P2Pコンピューティング、ネットワークセキュリティが専門でどちらかというと実装よりなので、数学はあまりやってこなかったのだが、今はプログラミング言語理論を習得するために論理学や計算モデルを勉強していたので引き受けることにした。この講義は大阪大学のProSecというコースを申し込むと、社会人でも受講することができるようになっている（コースは有料だけど）ので、詳細は「大阪大学 prosec」で検索してほしい。（現5月時点で申し込むと、秋からの受講になるだろうが）

プログラミング言語を真面目に初めた理由は、最近はネットワーク業界でもソフトウェア定義や、プログラマブルスイッチなどと言われているため、数年後にはプログラミング言語理論の知識が必要になるのではないかと漠然と思っていたからであった。実際に活かせるかどうかはこれからの研究にかかっているので、乞うご期待といったところである。

そんなこんなで講義を担当することが決まり慌ててシラバスを決めたのだが、自分の担当は以下のようにした。

1. 命題論理
2. 述語論理
3. 計算可能性
4. 不完全性定理
5. λ計算
6. 型システム

4回で不完全性定理まで行くのはかなり駆け足な気がするが（2人の先生で15回なのでこんな感じに）、大阪大学の学生は優秀なので大丈夫だろう。問題は自分の方である。内容を決めたは良いが、勉強のし直しが大変だった。3月からは、家に帰ってからは数学の本を読むことに時間を使った気がする。今はゴールデンウィークだが、不完全性定理はめちゃくちゃ大変で、ゴールデンウィークの半分は不完全性定理で消えてしまった。なぜシラバスに入れたかと自分を恨んだりもしたものだ。ツライ。

不完全性定理を学ぶ上でいろいろな文献を参考にしたが、数年前に買った「コンピュータは数学者になれるのか？」という書籍がとてもためになった。しかし、この本は一般書の顔をしているが数学がある程度わかる人向けなので、誰得感が否めない。前半の1、2章で述語論理の導入から初めて不完全性定理まで行くというハイペースぶりである。自分はとてもためになったので、俺得ではあるのだが。まだ不完全性定理の理解は不完全なので、今後はもう少し落ち葉拾いをしていきたい。

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-

この講義では簡単な原始帰納的関数をHaskellで実装したり、型付λ計算で簡単な型推論エンジンを実装したりもする予定なので、内容的にはかなり面白いのではないかと思う。特にうちは工学部なので、数学をプログラミングに活かせたほうが学生にもよいだろう。

他にも、大阪大学のProSecでは、ファイアウォール演習、レジスタマシンのエミュレータ実装演習、多層防御の演習なども自分が担当する予定なので、こちらも準備しないといけない。無事に乗り切りたいところである。