教堂数字

Question

我被困在接下来的一步中。如果有人可以帮助我，那就太好了：

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)

括号很好吗？我真的很困惑自己的替代和括号。是否有一种正式，更容易解决此类问题的技术？

Answer 1

尝试 鳄鱼鸡蛋！

这是我的步骤，我在鳄鱼鸡蛋的帮助下得出的步骤：

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))  )))))

Answer 2

我的建议，根据我自己有限但最近的经验：

1. 做 一 一次事情：执行α转换，降低beta或ETA转换。请注意，在您正在努力的页面余量中，您要采取的步骤到达下一行。如果这些话不熟悉，他们的作用将是 - 看看 维基百科.

这些简化步骤的快速摘要：

alpha只是意味着在上下文中更改变量的名称：

λfx. f (f x) => λgx. g (g x)

beta只是意味着将lambda应用于 一 争论

(λf x. f x) b => λx. b x

ETA只是“解开”不必要的包装函数，不会改变其含义。

λx.f x => f

然后

2. 采用 很多 alpha转换以更改变量的名称以使事情变得更清晰。所有那些 fS，这总是会令人困惑。您已经做了类似的事情 " 在你的第二行

3. 假装你是电脑！当您评估表达式时，请勿飞跃或跳过一步。只需做下一件事（只有一件事）。仅一旦信心缓慢移动，只有移动速度就更快。

4. 考虑命名一些表达式，仅在需要评估时才将它们代替其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

Answer 3

是否有一种正式，更容易解决此类问题的技术？

这是 很多 比起手工减少的减少，更容易为lambda术语编写还原和漂亮的术语。但 PLT REDEX 可以给您减少的腿；尝试定义降低正常订单的规则，然后您要做的就是担心 没有冗余括号的结果很好地打印.

您可能还会学到更多。