Computational Logic

計算論理学 (けいさんろんりがく)

担当教員: 亀山幸義 (kam[at]cs.tsukuba.ac.jp)、海野広志 (uhiro[at]cs.tsukuba.ac.jp)
担当TA: 坂口 (sakaguchi [at] logic.cs.tsukuba.ac.jp)
曜日・時限: 秋AB, 木 5-6
教室: 講義は 3A207、演習は情報科学類計算機室 3C113

このページには，2015年度の『計算論理学』の情報を置きます．

連絡事項

[2015/12/17] 来週実施する、期末試験についての情報をこのページの下の方に書きました。資料等の持ち込み「可」です。
演習用ファイルCoreML.v 問題番号 e267 のバグが取りきれていませんでした。これについても，別ページの説明に追記しました。
演習用ファイルCoreML.v とEval.v に，合計3箇所のバグがありました． (問題番号 e266, e267, ex524) これについて，別ページの説明を読んでください．
11/19 の授業は、5限、6限とも計算機室で演習です。
[2015/10/29] latex で証明図・型推論図をきれいに書きたい、という人のために、やり方の一例を書きました。このページの下の方の「演習資料」の「Latexの proofマクロで証明図を書く方法」を見てください。
[2015/10/29] 10/29 の6限は演習でした。課題が出ていますので、このページの下の方を見て提出してください。
命題論理(PropLogic.v)について、授業以外の時間にやってもらう演習の課題(締切: 2015/11/4深夜)をアップロードしました。
[2015/10/09] 演習システムでの、論理記号の結合力(左結合か、右結合か)について、補足情報のページに書きました。
[2015/10/08] 今日の演習でレポートを出題しました。締切は 10/9 (夜)です。manabaから提出してください。質問、問合せは、complogic[at] logic.cs.tsukuba.ac.jp に送ってください。(教員とTAが読みます。)
[2015/10/05] 2回目の授業の2コマ目(6限)は、情報科学類計算機室で演習です。演習で使うCoqシステムの説明等のページへのリンクを、このページからはりました。下の方を見てください。
[2015/10/05] 1回目の授業で使ったスライドをここに置きました。(説明したのは、このスライドの前半だけです。後半は、授業の8週目頃に説明します。)
[2015/09/30] 担当TA名などを更新。
[2015/03/09] このページを作成。

授業概要

シラバスはこちら。

論理体系と型理論体系は本質的に同じ構造を持つという観点に立ち、両者を一体のものとして、形式体系と意味について述べる。講義とともにソフトウェアを用いた演習を実施して理解を深める。

講義テキスト

[注意] 以下に置いてあるテキストは、授業2週間程度前までは変更の可能性があります。

演習資料

演習についての質問，問合せは，complogic@logic.cs.tsukuba.ac.jp あてにメールしてください．(このアドレスに送ると、教員およびTA に届きます。)
レポート提出先: manabaシステム (登録キーは 9019456 です)
Coqの使い方
補足情報 (最終更新 2015/10/9)
Latexの proofマクロで証明図を書く方法: proof.styファイルをダウンロードし、サンプルのような latexファイルを書いてコンパイルすると、このようなpdfファイルができます。

命題論理の演習 (PropLogic.v)
1. 命題論理のファイルについて
2. 10/8の演習における課題 (締切: 10/9深夜)
3. 命題論理の証明(PropLogic):
4. 課題 (締切: 2015/11/4深夜)
型付きラムダ計算の構文・型付け (SimpleType.v)
1. 講義資料と演習システムでの記号の違い (講義資料の一部)
2. 10/29の演習課題 (11/4夜まで)
関数型プログラム言語の体系の型付け (CoreML.v)
1. 11/12講義, 11/19演習 (締切は、12/2(水) 深夜)
2. CoreML.vというファイルを置きました。講義資料6章の「関数型プログラム言語の体系」の型付けに対応するファイルです。このファイルは、CoreMLDef.v (およびそれをコンパイルした CoreMLDef.vo)の定義を使っていますので、3つのファイルを全部、自分のところにコピーして使ってください。
関数型プログラム言語の体系における計算 (Eval.v)
1. 11/12講義, 11/19演習 (締切は、12/2(水) 深夜)
2. Eval.vというファイルを置きました。(以前に置いてあった CoreMLRed.v というファイルを整理したものなので、ファイル名も変更しました。) このファイルは、EvalDef.v (およびそれをコンパイルした EvalDef.vo)の定義を使っていますので、3つのファイルを全部、自分のところにコピーして使ってください。
3. 講義資料6章における「計算」の定式化に関するものです。なお、6章における「計算」の定義は、授業の時点で見つけたバグを修正したものを置いてあるので、演習の際には再度ダウンロードしてください。
4. Coqでの表現・記号の詳細は、 Coq上の演習システム(続き) を見てください。
多相型プログラム言語の体系の型付け (PolyML.v)
1. 多相型の講義は後まわしにすることにしたので、演習は、発展課題とします。

授業日程

以下の内容は予定であり、講義の進展に合わせて若干の変更があります。 (11/5 に微調整しました。)

10/1 (亀山) はじめに、型のないラムダ計算
10/8 (亀山) 命題論理、演習
10/15 授業なし (月曜授業日)
10/22 (亀山) 命題論理(続き)、単純型付きラムダ計算
10/29 (亀山) 単純型付きラムダ計算(続き)、演習
11/5 (亀山) 論理と計算の関係，関数型言語
11/12 (亀山) 型検査と型推論
11/19 (亀山) 計算機室で演習
11/26 授業なし (推薦入試)
12/3 (亀山) 多相型計算，ここまでのまとめ
12/10 (海野) 依存型とRefinement型
12/17 (海野) プログラム検証
12/24 (期末試験)

期末試験について

期末試験は以下の要領で実施します。

 期末試験 
	2015/12/24 (木)  15:15までに教室に集合すること
	場所: 3A207教室 (講義で使っている教室)
	試験時間 75分
	資料等持ち込み「可」とする。

 試験範囲
     亀山担当分1. 形式推論(PropLogicの証明, SimpleType, CoreML での型付けから選択式で出題)
     亀山担当分2. 記述問題: Curry-Howard同型対応、型推論、多相型などから自由記述形式で出題)
     海野担当分.  最後2週の講義分から出題

 成績評価: シラバス記載通り
    「授業への出席を前提として演習50%, 期末試験50% で評価する」

成績評価

演習および期末試験(レポート形式)の成績で評価します。演習と期末試験の比率は 5:5 です。また、ボーダーラインの成績の学生については、出席状況を考慮します。

担当教員: 亀山幸義 (kam[at]cs.tsukuba.ac.jp), 海野広志 (uhiro[at]cs.tsukuba.ac.jp)