次のステップで立ち往生しています。誰かが私を助けることができれば、それは素晴らしいことです:
2 = λfx.f(f x)
3 = λfx.f(f(f x))
ADD = λm n f x. m f (n f x)
私の手順は次のとおりです。
(λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> ((λn f x. (λf x.f(f(f x))) f (n f x))) (λf x.f(f x))
-> ((λf x. (λf' x'.f'(f'(f' x'))) f ((λf" x".f"(f" x")) f x)
括弧は大丈夫ですか？私は置換と括弧について本当に混乱しています。このような問題に対処するための正式で簡単な手法はありますか?
ワニの卵を食べてみよう！
ワニの卵の助けを借りて導き出した私の手順は次のとおりです。
ADD 2 3
-> (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> (λn f x. (λf x.f(f(f x))) f (n f x)) (λf x.f(f x))
-> (λf x. (λf x.f(f(f x))) f ((λf x.f(f x)) f x))
-> (λf x. (λx.f(f(f x))) ((λf x.f(f x)) f x))
-> (λf x. f(f(f(λf x.f(f x)) f x)))))
-> (λf x. f(f(f (λx.f(f x)) x)))))
-> (λf x. f(f(f (f(f x)) )))))
このような問題に対処するための正式で簡単な手法はありますか?
手動でリダクションを行うよりも、ラムダ項のレデューサーと prettyprinter を作成する方がはるかに簡単です。しかし、PLT Redexを使用すると、削減を有利に進めることができます。正規の順序の縮約のルールを定義してみてください。後は、冗長な括弧を使用せずに結果をきれいに印刷することを心配するだけです。
あなたもおそらくもっと多くを学ぶでしょう。