Lambda演算beta归约变量

Question

我有以下表达式：

(((\x y -> x y (\z -> z + 1)) 5)

除此之外，我还有以下公式：

​

​

我(认为)我知道如何正确地减少它：

((\y -> y)(\z -> z + 1) 5) 

((\y -> y)6)

(6)

但是我不知道如何填写公式中的变量。我不知道该把什么和为什么放在后面。除了这个例子之外，我还有另一个例子，它的表达式如下：

(\x y x -> ( (y z) x) )5

使用以下公式：

​

​

再一次，我想我知道如何减少它：

(\y -> (y z) 5))

(5 z)

但是我还是不知道如何填充变量。

有没有人能帮我填一下这些变量，并解释一下为什么这个变量应该有它的值

Answer 1

第一个公式意味着:如果您有一个应用程序(t u)，您首先将t缩减为一个值t'，该值应该是一个函数。然后将u减少为值u'，这将是函数的参数，然后调用函数。在您的第一个代码片段中，括号不是对称的。让我们假设您打算编写的内容是：

((\x y -> x y) (\z -> z + 1) 5)

第一步是使用两个参数调用函数(\x y -> x y)，并获取

((\z -> z + 1) 5)

然后将5传递给加1的函数，因此结果是6。

第二个公式是，当您想要进行函数调用时，您可以在函数体中用实参替换函数的形参。因此，您在t中将xs更改为us。在此步骤中，您需要稍微小心，以避免捕获变量。看看capture-avoiding substitution吧。