工学部情報学科

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

日時 火曜日2限(10:30〜12:00)
場所 総合研究4号館共通3総合研究7号館講義室1
担当教員:五十嵐 淳
オフィスアワー:金曜日 17:00〜18:00 (総合研究7号館224)
(その他の時間は要アポイントメント)
担当TA:四十坊 純也

お知らせ

講義内容

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

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

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

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

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

五十嵐 淳