lambda-calculus - Lambda 微积分缩减步骤

Question

我正在学习 Lambda 微积分并且我被困在归约上......任何人都可以用这个例子解释归约的类型，特别是以最简单的方式减少β。也不介意易于理解的教程。

(λxyz .xyz )(λx .xx )(λx .x )x

Answer 1

λ演算

Lambda 演算有一种方法可以螺旋式地分成很多步骤，使解决问题变得乏味，而且看起来确实很难，但实际上并没有那么糟糕。在 lambda 演算中，只有 lambda，你能用它们做的就是替换。 Lambda 就像一个函数或一个方法——如果您熟悉编程，它们是将函数作为输入并返回一个新函数作为输出的函数。

lambda 演算中基本上有两个半过程:

1) Alpha 转换 - 如果您在内部应用两个具有相同变量名称的 lambda 表达式，请将其中一个更改为新的变量名称。例如，(λx.xx)(λx.x) 在减少之后变成了类似 (λx.xx)(λy.y) 或 (λx.xx)(λx'.x') 的东西。结果与您开始时的结果相同，只是变量名称不同。

2) Beta 减少 - 基本上只是替换。这是使用输入调用 lambda 表达式并获取输出的过程。 lambda 表达式就像一个函数，您可以通过在整个表达式中替换输入来调用该函数。取 (λx.xy)z，(λx.xy) 的后半部分，句点之后的所有内容都被输出，您保留输出，但用提供的输入替换变量(在句点之前命名)。 z是输入，x是参数名称，xy是输出。查找输出中所有出现的参数，并将它们替换为输入，这就是它减少的结果，所以 (λx.xy)z => xy与 z代替 x , 即 zy .

2.5) Eta 转换/Eta 减少 - 这是一种特殊情况的减少，我只称其为半个过程，因为它有点 Beta 减少，有点，从技术上讲它不是。您可能会在维基百科或教科书中看到它写为“每当 x 在 f 中不出现自由时，Eta 转换就会在 λx.(f x) 和 f 之间转换”，这听起来很令人困惑。所有真正的意思是 λx.(f x) = f 如果 f 不使用 x。如果它实际上完全有意义，但通过示例更好地展示。考虑 (λx.(λy.yy)x)，这等价于通过 eta 减少到 (λy.yy)，因为 f = (λy.yy)，其中没有 x，您可以通过减少它来表示，因为它会解决(λx.xx)，这显然是同一件事。你说过要专注于减少 beta，所以我不打算详细讨论 eta 转换，但很多人都在尝试 on the cs theory stack exchange

关于 Beta 减少的符号:

我将使用以下符号将提供的输入替换为输出:
(λ param . output)input => output [param := input] => result
这意味着我们替换输出中出现的参数，这就是它减少到

例子:
(λx.xy)z
= (xy)[x:=z]
= (zy)
= zy
足够的理论，让我们解决这个问题。 Lambda 微积分很好玩。

您提出的问题可以仅通过 Alpha Conversion 和 Beta Reduction 来解决，不要被下面的过程所吓倒。毫无疑问，这很长，但解决它的步骤并不难。

(λxyz.xyz)(λx.xx)(λx.x)x

= (((λxyz.xyz)(λx.xx))(λx.x))x - 让我们在“正序”中添加括号，左结合，abc减少为((ab)c)，其中b应用于a, 和 c 应用于结果

= (( (λxyz.xyz)(λx.xx) )(λx.x))x - 选择最深的嵌套应用程序并首先减少它。

粗体部分减少为:

(λxyz.xyz)(λx.xx)

= (λx.λyz.xyz)(λx.xx) - 意思相同，但我们取出第一个参数，因为我们要减少它，所以我希望它清楚

= (λx.λyz.xyz)(λx'.x'x') - Alpha 转换，有些人坚持使用新字母，但我喜欢在末尾或 `s 附加数字，无论哪种方式都可以。因为两个表达式都使用参数 x 我们必须在一侧重命名它们，因为两个 X 是局部变量，所以不必表示相同的东西。

= (λyz.xyz)[x := λx'.x'x'] - Beta 缩减的表示法，我们删除第一个参数，并将其在输出中的出现替换为正在应用的内容 [a := b] 表示a 将替换为 b。

= (λyz.(λx'.x'x')yz) - 实际减少，我们用提供的 lambda 表达式替换 x 的出现。

= (λyz. ( (λx'.x'x')y) z) - 括号的正常顺序，再看，另一个要减少的应用程序，这次 y 应用于 (λx'.x 'x')，所以现在让我们减少它

= (λyz. ((x'x')[x' := y]) z) - 将其放入减少 beta 的符号中。

= (λyz. (yy) z) - 我们将 x'x' 的两次出现交换为 Ys，现在完全减少了。

将此添加回原始表达式:

(( (λxyz.xyz)(λx.xx) )(λx.x))x

= ((λyz.(yy)z)(λx.x))x - 这不是新的，只是把我们之前发现的东西放回去。

= ( (λyz.(yy)z)(λx.x) )x - 抓取最深的嵌套应用，它是 (λx.x) 应用于 (λyz.(yy)z)

我们将再次单独解决这个问题:

(λyz.(yy)z)(λx.x)

= (λy.λz.(yy)z)(λx.x) - 为了清楚起见，再次将第一个参数取出。

= (λz.(yy)z)[y := (λx.x)] - 放入 beta 约简记法，我们弹出第一个参数，注意 Ys 将切换为 (λx.x)

= (λz.( (λx.x)(λx.x) )z) - 实际减少/替换，粗体部分现在可以减少

= (λz.( (x)[x := λx.x] )z) - 希望你现在已经明白了，我们开始 beta reduce (λx.x)(λx.x)通过把它变成形式 (x)[x := λx.x]

= (λz.( (λx.x) )z) - 还有替换

= (λz. (λx.x)z ) - 清除了过多的括号，我们发现了什么，但另一个应用程序需要处理

= (λz.(x)[x:=z]) - 弹出 x 参数，放入符号

= (λz.(z)) - 执行替换

= (λz.z) - 清除多余的括号

把它放回主表达式:

( (λyz.(yy)z)(λx.x) )x

= ( (λz.z) )x - 填写我们上面证明的内容

= (λz.z)x - 清除过多的括号，现在减少到一个最终应用，x 应用到(λz.z)

= (z)[z:=x] - beta 减少，放入符号

= (x) - 进行替换

= x - 清除多余的括号

是的。答案是x ，它减少了只是常规。