工学部情報学科

計算と論理 (科目コード 90860)

日時 火曜日2限(10:30〜12:00)
場所 総合研究7号館情報1講義室
担当教員:五十嵐 淳
オフィスアワー:月曜日 17:00〜18:00 (総合研究7号館224)
(その他の時間は要アポイントメント)
担当TA: 西川 剛史

お知らせ

講義内容

数理論理学の基礎と,数理論理学を用いた計算機プログラムの検証について講述する.また,講義を補完するため,証明支援系(計算機上で数学的証明を行うシステム)である Coq を用いた演習を行う.

講義スケジュールと配布資料

回数date内容(予定)資料宿題
110/1 導入, Basics.v スライド0(改訂版), スライド1 Coq 環境の構築,テキストのダウンロードと Preface.v, Basics.v, Induction.v の予習復習
210/8 Basics.v, Induction.v スライド2 学生実験2のgitについての資料, GitHub での宿題提出 演習問題(締切 10/15 10:30: Basics.v の nandb, andb3, factorial, ltb, plus_id_exercise, zero_nbeq_plus_1) (締切 10/22 10:30: Induction.v の basic_induction, double_plus, eqb_refl)
310/15 単純型付ラムダ計算 配布資料1
410/29 単純型付ラムダ計算(つづき)
511/5 Lists.v
611/12 Poly.v
711/19 多相ラムダ計算 System F, Tactics.v
811/26 Tactics.v
912/3 教室での演習
1012/10 Logic.v
1112/17 自然演繹と Coq
1212/24 IndProp.v
131/7 カリーハワード同型対応,ProofObjects.v
141/21 教室での演習
期末試験?

自習の進め方(宿題について)

  1. 教科書の該当する章のファイルを Proof General (もしくは CoqIDE) で読み込む.
  2. Coq への読み込みコマンドを使いながら教科書を読み進める.
  3. 練習問題の指示に従ってファイルを書き換える(解答を埋める).
  4. Coq に読み込ませてみて,背景が青(緑)になれば無事に Coq のチェックに通った,ということ.ただし, Proof General, CoqIDE は Qed. の打ち忘れ(よくある!)を関知してくれないので,make XXXX.vo (XXXX.v をチェックするなら)を実行するか CoqIDE で Compile → Compile Buffer を実行して再確認してください.

FAQ

Proof General, CoqIDE の操作

機能 Proof General CoqIDE (メニュー操作)
一歩読み進める(Coq にテキストの内容を送信) C-c C-n Navigation → Forward
一歩戻る (undo) C-c C-u Navigation → Backward
カーソル位置まで進む(戻る) C-c RET Navigation → Go to
ファイル末尾まで読み込む C-c C-b Navigation → End
証明すべき命題(ゴール)を表示 C-c C-p
既になされた証明・定義を表示 C-c C-t
SearchAbout C-c C-a C-a Queries → SearchAbout (F2)

リソース

教科書
Benjamin C. Pierce 他著 Software Foundations シリーズ 第1巻 Logical Foundations (この本家版は時おりバージョンアップがあるので使わないでください.)
参考書
ボランティアによる教科書の和訳版(元になった版は2011年版です.内容の食い違いについては教科書の記述を優先します.)
Coq: INRIA の公式サイト
ProofGeneral
emacs から Coq を操作するためのソフトウェア.
Company-Coq
ProofGeneral の拡張集. forall と打つと ∀ で表示されたりするのでうれしい. 自動補完などもできる.
coquille
vim から Coq を操作するためのソフトウェア.(使ったことありません.動作報告求む.)
Coqoon
Eclipse から Coq を操作するためのプラグイン.(使ったことありません.動作報告求む.)
vscoq
Visual Studio Code から Coq を操作するためのプラグイン.(使ったことありません.動作報告求む.)

五十嵐 淳