ラムダ計算

手で計算するのは面倒だなと思ってRambdaクラス*1を作ったら200行超えた…．

行列の掛け算と同じで，機械的に操作すること自体は中学生にでも出来ると思うんだけど，計算の意味がまるで理解できない．論理回路でand,or,notを組み合わせて加算器を作るとかそういう感じ？

しかし，以前と比べると普通にlambdaだのmap,eachの類を使うようになった．少しはタメになっているのかも．

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

skk = s.apply(k).apply(k)
p skk.to_s
#=> "λz. ((λv. (λw. v) z) (λx. (λy. x) z))"
p skk == i
#=> true
p skk.simplify.rename.to_s
#=> "λx. x"



one = Rambda.new("λf x.f x")
two = Rambda.new("λf x. f(f x)")
three = Rambda.new("λf x.f(f(f x))")

plus = Rambda.new("λa b f x. a f ( b f x)")

plus_1 =  plus.apply(one).simplify
p plus_1.to_s
#=> "λb y z. (y (b y z))"
p plus_1.apply(two).simplify.rename.to_s
#=> "λx y. (x (x (x y)))"

plus_2_1 = plus.apply(two).apply(one)
p plus_2_1.to_s
#=> "λy z. (λu v. (u (u v)) y (λf x. (f x) y z))"
p plus_2_1.simplify.to_s
#=> "λy z. (y (y (y z)))"

renameがα変換．simplifyがβ簡約に当たるはず．

*1:もちろんLambdaではない