1

语境

昨晚我开始自学 lambda 演算，我试图确定我到目前为止所理解的是否正确。

理解

SKK 等价于 Identity 组合器，I。

其中 L 代表 lambda：

S = LxLyLz((xz)(yz))

K = LxLy(x)

K 基本上采用接下来的 2 (lambda) 项并返回其中的第一个。S 在无类型 lambda 演算中似乎更复杂一些。

我的解释

SK(any-lambda-term) 也等价于 I。

即应用 S 到 K 到 Any-lambda-term 的应用等价于 Identity 组合子：

((SK)(任何)) = I = SKK = ((SK)(K))

如果有帮助的话，我在上面的符号中使用了“左关联”的约定（我试图在上面的第 4 项中用括号明确表示。到目前为止我所读的所有内容似乎都使用了这个约定）。

推理

SK = LyLz((K z)(yz))

下一个 lambda 项将替换 y，设该项为 Y。

天空 = Lz((K z)(Y z))

(Y z) 是 Y 对 z 的应用，也是一个 lambda 项。(K z) 返回返回 z 的常数函数，给定另一个项输入：(Y z)。

我的解释是真的吗？如果不是，你能解释一下吗？我将不胜感激。特别是如果可以解释某种操作顺序——我在考虑何时评估时经常会感到困惑。也许这将通过实践来完善。

4

1 回答 1

0

你的直觉是正确的，但直觉并不能证明什么（唉……）

那么，我们如何证明你的说法呢？只需证明 SKK 和 SKS 具有相同的行为即可。“行为”是一个非正式的概念，它被“语义”正式捕获：如果 SKK 和 SKS 相等，那么根据 SKI 演算语义，它们应该始终归约为同一个术语。

现在，有一个很深的问题，那就是：什么是 SKI 演算？实际上，没有单一的方法可以回答这个问题。您在问题中隐含的做法是您用 λ 项来表达 SKI，并且您依赖于 λ 演算的语义。这是绝对正确的。另一种方法是直接定义 SKI 语义。例如，如果您查看wikipedia page，您会发现语义不是用 lambda 术语定义的（而且它对应于 lambda 术语的事实是一个（好的和预期的）副作用）。在这个答案的其余部分，我将采用与您相同的方法，并将 SKI 项转换为 λ 项。一个很好的练习是使用正确的 SKI 语义重做证明。

所以，让你的问题正式化：你的问题是，对于任何 SKI 术语t，SKKt = SKSt？走着瞧。

SKKt被编码为(λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.x)tλ演算。我们现在只需要将它减少到正常形式（我会详细说明每一步，每次我减少最左边的 λ，即使它不是最快的策略）：

(λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.x)t
= (λy.λz.((λx.λy.x)z)(yz))(λx.λy.x)t
= (λz.((λx.λy.x)z)((λx.λy.x)z))t
= ((λx.λy.x)t)((λx.λy.x)t)
= (λy.t)((λx.λy.x)t)
= t

SKKt因此， λ演算中的编码简化为t（作为旁注，我们刚刚证明了SKK与此处等价I）。为了结束我们的证明，我们必须归约SKSt，看看它是否也归约为t。

SKSt被编码为(λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.λz.(xz)(yz))t。让我们减少它。（这次就不详细说了）

(λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.λz.(xz)(yz))t
= ((λx.λy.x) t)((λx.λy.λz.(xz)(yz)) t))
= (λy.t)((λx.λy.λz.(xz)(yz)) t))
= t

欢呼！它也减少到t，确实如此，SKS并且SKK是等价的。似乎第三个组合子并不重要：只要你有SK?，它就相当于I。作为练习，您可以轻松地证明它（相同的策略，如果是这种情况，那么对于任何术语t和s，SKts = s）。如上所述，另一个很好的练习是在不使用 λ 语义但使用正确的 SKI 语义的情况下重做证明。

最后，我的回答应该向你提出一个新问题：我们有两种语义，一种将 SKI 项编码为 λ 项，另一种则没有。您可能有的问题是：这两种语义是否等价？两个语义等价意味着什么？如果您才刚刚开始自学 λ 演算，那么现在尝试回答这些问题可能还为时过早，但您可以将其保留在脑海中，以便您对正式语言更加熟悉。

于 2021-02-11T13:24:52.040 回答