SKS 等于 SKK 吗？
Does SKS equal SKK?
上下文
我昨晚开始自学 lambda 演算，我想确定我目前所理解的是否正确。
了解
SKK 等价于恒等组合子 I.
其中 L 代表 lambda：
S = LxLyLz((xz)(yz))
K = LxLy(x)
K 本质上接受接下来的 2 个（lambda）项并返回其中的第一个。 S 在无类型 lambda 演算中似乎有点复杂。
我的解读
SK(any-lambda-term) 也等价于 I.
即将 S to K 的应用应用于 Any-lambda-term 等价于 Identity combinator:
((S K)(任意)) = I = S K K = ((S K)(K))
我在上面的符号中使用了“左关联”的约定，如果这有帮助的话（我试图在上面的第 4 项中用括号阐明这一点。到目前为止我读过的所有内容似乎都使用这个惯例）。
推理
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)returns常数函数即returns z，给定另一项输入：(Y z).
我的解释正确吗？如果不是，你能提供一个解释吗？我将不胜感激。特别是如果可以解释某种操作顺序——我经常发现自己在考虑何时评估时感到困惑。也许这会随着实践而完善。
你的直觉是正确的，但直觉证明不了什么（唉...）
那么，我们如何证明你的说法呢？只需证明 SKK 和 SKS 具有相同的行为。 “行为”是一个非正式的概念，它被“语义”正式捕获：如果 SKK 和 SKS 相等，那么根据 SKI 演算语义，它们应该总是归结为相同的术语。
现在，有一个很深的问题，那就是：什么是SKI-calculus？实际上，没有一种方法可以回答这个问题。您在问题中隐含地做的是 根据 λ 术语 表达 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 项编码为 λ 项，另一种不这样做。你可能会有的问题是：这两种语义是等价的吗？两个语义等价是什么意思？如果您刚刚开始自学 λ 演算，那么现在尝试回答这些问题可能有点早，但您可以将其放在头脑的某个角落，等您对形式语言更加熟悉时再使用。
上下文
我昨晚开始自学 lambda 演算，我想确定我目前所理解的是否正确。
了解
SKK 等价于恒等组合子 I.
其中 L 代表 lambda：
S = LxLyLz((xz)(yz))
K = LxLy(x)
K 本质上接受接下来的 2 个（lambda）项并返回其中的第一个。 S 在无类型 lambda 演算中似乎有点复杂。
我的解读
SK(any-lambda-term) 也等价于 I.
即将 S to K 的应用应用于 Any-lambda-term 等价于 Identity combinator:
((S K)(任意)) = I = S K K = ((S K)(K))
我在上面的符号中使用了“左关联”的约定，如果这有帮助的话（我试图在上面的第 4 项中用括号阐明这一点。到目前为止我读过的所有内容似乎都使用这个惯例）。
推理
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)returns常数函数即returns z，给定另一项输入：(Y z).
我的解释正确吗？如果不是，你能提供一个解释吗？我将不胜感激。特别是如果可以解释某种操作顺序——我经常发现自己在考虑何时评估时感到困惑。也许这会随着实践而完善。
你的直觉是正确的，但直觉证明不了什么（唉...）
那么，我们如何证明你的说法呢？只需证明 SKK 和 SKS 具有相同的行为。 “行为”是一个非正式的概念，它被“语义”正式捕获：如果 SKK 和 SKS 相等，那么根据 SKI 演算语义，它们应该总是归结为相同的术语。
现在，有一个很深的问题，那就是：什么是SKI-calculus？实际上，没有一种方法可以回答这个问题。您在问题中隐含地做的是 根据 λ 术语 表达 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 项编码为 λ 项，另一种不这样做。你可能会有的问题是：这两种语义是等价的吗？两个语义等价是什么意思？如果您刚刚开始自学 λ 演算，那么现在尝试回答这些问题可能有点早，但您可以将其放在头脑的某个角落，等您对形式语言更加熟悉时再使用。