2002-12-28 [長年日記]
λ. 朝
「おはようボンジュール」で俺を起こすのは止めてくれー。いやマジで鳥肌が……
λ. Ruby-CPL (仮称)
CDTから conditional equation を得る部分を書いた。こないだは無駄かもと書いたけど、自分が理解するのが目的なのだから、無駄だって全然構わないのである。
例えば、直積(product)の宣言、
right object prod(X,Y) with pair is pi1: prod -> X pi2: prod -> Y end object
からは以下のような(条件付き)等式が得られ、この宣言がproductの定義になっていることが確認できる。(あ、「.」は関数結合ね。メソッド呼び出しぢゃないぞっ♥)
- pi1.pair(f0,f1) = f0
- pi2.pair(f0,f1) = f1
- pi1.g = f0 ∧ pi2.g = f1 ⇒ g = pair(f0,f1)
- prod(f0,f1) = pair(f0.pi1,f1.pi2)
同様にleft objectの例として、自然数の宣言、
left object nat with pr is zero: 1 -> nat succ: nat -> nat end object
からは、以下のような(条件付き)等式が得られ、自然数の定義になっていることがわかる。
- pr(f0,f1).zero = f0
- pr(f0,f1).succ = f1.pr(f0,f1)
- g.zero = f0 ∧ g.succ = f1.g ⇒ g = pr(f0,f1)
λ. RHG
少し余裕が出来たので、RHGをパラパラとめくってみたり。たしかに難しいけど、脳の奥が痺れて気が遠くなるようなconceptualな難しさではないようなので、とりあえず安心。じっくり読めば何とかなりそう。
ところで、参考文献が随分マニアックな気が……。『プログラム意味論』(横内寛文[著])まで入ってるよ……