标签: lambda-calculus

我发誓曾经有一件T恤出售,上面写着不朽的话:

什么部分

你不明白吗？

就我而言,答案就是......全部!

特别是,我经常在Haskell论文中看到这样的符号,但我不知道它的含义是什么.我不知道它应该是什么样的数学分支.

我当然认识到希腊字母的字母,以及诸如"∉"之类的符号(通常意味着某些东西不是一组的元素).

另一方面,我以前从未见过"⊢"(维基百科称它可能意味着"分区").我也不熟悉这里使用的vinculum.(通常它表示一个级分,但是这并不出现在这里是这种情况.)

如果有人至少可以告诉我从哪里开始想要理解这个符号海洋的含义,那将会有所帮助.

Haskell(使用GHC编译器)比你期望的要快很多.如果使用得当,它可以与低级语言保持密切联系.(Haskellers最喜欢的事情是尝试在C的5%范围内(或者甚至击败它,但这意味着你使用的是低效的C程序,因为GHC将Haskell编译为C).)我的问题是,为什么？

Haskell是声明性的,基于lambda演算.机器架构显然势在必行,粗略地基于图灵机.实际上,Haskell甚至没有具体的评估顺序.此外,您不必处理机器数据类型,而是始终生成代数数据类型.

最奇怪的是更高阶函数.你会认为动态创建函数并抛出它们会使程序变慢.但是使用更高阶函数实际上使Haskell更快.实际上,似乎要优化Haskell代码,你需要使它更优雅和抽象,而不是更像机器.如果Haskell的更高级功能没有改进,它们似乎甚至都不会影响它的性能.

很抱歉,如果这听起来不错,但这是我的问题:为什么Haskell(使用GHC编译)如此之快,考虑到它的抽象性质和与物理机器的差异？

注意:我说C和其他命令式语言有点类似于图灵机的原因(但不是Haskell类似于Lambda微积分)是因为在命令式语言中,你有一个有限数量的状态(也就是行号) ,以及磁带(ram),以便状态和当前磁带确定对磁带做什么.有关从图灵机到计算机的过渡,请参阅维基百科条目,图灵机等效项.

教会号码是自然数字作为函数的编码.

(\ f x ? (f x))             -- church number 1
(\ f x ? (f (f (f x))))     -- church number 3
(\ f x ? (f (f (f (f x))))) -- church number 4

整齐地说,你可以通过应用它们来取代2个教会数字.也就是说,如果你申请4到2,你就得到教会号码16,或者2^4.显然,这完全是不切实际的.教会数字需要一定数量的记忆,而且非常非常慢.像10^10GHCI快速正确回答的类似计算的东西需要很长时间,无论如何都无法适应你计算机上的内存.

我最近一直在尝试最佳的λ评估员.在我的测试中,我不小心在我的最佳λ计算器上键入了以下内容:

10 ^ 10 % 13

它应该是乘法,而不是取幂.在我绝望地移动我的手指中止永久运行的程序之前,它回答了我的要求:

3
{ iterations: 11523, applications: 5748, used_memory: 27729 }

real    0m0.104s
user    0m0.086s
sys     0m0.019s

随着我的"错误警报"闪烁,我去谷歌并确认了10^10%13 == 3.但是λ计算器不应该找到那个结果,它几乎不能存储10 ^ 10.对于科学,我开始强调它.这立刻回答我20^20%13 == 3,50^50%13 == …

对于所有了解lambda演算的人:在编程方面它给你带来了什么好处？你会建议人们学习吗？

因此关于Lambda微积分的维基百科条目很有意思,但我已经完成了.我希望深入一点,更好地理解Lambda微积分.

任何人都可以推荐他们认为是Lambda微积分的最佳书籍或入门书吗？

我已多次尝试掌握continuation和call/cc的概念.每一次尝试都是失败的.有人可以向我解释这些概念,理想情况下,这些概念比维基百科或其他SO帖子更具现实性.

我有网络编程和OOP的背景.我也理解6502汇编并且与Erlang有一个小的randez-vous.不过,我无法绕过电话/ cc.

我一直在阅读各种类型的系统和lambda calculi,我发现lambda立方体中的所有类型的lambda结石都是强烈正常化而不是图灵等效.这包括系统F,简单类型的lambda演算加多态.

这引出了以下问题,我一直无法找到任何可理解的答案:

• (例如)Haskell的形式主义与表面上基于的微积分有何不同？
• Haskell中的哪些语言功能不属于System F形式主义？
• 允许图灵完整计算所需的最小变化是什么？

非常感谢你帮助我理解这一点.

纯粹的无类型lambda演算是一个强大的概念.然而,构建用于实际使用的机器或解释器通常被描述为(接近)不可能.我想调查一下.理论上可以建立一个相对快速的无类型lambda演算机器吗？

相对较快,我通常意味着可以在类似数量的资源(门,操作,物理空间,电力使用等)内,对类似范围的任务进行现代图灵式架构的比较.

我对机器的实现和架构层没有任何限制,只是它必须在某种程度上在物理上和某种程度上可实现.对如何处理IO也没有限制.

• 如果可能,主要挑战是什么？
• 如果不可能,为什么以及如何？
• 这个领域的研究状况如何？
• 哪些领域和科目最相关？

关于基于lambda演算的计算机体系结构的可行性了解多少？

涉及类似理由的问题:

• 功能编程的机器模型
• 采用图灵机作为主要模型的历史原因

我是Ruby的新手,仍然试图理解一些语言设计原则.如果我做对了,Ruby中的lambda表达式调用必须是方括号,而"常规"函数调用是"常规"/圆括号.

语法有什么不同的特殊原因吗？或者,换句话说,(为什么)调用者应该知道他们是调用函数还是应用lambda表达式？

我无法解释lambda立方体这个术语比维基百科更好:

[...]λ-cube是一个框架,用于探索Coquand构造计算中的细化轴,从简单类型的lambda演算开始,作为放置在原点的立方体的顶点,以及构造的微积分(更高阶)依赖型多态lambda演算作为其完全相反的顶点.立方体的每个轴代表一种新的抽象形式:

• 术语取决于类型或多态性.系统F,又名二阶lambda演算,仅通过强加此属性获得.
• 类型取决于类型或类型运算符.简单地键入lambda-calculus与类型运算符λω,只通过强加此属性获得.与系统F结合,产生系统Fω.
• 类型取决于术语或依赖类型.仅施加此属性会产生λΠ,这是一种与LF密切相关的类型系统.

所有八个计算都包括最基本的抽象形式,术语取决于术语,普通函数与简单类型的lambda演算一样.立方体中最富有的微积分,包括所有三个抽象,是结构的微积分.所有八个结石都强烈正常化.

是否有可能在Java,Scala,Haskell,Agda,Coq等语言中找到代码示例,以便在缺少此优化的结石中无法实现每个细化？