问题标签 [s-combinator]

我是 lambda 演算的新手，正在努力证明以下内容。

SKK 和 II 是 beta 等效的。

在哪里

S = λ xyz.xz(yz) K = λ xy.x I = λ xx

我试图通过打开它来测试减少SKK，但无济于事，它变得一团糟。不要以为SKK可以在不扩大S、K的情况下进一步缩小。

我开始学习 lambda 演算，我需要在 Erlang 中实现 I、S、K 组合器。当然，S、K、I 代表：

S = λxyz.xz(yz) K = λxy.x I = λx.x

我在纸上理解 I=SKK 转换没有问题（就像这里介绍的：为了证明 SKK 和 II 是 beta 等价的，lambda calculus）但是当涉及到函数式语言和高阶函数时，我似乎不理解它。 ..

我设法做到了 I 和 K （让我们在模块中说test）：

我也知道如何运行 K x (K x) (SKK x = K x (K x))

但是我无法编写 S 组合器。我试过：

但是，我仍然无法将 SKK x 转换为 x

我尝试像这样运行它：

任何帮助将不胜感激，因为我完全迷路了。

假设有一些数据类型来表达 lambda 和组合项：

还有一个函数可以获取 lambda 项的自由变量列表：

将 lambda 项转换为组合项抽象消除规则可能很有用：

1) T[x] => x

2) T[(E₁ E₂)] => (T[E₁] T[E₂])

3) T[λx.E] => (KT[E]) （如果 x 在 E 中不自由出现）

4) T[λx.x] => 我

5) T[λx.λy.E] => T[λx.T[λy.E]] （如果 x 在 E 中自由出现）

6) T[λx.(E₁ E₂)] => (ST[λx.E₁] T[λx.E₂])

这个定义是无效的，因为5)：

所以，我现在拥有的是：

我想要的是（希望我计算正确）：

问题：

如果 lambda 项和组合项具有不同类型的表达式，那么如何5)正确表述呢？

您好，我无法证明这些组合子 SK = KI

带括号 [] 的步骤只是告诉您我正在执行的步骤。例如，λyz.xz(yz) 中的 [λxy.x / x] 表示我将用 (λxy.x) 替换表达式 λyz.xz(yz) 中的每个 x

到目前为止，我尝试的是减少 SK，我得到了这个：

然后减少KI，我得到了这个：

虽然这两个答案似乎不等于我（λyz.zz）和λy。λx.x 有人可以向我解释我做错了什么吗？谢谢你。

可以仅使用标准函数（不通过方程式定义它）而不使用 lambda（匿名函数）在 Haskell 中表达S组合器的模拟吗？我希望它是 type (a -> b -> c) -> (a -> b) -> a -> c。

例如，K组合子的模拟就是const.

事实上，我正在尝试\f x -> f x x使用标准函数来表达函数，但想不出任何标准的非线性函数开始（即多次使用其参数的函数）。

我无法将用于翻转的 lambda 转换为 SKI 组合器（我希望这是有道理的）。这是我的转换：

如果我在 B、C、K、W 系统中正确理解，C 是翻转的，它在 SKI 术语中的定义是S (S (K (S (K S) K)) S) (K K). 显然我的答案与 C 组合器不同......这是我用于转换的规则：

我错过了什么？

我有方程 Y = FY（定点方程）。如何通过其他组合器（特别是具有第一个固定参数的 S-组合器）得到 F 的方程？

我正在尝试实现一个简单类型的 lambda 演算类型检查器。在运行健全性测试时，我尝试输入 (SKK) 并且我的类型检查器抛出此错误：

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

有问题的术语显然是（SKK）

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

我认为问题出在缺乏多态性，因为当我输入检查这个haskell代码时它工作正常：

但如果我专门研究类型：

仅供参考，我的类型系统很简单：

data Type = T | TArr Type Type

完整来源

我的任务是展示

S(KK)I = K

现在由于S需要三个参数，所以我只是一开始就卡在不知道如何解决这个问题。我看到两个论点，即(KK)和I，但没有第三个我可以“发现”。在这种情况下会发生什么？它已经对我有用了，只需省略S xyz = xz(yz)中的z，这产生了KK(I)并因此产生了K。不过这对我来说似乎是错误的，所以我想在这里问一下。这是正确的方法吗？

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

语境

昨晚我开始自学 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)。

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