如果已经给出括号，则 lambda 演算中括号的顺序？

问题描述

我知道应用程序是左关联的，而抽象是右关联的。函数也被优先考虑，但我遇到了一些问题，这些问题已经在表达式中出现了“一些”括号。这些括号是否会导致计算表达式的方式有所不同？还有第一个表达式前的括号是什么意思？

我在决定这些之间时感到困惑 -

1. (lambda x. xy)(lambda y. xy)z --- 在 e1.e2.z 的情况下，我应该从左还是从右开始评估？我会做替换，这很好，但我应该先替换 lambda x 的 x 还是先替换 lambda y 的 y？

2. (((λx.λy.λz.((xy)z)(λu.λv.u))A)B) --- 在这种情况下，我对括号感到困惑。我应该从哪里开始评估？先打开哪个支架？我应该由内向外计算还是由外向内计算？

解决方法

没有为 lambda 演算指定 evaluation strategy。它由您的系统或环境定义。两种常见的策略是正常顺序和应用顺序。对于这个特定问题，无论采用何种策略，答案都是相同的。如果您使用另一种非常规策略，您可以预期结果会有所不同。

(λx.xy)(λy.xy)z    →β x [x := (λy.xy)]

((λy.xy)y)z        remove unnecessary parens

(λy.xy)yz          →β y [y := y]

(xy)z              remove unnecessary parens

xyz

如您所知，应用程序是左关联的。所以删除不必要的括号可以更容易阅读表达式 -

(((λx.λy.λz.((xy)z)(λu.λv.u))a)b)    remove unnecessary parens

(λx.λy.λz.(xyz)(λu.λv.u))ab          →β x [x := a]

(λy.λz.(ayz)(λu.λv.u))b              →β y [y := b]

(λz.(abz)(λu.λv.u))                  remove unnecessary parens

λz.(abz)(λu.λv.u)

在第二个例子中，我们达到了弱头范式，即我们有 λz. 没有任何参数可以应用于它