SKS 是否等于 SKK？

问题描述

背景

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

了解

SKK 相当于标识组合子 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 组合子：

((S K)(Any)) = I = S K K = ((S K)(K))

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

推理

S K = LyLz((K z)(y z))

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

S K Y = Lz((K z)(Y z))

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

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

解决方法

你的直觉是正确的，但直觉证明不了任何事情（唉......）

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

现在，有一个很深的问题，那就是：什么是 SKI 演算？实际上，没有一种方法可以回答这个问题。你在你的问题中隐含地做的是，你根据λ项表达SKI，并且你依赖λ演算的语义。这是完全正确的。另一种方法可能是直接定义 SKI 语义。例如，如果您查看 wikipedia page，您可以看到语义不是用 lambda 术语定义的（并且它对应于 lambda 术语的事实是（好的和预期的）副作用）。在本答案的其余部分中，我将采用与您相同的方法，并将 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 术语编码为 λ 术语，另一种则没有。您可能会遇到的问题是：这两种语义是否等价？两个语义等价是什么意思？如果您刚开始自学 λ 演算，现在尝试回答这些问题可能有点早，但是您可以将它保留在您的脑海中，以便您更熟悉正式语言时。