|
サイズ: 20314
コメント:
|
← 2011-06-06 01:55:12時点のリビジョン41 ⇥
サイズ: 1071
コメント:
|
| 削除された箇所はこのように表示されます。 | 追加された箇所はこのように表示されます。 |
| 行 1: | 行 1: |
| ## page was renamed from 関数・論理型プログラミング実験/memo | |
| 行 6: | 行 7: |
| ---- | |
| 行 10: | 行 10: |
| == 第2回 == === 課題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]]に載っています *できたー {{{#!highlight ocaml type ('a, 'b) fix_f = NONE | FIX of ((('a -> 'b) -> 'a -> 'b) -> 'a -> 'b);; let fix f x = let r = ref NONE in let func g y = match !r with |FIX h -> g (h g) y in (r := FIX func; match !r with |FIX h -> h f x);; }}} === 課題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を使うのを制限した理由かもしれません。 ・加筆（上の筆者とは違う人です） 4,7はそれぞれ排中律と二重否定の除去則ですが、（call/ccなしの）カリー・ハワード対応は『「型つきラムダ計算」と「直観主義論理の自然演繹」が対応する』というものらしい（不確実）ので、 直観主義論理で証明できない排中律と二重否定の除去則はおそらくlet recやcall/ccなしでは定義できないのだと思います。 ただし、call/ccを用いると直観主義論理でなく古典論理の自然演繹との対応がつけられるそうなので、これが再帰などを使わずに定義できれば4,7も出来る筈です。 ・さらに加筆 call/ccは副作用をどうしても伴うそうです。 === 課題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で、遅延評価のために用意されている型・関数です。 == 第3回 == === 課題4 === 平均(最悪でない)時間計算量がO(log n)であればいいので、例えば二分木を作ればいいはず。 二分木を作る場合、特に大変なのはremoveでしょうか。 {{{#!highlight ocaml module MyMultiset2 = functor (Elem : ORDERED_TYPE) -> struct exception Error_btree type t = Node of Elem.t * t * t | Leaf (* 中略 *) (* 木の最小要素を返す *) let rec search_min set = match set with | Leaf -> raise Error_btree | Node (x, Leaf, _) -> x | Node (_, left, _) -> search_min left (* 木の最小要素を消す *) let rec delete_min set = match set with | Node (v, Leaf, right) -> right | Node (v, left, right) -> Node (v, (delete_min left), right) | Leaf -> raise Error_btree (* 要素の削除 *) let rec remove elem set = match set with | Leaf -> Leaf | Node (v, left, right) when eq v elem -> if (right = Leaf) then left else if (left = Leaf) then right else let min = search_min right in Node (min, left, delete_min right) | Node (v, left, right) -> if (grt elem v) then Node (v, left, remove elem right) else Node (v, remove elem left, right) (* 中略 *) end }}} === 課題5 === 定義は自分で決めていいらしいので、「1000回addやremoveを繰り返しても、２つの実装の実行結果が変わらないこと」とか適当に定義すればいい思う。 真面目な解き方は誰かが加筆してくれることでしょう(ﾁﾗｯ === 課題7 === let recを使って {{{#!highlight ocaml let rec map f = function | Leaf -> Leaf | Node (v, next) -> Node (f v, map (map f) next);; }}} とすると、「Error: This expression has type 'a t -> 'b t but an expression was expected of type 'a -> 'b」と型エラーがでます。 そこでmodule recを駆使して書いてみると、 {{{#!highlight ocaml module rec Tree : sig val map : ('a -> 'b) -> ('a t -> 'b t) end = struct let map f = function | Leaf -> Leaf | Node (v, next) -> Node(f v, Tree.map (Tree.map f) next);; end;; }}} うまくいきます。詳しい解説はis2009のwikiに書かれています。 === 課題8 === ('a, 'b) equalは同値関係（=とか<=>）に対応する型だと思われます。（reflは反射律、symmは対称律、transは推移律に対応） 同値関係は「（AならばB）かつ（BならばA）」という命題と同じ（？）と考えられるので、('a, 'b) equalは、例えば {{{#!highlight ocaml type ('a, 'b) equal = ('a -> 'b) * ('b -> 'a) }}} と定義すればいいと思います。 === 課題9 === よく分かりません（ valueやexprの引数に('a, 'b) equalを持たせる理由が謎です。 なんとなく型キャストができるようにしなさいと言っているような気がしますが気のせいかもしれません。 だれか分かる人は加筆してください。 == 第4回 == === 課題2 === コメントアウトの形式は色々あると思いますが、筆者はC言語のコメントアウト２つとOcamlの入れ子のコメントアウトの計３つを作りました。 各コマンドは、commentというエントリーポイントを新しく作り、再帰的に呼びだす（「token lexbuf」「comment lexbuf」などとすると、それぞれtoken・commentエントリーポイントが再帰的に呼び出されます）ことで実現しています。 {{{#!highlight ocaml (* lexer.mll *) rule token = parse | space+ { token lexbuf } (* スペース *) | "(*" { comment1 lexbuf; token lexbuf } (* コメント１：OCamlの入れ子にできるコメント *) | "/*" { comment2 lexbuf; token lexbuf } (* コメント２：C言語のコメントその１ *) | "//" { comment3 lexbuf; token lexbuf } (* コメント３：C言語のコメントその２ *) | ("exit" | "quit" | eof) { raise End_of_file } (* 終了用のコマンド *) | ";;" { EOC } (* コマンド終わり *) | num+ as lxm { INT (int_of_string lxm) } (* 数字 *) | "true" { BOOL (true) } (* true *) | "false" { BOOL (false) } (* false *) (* 中略 *) | '_' { ALL } | ((alp | '_') (alp | num | '_')*) as lxm { STRING (lxm) } (* 識別子 *) | [^'\n'] { raise (Failure "lexing: empty token") } and comment1 = parse | "*)" { () } (* 現在の深さのネストから脱出 *) | "(*" { comment1 lexbuf; comment1 lexbuf } (* ひとつ深いネストに入って"*)"が現れるまで読み進み、その後もとのネストで"*)"が現れるまで読み進める。 *) | eof { raise (Failure "lexing: eof appeared in comment") } (* コメント中で入力が終わったらエラー *) | _ { comment1 lexbuf } (* "*)"がでるまで読み進みつづける *) and comment2 = parse | "*/" { () } (* 現在の深さのネストから脱出 *) | eof { raise (Failure "lexing: eof appeared in comment") } (* コメント中で入力が終わったらエラー *) | _ { comment2 lexbuf } (* "*)"がでるまで読み進みつづける *) and comment3 = parse | "\n" { () } (* 現在の深さのネストから脱出 *) | eof { () } (* コメント中で入力が終わったらエラー *) | _ { comment3 lexbuf } (* "*)"がでるまで読み進みつづける *) }}} === 課題3 === ・授業では副作用使うなといわれましたが、個人的には環境の定義に参照とか使っていいと思います。 第5回の課題で再帰関数をつくるみたいですが、そのための方法のひとつに環境を副作用ありのものに変更するというものがあります。 多分半分くらいの人はそちらの方法で実装することになると思うので、今副作用バリバリの環境を作っても特に問題ないように思います。 ・今回必要なものは、環境モジュールと、let文や変数が参照されたときの処理です。筆者のlet文などの処理は下のようになりました。 {{{#!highlight ocaml (**識別子**) | Id (e1) -> Env.get e1 env (**let in**) | LetIn (e1, e2, e3)-> let ans = eval env e2 in Env.add e1 ans env; let ret = eval env e3 in (Env.remove e1 env; ret) (**let**) | Let (e1, e2) -> let ans = eval env e2 in Env.add e1 ans env; ans }}} MinCamlというOCamlで書かれた小さいMLコンパイラがあり、それを参考にするとほぼそのまま50点は取れる、はず。 -- [[Naoaki Iwakiri]] === 課題6 === ・授業では教えられてないのですが次のようなレコードの定義の仕方があります。 {{{#!highlight ocaml type tp = { f: 'a. 'a -> 'a };; }}} 中括弧の中の「f : 'a. 'a -> 'a」というのは、「fというフィールドは'a->'aという型を持っていて、'aは多相型として扱われます。」という意味です。 イメージとしては {{{#!highlight ocaml type 'a tp = { f: 'a -> 'a };; }}} という書き方と同じようなものだと思えばいいでしょう。 ただしこの二つの書き方は本質的に異なっています。 tp(あるいは'a tp)型の変数を参照するとき、前者の書き方では'aという型変数は多相型として扱われますが、後者では単相型として扱われてしまいます。 例えば、次のようなコードを書くと、 {{{#!highlight ocaml let test x = x.f x.f;; }}} tp型を「type tp = {f: 'a. 'a -> 'a}」と定義したときはエラーは吐かれずに「val test : tp -> 'a -> 'a = <fun>」という結果が返ってきますが、 「type 'a tp = {f: 'a -> 'a}」と定義すると「Error: This expression has type 'a -> 'a but an expression was expected of type 'a」という型エラーが吐かれます。 上のようにx.fなどとしてレコードのフィールドが参照されるとき、ocamlのインタープリタはフィールドfの定義の部分にかかれている文言だけを見て、それぞれの型変数が多相型かそうでないかを判断します。 前者の書き方の場合、fの横には「'a. 'a -> 'a」とかかれており、'aという型変数が多相型であるとインタープリタは判断します。一方、後者の場合、フィールドfの横には「'a -> 'a」としか書かれていないので、型変数'aは単相型だと判断されます（'aが多相型であるという情報はfの定義の外の「type 'a tp = …」の部分にあるため、インタープリタはそれを認識しません）。 なので、x.fという式を評価するときに前者では毎回型'aを実体化（instantiate）するため型エラーが発生せず、後者ではそうしないために型エラーが発生します。（instantiateや型推論の話は一応第6回でされると思います） このように2つのレコードの書き方には違いがあるので注意しましょう。 ・で本題ですが、EXISTというmoduleを定義しなさいという問題でした。 ・このEXISTは「exist（とある/記号：∃）」に対応するもので、EXIST(struct … end).tは「∃A, T(A)」(あるAが存在して、T(A)が真)という命題に対応する型です。今回の場合、T(A)に対応する型は'a T.tになるはずなので、気持ち的には「∃'a, 'a T.t」のような型を作ればいいことになります。（existential typeという名前があるようです） ・結論から言うと、「∃'A, T(A)」という命題は「∀A, (∀B, T(B)ならばA)ならばA」という命題と同値（未確認）らしく、existential typeは気持ち的には「∀'a. (∀'b. 'b T.t -> 'a) -> 'a」とも書けるはずです。よって、 * 「∀（型変数）」という部分の表現にレコードにおける多相型の明示が使えること * レコードを定義するとき中括弧は入れ子にできないこと に注意すると、EXISTモジュールの中のtは、'b uを利用して、 {{{#!highlight ocaml type t = {t: 'a. 'a u -> 'a} }}} と書けます。 ・あとは頑張ってpack, unpackを定義しましょう。 === 課題7 === ・課題6で定義したEXISTの使い方の例を示しておきます。参考にしてください。 ・任意の型の値をE.pack関数によってE.t型に変換して、E.unpackによって変換前の値の情報をstring型として取得しています。 {{{#!highlight ocaml (* 扱いたい型(int, string, boolなど)と、その型の値を別の型（この例ではstring型）に変換する関数のペアを'a T.tにする *) module E = EXIST(struct type 'a t = 'a * ('a -> string) end);; let pk1 = E.pack ("x", fun x -> x);; (* "x"という文字列をパック *) let pk2 = E.pack (1, string_of_int);;(* １という整数をパック *) [pk1; pk2];; (* pk1, pk2は同じ型(E.t)なのでリストにできる *) E.unpack pk1 {f = fun (x, f) -> f x};; (* "x"という文字列が返される *) E.unpack pk2 {f = fun (x, f) -> f x};; (* "1"という文字列が返される *) }}} == 第5回 == === 課題1 === ・クロージャの定義をClojure ＝（（関数の名前、）変数、関数本体、環境）としている人へ 関数本体を「式」型を表す expr で表す必要がありますが、Clojure は「値」型の value のバリアント型のひとつに付け加える必要が出てくるかと思います。 しかし、すでにexpr型はvalue型を用いて定義されているため、このような仕様にしてしまうとさらにその上value型をexpr型で定義することになってしまい、 ちょうど型を相互再帰する形になると思います。 さらには、環境にも同様の問題が生じるかと思います。 そこで、以下のような形で「型の相互再帰的定義」ができるようなので参考にしてください。どうもレジュメに載ってないようなので。 {{{#!highlight ocaml type expr = (* expr型の定義 *) and value = (* value型の定義： ここで例えばクロージャを Clojure of string * string * expr * env などとする。 *) and env = (* 環境の定義： 環境をモジュール module Env ＝…… で実装している人は 環境の定義において value が使われている箇所（例えば add : string -> value -> t -> t を add : string -> 'a -> t -> t と定義しておく）をとりあえず型パラメタでおいて定義してから env = value Env.t と定義するとできます（できました）。 *);; }}} もし同じところで詰まってたら参考にしてください。-- TakuyaKuwahara |
* [[関数・論理型プログラミング実験/課題メモ/第2回|第2回]] * [[関数・論理型プログラミング実験/課題メモ/第3回|第3回]] * [[関数・論理型プログラミング実験/課題メモ/第4回|第4回]] * [[関数・論理型プログラミング実験/課題メモ/第5回|第5回]] * [[関数・論理型プログラミング実験/課題メモ/第6回|第6回]] * [[関数・論理型プログラミング実験/課題メモ/第7回|第7回]] * [[関数・論理型プログラミング実験/課題メモ/第8回|第8回]] |
ML演習の課題メモ
ML演習で出された課題に関するメモ的な何か。みんな加筆してー。
加筆について
加筆したところに@USER@を付けてくれると、誰が書いたか分かりやすくていいと思うんだけど、どうだろう？ -- carbon_twelve