2002-05-03 [長年日記]
λ. たしかに適度に勘違いしてるほうが幸せだとは思うのだけど……う〜ん。
休学も割とよく考えるのだけど、自分を高めるための当面の手段として、大学に通い続ける事以上の手段が思いつかないのが悲しいところ。
λ. 1+1=2 であることを証明できる?
ユークリッド幾何学で「正三角形の内角はすべて 60 °である」が証明できるのと同様に、「1+1=2」はペアノ算術で証明できますよん。去年の12/20に書いたペアノ算術の公理から、1 + 1 = s(0) + s(0) = s(s(0) + 0) = s(s(0)) = 2
それから、「実際，ブール代数は1+1=0 となる数学の一分野です」と書いてあるけど、そうだっけ? それってブール代数ではなくて、2を法とする演算なのでは?
λ. Classificationと情報射の圏
昨日の定義だと「対象のペア (X,Y), (X',Y') が異なる ⇒ Hom(X,Y)∩Hom(X',Y')=φ」が成り立たなかった。でも、射の定義を拡張して、⊨X と ⊨Y の情報も含むようにすればよいだけの事。
λ. Hassan Ait-Kaci: Warren's Abstract Machine --- A Tutorial Construction
WAMの解説としてはこの本が良いと誰かに薦められた事があるのだけど、この本オンライン版があるようです。http://www.isg.sfu.ca/~hak/documents/wam.html が元々のURLらしいのだけど、アクセスでいないので……
あのページはツッコミどころが他にもありますよねえ。あんまり読んでないですが。。<br>Texのページと思って読むものなのかも知れません。<br>とか、偉そうに書いてみましたが、きっとぼくの書いたものもつっこみどころが満載なんだろうなあと、思う次第。
λ算法にChurch numeralてゆう数があるそうなんですがRubyで書けるのかなあ? 自信なし。<br># Church numeral<br><br>def zero<br> lambda(f){lambda(x){x}}<br>end<br><br>def add_1(n)<br> lambda(f){lambda(x){f[n[f][x]]}}<br>end<br><br>def one<br> lambda(f){lambda(x){f[x]}}<br>end<br><br>def two<br> lambda(f){lambda(x){f[f[x]]}}<br>end<br><br>def inc(n)<br> n+1<br>end<br><br>def +(m,n)<br> lambda(f){lambda(x){m[f][n[f][x]]}}<br>end<br><br>def four<br> two + two<br>end
zoeさんの書いたのって<br>http://www.kasumi.sakura.ne.jp/~zoe/tdiary/?date=20020502#p04<br>ですね。これ見て僕も目から鱗が落ちました。<br># 僕も、偉そうな事を書いているわりには、<br># あんまし数学得意じゃないんで。(^^;;<br><br>Church numerals を Ruby で書くとこんな感じかな。<br><br>zero = lambda{|f| lambda{|x| x } }<br>one = lambda{|f| lambda{|x| f[x] } }<br><br>succ = lambda{|n| lambda{|f| lambda{|x| f[n[f][x]] } } }<br>plus = lambda{|m| lambda{|n| lambda{|f| lambda{|x| m[f][n[f][x]] } } } }<br>times = lambda{|m| lambda{|n| m[plus[n]][zero] } }<br>power = lambda{|m| lambda{|n| m[times[n]][one] } }<br><br>ところで、自然数は Church numerals で良いとして、<br>整数や有理数はどんなλ項で表現するのが普通なんだろう……
うぐ。powerのmとnが逆ですね。<br>power = lambda{|m| lambda{|n| n[times[m]][one] } }<br><br>あと、もうちょっとシンプルに出来るか。<br>times = lambda{|m| lambda{|n| lambda{|f| m[n[f]] } } }<br>power = lambda{|m| lambda{|n| n[m] } }<br><br>こんなもんでどうでしょう? > moriqさん
むふー。なるほど。ありがとうございます。