问题标签 [k-combinator]

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

SKK 和 II 是 beta 等效的。

在哪里

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

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

K组合器是和K := (λxy.x)定点组合器是Y := λf.(λx.f x x) (λx.f x x)。我试图计算YK：

所以因为YK是 的不动点K：

对于任何 e。但KIe应该等于I！

回想一下，K 组合子是一个常数函数。它总是返回它的第一个参数：

在《模仿一只知更鸟》一书中，作者展示了一个包含会说话的鸟儿的魔法森林的例子。鸟类有以下行为：

给定任何鸟 A 和 B，如果你向 A 喊 B 的名字，那么 A 会通过向你呼唤某种鸟的名字来回应：我们将用 AB 指定这只鸟。

假设森林由三只鸟 A、B 和 C 组成。是否有可能至少有一只鸟表现得像 K 组合子？

下表显示了魔法森林中鸟类可能的一组行为。第一列是森林中每只鸟的名字。最上面一行有可以叫到每只鸟的名字。身体是鸟对名字的反应。例如，如果你向鸟 A 喊 A 的名字，那么鸟 A 会用 C 回应（见第 2 行第 2 列）。简而言之，AA = C。如果你向鸟 A 喊 B 的名字，那么鸟 A 会用 B 回应（见第 2 行第 3 列）。简而言之，AB = B。AC 的空槽应该输入什么值？

让我们看看我们是否可以让鸟 A 表现得像 K 组合器。上面的一组值看起来很有希望：

• 对于所有 y，AA = C 和 Cy = A。也就是说，对于所有 y，(AA)y = A。

• 对于所有 y，AB = B 和 By = B。也就是说，对于所有 y，(AB)y = B。

应该在空槽（AC）中放置什么值？考虑所有情况：

• 如果 AC = A，那么对于所有 y，Ay 的值必须是 C，这显然是错误的。因此 A 不能是空槽的正确值。

• 如果 AC = B，那么对于所有 y，By 的值必须是 C，这显然是错误的。因此 B 不可能是空槽的正确值。

• 如果 AC = C，那么对于所有 y，Cy 的值必须是 C，这显然是错误的。因此 C 不能是空槽的正确值。

因此，对于每个 y，都不能在空槽中放置任何值来满足条件 (AC)y = C。

据我所知，不可能让任何鸟表现得像 K 组合子。我希望你能证明我错了。

假设有一些数据类型来表达 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 有人可以向我解释我做错了什么吗？谢谢你。

我最近一直在学习 F#（我的背景是 C#）并且正在阅读网站http://fsharpforfunandprofit.com，我发现它非常有帮助。

我必须访问http://fsharpforfunandprofit.com/posts/defining-functions/这是关于组合器的部分。除了红隼之外，我都了解它们（尽管 Y 组合器或 Sage 鸟在我的脑海中拧紧！）。Scott Wlaschin 给出的定义（在 F# 中）为：

我一生都无法理解这将是有用的任何情况。起初我认为它可以用作链运算符，以便您可以将值传递给函数，然后返回原始值。我以前自己也写过这样的运算符，但你可以看到它不一样：

如果我们部分应用 K 组合子（值为 5），那么我们会返回一个忽略其参数并返回 5 的函数。同样，没有用。

谁能给我一个简单的例子来说明这可能在哪里使用？

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

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

我错过了什么？

我正在尝试实现一个简单类型的 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

完整来源

我在一本书中读过，点击函数（也称为K-Combinator）的函数签名如下：

“这个函数接受一个输入对象 a 和一个对 a 执行某些操作的函数。它使用提供的对象运行给定的函数，然后返回该对象。”

1. 有人可以帮我解释函数签名中星号（*）的含义吗？
2. 下面的实现是否正确？
3. 如果这三种实现都正确，那么什么时候应该使用哪一种？有什么例子吗？

实施1：

实施2：

实施3：

我的任务是展示

S(KK)I = K

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

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