是否有可能有效地评估lambda演算术语?

问题描述 投票:11回答:2

我最近在lambda演算中编写了很多程序,我希望我可以实时运行其中一些程序。然而,尽管趋势功能范例基于lambda演算和B减少规则,但我找不到一个不是玩具的单一评估者,而不是效率。功能语言应该很快,但我知道的那些实际上并不提供对普通表单的访问(参见Haskell的惰性求值程序,Scheme的闭包等),因此不能用作LC求值程序。

这让我想知道:只是不可能有效地评估lambda演算术语,它只是一个历史事故/缺乏兴趣,没有人决定为它创建一个快速评估者,或者我只是缺少一些东西?

algorithm lambda functional-programming computer-science lambda-calculus
2个回答
13
投票

在目前的知识状态下,评估λ项的最佳方法是所谓的最优图减少技术。该技术于1989年由J.Lamping在他的POPL文章“An algorithm for optimal lambda calculus reduction”中引入,然后由几位作者进行了修订和改进。您可以在我的书中找到S.Guerrini“The optimal implementation of functional programming languages”,剑桥理论计算机科学杂志,第44页,1998年。

“最优”一词指的是共享管理。在lambda演算中,你有很多重复,减少的效率至关重要地基于复制工作。在第一顺序设置中,有向非循环图(dags)足以管理共享,但只要您输入更高阶设置,您就需要更复杂的图形结构,包括共享和取消共享。

在纯lambda术语中,最优图减少比所有其他已知的减少技术(环境机器,超级组合器或其他)更快。上面的书中给出了一些基准(参见第296-301页),我们证明了我们的实现优于caml-light(ocaml的前身)和Haskell(非常慢)。所以,如果你听到人们说从未证明最佳减少比其他技术更快,那就不是真的:它在理论和实验上得到了证明。

函数式语言尚未以这种方式实现的原因是在函数式编程的实践中,你很少使用具有非常高级别的函数,并且当你这样做时它们通常是线性的。一旦提高等级,lambda术语的内在复杂性就会变得非常危险。有一种技术可以让你减少一个时间段O(2 ^ n)而不是O(2 ^(2 ^ n))并没有在实践中产生那么大的差别:两种计算都是不可行的。

我最近写了一篇试图解释这些问题的短文:“About the efficient reduction of lambda terms”。在同一篇文章中,我还讨论了采用超优化还原技术的可能性。


9
投票

评估lambda术语有多种方法。根据类型信息是否可用,您可以获得更高效和更安全的评估程序(不需要运行时检查,因为已知程序运行良好)。我将简要介绍一些技巧。

大步评估员

您可以设计一种算法,试图通过在“大步骤”中评估术语来最小化工作,而不是重复定位lambda-redex并触发它们(这意味着多次遍历该术语)。

例如。如果你要标准化的术语是t u然后你将tu标准化,如果norm t是一个lambda抽象,你可以触发相应的redex并重新启动你刚刚得到的术语的规范化。

抽象/虚拟机

现在,您可以使用抽象机器完成相同的工作但速度更快。这些小型虚拟机具有自己的指令和缩减规则,您可以用自己喜欢的语言实现并编译lambda术语。

历史的例子是SECD machine

Danvy et al.已经证明,众所周知的抽象机器可以通过连续传递风格和去功能化的组合从前面提到的评估者中获得。

要从抽象机器中获取lambda-term,需要实现一个基于机器所处状态构建lambda术语的reification / readback函数.Grégoire and Leroy展示如何在类型的上下文中完成这样的事情。语言理论是Coq之一。

通过评估进行标准化

通过评估规范化是利用宿主语言的评估机制来实现另一种语言的规范化过程的实践。

Lambda抽象被转换为宿主语言中的函数,应用程序成为宿主语言的应用程序等等。

该技术可以以类型化的方式使用(例如,对简单类型的λ演算in Haskellin OCaml进行归一化)或无类型的方法(例如,简单类型的lambda-calculus once moreCoq terms编译为OCaml(!))。

© www.soinside.com 2019 - 2024. All rights reserved.