评估参数不足的 SKI 组合器

Question

我的任务是展示这一点

S(KK)I = K

现在由于S需要三个参数，我只是一开始就陷入困境，不知道如何解决这个问题。我看到两个论点，即 (KK) 和 I，但没有我可以“发现”的第三个论点。在这种情况下会发生什么？它已经对我有用了，只需省略 S x y z = xz(yz) 中的 z，就产生了 KK(I)，结果是 K。但我觉得这似乎不对，所以我想在这里问。这是正确的处理方式吗？

我也不明白 KI 会发生什么，例如 K 也需要两个参数，并且只能得到 I。我的解决方案是正确的还是我必须采取不同的方式？

Answer 1

我的想法是 S(KK)I 是一个采用单个参数的函数 - 称之为

z

。当我们用任意

z

调用此函数时会发生什么？

S(KK)Iz -> KKz(Iz) -> Kz

因此，用 z 调用

S(KK)I

与用 z 调用

K

完全相同。因此，S(KK)I 和 K 是相同的函数。

Answer 2

解决您的问题的最简单方法是使用 eta 转换。 也就是说，每一项 M 的行为就像一项 (λx.M x)（当然，x 在 M 中不可能是自由的）。因此，如果您想要评估的组合器缺少一些参数，您可以对术语进行 eta 转换，然后应用这些组合器。

根据您的示例，您需要两次 eta 转换。下面给出了第一个之后的减少。

S(KK)I -> λx.S(KK)Ix -> λx.KKx(Ix) -> λx.K(Ix) 

现在你有了缺少第二个参数的外组合器 K。如果你对最外层的项： λy.(λx.K(Ix)) y 进行 eta 转换，你会得到 λy.K(Iy)，这不是很有趣。但是您可以将 eta 转换应用于该术语的子术语，例如lambda 抽象体。因此，您可以将 λx.K(Ix) 转换为 λx.(λy.K(Ix) y)。结果是 λx.λy.Ix，它简化为 λx.λy.x，这个术语是 K 组合器的定义。瞧！

事实上，你可以在不使用eta转换的情况下证明组合子的等价性，但是你需要使用一些不太友好的公理作为重写规则（详细信息，请参见Henk P. Barendregt（1984）的第7章。微积分：其语法和语义）。

Answer 3

实际上，这就是 Combo（我将其放在 GitHub 上）在打开扩展性的情况下运行时所做的事情：

    S (K K) I
    = λx·S (K K) I x        ⇒       λx·K K x (I x)  ⇒       λx·K (I x)      
    = λx·λy·K (I x) y       ⇒       λx·λy·I x       ⇒       λx·λy·x
    = λx·K x
    = K

它实际显示的步骤是：

    S (K K) I #0 => K K #0 (I #0)
    K K #0 => K
    K (I #0) #1 => I #0
    I #0 => #0
    K