|
サイズ: 5981
コメント:
|
サイズ: 905
コメント:
|
| 削除された箇所はこのように表示されます。 | 追加された箇所はこのように表示されます。 |
| 行 1: | 行 1: |
| ## page was renamed from 関数・論理型プログラミング実験/memo | |
| 行 6: | 行 7: |
| ---- | |
| 行 10: | 行 10: |
| == 第２回 == | * [[関数・論理型プログラミング実験/課題メモ/第2回|第2回]] * [[関数・論理型プログラミング実験/課題メモ/第3回|第3回]] * [[関数・論理型プログラミング実験/課題メモ/第4回|第4回]] * [[関数・論理型プログラミング実験/課題メモ/第5回|第5回]] * [[関数・論理型プログラミング実験/課題メモ/第6回|第6回]] |
| 行 12: | 行 16: |
| === 課題4 === * 実装の仕方はいろいろあると思いますが、筆者は下のように'a queueをリンクリストを使って定義しました。 {{{#!highlight ocaml type 'a myQueue = Null | Q of 'a * ('a myQueue ref);; type 'a queue = {head: 'a myQueue ref; tail: 'a myQueue ref};; }}} === 課題5 === * Yコンビネータを使ったものなら[[http://ja.wikipedia.org/wiki/%E4%B8%8D%E5%8B%95%E7%82%B9%E3%82%B3%E3%83%B3%E3%83%93%E3%83%8D%E3%83%BC%E3%82%BF#.E5.86.8D.E5.B8.B0.E5.9E.8B.E3.81.AB.E3.82.88.E3.82.8B.E7.AC.A6.E5.8F.B7.E5.8C.96.E3.81.AE.E4.BE.8B|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を使う方法ならできました。 {{{#!highlight ocaml (* let recを使えばいける *) let func4 = let rec myFalse = B myFalse in (R (fun x -> myFalse): ('a, 'a not_t) or_t);; }}} * let recを使って再帰的にfalse_t型の変数myFalseを作り、これを使って'a not_tを定義。そのあと、直に型を指定して無理やり目的の型を作ります。 * 強引なやり方ですが、これでうまくいきます。 * fixを使えばlet recを使わずにmyFalseのようなものを作れそうですが、fixの定義自体にlet recや参照、あるいは再帰型が使われているはずなので、結局let rec・再帰型なしでの定義はできなさそうです。 * ５は多分無理。というか絶対無理だと信じてます。「AかつAでない」という命題は常に偽なので証明できないはずだから。 * ７は参照やlet rec、あるいは継続を使えば作れるようです。筆者はoption型と参照を使って定義しました。 {{{#!highlight ocaml (* 参照とoptionを使って無理やり *) let func7 (x: 'a not_t not_t) = let ans = ref (None) in let g1 (x: 'a) = ans := Some x in match !ans with Some x -> x | _ -> raise Exception;; }}} * ー＞参照は使っちゃいけないんでした。すいませんでした。 * 次にバリアントを使うものを考えました、 {{{#!highlight ocaml (* 特殊な型を作る *) (* 例外を暗に使っている *) type 'a tp = C of 'a not_t not_t | D of 'a let func7_2 (x: 'a not_t not_t)= match C x with | D x -> x;; }}} 参照などは使ってないように見えますが、これは {{{#!highlight ocaml type 'a tp = C of 'a not_t not_t | D of 'a let func7_2 (x: 'a not_t not_t)= match C x with | D x -> x | _ -> raise Exception;; }}} という例外を使った書き方と本質的に同じ（バレないように書いてないだけ）なのでボツ。 その後考えたのは、let recを使う方法です。 {{{#!highlight ocaml (* let recを使えばいける *) let rec (func7_1: 'a not_t not_t -> 'a) = fun x -> func7_1 x;; }}} これは参照も例外も使ってないので良さそうです。 できればlet recも使わずに定義したいところですが、今のところこれが筆者の精一杯です。もっといい方法があれば加筆してね！ * 7は二重否定の除去という推論規則なのですが、実はschemeにおけるcall/cc（call-with-current-continuationの略）という関数がそれに対応するそうです。なので、call/ccのようなものをocamlで作れたら（継続などを使えば作れるようです）多分let recなしでも定義できると思います。だれかやってみてください（ * ちなみに上のようにlet recを使うと、任意の'a->'b型の式が定義できます。 {{{#!highlight ocaml (* 'a -> 'bを作る *) let rec (func: 'a -> 'b) = fun x -> func x;; (* 'a -> 'a not_tを作る *) let rec (func: 'a -> 'a not_t) = fun x -> func x;; }}} チートくさいです。これがlet recを使うのを制限した理由かもしれません。 === 課題9 === * SMLという言語で書かれたものなら[[http://www.eecs.usma.edu/webs/people/okasaki/jfp95/index.html|ここ]]に載っています。 * これをがんばってOcamlのコードに直せばちゃんと動くと思います。 * module,struct,sig,functorなどは第３回の授業で習うと思います。 * susp,force,delayはOcamlでいうLazy.t,Lazy.force,lazyで、遅延評価のために用意されている型・関数です。 |
== 加筆について == 加筆したところに@``USER@を付けてくれると、誰が書いたか分かりやすくていいと思うんだけど、どうだろう？ -- [[carbon_twelve]] |
| 行 130: | 行 21: |
ML演習の課題メモ
ML演習で出された課題に関するメモ的な何か。みんな加筆してー。
加筆について
加筆したところに@USER@を付けてくれると、誰が書いたか分かりやすくていいと思うんだけど、どうだろう？ -- carbon_twelve