11

我可以理解如何创建和思考 SKI 和 BCKW 微积分,但我永远无法找到实际用途。也许我看的不够深入?也就是说,我想知道(仅举一个例子,我并不是暗示这是真的)Java Servlet 广泛使用 S,而 Python 生成器是 BCW 的一个例子,而我只是无法看穿森林吗?

4

4 回答 4

14

在 Haskell 中,它们无处不在

  • <$>
  • Cflip
  • Kpure
  • id
  • S<*>
  • Wjoin

从 Haskell 的角度来看,<$>意思是“在上下文中做”。

  • (+2) <$> (*3)表示乘以三后加二。
  • (+2) <$> [1,2,3]意味着将两个添加到列表中的每个元素
  • (+2) <$> (read . getLine)意思是在我刚刚读到的数字上加二。
  • (+2) <$> someParser意味着在我刚刚解析的数字上加二。

具有上下文的事物称为函子。你所有的 Java/Python/C++ 迭代器都是奇怪的由内而外的仿函数。

另一个联系:S 和 K 组合器一起是图灵完备的。在 Haskell 中,pure<*>一起形成一个应用函子。

当然,了解其他组合器如何适应需要学习 Haskell。但是这个例子展示了组合子是如何在语言中如此根深蒂固的。

于 2011-11-29T04:30:48.067 回答
3

尽管 lambda 和 SKI 演算不反映大多数编程语言的输入和输出系统(例如图形、网络连接,甚至可以说是标准输入和输出),但实际计算机编程的结构方式对应于 Lambda(因此 SKI 和BCKW),例如递归的想法和调用函数的方式。许多这些编程语言都具有用作函数的 lambda 抽象。

于 2010-11-30T02:34:42.540 回答
3

SKI 和 BCKW 演算与 Lambda 演算(在函数式编程概念中有众所周知的应用)不同,因为它们是无点形式的。另请参阅默认编程。它们构成了理解如何在没有命名参数的情况下构造函数式程序的基础。

我们看到它在某些语言中的应用(例如JoyCat)。我曾经在 Lambda-the-Ultimate.org 上发布过关于 SK 微积分与 Cat 和 Joy 的关系。

就其价值而言:BCKW 和 SKI(或 SK)微积分几乎相同,但 BCKW 基础已经过时。

于 2011-09-22T22:22:04.123 回答
2

这都是关于控制的。

也许从较低的水平开始。应用系统只是对象可以应用于其他对象的系统。应用系统的一个简单示例是 bash。ls | more 可能会假设他们在某个环境中,并且上面的意思是在环境中执行 ls,然后执行更多操作。在应用符号中,这更多是 @ (ls @ environment) 但是,可以做更复杂的事情,例如 ls | grep 模式 | 更多所以现在在应用符号中这是更多@((grep @pattern)@(ls @ environment))。注意 grep @ 模式。Grep 应用于模式,它返回程序以匹配 ls 的结果中的模式。这是应用程序的重点,将程序应用于参数,从“原子”(又名内置)程序构建新程序。但是,我们可以' 不要只使用原始应用程序或内置程序进行太多编程。我们需要一种方法来构建我们的输入并将我们的原语应用于我们的输入。

这就是 lambda 的用武之地。使用 lambda 可以概括 (grep @ 模式) 将 grep 应用于任何输入, (grep @ X) 但是,我们必须有一种方法来获取 grep 的输入。因此我们通常使用函数。f(X) = grep @X 上述过程称为抽象出参数。但是没有理由认为 f 这个名字很特别,所以我们有一个语法: lambda X 。grep@X 然后 lambda X.grep@X, 可以应用于输入,输入将被替换到正文中并进行评估。但是,替换可能会变得混乱,绑定变量在机器上实现起来可能很麻烦。SKI(或 B、C、K、W)提供了一种无需替换即可执行 lambda 内容的方法,而只是交换应用程序。

回顾一下,应用程序就是它的全部内容。在将程序应用于某物(可能是另一个程序)的级别进行推理非常方便。Lambda 演算提供了一种结构化输入和程序对参数的应用的方法。SKI 提供了一种无需显式替换即可执行 lambda 的方法。

应该注意的是,SKI 缩减本质上是惰性的,因此在实际使用 SKI 来构建应用程序时可能需要进行一些考虑。事实上,这些论点现在可能已经被充分评估,也可能是部分应用。人们可以通过类型理论来解决这个问题,并且仅当程序位于应用程序的头部位置时才根据其输入评估程序。即,如果一个人用封闭的 lambda 项编写,翻译成 SKI,那么如果 p @ arg1 @ ...。如果 p 是一个原始程序,那么重写已经完成,所以它的所有参数都是 1 ) 可用,2) 全面评估。但是,我还没有证明这一点,如果有足够强大的类型理论,这可能不是真的……

于 2011-05-26T21:45:12.260 回答