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 環境の定義において value が使われている箇所（例えば add : string -> value -> t -> t を add : string -> 'a -> t -> t と定義しておく）をとりあえず型パラメタでおいて定義してから
  13 env = value Env.t
  14 と定義するとできます（できました）。
  15 *);;

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

・関数適応の右結合癖が治らない人へ

おそらく大半の人が、関数適応を文法規則「expr -> expr expr」によって実装しているかと思います。（レジュメの例と同じ） この時に生じがちな問題について。

例えば、次のような関数

   1 let f = (fun x -> (fun y -> x+y));;

を定義したとします。（ただの加算です）

これに対し、普通に関数適応式を書くなら

   1 f 1 2;;

となりますが、このとき評価エラーが生じてしまうことがあります。（生じなかったら多分この項読む意味ないです）

これはパーサが構文を

   1 (f (1 2));;

と誤って解析してしまうことによります。

対策は次の２つ。

１．「左結合」を明示する（情報源：IS2009wiki）

レジュメのUMINUSの様に、関数の左結合則を明示するためのダミーのトークンFUNCを

   1 %token FUNC
   2 %token (*
   3 ……
   4 その他のトークンの定義
   5 ……
   6 *)
   7 %token INT BOOL
   8 
   9 %left ADD (*
  10 ……
  11 優先度の指定
  12 ……
  13 *)
  14 %left FUNC

と定義します。このときFUNCには最も優先度の高い左結合を設定してください。

次に関数適応の規則に

   1 expr expr %prec FUNC {(* … *)}

で優先度をFUNCに従うようにします。これで、関数適応には最も優先度の高い左結合則が割り当てられます。

２．VAL、INT、BOOLの還元タイミングを早める

上の優先度設定を行っただけで、うまくいく人はうまく行きます。

そうでない--俺のような--人は、おそらくINT,BOOL,VAL(VALは変数型)がそれだけで記号exprに還元されるタイミングが遅く、それゆえに

(1) [スタック: (empty) ] <- [入力:f 1 2]

(2) [スタック: f:VAL ] <- [入力:1 2]

(3) [スタック: f:VAL,1:INT, ] <- [入力:2]

(4) [スタック: f:VAL,1:INT,2:INT ] <- [入力:(empty)]

(5) [スタック: f:VAL,1:INT,2:expr ] <- [入力:(empty)]

(6) [スタック: f:VAL,1:expr,2:expr ] <- [入力:(empty)]

(7) [スタック: f:VAL,(1 2):expr] <- [入力:(empty)]

(8) [スタック: f:VAL,1:INT,2:INT ] <- [入力:(empty)]

(9) [スタック: (f (1 2)):expr] <- [入力:(empty)]

のように構文解析が進んでしまう可能性が高いそうです。（説明のアイデアはNaoaki Iwakiriさんより。もしかしたらもっと別の理由かもしれません。情報求む。）

このように構文解析が進んでしまうと、結合則云々よりも適応可能な文法規則の制約から文の解釈が「(f (1 2))」に決まってしまいます。

これを防ぐには、先の結合規則の部分に

   1 %left ADD (*
   2 ……
   3 優先度の指定
   4 ……
   5 *)
   6 %nonassoc INT BOOL VAL
   7 %left FUNC

を追加してみてください。これで還元のタイミングが「スタックに積まれた直後」になり、

(1) [スタック: (empty) ] <- [入力:f 1 2]

(2) [スタック: f:VAL ] <- [入力:1 2]

(3) [スタック: f:expr ] <- [入力:1 2]

(4) [スタック: f:expr,1:VAL ] <- [入力:2]

(5) [スタック: f:expr,1:expr ] <- [入力:2]

(6) [スタック: (f 1):expr ] <- [入力:2]

(7) [スタック: (f 1):VAL,2:VAL] <- [入力:(empty)]

(8) [スタック: (f 1):expr,2:expr ] <- [入力:(empty)]

(9) [スタック: ((f 1) 2):expr] <- [入力:(empty)](1) [スタック: (empty) ] <- [入力:f 1 2]

(2) [スタック: f:VAL ] <- [入力:1 2]

(3) [スタック: f:VAL,1:INT, ] <- [入力:2]

(4) [スタック: f:VAL,1:INT,2:INT ] <- [入力:(empty)]

(5) [スタック: f:VAL,1:INT,2:expr ] <- [入力:(empty)]

(6) [スタック: f:VAL,1:expr,2:expr ] <- [入力:(empty)]

(7) [スタック: f:VAL,(1 2):expr] <- [入力:(empty)]

(8) [スタック: f:VAL,1:INT,2:INT ] <- [入力:(empty)]

(9) [スタック: (f (1 2)):expr] <- [入力:(empty)]

のように構文解析が進み、うまくいくはずです。

（注意:ホントに優先度設定の時点で下の方に書けば還元のタイミングが早められるんだろうかとか、そもそも構文解析の進行は上の（要は言語処理系論第四回で習った）方法で行われてるのかとかいろいろ疑問が残りますが、そう解釈すると上のようにスパッと説明が付くので一応書いときます--っていうかみんな動けばそこまで深いこと気にしないよね--。）-- TakuyaKuwahara

・関数の多変数化について

関数は「let VAL VAL = expr」のような文法で実装すると当然１変数にしか対応できません。変数に対応するIdentiferがたった一つなので当たり前です。 ただ、これがレジュメに（例）として載ってる以上、コレで実装できれば十分な気もします（保証はしませんよ？）

多変数対応にするには、例えば筆者は

   1     |LET VAL arg EQUAL expr IN expr {(* hogehoge *)}
   2 
   3 (* hugahuga *)
   4 
   5     |expr expr %prec FUNC {(* hogehoge *)}
   6 ;
   7 
   8 arg:
   9     |VAL arg         {(*   1   *)}
  10     |VAL             {(*   2   *)}

と「変数部分」を表す非終端記号argを導入しました。

あとは(* 1 *) (* 2 *)を実装するだけですが、これは

   1 let f x y z = e;;

が

   1 f = (Clojure x (Clojure y (Clojure z (e))))
   2 (* Clojureはクロージャの型 *)

と解釈されればいいので、argが「構文木exprを受け取って変数VをもつクロージャClojure(V,e)のeの部分に代入する関数」を返すようにすれば、上のような階層的に連なって最終的に関数本体がそれらの変数で拡張された環境でもって評価されるような構造を作ることができます。-- TakuyaKuwahara

加筆について

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

Categoryノート