ラムダ計算(3.1)

一度書いたやつを書き直しました．

元の式はこんびねーたｖ - 女子大生ぷろぐらまーなお☆ないわー Not Foundのブログ9.0から．
ここが大元？

i = Rambda.new("(λx. x)")
k = Rambda.new("(λx. (λ y. x))")
s = Rambda.new("(λx. (λ y. (λ z. ((x z)(y z)))))").simplify


# v = ` ``s``s`kskk ``s``s`kskk
p s[s[k[s]][k]][k][s[s[k[s]][k]][k]].simplify(17).rename.to_s
#=> "(λx y z u. ((λv w. (v v)) (λv w. (v v))))"


nu = k[s].simplify			# `ks
me = s[nu][k].simplify		# ``s`ksk は ``sぬk
ne = s[me][k].simplify		# ``s``s`kskk は ``sめk
v = ne[ne]
a = Rambda.new("A")
va = v[a]
va1 = v[a].simplify(1)

[nu,me,ne,v,va,va1].each{|x| p x.rename.to_s }
#=> "(λx. ((λy z u. ((y u) (z u)))))"
#=> "(λx y z. (x (y z)))"
#=> "(λx y. (x x))"
#=> "(λx. ((λy z. (y y)) (λy z. (y y))))"
#=> "((λx y. (x x)) (λx y. (x x)))"
#=> "(λx. ((λy z. (y y)) (λy z. (y y))))"

簡約する順番で結果が変わってるのと，vの中身が自己増殖を繰り返す所為で，簡約を繰り返すとスタックが溢れて死ぬ．

無限ループ対策に簡約する回数に上限を付けられるようにしてみた．

しかし，簡約化しないと2つの式が等しいか判らないのに簡約しすぎるのもマズいというのでは，一体どうしたらいいのか？

木を触るコードを書くのが苦手だということを再認識．