工学部情報学科

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

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

お知らせ

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

  1. 教科書の該当する章のファイルを Proof General (もしくは CoqIDE) で読み込む.
  2. Coq への読み込みコマンドを使いながら教科書を読み進める.
  3. 練習問題の指示に従ってファイルを書き換える(解答を埋める).
  4. Coq に読み込ませてみて,背景が青(緑)になれば無事に Coq のチェックに通った,ということ.(それでもエラーになる場合があります.下記 FAQ 参照.)
  5. 宿題提出システムを使って該当ファイルを zip したものをアップロードする.

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)

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

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

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

回数date内容(予定)資料宿題
110/6導入, Basics.vスライド0, スライド1テキスト Preface.v, Basics.v の予習,Coq 環境の構築,予習で生じた質問の報告(締切 10/13 10:30)
210/13Basics.v演習問題(締切 10/20 10:30: Basics.v の nandb, and_b3, factorial, blt_nat, plus_id_exercise), Induction.v の予習
310/20Induction.vスライド2演習問題(締切 10/27 10:30: Basics.v の andb_true_eliml2,Induction.v の basic_induction, double_plus, beq_nat_refl), 配布資料1の予習
410/27単純型付ラムダ計算配布資料1配布資料1の予習,Lists.v (の最初の方)の予習
(5)補講: 11/5(木5限)@7号館情報2 単純型付ラムダ計算(つづき),Lists.vスライド3演習問題(締切 11/17 10:30: Lists.v の snd_fst_is_swap, list_funs),Lists.v の残りの予習
511/10(休講)
611/17Lists.v, Poly.vスライド4演習問題(締切 11/27(金) 10:30: Lists.v の list_exercises, beq_natlist, hd_opt), Poly.v と配布資料2の予習
711/27(金2限)Poly.v演習問題(締切 12/8 10:30: Poly.v の poly_exercises, split, flat_map, override_neq) と配布資料2の予習
812/1教室での演習問題集
912/8System F, BasicTactics.v配布資料2
(10)補講 12/11(金5限) BasicTactics.vスライド5演習問題(締切 12/22 10:30: BasicTactics.v の silly_ex, sillyex1, sillyex2, plus_n_n_injective, beq_nat_true, destruct_eqn_practice)
1012/15(休講)
1112/22自然演繹とCoq配布資料3
121/5Logic.vスライド6演習問題(締切 1/12 10:30: Logic.v の and_assoc, iff_properties, or_distributes_over_and_2, contrapositive, not_both_true_and_false, false_beq_nat)
131/12Prop.v, MoreLogic.v スライド7, スライド8 演習問題(締切 1/26 10:30: Prop.v の b_times2 (2), gorgeous_plus13 (1), gorgeous_sum (2), ev_sum (2), inversion_practice (1), MoreLogic.v の dist_not_exists+ (1), dist_exists_or+ (2))
141/19カリーハワード同型対応講義資料
151/26教室での演習,期末試験について
期末試験2/2

リソース

教科書
Benjamin C. Pierce 他著 Software Foundations (本講義用: sf-201510.zip, 本家は版が古いので使わないでください.)
参考書
ボランティアによる教科書の和訳版(内容の食い違いについては教科書の記述を優先します.)
Coq: INRIA の公式サイト
ProofGeneral
emacs から Coq を操作するためのソフトウェア

igarashi@kuis.kyoto-u.ac.jp