3と17のリビジョン間の差分 (その間の編集: 14回)

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の入れ子のコメントアウトの計３つを作りました。

Ocamlのコマンドは、commentというエントリーポイントを新しく作り、再帰的に呼びだす（「token lexbuf」「comment lexbuf」などとすると、それぞれtoken・commentエントリーポイントが再帰的に呼び出されます）ことで実現しています。

   1 (* lexer.mll *)
   2 
   3 rule token = parse
   4         | space+                                        { token lexbuf } (* スペース *)
   5         | ("//" [^'\n']* "\n")                          { token lexbuf } (* C言語のコメント１ *)
   6         | ("/*" ([^'*']* (['*'] [^'/'])?)+ "*/")        { token lexbuf } (* C言語のコメント２ *)
   7         | "(*"                                          { comment lexbuf; token lexbuf } (* Ocamlの入れ子にできるコメント *)
   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         | '_'                                           { DONT_CARE } (* パターンマッチングとかで使うアレ *)
  15         | ((alp | '_') (alp | num | '_')*) as lxm       { STRING (lxm) } (* 変数に使える文字列 *)
  16         | [^'\n']                                       { raise (Failure "lexing: empty token") }
  17 and comment = parse
  18         | "*)" { () } (* 現在の深さのネストから脱出 *)
  19         | "(*" { comment lexbuf; comment lexbuf } (* ひとつ深いネストに入って"＊）"が出るまで読み進めたあと、元のネストで"＊）"がでるまで読み進める。 *)
  20         | eof { raise (Failure "lexing: eof appeared in comment") } (* コメント中で入力が終わったらエラー *)
  21         | _ { comment lexbuf } (* ＊）がでるまで読み進みつづける *)

課題3

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

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

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

加筆について

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

Categoryノート

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

-  ⇤ ← 2011-04-26 15:15:42時点のリビジョン3 → 
  サイズ: 6667
  編集者: TakuyaKuwahara
  コメント:
+   ← 2011-05-13 22:21:40時点のリビジョン17 → ⇥
  サイズ: 12814
  編集者: furaga
  コメント:
-削除された箇所はこのように表示されます。
+追加された箇所はこのように表示されます。
 行 10:
-== 第２回 ==
+== 第2回 ==
 行 24:
+*できたー
{{{#!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);;
}}}
-行 119:
+行 134:
-,7はそれぞれ排中律と二重否定の除去則ですが、（call/ccなしの）カリー・ハワード対応は型つきラムダ計算と「直観主義論理の自然演繹」が対応するというものらしい（不確実）ので、
+,7はそれぞれ排中律と二重否定の除去則ですが、（call/ccなしの）カリー・ハワード対応は『「型つきラムダ計算」と「直観主義論理の自然演繹」が対応する』というものらしい（不確実）ので、
-行 121:
+行 137:
-行 123:
+行 140:
+・さらに加筆

call/ccは副作用をどうしても伴うそうです。
-行 132:
+行 153:
+== 第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の入れ子のコメントアウトの計３つを作りました。

Ocamlのコマンドは、commentというエントリーポイントを新しく作り、再帰的に呼びだす（「token lexbuf」「comment lexbuf」などとすると、それぞれtoken・commentエントリーポイントが再帰的に呼び出されます）ことで実現しています。

{{{#!highlight ocaml
(* lexer.mll *)

rule token = parse
 | space+					{ token lexbuf } (* スペース *)
 | ("//" [^'\n']* "\n")      			{ token lexbuf } (* C言語のコメント１ *)
 | ("/*" ([^'*']* (['*'] [^'/'])?)+ "*/") 	{ token lexbuf } (* C言語のコメント２ *)
 | "(*" 						{ comment lexbuf; token lexbuf } (* Ocamlの入れ子にできるコメント *)
 | ("exit" | "quit" | eof)         		{ raise End_of_file } (* 終了用のコマンド *)
 | ";;"						{ EOC } (* コマンド終わり *)
 | num+ as lxm 					{ INT (int_of_string lxm) } (* 数字 *)
 | "true"					{ BOOL (true) } (* true *)
 | "false" 					{ BOOL (false) } (* false *)
(* 中略 *)
 | '_'						{ DONT_CARE } (* パターンマッチングとかで使うアレ *)
 | ((alp | '_') (alp | num | '_')*) as lxm 	{ STRING (lxm) } (* 変数に使える文字列 *)
 | [^'\n']      					{ raise (Failure "lexing: empty token") }
and comment = parse
 | "*)" { () } (* 現在の深さのネストから脱出 *)
 | "(*" { comment lexbuf; comment lexbuf } (* ひとつ深いネストに入って"＊）"が出るまで読み進めたあと、元のネストで"＊）"がでるまで読み進める。 *)
 | eof { raise (Failure "lexing: eof appeared in comment") } (* コメント中で入力が終わったらエラー *)
 | _ { comment lexbuf } (* ＊）がでるまで読み進みつづける *)
}}}


=== 課題3 ===

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

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

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

== 加筆について ==
加筆したところに@``USER@を付けてくれると、誰が書いたか分かりやすくていいと思うんだけど、どうだろう？ -- [[carbon_twelve]]
-行 135:
+行 302:

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

ML演習の課題メモ

第2回

課題4

課題5

課題8

課題9

第3回

課題4

課題5

課題7

課題8

課題9

第4回

課題2

課題3

加筆について