Lambda演算约简策略及其实验工具的描述

424理论计算机科学电子笔记45（2001）网址：http://www.elsevier.nl/locate/entcs/volume45.html9页演示Lambda演算的简化Peter Sestoft1数学与物理丹麦皇家兽医和农业大学丹麦哥本哈根IT大学摘要我们描述了lambda演算约简策略，使用大步操作语义，并展示了如何有效地跟踪这 种 约 简 。 这 是 在 一 个 基 于 web 的 lambda 演 算 减 少 器 中 使 用 的 ， 在http://www.dina.kvl.dk/~sestoft/lamreduce/。1介绍纯无类型lambda演算[2]经常作为计算机科学课程的一部分教授。它可以在可计算性课程中作为经典计算模型教授[3]。它可以作为指称语义学的基础在语义学课程中教授。它可以在函数式编程课程中作为原型最小函数式编程语言来教授。出于同样的原因，它可能会在编程语言概念课程中教授，或者为了证明一个非常小的语言可以是通用的，例如可以编码算术（以及数据结构，递归函数定义等），使用这样的编码：两个<$λf.λx.f（fx）(1)四个<$λf.λx.f（f（f（fx）加上<$λm.λn.λf.λx.mf（nf x）这篇论文的动机是这样一个假设，即为了欣赏纯无类型lambda演算的操作方面，学生必须对其进行实验，并且工具通过使其不那么乏味和更有趣来鼓励编码和还原策略在本文中，我们描述了一种简单的方法来创建一个工具，演示lambda演算减少。而不是用一个1sestoft@dina.kvl.dk，Thorvaldsensvej 40，DK-1871 Frederiksberg C，Denmark。2000年1月，出版社dbyElsevierScienceB。 V. 在CC BY-NC-ND许可下开放访问。塞斯托夫特425定位下一个要签约的redex的过程，我们通过以下方式描述它：一个大步骤的操作语义学。我们展示了如何跟踪在还原过程中进行的β我们还讨论了编程语言概念之间的关系，如按名称调用和按值调用，和lambda演算概念，如正常的顺序减少和适用的顺序减少。2纯无类型Lambda演算我们使用纯无类型lambda演算[2]。lambda项是一个变量x，一个将x绑定到e中的lambda抽象λx.e，或者一个应用程序（e e）：(2)e：：= x| λx.e|eeLambda项可以有自由变量，不受任何封闭的lambda抽象的约束。项恒等式e1∈e2取lambda约束变量的模重命名，像往常一样.符号e[ex/x]表示ex替换e中的x，并重命名绑定变量以避免捕获。3函数式编程语言在实际的函数式编程语言中，如Scheme [11]，Standard ML [6]或Haskell[10]，程序（术语）不能有自由变量，并且在lambda抽象或其他变量绑定下不会执行约简，因为这会使其有效实现变得相当复杂[9]。然而，lambda演算归约的实现必须在lambda抽象下执行归约。否则，使用编码（1）将2加2不会减少到4，这会让学生失望。因为函数式语言中没有自由变量和抽象下的归约，所以编程语言中的按值调用和按名称调用概念在lambda演算中的含义还不清楚。特别是，应该如何处理自由变量，以及按值调用和按名称调用应该计算什么范式我们提出以下答复：• 自由变量类似于数据构造函数（在标准ML或Haskell中），即未解释的函数符号。如果自由变量位于函数位置（x e2），那么按值调用应该减少参数表达式e2，而按名称调用不应该。这与构造函数在严格语言（例如ML）中是严格的和在非严格语言（例如ML）中是非严格的是一致的。Haskell）。• 函数式语言在抽象下不进行约简，因此只约简到弱范式。特别是，按值调用简化为弱范式，而按名称调用简化为弱头范式。塞斯托夫特426≥4懒惰函数式编程语言在惰性求值下，变量绑定项最多被求值一次，而不管变量使用的频率如何[9]。这种评估机制可以称为按需调用，或共享参数评估的按名调用。惰性语言还允许在堆中创建循环项或循环，通过这样的定义，它创建了无限个1的val ones = 1：： ones用项替换变量不能真正模拟这种由惰性求值创建的恒定大小的循环结构，只能通过递归项定义的无界展开来近似它（例如，使用某种版本的递归组合子Y编码）。为了正确地表达子项求值的共享和循环项的创建，必须用相互递归绑定来扩展演算（2）：(3)e：：= x| λx.e|ee|letrec{xi=ei}in e子项求值的共享和循环项的创建可以使用图归约（Wadsworth 1971，Turner 1979和后续工作[1，9]）或显式堆[5，12]来建模。在任何情况下，懒惰评估的正确建模都需要语法扩展以及比术语缩减更复杂的评估模型在本文中，我们将不再考虑惰性求值，而将只考虑上面（2）中的语法。5正规形我们需要区分四种不同的范式，这取决于我们是否在抽象下减少（在lambda演算中）或不减少（在函数式编程语言中），以及取决于我们是否在替换之前减少参数（在严格语言中）或不减少（在非严格语言中）。下表总结了使用上下文无关语法的四种范式。语法符号E表示相关范式中的项，e表示由（2）生成的任意λ项，并且n为0。注意这两个二分法是如何通过改变e或E来生成四个语法的：在抽象减少争论是的没有是的范式E：：= λx.E| xE1. En弱正规形E：：= λx.e| xE1. En没有头正规形E：：= λ x. E| x e 1. en弱头范式E：：= λx.e| xe1. en塞斯托夫特427BN21 2BN26约简策略和约简函数我们提出了一些使用大步操作语义或自然语义的约简策略[4]，以及它们在标准ML中的实现。我们利用标准ML具有定义良好的语义[6]：它在调用函数之前评估函数我们将lambda项x、λx.e和（e e）建模为ML构造的数据，用字符串表示变量：数据类型lam =字符串的| Lamof string* lam| lam* lam的应用程序我们还假设一个辅助函数subst：lam -> lam -> lam实现了无捕获替换，因此substex（Lam（x，e））是e[ex/x]的ML表示，即（λx.e）ex的β-约化的结果。6.1按名称呼叫减少e−b→n的约化eJ是最左弱约化：x-b→n（λx.e）−b→nX（λx.e）(4)e1−→ （λx.e）e[e/x]−b→neJ（ee）−b→neJe1−→eJ1 /λx.eBN（e1e）−→ （eJ1e2）很容易看出，所有四个规则都以弱头范式生成项。下面的ML函数cbn计算lambda项的弱头范式，以上面的运算语义（4）中隐含的顺序收缩赎回。下面的两个函数子句实现了上面的两个语义规则。下面的第三个函数子句实现了第三和第四个规则，区分了减少e1的结果：fun cbn（Var x）= Var x| cbn（Lam（x，e））= Lam（x，e）| cbn（App（e1，e2））= case cbn e1ofLam（x，e） =>cbn（subst e2（Lam（x，e）| e1’=> App(e1’, e2)塞斯托夫特428−→没有没有BVBV22BVBV−→26.2正规阶约简Normalorderreductionne−n→oeJissleftmostreduction. 函数项me1在应用程序中（e1e2）必须使用按名称调用（4）来减少。也就是说，如果e1约简为抽象（λx.e），那么（（λx.e）e2）是e中任何redex之外的redex，并且必须首先约简。x−n→oxenoeJ没有(5)（λx.e）−→（λx.eJ）bne[e/x]−n→oeJe1（λx.e）2没有（e1e2）−→eJ本杰eJ−→ eJJe−→eJe1−→e1/（λx.e）1没有122（e1e2）−→（eJ1JeJ2）很容易看出这些规则只生成范式项。在标准ML中，实现归约策略作为函数nor是很简单的。它使用上面6.1节中的函数cbnfun nor（Var x）= Var x| nor（Lam（x，e））= Lam（x，nor e）| nor（App（e1，e2））= case cbn e1ofLam（x，e）=> nor（subst e2（Lam（x，e）| e1“ => le t va l e1 ” = no r e1 “在App（6.3按值调用减少调用-by-valuereductionne−b→veJisdefineddbeloww.我不能用你的名字来称呼你（第6.1节）只有通过减少申请的论点（e1e2）之前签订redex合同，在建立应用条款之前：e1−→ （λx.e）e2−→eJ2e[eJ/x]−b→veJ(6)BV（e1e）−→eJe1−→ eJ1 /（λx.e）e2−→eJ2（e1） e）−b→v（eJeJ）12很容易看出这些规则只生成弱范式项。ML函数对规则的实现是直接的，因此被省略了。塞斯托夫特4296.4应用降阶应用顺序约简e−a→oeJ定义如下。我不想打电话-值（第6.3节）仅通过在抽象下减少规则很容易只生成正规形式：e−a→oeJ(7)--（λx.e）−→（λx.eJ）7追踪：侧边删除替换和上下文上 面 ML 中 定 义 的 归 约 器 按 照 操 作 语 义 规 定 的 相 同 顺 序 执 行 替 换e[e2/x]，这要归功于标准ML语义：严格求值和从左到右求值。但它们只返回最终的约化lambda项;它们不跟踪约化的中间步骤，从教学的角度来看，这往往更有趣。ML允许表达式有副作用，所以我们可以让替换函数在收缩之前报告（例如print）redex。为此，我们定义了一个修改的替换函数csubst，它将另一个函数c作为参数，并将其应用于redexApp（Lam（x，e），ex），表示收缩之前的（λx.e）exfun csubst（c： lam -> unit）ex（Lam（x，e））=（c（App（Lam（x，e），ex））;subst ex（Lam（x，e）函数c：lam-> unit只计算其边的结果，如平凡结果类型unit所示。对csubstc ex（Lam（x，e））求值具有在redexApp（Lam（x，e），ex）上调用c的效果，以及对substex（Lam（x，e））求值的结果，其是收缩的redex。我们可以定义一个函数printlam：lam ->unit，它将lambda项打印为一个副项。然后我们可以用csubst printlame2（Lam（x，e））替换6.1节cbn中的调用subst e2（Lam（x，e））。然后，cbn对一个项的约简将产生一个打印的迹线，它是所有的赎回（（λx.e）ex），按照它们收缩的顺序。这仍然没有给我们一个可用的求值跟踪：我们不知道在当前项中，所讨论的redex发生在哪里。这是因为函数c只应用于redex本身;围绕redex的项是隐式的。为了使redex的上下文显式，我们可以使用上下文，或单孔术语，如λx。[]和（e1[ ]）和（[ ]e2）。用lambda项填充上下文的空洞会产生lambda项。以下语法生成所有上下文：(8)C：：= [ ] |λx.C|EC|Ce塞斯托夫特430BN上下文可以由lam -> lam类型的ML函数表示。四种形式的上下文（8）可以使用四个ML上下文构建函数来构建：fun id e = efun Lamx x e = Lam（x，e）fun App2 e1 e2 = App（e1，e2）fun App1 e2 e1 = App（e1，e2）例 如 ， App1e2 是 ML 函 数 fn e1 => App （ e1 ， e2 ） ， 它 表 示 上 下 文（[]e2）。 通过计算（App1e2）e1来完成用项e 1填充孔，其中将s评估为App（e1，e2），表示（e1e2）。函数组合（fo g）组成上下文。例如，上下文λx的组成。[]和（[] e2）是Lamxxo App1e2，其表示上下文λx。（[ ]e2）。类似地，上下文（[ ]e2）和λx. []是App1e2o Lamxx，其表示（（λx. [ ]）e2）。8减少上下文：按名称调用为了产生约简的踪迹，我们修改第6节中定义的约简函数，以获取额外的上下文参数c，并使用扩展的替换函数csubst，将c传递给csubst。然后csubst将在收缩之前将c应用于redex我们以按名称调用的约简函数cbn（6.1节）为例;其他约简函数的处理方式类似。归约函数必须在它下降到项中时建立上下文c它通过使用适当的上下文构建器组合上下文来实现这一点（在本例中，仅在App分支中）：fun cbnc c（Var x）= Var x| cbnc c（Lam（x，e））= Lam（x，e）|cbncc（App（e1，e2））=case cbnc（c oApp1 e2）e1 ofLam（x，e） =>cbnc c（csubst c e2（Lam（x，e）））| e1’=> App(e1’, e2)通过构造，如果c：lam -> lam且cbnc ce的求值涉及一个callcbnccJeJ，则c[e]−→<$βcJ[eJ]。此外，当veracallcbnccJ（e1e2）是eval时，如果e1−→（λx.e），则函数cJ应用于redex（（λx.e）e2）就在它收缩之前。 因此，项e的减少的迹线可以是通过调用cbnc获得，如下所示：cbnc印刷厂其中printlam：lam ->unit是一个将lambda项打印为边项的函数。实际上，计算cbnc printlam（App（Appadd two）two），使用（1）中的编码，打印下面的两个中间项所示的第三项是最终结果（弱头标准形）：塞斯托夫特431（\m.\ n. f. x.m f（n f x））（\f.\x.f（f x））（\f.\x.f（f x））（\n\n f. X.（f. x.f（f x））f（n f x））（\f.\x.f（fx））f. X.（f. x.f（fx）） f（（\f.\x.f（fx）） f x）基于Web的接口可以通过定义一个打印HTML代码的函数htmllam，并在Web服务器上以htmllam作为参数从CGI脚本调用cbnc来创建。 这种 用 Moscow ML 编写的实现[7] 可 以 在 www.example.com 上 获 得http://www.dina.kvl.dk/~sestoft/lamreduce/。9单步降阶对于实验而言，能够一次进行一次β还原，或者换句话说，单步还原是有用的。同样，这可以使用元语言标准ML中的副作用来实现。我们简单地让上下文函数c计算合同的赎回数量（执行的替换），并在开始评估之前设置步长限制N当N次赎回已经收缩时，c通过提出一个异常EnougheJ来中止还原，该异常携带在达到极限时获得的项eJ作为其参数一个封闭的异常处理程序处理这个异常，并报告eJ作为减少的结果。缩减函数的下一次调用只是将步长限制N设置为高一，依此类推。因此，每走一步，原始项的缩减都要重新开始，但我们创造了一次缩减一步的错觉这种方法的主要缺点是执行n步约简所花费的总时间是O（n2）。在实践中，这并不重要：人们不关心单步非常长的计算。10结论我们已经描述了一种实现lambda演算归约的简单方法，使用大步操作语义描述归约策略，通过标准ML中的直接归约函数实现归约，并使用上下文对其进行检测以产生归约的踪迹。这种方法很容易扩展到其他的约简策略描述的大步操作语义。对惰性求值的扩展，无论是使用图归约还是显式堆，都将是复杂的，主要是因为需要打印当前图或堆。在上下文中进行归约的函数对于创建Web接口也很有用，可以将归约函数作为用ML编写的CGI脚本运行。Web界面为学生提供了一个简单的实验平台，可以塞斯托夫特432引用[1] Augustsson ， L. ， 1984 年 ACM Symposium on Lisp and FunctionalProgramming，Austin，Texas，218[2] Barendregt，H.P.，Lambda Calculus（英语：Lambda Calculus）它的语义学和语义学[3] Church，A.，A Note on the Entscheidungsproblem，Journal of Symbolic Logic 1（1936）40[4] Kahn，G.，自然语义学，在STACS 87。第四届计算机科学理论年会，德国帕绍。（Lecture Notes in Computer Science，vol.247，Springer-Verlag1987，22[5] Launchbury ， J. ， A Natural Semantics for Lazy Evaluation ， in Twenty-Years ACM Symposium on Principles of Programming Languages ，Charleston，South Carolina，January 1993，144[6] 米尔纳河，M.托夫特河哈珀和D.B. MacQueen，[7] 莫斯科 ML 是 可用 在http://www.dina.kvl.dk/~sestoft/mosml.html[8] Paulson ， L.C. ， “ML for the Working Programmer”, second edition,Cambridge University Press[9] 佩 顿 · 琼 斯 ， S.L. ， “The Implementation of Functional ProgrammingLanguages”, Prentice-Hall[10] PeytonJones，S.L.和J.Hughes（编辑）：http://www.haskell.org/onlinereport/[11] “Revised[12] Sestoft ， P. ， Deriving a lazy abstract machine ， Journal of FunctionalProgramming 7，3（1997）231