第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の型は定義可能ということになります。

* いろいろ書きましたが、多分ググってもらった方が確実だし分かりやすいと思います。

* 1・2・3・6は参照、let recなしでできました。

* 4は対応する命題「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・再帰型なしでの定義はできなさそうです。

* 5は多分無理。というか絶対無理だと信じてます。「AかつAでない」という命題は常に偽なので証明できないはずだから。

* 7は参照や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で、遅延評価のために用意されている型・関数です。

Categoryノート