ML演習の課題メモ
ML演習で出された課題に関するメモ的な何か。みんな加筆してー。
第２回
課題4
* 実装の仕方はいろいろあると思いますが、筆者は下のように'a queueをリンクリストを使って定義しました。
- type 'a myQueue = Null | Q of 'a * ('a myQueue ref);;
- type 'a queue = {head: 'a myQueue ref; tail: 'a myQueue ref};;
課題5
* Yコンビネータを使ったものならWikipediaに載っています
課題8
* カリーハワード対応というものがあって、これによると命題と型、証明とプログラムとの間に対応関係があるそうです。
* つまり「あらゆる型にはそれと1対1に対応する命題が存在する」「ある型に対応する命題が証明できるなら、その型を持つ式が書ける」ということらしいです。
* 今回の場合、型と命題の対応は
「'a -> 'b」と「AならばB」が対応
- 「('a, 'b) and_t」と「AかつB」が対応
- 「('a, 'b) or_t」と「AまたはB」が対応
- 「'a not_t」と「Aでない」が対応
となっています。
* 例えば2の「('a, ('b, 'c) and_t) or_t ->(('a, 'b) or_t, ('a, 'c) or_t) and_t」という型は「（Aまたは（BかつC））ならば（（AまたはB）かつ（BかつC））」という命題に対応しています。この命題は証明可能なので2の型は定義可能ということになります。
* いろいろ書きましたが、多分ググってもらった方が確実だし分かりやすいと思います。
* １・２・３・６は参照、let recなしでできました。
* ４は対応する命題「AまたはAでない」は（多分）証明可能なので定義できるはずですが、筆者はまだできてません。できた人は加筆してー。
* ５は多分無理。
* ７は参照やlet rec、あるいは継続を使えば作れるようです。筆者はoption型と参照を使って定義しました。
課題9
* SMLという言語で書かれたものならここに載っています。
* これをがんばってOcamlのコードに直せばちゃんと動くと思います。
* module,struct,sig,functorなどは第３回の授業で習うと思います。
* susp,force,delayはOcamlでいうLazy.t,Lazy.force,lazyで、遅延評価のために用意されている型・関数です。