Mai*_*tor 12 algorithm lambda computer-science functional-programming lambda-calculus
我最近在lambda演算中编写了很多程序,我希望我可以实时运行其中一些程序.然而,尽管趋势功能范例基于lambda演算和B减少规则,但我找不到一个不是玩具的单一评估者,而不是效率.功能语言应该很快,但我知道的那些实际上并不提供对普通表单的访问(参见Haskell的惰性求值程序,Scheme的闭包等),因此不能用作LC求值程序.
这让我想知道:只是不可能有效地评估lambda演算术语,它只是一个历史事故/缺乏兴趣,没有人决定为它创建一个快速评估者,或者我只是缺少一些东西？
And*_*rti 14
在目前的知识状态下,评估λ项的最佳方法是所谓的最优图减少技术.该技术于1989年由J.Lamping引入,是他的POPL文章" 一种最佳λ微积分减少算法 ",然后由几位作者修改和改进.您可以在我的书中找到S.Guerrini" 函数式编程语言的最佳实现 ",剑桥理论计算机科学杂志,第44页,1998年.
"最优"一词指的是共享管理.在lambda演算中,你有很多重复,减少的效率至关重要地基于复制工作.在第一顺序设置中,有向非循环图(dags)足以管理共享,但只要您输入更高阶设置,您就需要更复杂的图形结构,包括共享和取消共享.
在纯lambda术语中,最优图减少比所有其他已知的减少技术(环境机器,超级组合器或其他)更快.上面的书中给出了一些基准(见第296-301页),我们证明了我们的实现优于caml-light(ocaml的前身)和Haskell(非常慢).所以,如果你听到人们说从未证明最佳减少比其他技术更快,那就不是真的:它在理论和实验上得到了证明.
功能语言尚未以这种方式实现的原因是在函数式编程的实践中,你很少使用具有非常高级别的函数,并且当你这样做时它们通常是线性的.一旦提高等级,lambda术语的内在复杂性就会变得非常危险.有一种技术可以让你减少一个时间段O(2 ^ n)而不是O(2 ^(2 ^ n))并没有在实践中产生那么大的差别:两种计算都是不可行的.
我最近写了一篇简短的文章,试图解释这些问题:" 关于有效减少lambda术语 ".在同一篇文章中,我还讨论了采用超优化还原技术的可能性.
评估lambda术语有多种方法.根据类型信息是否可用,您可以获得更高效和更安全的评估程序(不需要运行时检查,因为已知程序运行良好).我将简要介绍一些技巧.
您可以设计一种算法,试图通过在"大步骤"中评估一个术语来最小化工作,而不是重复定位lambda-redex并触发它们(这意味着多次遍历该术语).
例如,如果要标准化的术语是规则化,t u那么你将两者标准化t,u并且如果norm t是一个lambda抽象,则激活相应的redex并重新启动你刚刚得到的术语的规范化.
现在,您可以使用抽象机器完成相同的工作但速度更快.这些小型虚拟机具有自己的一组指令和简化规则,您可以用自己喜欢的语言实现这些规则并将lambda术语编译为.
历史的例子是SECD机器.
Danvy等.已经表明,众所周知的抽象机器可以通过连续传递风格和去功能化的组合从前面提到的评估者中得出.
要从抽象机器中获取一个lambda-term,你需要实现一个基于机器所处状态构建lambda术语的reification/readback函数.Grégoire和Leroy展示了如何在一个上下文中完成这样的事情.该语言的类型理论是Coq.
通过评估规范化是利用宿主语言的评估机制来实现另一种语言的规范化过程的实践.
Lambda抽象被转换为宿主语言中的函数,应用程序成为宿主语言的应用程序等等.
这种技术可以以类型化的方式使用(例如,在Haskell或OCaml中对简单类型的lambda演算进行归一化)或无类型的(例如,简单类型的lambda演算再次或Coq术语编译为OCaml(!)) .