21と25のリビジョン間の差分 (その間の編集: 4回)

ML演習の課題メモ

ML演習で出された課題に関するメモ的な何か。みんな加筆してー。

第2回

課題4

* 実装の仕方はいろいろあると思いますが、筆者は下のように'a queueをリンクリストを使って定義しました。

   1 type 'a myQueue = Null | Q of 'a * ('a myQueue ref);;
   2 type 'a queue = {head: 'a myQueue ref; tail: 'a myQueue ref};;

課題5

* Yコンビネータを使ったものならWikipediaに載っています

*できたー

   1 type ('a, 'b) fix_f = 
   2    NONE
   3  | FIX of ((('a -> 'b) -> 'a -> 'b) -> 'a -> 'b);;
   4 
   5 let fix f x =
   6   let r = ref NONE in
   7     let func g y =
   8       match !r with
   9       |FIX h -> g (h g) y
  10     in (r := FIX func;
  11         match !r with
  12         |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を使う方法ならできました。

   1 (* let recを使えばいける *)
   2 let func4 =
   3         let rec myFalse = B myFalse in
   4         (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型と参照を使って定義しました。

   1 (* 参照とoptionを使って無理やり *)
   2 let func7 (x: 'a not_t not_t) = 
   3         let ans = ref (None) in
   4         let g1 (x: 'a) = ans := Some x in
   5         match !ans with Some x -> x | _ -> raise Exception;;

* ー＞参照は使っちゃいけないんでした。すいませんでした。

* 次にバリアントを使うものを考えました、

   1 (* 特殊な型を作る *)
   2 (* 例外を暗に使っている *)
   3 type 'a tp = C of 'a not_t not_t | D of 'a
   4 let func7_2 (x: 'a not_t not_t)=
   5         match C x with
   6                 | D x -> x;;

参照などは使ってないように見えますが、これは

   1 type 'a tp = C of 'a not_t not_t | D of 'a
   2 let func7_2 (x: 'a not_t not_t)=
   3         match C x with
   4                 | D x -> x
   5                 | _ -> raise Exception;;

という例外を使った書き方と本質的に同じ（バレないように書いてないだけ）なのでボツ。

その後考えたのは、let recを使う方法です。

   1 (* let recを使えばいける *)
   2 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型の式が定義できます。

   1 (* 'a -> 'bを作る *)
   2 let rec (func: 'a -> 'b) = fun x -> func x;;
   3 
   4 (* 'a -> 'a not_tを作る *)
   5 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という言語で書かれたものならここに載っています。

* これをがんばってOcamlのコードに直せばちゃんと動くと思います。

* module,struct,sig,functorなどは第３回の授業で習うと思います。

* susp,force,delayはOcamlでいうLazy.t,Lazy.force,lazyで、遅延評価のために用意されている型・関数です。

第3回

課題4

平均(最悪でない)時間計算量がO(log n)であればいいので、例えば二分木を作ればいいはず。

二分木を作る場合、特に大変なのはremoveでしょうか。

   1 module MyMultiset2 = functor (Elem : ORDERED_TYPE) -> struct
   2         exception Error_btree
   3         type t = Node of Elem.t * t * t | Leaf
   4 
   5         (* 中略 *)
   6 
   7         (* 木の最小要素を返す *)
   8         let rec search_min set =
   9                 match set with
  10                         | Leaf -> raise Error_btree
  11                         | Node (x, Leaf, _) -> x
  12                         | Node (_, left, _) -> search_min left
  13 
  14         (* 木の最小要素を消す *)
  15         let rec delete_min set = 
  16                 match set with
  17                         | Node (v, Leaf, right) -> right
  18                         | Node (v, left, right) -> Node (v, (delete_min left), right)
  19                         | Leaf -> raise Error_btree
  20 
  21         (* 要素の削除 *)
  22         let rec remove elem set =
  23                 match set with
  24                         | Leaf -> Leaf
  25                         | Node (v, left, right) when eq v elem -> 
  26                                 if (right = Leaf) then left
  27                                 else if (left = Leaf) then right
  28                                 else 
  29                                         let min = search_min right in
  30                                         Node (min, left, delete_min right)
  31                         | Node (v, left, right) ->
  32                                 if (grt elem v) then Node (v, left, remove elem right)
  33                                 else Node (v, remove elem left, right)
  34 
  35 
  36         (* 中略 *)
  37 end

課題5

定義は自分で決めていいらしいので、「1000回addやremoveを繰り返しても、２つの実装の実行結果が変わらないこと」とか適当に定義すればいい思う。

真面目な解き方は誰かが加筆してくれることでしょう(ﾁﾗｯ

課題7

let recを使って

   1 let rec map f = function
   2         | Leaf -> Leaf
   3         | 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を駆使して書いてみると、

   1 module rec Tree :
   2 sig val map : ('a -> 'b) -> ('a t -> 'b t) end =
   3 struct
   4         let map f = function
   5                 | Leaf -> Leaf
   6                 | Node (v, next) -> Node(f v, Tree.map (Tree.map f) next);;
   7 end;;

うまくいきます。詳しい解説はis2009のwikiに書かれています。

課題8

('a, 'b) equalは同値関係（=とか<=>）に対応する型だと思われます。（reflは反射律、symmは対称律、transは推移律に対応）

同値関係は「（AならばB）かつ（BならばA）」という命題と同じ（？）と考えられるので、('a, 'b) equalは、例えば

   1 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エントリーポイントが再帰的に呼び出されます）ことで実現しています。

   1 (* lexer.mll *)
   2 
   3 rule token = parse
   4         | space+                                        { token lexbuf } (* スペース *)
   5         | "(*"                                          { comment1 lexbuf; token lexbuf }       (* コメント１：OCamlの入れ子にできるコメント *)
   6         | "/*"                                          { comment2 lexbuf; token lexbuf }       (* コメント２：C言語のコメントその１ *)
   7         | "//"                                          { comment3 lexbuf; token lexbuf }       (* コメント３：C言語のコメントその２ *)
   8         | ("exit" | "quit" | eof)                       { raise End_of_file } (* 終了用のコマンド *)
   9         | ";;"                                          { EOC } (* コマンド終わり *)
  10         | num+ as lxm                                   { INT (int_of_string lxm) } (* 数字 *)
  11         | "true"                                        { BOOL (true) } (* true *)
  12         | "false"                                       { BOOL (false) } (* false *)
  13 (* 中略 *)
  14         | '_'                                           { ALL }
  15         | ((alp | '_') (alp | num | '_')*) as lxm       { STRING (lxm) }        (* 識別子 *)
  16         | [^'\n']                                       { raise (Failure "lexing: empty token") }
  17 and comment1 = parse
  18         | "*)"  { () }                                  (* 現在の深さのネストから脱出 *)
  19         | "(*"  { comment1 lexbuf; comment1 lexbuf }    (* ひとつ深いネストに入って"*)"が現れるまで読み進み、その後もとのネストで"*)"が現れるまで読み進める。 *)
  20         | eof   { raise (Failure "lexing: eof appeared in comment") }   (* コメント中で入力が終わったらエラー *)
  21         | _     { comment1 lexbuf }                     (* "*)"がでるまで読み進みつづける *)
  22 and comment2 = parse
  23         | "*/"  { () }                                  (* 現在の深さのネストから脱出 *)
  24         | eof   { raise (Failure "lexing: eof appeared in comment") }   (* コメント中で入力が終わったらエラー *)
  25         | _             { comment2 lexbuf }             (* "*)"がでるまで読み進みつづける *)
  26 and comment3 = parse
  27         | "\n"  { () }                                  (* 現在の深さのネストから脱出 *)
  28         | eof   { () }                                  (* コメント中で入力が終わったらエラー *)
  29         | _             { comment3 lexbuf }             (* "*)"がでるまで読み進みつづける *)
  30

課題3

・授業では副作用使うなといわれましたが、個人的には環境の定義に参照とか使っていいと思います。

第5回の課題で再帰関数をつくるみたいですが、そのための方法のひとつに環境を副作用ありのものに変更するというものがあります。

多分半分くらいの人はそちらの方法で実装することになると思うので、今副作用バリバリの環境を作っても特に問題ないように思います。

・今回必要なものは、環境モジュールと、let文や変数が参照されたときの処理です。筆者のlet文などの処理は下のようになりました。

   1 (**識別子**)
   2 | Id (e1) ->
   3         Env.get e1 env
   4 
   5 (**let in**)
   6 | LetIn (e1, e2, e3)->
   7         let ans = eval env e2 in
   8         Env.add e1 ans env;
   9         let ret = eval env e3 in (Env.remove e1 env; ret)
  10 
  11 (**let**)
  12 | Let (e1, e2) -> 
  13         let ans = eval env e2 in 
  14         Env.add e1 ans env;
  15         ans

MinCamlというOCamlで書かれた小さいMLコンパイラがあり、それを参考にするとほぼそのまま50点は取れる、はず。 -- Naoaki Iwakiri

課題6

・授業では教えられてないのですが次のようなレコードの定義の仕方があります。

   1 type tp = { f: 'a. 'a -> 'a };;

中括弧の中の「f : 'a. 'a -> 'a」というのは、「fというフィールドは'a->'aという型を持っていて、'aは多相型として扱われます。」という意味です。

イメージとしては

   1 type 'a tp = { f: 'a -> 'a };;

という書き方と同じようなものだと思えばいいでしょう。

ただしこの二つの書き方は本質的に異なっています。

tp(あるいは'a tp)型の変数を参照するとき、前者の書き方では'aという型変数は多相型として扱われますが、後者では単相型として扱われてしまいます。

例えば、次のようなコードを書くと、

   1 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を利用して、

   1 type t = {t: 'a. 'a u -> 'a}

と書けます。

・あとは頑張ってpack, unpackを定義しましょう。

課題7

・課題6で定義したEXISTの使い方の例を示しておきます。参考にしてください。

・任意の型の値をE.pack関数によってE.t型に変換して、E.unpackによって変換前の値の情報をstring型として取得しています。

   1 (* 扱いたい型(int, string, boolなど)と、その型の値を別の型（この例ではstring型）に変換する関数のペアを'a T.tにする *)
   2 module E = EXIST(struct type 'a t = 'a * ('a -> string) end);;
   3 let pk1 = E.pack ("x", fun x -> x);; (* "x"という文字列をパック *)
   4 let pk2 = E.pack (1, string_of_int);;(* １という整数をパック *)
   5 [pk1; pk2];; (* pk1, pk2は同じ型(E.t)なのでリストにできる *)
   6 E.unpack pk1 {f = fun (x, f) -> f x};; (* "x"という文字列が返される *)
   7 E.unpack pk2 {f = fun (x, f) -> f x};; (* "1"という文字列が返される *)

第5回

課題1

・クロージャの定義をClojure ＝（（関数の名前、）変数、関数本体、環境）としている人へ

関数本体を「式」型を表す expr で表す必要がありますが、Clojure は「値」型の value のバリアント型のひとつに付け加える必要が出てくるかと思います。

しかし、すでにexpr型はvalue型を用いて定義されているため、このような仕様にしてしまうとさらにその上value型をexpr型で定義することになってしまい、

ちょうど型を相互再帰する形になると思います。

さらには、環境にも同様の問題が生じるかと思います。

そこで、以下のような形で「型の相互再帰的定義」ができるようなので参考にしてください。どうもレジュメに載ってないようなので。

   1 type expr = 
   2 (* expr型の定義 *)
   3 and value = 
   4 (* value型の定義：
   5 ここで例えばクロージャを
   6 Clojure of string * string * expr * env
   7 などとする。
   8 *)
   9 and env =
  10 (* 環境の定義：
  11 環境をモジュール module Env ＝……　で実装している人は
  12 環境の実体を表す型 t において value が使われている箇所をとりあえず型パラメタでおいて定義してから
  13 env = value Env.t
  14 と定義するとできます（できました）。
  15 *);;

もし同じところで詰まってたら参考にしてください。

加筆について

加筆したところに@USER@を付けてくれると、誰が書いたか分かりやすくていいと思うんだけど、どうだろう？ -- carbon_twelve

Categoryノート

関数・論理型プログラミング実験/課題メモ (最終更新日時 2011-06-06 01:55:12 更新者 furaga)

-  ⇤ ← 2011-05-24 01:12:59時点のリビジョン21 → 
  サイズ: 18186
  編集者: furaga
  コメント:
+   ← 2011-05-24 15:54:34時点のリビジョン25 → ⇥
  サイズ: 20210
  編集者: TakuyaKuwahara
  コメント:
-削除された箇所はこのように表示されます。
+追加された箇所はこのように表示されます。
 行 299:
-授業では副作用使うなといわれましたが、個人的には環境の定義に参照とか使っていいと思います。
+・授業では副作用使うなといわれましたが、個人的には環境の定義に参照とか使っていいと思います。
 行 305:
+・今回必要なものは、環境モジュールと、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
}}}
-行 382:
+行 401:
+== 第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 ＝……　で実装している人は
環境の実体を表す型 t において value が使われている箇所をとりあえず型パラメタでおいて定義してから
env = value Env.t
と定義するとできます（できました）。
*);;
}}}

もし同じところで詰まってたら参考にしてください。

"関数・論理型プログラミング実験/課題メモ"の差分

ML演習の課題メモ

第2回

課題4

課題5

課題8

課題9

第3回

課題4

課題5

課題7

課題8

課題9

第4回

課題2

課題3

課題6

課題7

第5回

課題1

加筆について