電気通信大学1年の伊藤です。情報工学工房の今年のコースの1つ、「Coqで学ぶ計算機ソフトウェアの基礎」の紹介をします。
授業内容を簡単に説明すると、毎回宿題として教科書を読み、証明の問題を解いてきて、解いてきた証明について、授業中に解説などをする、と言った感じです。
この授業の大きな特徴は、証明に「Coq」を使うことです。Coqというのは、証明が正しいかどうかを検証してくれるツールです。証明というと日本語や英語などの自然言語で書くのが普通ですが、Coqを使った証明では、プログラミング言語を使います。
証明の内容は、基本的な自然数の性質やリスト(配列)の性質を証明したり、とても簡単なプログラミング言語を定義してその性質を証明をしたり、アルゴリズムの正しさ(思った通りの振る舞いをするか)を確かめたり、といった感じです。教科書で扱うものはどれも、世の中で実際に扱われている対象を簡易化したものですが、演習問題は難しく、私は結構苦戦しています。
上の画像は、実際に証明を組み立てている画面です。鳩の巣原理を証明しようとしています(鳩の巣原理を知らない場合は調べて下さい)。まだ証明できていません。演習問題の答えをネット上の検索エンジンで検索できる場所に上げないで下さいと教科書に書いてあるので、一応まだ解けていない問題を選んでみました。こんなことも証明できるのかと驚いた問題の1つです。まだ証明できていませんが…
まだまだ授業は続くので、引き続き腕を磨いていきたいと思います。