計算論理： 2015/10/29 の課題
-
単純型付ラムダ計算(直積と直和を持つもの)に対応する
SimpleTypeDefファイルと、SimpleTypeファイルを、自分の作業場に
コピーせよ。(正確には SimpleTypeDef.vo など、
SimpleTypeDef と SimpleType ではじまるファイル全てを
自分の Coq作業用ディレクトリにコピーせよ。)
cd ~/coq (ここで "coq"は、前回作成した作業ディレクトリの名前とする)
cp ~kam/coq/SimpleType* .
-
もし、情報科学類計算機室でなく、
自分のノートPCなど、異なるOS,マシンで実行している人は、
"coqc -v SimpleTypeDef" を実行して、
SimpleTypeDef.vo ファイル等を作りなおしなさい。この際、
若干の警告メッセージが出るが気にしなくてよい。
もし、ここでコンパイルエラーが出る場合は、
あなたの使っている Coq のバージョンが古い可能性があるので設定を確認す
ること(それでもわからなければ、Coqエキスパートの TA 坂口君に聞くこと;
ただし、彼はMacユーザなのでそれ以外のOS特有の話は自力で解決してほしい)。
-
次に、SimpleType.v ファイルを emacs で読みこんで、
単純型付ラムダ計算における型付けを学習しなさい。
黒板で説明した体系と、演習システムの体系との記号の違いについては、
配布資料(ウェブページにもある)で説明している。
演習問題のうち ex101 から ex107 までの 7問は既に答えを記入しているので、
これをCoqで実行しながら、どういう型付け図に対応するかを考えなさい。
なお、問題の番号は、一部抜けているところがある。(たとえば ex119 という
問題はない。これは理由があるので、自分で追加しないでほしい。)
-
最後に、ex112 もしくは ex113 のいずれか1問以上の問題を解いて、
それに対応する型付け図を、レポートにはりつけて作成し manaba から提出しなさい。
-
なお、ex133以降は、問題が難しくなる。それより前は、
項と型が与えられてその型付け図を作る問題だが、
ex133以降は、型のみ与えられ、項とその型付けを自分で考える必要がある。
-
レポートは、電子ファイルとし(テキストまたはPDF、日本語または英語)
manabaシステムから提出せよ。
かならず、本文中に学籍番号と名前を書くこと。
このレポートの締切は、
締切は 11/4 (夜)である。
例によって、こちらのレポートは出席がわりにもなっているので、
必ずそれまでにレポートをだすこと。(不完全なレポートでもよいので必ずだ
すこと。)
なお、命題論理(PropLogic)レポートの締切も同じ日である。
「SimpleType.v の問題をたくさん解く」という課題は、
2週間程度先の予定であり、そのレポートは別に出してほしい。