工学部専門科目「計算と論理」

日時 火曜日2限(10:30〜12:00)
場所 総合研究7号館情報1
担当教員:五十嵐 淳
オフィスアワー:火曜日 16:00〜18:00 (総合研究7号館224)
(その他の時間は要アポイントメント)
担当TA:村瀬唯斗(通信情報システム専攻D2)

お知らせ

講義内容

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

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

回数date内容(予定)資料宿題
110/3 導入, Basics.v スライド0, スライド1 Coq 環境の構築,テキストのダウンロード
210/10 Basics.v, Induction.v スライド2 学生実験2のgitについての資料, GitHub での宿題提出 演習問題(締切 10/24 10:30: Basics.v の nandb, andb3, factorial, ltb, plus_id_exercise, zero_nbeq_plus_1, Induction.v の basic_induction, double_plus, eqb_refl, add_comm_informal)
310/17 単純型付ラムダ計算 配布資料1
410/24 単純型付ラムダ計算(つづき)
510/31 Lists.v スライド3 演習問題(締切 11/14 10:30: Lists.v の snd_fst_is_swap, list_funs, list_exercises, eqblist, hd_error)
611/7 Poly.v スライド4 演習問題(締切 11/21 10:30: Poly.v の poly_exercises, split, flat_map, currying)
711/14 多相ラムダ計算 System F 配布資料2 問題集
811/21 Tactics.v スライド5 演習問題(締切 12/5 10:30: Tactics.v の apply_exercise1, injection_ex3, discriminate_ex3, eqb_true, destruct_eqn_practice)
911/28 演習 (範囲: 問題集1〜3節)
1012/5 Logic.v スライド6 演習問題(締切 12/19 10:30: Logic.v の and_assoc, contrapositive, not_both_true_and_false, or_distributes_over_and, dist_exists_or, In_app_iff, logical_connectives)
1112/12 自然演繹と Coq 配布資料3
1212/19 IndProp.v スライド7 演習問題(締切 1/16 10:30: IndProp.v の ev_double, inversion_practice, ev_sum, le_and_lt_facts の一部 (le_trans と O_le_n と le_plus_l)
131/9 カリーハワード同型対応,ProofObjects.v 配布資料4, スライド8
141/16 演習 (範囲: 問題集全部)
期末試験?

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

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

五十嵐 淳