Lambda演算规约

Question

大家好，

以下是我发现难以简化的lambda表达式，即我不知道如何解决这个问题。

谢谢。

(λm λn λa λb . m (n a b) b) (λ f x. x) (λ f x. f x)

这是我尝试过的，但我卡住了：

将上述表达式视为：(λm. E) M 等于

E = (λn λa λb. m (n a b) b)  
M = (λf x. x) (λ f x. f x)  

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

将上述表达式视为(λn. E) M等同于

E = (λa λb. (λ f x. x) (λ f x. f x) (n a b) b)  
M = ??  

我迷失了！！

请问有人能帮我理解，对于任何lambda演算表达式，执行规约的步骤应该是什么？

- name_masked

---

我认为你的想法是正确的。一个问题—— lambda 表达式是从左到右关联还是从右到左？例如，在你的例子中，你是从右往左关联它们的。 - danben

还有，(λ f x. x) 是什么？这是 (λ f. λx. x) 的某种简写吗？ - danben

@danben：函数应用是左结合的，抽象是右结合的。如果我没记错的话，上面是一个抽象？！是的，那是一种简写形式。 - name_masked

@danben：Lambda演算不属于函数式编程吗？ - name_masked

@darkie15 - 不，这就像在关于大O分析的问题上打上“C ++”标签一样。 - danben

Answer 1

您可以按照以下步骤来简化lambda表达式：

1. 全面使用括号避免错误，使函数应用的位置更加明显。
2. 寻找一个函数应用，即查找模式(λX.e1) e2的出现，其中X可以是任何有效标识符，e1和e2可以是任何有效表达式。
3. 通过将每个自由出现在e1中的x替换为e2的结果来应用该函数，从而将(λx.e1) e2替换为e1'。
4. 重复步骤2和3，直到模式不再出现。请注意，对于非规范化表达式，这可能会导致无限循环，因此您应该在大约1000次迭代后停止；-）

因此对于您的示例，我们从以下表达式开始：

((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x)))

这里的子表达式(λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))符合我们的模式，其中X = m，e1 = (λn. (λa. (λb. (m ((n a) b)) b))))和e2 = (λf. (λx. x))。因此，经过替换，我们得到 (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)))，这使得整个表达式为：

(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x)))

现在我们可以用 X = n，e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)) 和 e2 = (λf. (λx. (f x))) 应用该模式到整个表达式。因此，在进行替换后，我们得到：

(λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b))

现在((λf. (λx. (f x))) a)符合我们的模式，变成了(λx. (a x))，这导致:

(λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b))

这一次我们可以将这个模式应用到 ((λx. (a x)) b)，它会化简成 (a b)，得到：

(λa. (λb. ((λf. (λx. x)) (a b)) b))

现在将这个模式应用于 ((λf. (λx. x)) (a b))，它会简化为(λx. x)，得到：

(λa. (λb. b))

现在我们完成了。

- sepp2k

---

sepp2k: 我有一个问题，缩减应该从左到右还是从右到左进行？或者无所谓吗？ - name_masked

你不能通过不同的顺序来减少得到不同的答案。然而，用某种方式可能会一直减少下去。为了避免这种情况，可以使用“正常顺序规约”，即从最左边开始减少（或者更精确地说是最左边和最外层的 - 基本上是从最左边开始的那个）。如果存在答案，则保证能够得到一个答案。 - RD1

谢谢 RD1..这很有帮助。我也在处理ISZERO 2的简化，其中ISZERO = λn. n (λx. FALSE) TRUE，而2 = λg λy. g (g y)。我已经到达了步骤= ( (λx. FALSE) ((λx. FALSE) TRUE) )。现在这应该返回FALSE，因为外部函数的主体中没有自由的x，对吧？ - name_masked

是的，没错。这是一个忽略参数x并始终返回FALSE的函数。 - RD1

Answer 2

你翻译的内容如下：

你做错了的地方在于第一步，你不能有

。

M = (λf x. x)(λ f x. f x)   

因为原始表达式不包括应用程序表达式。为了清晰起见，您可以根据应用程序是左关联的规则（使用 [ 和 ] 作为新括号，并放入一些缺失的“.”）放置隐式括号：

[ (λm . λn . λa . λb . m (n a b) b) (λ f x. x) ] (λ f x. f x)

从这里开始，在其中找到一个形式为(λv.E) M的表达式，并通过将v替换为M来减少它在E中。 要小心，确保它确实是将函数应用于M：如果您有像N (λv.E) M这样的东西，那么N将作为两个参数应用于函数和M。

如果您仍然卡住了，请尝试为每个lambda也放入括号-基本上是在每个“。”后面加上一个新的“（”，并且匹配的“）”尽可能向右移动，同时仍然匹配新的“（”。 例如，我在此处完成了一个（使用[和]使它们突出）：

( (λm . λn . λa . [λb . m (n a b) b]) (λ f x. x) ) (λ f x. f x)

- RD1

Answer 3

只需用相应的东西替换一个东西：

(λ<b>m</b> λn λa λb . <b>m</b>          (n            a b) b) (λ f x. x) (λ f x. f x)
= ~            ^________                        ~~~~~~~~~~
   (λ<b>n</b> λa λb . (λ f x. x) (<b>n</b>            a b) b)            (λ f x. f x)
=    ~                     ^__________                     ~~~~~~~~~~~~
      (λa λb . (λ <b>f</b> x. x) ((λ f x. f x) a b) b)
=                 ~       ~~~~~~~~~~~~~~~~~~
      (λa λb .   (λ <b>x</b>. <b>x</b>)                    b)
=                   ~  ^                     ~
      (λa λb .         b                      )

那就这样。

- Will Ness