Lambda演算β减少变量

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。 第二个公式是说当你想要进行函数调用时，你可以在函数体中用函数的形式参数替换参数。所以，你在x中将us更改为ts。在此步骤中，您需要小心谨慎以避免变量捕获。看看capture-avoiding substitution。