我被困在以下步骤中。如果有人可以帮助我，那就太好了：
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)
括号好不好？我真的对替换和括号感到困惑。有没有一种正式的、更简单的技术来解决这些问题？
试试鳄鱼蛋！
以下是我在 Alligator Eggs 的帮助下得出的步骤：
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)) )))))
我的建议，来自我自己有限但最近的经验：
这些减少步骤的快速总结：
Alpha 只是意味着一致地更改上下文中的变量名称：
λfx. f (f x) => λgx. g (g x)
Beta 只是意味着将 lambda 应用于一个参数
(λf x. f x) b => λx. b x
Eta 只是简单地“解包”一个不会改变其含义的不必要包装的函数。
λx.f x => f
然后
使用大量alpha 转换来更改变量的名称以使事情更清晰。所有这些f，它总是会令人困惑。你在"第二行做了类似的事情
假装你是电脑！在评估表达式时不要跳过或跳过一步。只做下一件事（而且只有一件事）。只有当你有信心慢慢移动时才能更快地移动。
考虑命名一些表达式，并且仅在需要评估它们时将它们替换为它们的 lambda 表达式。我通常会注意到页面边缘的替换，by def因为它并不是真正的减少步骤。就像是：
add two three
(λm n f x. m f (n f x)) two three | by def
因此，遵循上述规则，这是我的工作示例：
two = λfx. f (f x)
three = λfx. f (f (f x))
add = λmnfx. m f (n f x)
0 | add two three
1 | (λm n f x. m f (n f x)) two three | by def
2 | (λn f x. two f (n f x)) three | beta
3 | (λf x. two f (three f x)) | beta
4 | (λf x. two f ((λfx. f (f (f x))) f x)) | by def
5 | (λf x. two f ((λgy. g (g (g y))) f x)) | alpha
6 | (λf x. two f ((λy. f (f (f y))) x)) | beta
7 | (λf x. two f (f (f (f x)))) | beta
8 | (λf x. (λfx. f (f x)) f (f (f (f x)))) | by def
9 | (λf x. (λgy. g (g y)) f (f (f (f x)))) | alpha
10 | (λf x. (λy. f (f y)) (f (f (f x)))) | beta
11 | (λf x. (λy. f (f (f (f (f x)))))) | beta
有没有一种正式的、更简单的技术来解决这些问题？
为lambda 项编写 reducer 和 prettyprinter 比手动进行归约要容易得多。但是PLT Redex可以让您在减价上占得先机；尝试为正常顺序减少定义规则，然后您所要做的就是担心在没有多余括号的情况下漂亮地打印结果。
你可能也会学到更多。