第五回目の予習での QA (11/12提出分, Poly.v について)

第四回目の予習での QA (11/5提出分, Lists.v について)

第三回目の予習での QA (10/29提出分, 単純型付ラムダ計算について)

第二回目までの宿題での QA

第二回目の予習での QA (10/22提出分, Basics.v, Induction.v について)

(前回答えていないものの一部の質問への回答もつけました.)

第一回目の予習での QA (10/8提出分, Preface.v, Basics.vについて)

全ての回答に目を通しましたが,後で回答する方が適切と考えた質問はここ では答えていません.そのうち答えます.また講義中に説明したと考えている 質問についても回答していません.回答に納得できない場合は,またしてくだ さい.また,似た質問はひとつにまとめたり,質問の文章は適宜変更していま す.

全体的に nat の O と S を使った記法と,アラビア数字表記のつながりが魔法 のようで紛らわしかったようです.下の質問への回答にも書きましたが,実は nat という名前の型はテキストの Module Playground ... End Playground の 間とライブラリで二度定義されています.後者についてのみシステムがアラビ ア数字表記と対応が取れるように細工をしてくれていますが,前者については, テキストで新たに定義したものなので,そういうサポートがありません. (Module は定義が使える範囲を区切るための仕組み)ですので,例えば

 Check S(S(S(O))).
をしてアラビア数字が出てくるのは,End Playground の外(つまりテキストの 定義の有効範囲を出た後)に限られるはずです.また,O と S を使った「自然 数」を自然数として見ているのは,ある意味で我々の勝手です. 重要なのは,O と S を nat の定義の仕方で組み合わせると,自然数と「同型」 な集合が作れる(つまり,各要素を自然数と思い込んでも問題がない),という ことです.