教堂数字的补充

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

尝试鳄鱼蛋!

以下是我在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))  )))))

Answer 2

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

1. 一次只做一件事：执行 alpha 转换、beta 缩减或 eta 转换。请在页面的空白处记下您为到达下一行所采取的步骤。如果这些词对您来说不熟悉，那么它们的作用将是 - 只需查看Wikipedia 即可。

这些减少步骤的快速摘要：

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 转换来更改变量的名称以使事情更清晰。所有这些f，它总是会令人困惑。你"对第二行做了类似的事情

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