工学部情報学科

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

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

お知らせ

講義内容(シラバスより)

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

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

回数date内容(予定)資料宿題
110/2 導入, Basics.v スライド0, スライド1 Coq 環境の構築,テキストのダウンロードと Preface.v, Basics.v の予習
210/9 Basics.v, Induction.v スライド2 学生実験2のgitについての資料, GitHub での宿題提出 演習問題(締切 10/16 10:30: Basics.v の nandb, andb3, factorial, ltb, plus_id_exercise, zero_nbeq_plus_1) (締切 10/23 10:30: Induction.v の basic_induction, double_plus, eqb_refl)
310/16 単純型付ラムダ計算 配布資料1
410/23 単純型付ラムダ計算(つづき)
510/30 Lists.v スライド3 演習問題(締切 11/13 10:30: Lists.v の snd_fst_is_swap, list_funs, list_exercises, eqblist, hd_error)
611/6 Poly.v スライド4 演習問題(締切 11/20 10:30: Poly.v の poly_exercises, split, flat_map, currying)
711/13 多相ラムダ計算 System F, Tactics.v 配布資料2, スライド5
811/20 Tactics.v 演習問題(締切 12/4 10:30: Tactics.v の apply_exercises1, injection_ex3, discriminate_ex3, plus_n_n_injective, eqb_true, destruct_eqn_practice)
911/27 Logic.v スライド6 演習問題(締切 12/11 10:30: Logic.v の and_assoc, contrapositive, not_both_true_and_false, or_distributes_over_and, dist_exists_or, In_app_iff, eqb_neq)
1012/4 教室での演習 問題集
1112/11 自然演繹と Coq 配布資料3
1212/18 IndProp.v スライド7
1312/25 (休講)
141/8
151/29(?) 教室での演習
期末試験?

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

  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 を操作するためのプラグイン.(使ったことありません.動作報告求む.)

五十嵐 淳