功能逻辑语言的操作语义研究及其等价性证明

1理论计算机科学电子笔记76（2002）网址：http://www.elsevier.nl/locate/entcs/volume76.html19页函数逻辑语言Elvira Albert1Michael Hanus2FrankHuch2JavierOliver3Germ'anVidal31DSIP，UCM，Avda. Computense s/n，E-28040 Madrid，Spainelvira@fdi.ucm.es2InstitutfurInformatik，CAUKiel，Olshausenstr. 40，D-24098Kiel，Germany@ informatik.uni-kiel.de3DSIC，UPV，Camino de Vera s/n，E-46022瓦伦西亚，西班牙{fjoliver，gvidal}@ dsic.upv.es摘要在这项工作中，我们提供了一个语义描述的功能逻辑语言涵盖的概念，如懒惰，共享和非决定性。这样的语义描述是必不可少的，例如，有适当的语言定义，以便对程序进行推理并检查实现的正确性。 首先，我们定义一个自然风格的“big-step”语义，用于关联表达式及其评估结果。由于这种语义不足以推理程序的操作方面，我们还定义了一个“小步”操作语义，涵盖了函数逻辑语言的主要特征。最后，我们证明了“小步”语义和自然语义的等价性1介绍这项工作的动机是，不存在一个精确的定义，涵盖现代函数逻辑语言的所有方面的操作语义，如懒惰和模式匹配，共享，逻辑变量和非确定性。例如，关于多范式语言Curry的报告[14]包含了相当精确的操作语义，但仅非正式地涵盖了函数逻辑语言Toy [18]的操作语义基于窄化和共享，但形式定义基于*本工作已部分得到CICYTTIC2001-2705-C 03 -01、Accio'nIntegrada Hispano-AlemanaHA 2001 -0059、Acc. Int. Hispano-Italiana HI 2000 -0161和DFG根据授权Ha 2457/1-2。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔2在一个缩小演算[10]，其中不包括一个特定的模式匹配策略。然而，后者变得重要，例如，如果有人想推理计算的成本（参见[4]关于缩小策略和演算的讨论）。为了定义一个适当的基础，推理程序，正确的实现，优化，或计算成本，我们提供了一个语义描述，涵盖了当前功能逻辑语言的重要方面为此，我们分两步进行。 首先，我们引入一个自然的语义，它通过将表达式与值相关联来定义预期的结果。这种然后，我们提供了一个更面向实现的语义的基础上定义的个人计算步骤。这种最终语义是对程序操作方面的推理的正式引用（例如，开发适当的调试工具）。它也是一个基础，以提供一个全面的定义咖喱（相对于[12，14]，其中只包含部分定义）。此外，人们可以使用它来证明实现的正确性，如[20]所做的这项工作安排如下。 在下一节中，我们将介绍一些理解后续发展的基础。第三节介绍了自然风格函数逻辑程序的语义。这在第4被定义为描述各个执行步骤的语义，并证明了两种语义之间的等价性第5节包括与相关工作的比较最后，第六节总结并指出了进一步研究的方向。2基础在本节中，我们将描述现代函数逻辑语言的内核，其执行模型将惰性求值与非确定性和剩余相结合。这个模型已经在[12]中引入，但没有正式定义公共子项的共享。后一个方面的准确定义是随后各节的目的。在这种情况下，程序是一组函数定义，其中每个函数都由描述输入参数的不同情况的规则定义。例如，布尔值（True，False）的合取可以通过以下规则定义：True x = xFalse x = False(data构造函数通常以大写字母开头，函数应用由并置表示）。没有限制w.r.t. 超过-阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔3∈重叠规则;特别是，人们也可以用非连续规则来定义对给定输入产生多个结果 的 函 数 （ 这 些 被 称 为 非 确 定 性 或 集 值 函 数 ） 。 例 如 ， 下 面 的 函 数“ c h o o s e “ 非 确 定 性 地 返 回 其 两 个 参 数 之 一 ：选择x y =x选择x y=y一个微妙的问题是包含这些函数的嵌套应用程序的含义，例如，“double（choose 1 2）“的可能值的集合定义 类似于[10]，我们遵循“调用时选择”语义，其中子项的所有后代在推导中被简化为相同的值，即，前面的表达式非确定性地减少到值2或4之一（但不是3）。这种选择与惰性评估策略一致，其中子项的所有后代都是共享的[17]。这项工作的目标是以一种精确和可理解的方式描述懒惰，分享和非决定论的组合为了提供一个可理解的操作描述，我们假设源程序被翻译成一个该格式的主要优点是通过使用对操作阅读很重要的格表达式来明确表示模式匹配此外，源程序可以很容易地翻译成这种形式[13]。Tumblat程序的语法P：：= D1. DMD：：= f（x1，...，xn）= ee：：=x（变量）|c（e1，.，en）（构造函数调用）| f（e1，.，en）（函数调用）| {p1→e1;. ;n→n}（刚性情况）|fcaseeof{p1→e1;. ;n→n}（不灵活的情况）|e1或e2（disjunction）|设x1= e1，...，xn= enin e(let约束力）p：：= c（x1，.， xn）其中P表示程序，D是函数定义，p是模式，e是任意表达式。程序P由一系列函数定义D组成，使得左边有两两不同的变量参数。右侧是由变量Var={x，y，z，. . }、数据构造器（例如，a，b，c，.）、函数调用（例如，阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔4f，g，h，.）、格表达式、析取（例如， 来表示集值函数），并让局部变量x1，...，xn仅在e 1中可见，...，en，e. case表达式的形式为：1（f）{c1（xn1）→e1;. ; ck（xnk）→ek}其中e是表达式，c1，.，ck是不同的构造函数，而e1，...，k是表达式。模式变量xni是局部引入的，并绑定子表达式ei的相应变量。case和fcase之间的区别只在参数e是自由变量时才表现出来：case挂起，而fcase非确定性地将这个变量绑定到case表达式的分支中的Let绑定原则上不是翻译源程序所必需的，但是它们便于表达共享而不使用复杂的图结构（例如，[9，11]）。在操作上，让绑定引入新的内存中的结构在计算后更新，这对于惰性计算是必不可少作为一个例子的martinat表示，我们显示的翻译功能“与且（x，y）={True→y; 错误→错误}choose（x，y）=x或y计算的惰性（或需要性）将在函数调用和case表达式的行为描述中表现出来在函数调用中，参数不被计算，而是直接传递给函数体。在case表达式中，需要case参数的最外层符号的形式;因此，case参数应该被评估为头部范式（即，在最外层位置具有构造函数的变量或表达式因此，我们的操作语义学将描述表达式的评估，只有头部范式。这不是一个限制，因为对范式的求值或方程的求解可以简化为头部范式计算（参见[13]）。类似地，当前函数式语言的高阶特征可以通过引入辅助的“apply”函数来简化为一阶定义因此，我们将我们的操作语义的定义建立在上面描述的抽象形式的这也与使用相同中间语言的当前实现一致[5]。事实上，程序的Representation构成了现代声明式多范式语言的核心，额外变量是指规则中不在左边出现的变量这些额外的变量旨在通过条件或右侧的约束来实例化例如，它们通常在Curry程序中通过以下形式的声明引入让x自由进入1我们把on写为对象序列o1，.， on和（f）case表示fcase或case。阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔5正如Antoy [4]所指出的，在函数逻辑语言中使用额外的变量不会引起概念上的问题，如果这些额外的变量在应用规则时被我们将对这种重命名进行建模，类似于let绑定中局部变量的重命名。为了这个目的，我们假设所有额外的变量x都是显式地通过一个直接的循环let绑定形式letx=xine引入到Rollat程序中的。在本文中，我们称这些变量为逻辑变量。例如，具有逻辑变量x和y的表达式x+y表示为：设x=x，y=y在x+y中。 我们的逻辑变量表示法并不排除使用其他循环数据结构，如letx = 1：xin. 值得注意的是，在实现中也使用了循环绑定用Prolog来表示逻辑变量[23]。3函数逻辑程序的自然语义在本节中，我们介绍了一个自然的（大步）语义的功能逻辑程序，这是一个（简单）指称语义和（复杂）操作语义的具体抽象机之间的中间 我们的语义是不确定的，准确的模型共享。 这是通过使用let构造来实现的，let构造可以被认为是仅在需要时进行评估的子计算的命名。让我们通过一个例子来说明分享例3.1考虑下面的程序：foo（x）=addB（x，x）bit= 0或 1addB（x，y） ={0→y;1→{0→1;1→B0}}的情况在基于共享的实现中，“foo（e）“的计算必须仅评估表达式e一次。因此，对目标“foo（bit）“的求值必须返回0或BO（binaryoverbitow）。请注意，如果不共享，结果将是0、1或BO。我们的语义定义主要遵循Launchbury [17]为函数式程序的惰性评估定义的自然语义在这种（高阶）函数语义中，let构造用于创建和共享闭包（即，作为lambda表达式的值创建的函数对象Launchbury的自然语义学的核心思想同样，我们也描述了我们的（一阶）语义函数逻辑程序在两个独立的阶段。在第一阶段，我们应用规范化过程，以确保函数和构造函数的参数始终是变量。这些变量将被解释为阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔6›→引用以表达共享，并且不需要是成对不同的。定义3.2（规范化）表达式的规范化通过映射函数（或构造函数）调用的所有参数，其归纳定义如下：xx=x（x1，.， xn）= （x1，.，xn）（x1，.，xi−1，ei，ei+1，.，en）n = let xi= ein nin n（x1，.，xi−1，xi，ei+1，.， en）其中ei不是变量，xi是新鲜的（let{xk=ek}ine）=let{xk=ek}ine（e1ore2）=e1ore2（（f）{pk→ek}的情况e）=（f）{pk<$→ek<$}的情况e在这里，表示构造函数或函数符号。 将这个规范化过程扩展到程序是很简单的。规范化为每个非变量参数引入了一个新的let构造简单地说，这可以被修改，以产生一个单一的let，并绑定函数（或构造函数）调用的所有不可变参数，我们在后面的例子中假设这与[17]相比，我们的归一化过程不需要执行使用完全新的变量重命名E中的绑定变量），因为我们的自然语义已经为E中的所有绑定变量引入了新的变量名，如我们将在随后的段落中解释的。对于我们的语义的定义，我们认为程序和要计算的表达式都已经像定义3.2那样被规范化了。例3.3再次考虑例3.1的计划和目标。它们的正常化返回程序不变和以下目标：letx1=bitinfoo（x1）图1中定义了状态转换语义。我们的规则遵循以下命名约定：Γ，θ，θ ∈堆= Var → Expv∈值：：= x|c（en）堆是从变量到表达式的部分映射（空堆用[ ]表示）。与堆Γ中的变量x相关联的值由Γ[x]表示。r [x e]表示具有r [x] =e的堆，即，我们使用这个符号或者作为堆Γ上的条件，或者作为对Γ的修改。在堆Γ中，逻辑变量x由形式为Γ[x] =x的循环绑定表示，即， x不是w.r.t.实例化的I. 值是一个以构造函数为根的项或逻辑变量（w.r.t.关联的堆）。阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔7⇓联系我们⇓（VarCons）Γ[x<$→t]：x<$Γ[x<$→t]：t 其中t是构造根的（VarExp）Γ[x <$→e]：e<$：vΓ[x<$→e]：x<$[x<$→v]：v其中e不是构造函数根的，并且e/=x（Val）r：v r：v其中v是构造根的或者一个变量，其中r [v]=v(Fun)Γ：ρ（e）π：vr：f（x n） 中文（简体）其中f（yn ）=e∈P且ρ={yn›→xn}(Let)Γ[yk<$→ρ（ek）]：ρ（e）：vr：let{xk=ek}ine∈v：v其中ρ=xkyk和yk是新变量(Or)r：ei：vΓ：e1或e2Γ：v其中i∈ {1，2}（选择）Γ：e：c（yn）：ρ（ei）θ：vΓ：（f）{pk→ek}θ：v的情况e其中pi=c（xn）且ρ={xn<$→yn}（猜测）Γ：e：x[x<$→ρ（pi），yn<$→yn]：ρ（ei）<$Θ：v{pk→ek}的情形e的Γ：f θ：v其中pi=c（xn），ρ={xn<$→yn}，yn是新鲜变量图1.一、函数逻辑程序的自然语义我们使用形式为“Γ：e：v“的判断，它应该被解释为“在堆Γ的上下文中，表达式e的值为v，而堆Γ（可能被修改）为v让我们简要解释一下我们的语义规则：（VarCons）. 为了计算一个绑定到堆中以构造函数为根的项的变量，我们只需将变量简化为该项。堆保持不变。（VarExp）。 这个规则达到了共享的效果。如果要评估的变量绑定到堆中的某个表达式，那么表达式将被评估，堆将使用计算值更新;最后，我们将此值作为结果返回。与[17]相反，我们没有从堆中删除变量的绑定;这对于轻松生成新的变量名很有用。[20]通过引入Launchbury关系的一个变体解决了这个问题我们的方法的唯一缺点是，黑洞（一个可检测的自依赖无限循环）在语义水平上无法检测到然而，这并没有违背自然语义，因为黑洞没有价值。阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔8›→（Val）。 对于一个值的计算，我们返回它而不修改堆。（Fun）. 此规则对应于函数调用的展开。结果是通过减少相应规则的右手边得到的。我们假设所考虑的程序P是微积分的全局参数（Let）. 为了减少let构造，我们将绑定添加到堆中，并继续计算let的主参数。请注意，为了避免变量名冲突，我们用新的名称重命名let构造引入的变量（或）。 此规则通过对第一个参数或第二个参数求值来非确定性地计算或表达式。（选择）。 这个规则对应于一个case表达式的求值，该表达式的参数减少为一个构造函数根项。在这种情况下，我们选择适当的分支，然后通过应用相应的匹配替换来继续计算该分支中的表达式。（猜测）。这条规则对应于一个可变的case表达式的求值，该表达式的参数可简化为一个逻辑变量。它非确定性地将这个变量绑定到其中一个模式，并继续计算相应的分支。为了避免变量名冲突，模式变量的重命名也是必要的此外，我们用模式的（重命名的）逻辑变量更新堆判断的证明对应于使用图1的规则的推导序列 给定一个规范化程序P和一个规范化表达式e（待评估），初始计算为m我们是一个YTTATA如果它计算了一个值，则派生成功计算的答案可以通过解引用的简单过程从Γ中提取，以便获得与初始表达式e中的逻辑变量相关联的值。如果我们试图构造一个证明，那么这可能会因为两种不同的情况而失败：可能没有有限的证明来证明一个归约是有效的--这对应于一个无限循环--或者可能没有适用于证明的一个（子部分）的规则在后一种情况下，我们有两种可能性：要么规则Select不适用，因为没有匹配的分支，要么规则Guess不能应用，因为一个逻辑变量已经作为刚性case表达式的参数获得图1的自然语义并不区分上述所有故障。然而，它们将在小步操作语义中变得可观察图2说明了语义描述的共享行为，其中一个可能的（非确定性的）派生程序和例3.3的表达式注意，最终配置中的堆，[x21]：BO，不包含初始表达式的变量x1的绑定(due到let表达式中局部变量的重命名这对应于计算出的答案是空替换的事实阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔9分校样⇓⇓Val[x2›→bit]：1 位[x2<$→bit]：1或[x2<$→bit]：0或1 游戏[x2›→bit]：1 Fun[x2<$→bit]：bit[x2<$→bit]：1VarExp[x2›→位]： x2 点击[x2›→ 1]： 1选择[x2<$→bit]：casex2of{0→0;1→casex2. . . {\displaystyle{\frac{x2}→1}}：BOFun[x2<$→bit]：addB（x2，x2）[x2<$→1]：BO Fun[x2<$→bit]：foo（x2）[ x2<$→ 1]：BOLet[]：letx1=bitinfoo（x1）<$[x2<$→1]：BO分证明文件的格式如下：[x2<$→1]：x2[x2<$→1]：1VarCons [x2<$→1]：BO[x2<$→1]：BOVal选择[x2<$→1]：{0→1;1→BO}的情况x2{x2<$→1]：BO图二. 例3.3下面的结果表明，我们的自然语义只计算值。引理3.4如果Γ：e ∈：v，则v以构造器符号为根，或者它是一个逻辑变量（即，[v] = v）。证据 这是自然语义的非递归规则（即，VarCons和Val）只能返回一个构造函数根项或逻辑变量w.r.t.相关的heap✷4一小步语义学从操作的角度来看，自然语义中的评估以自下而上的方式构建了“[ ]：e 0r：e 1“的证明为了将自然（大步）语义转换为小步语义，我们需要在大步语义中表示子证明的上下文例如，当应用规则VarExp时，构建前提的子证明上下文（即，规则）指示我们必须用表达式e的计算值v来更新x处的堆Ep。这个上下文必须在小步语义中显式表示与[20]类似，上下文是可扩展的（即，如果PJ是P的子证明，则P的上下文j是P）。因此，上下文的表示是由堆栈构成的。大步骤语义的配置现在，小步语义的状态（或目标）是三元组（Γ，e，S），其中Γ是当前堆，e是要评估的表达式（通常称为小步语义的控制），S是表示当前上下文的堆栈。目标表示域阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔10⇓›→⇒⇒{→}⇒堆×控制×堆栈。完整的小步语义如图3所示让我们简单描述一下过渡规则：• 规则varcons与自然语义中的规则VarCons完全相似。• 在规则varexp中，对绑定到表达式e（不是值）的变量x的求值通过对e求值并将对变量x的引用添加到堆栈来进行。这里，栈S是列表（空栈由[]表示）。 如果最终计算出一个值v，并且栈顶有一个变量x，则规则val用x v更新堆。在大步语义中，这种情况对应于规则VarExp的应用。• 规则fun、let和or与它们在自然语义中的对应物非常相似。• 规则case通过评估case参数并推送备选项（f）pkek来在堆栈的顶部。如果我们到达了一个以构造函数为根的项，那么使用规则选择来选择适当的分支，并继续对该分支进行求值。如果我们到达一个逻辑变量，则使用规则猜测来非确定性地选择一个替代方案并继续该分支的评估;此外，堆将使用逻辑变量与相应模式的绑定进行更新。为了计算表达式e，我们构造一个形式为（[]，e，[]）的初始目标，并应用图3的规则我们用=表示=的自反传递闭包。如果eJ是头范式（即，计算值），S是空栈。与大步语义类似，计算出的答案可以很容易地通过解引用初始目标的变量从Γ中提取。小步长语义和自然语义的等价性在下面的定理中陈述定理4.1（[ ]，e，[ ]）=（，v，[]）当且仅当[]：e ⇓：v.为了证明这个定理，我们首先需要一些辅助结果。我们的证明技术是[20]中证明方案的扩展下面的引理表明，我们的小步语义可以模拟自然语义的派生。引理4.2（完备性）如果Γ：e：v则（Γ，e，S）=（，v，S）。证据我们通过推导的结构上的归纳法证明了它：v. 我们区分以下情况：（VarCons）. 则有Γ[x<$→t]：x<$Γ[x<$→t]：t。简单地说，（Γ[x<$→t]，x，S） = n（r [x <$→t]，t，S）（通过varcons规则）（VarExp）。我们有Γ[x<$→e]：x<$$>[x<$→v]：v。那么，下面阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔11规则瓦尔孔斯堆Γ[x→t]=r [x<$→t]Γ[x<$→e]=r[x→e]Γ=r[x<$→v]Γ=100Γ=<$r [yk<$→ρ（ek）] r=100Γ=100Γ=100控制X堆叠S不XeValvSSx：Sx：S有趣vf（xn）ρ（e）设{xk=ek}在e ρ（e）中e1或e2ei（f）{pk→ek}e的情形ec（yn）ρ（ei）xSS让SS或SS情况选择猜Γ[x<$→x]=<$r [x<$→ρ（pi），yn<$→yn]ρ（ei）S（f）{pk→ek}：S（f）{pk→ek}：SSf{pk→ek}：S其中在varcons中：t是构造函数根的varexp： e不是构造函数根的，e/=xval：v是构造函数根变量或变量，其中Γ[v]=vfun：f（yn）=e∈P且ρ={yn<$→xn}设：ρ={xk<$→yk}且yk是新鲜的或：i∈{1，2}select：pi=c（xn）andρ={xn<$→yn}guess：i∈{1， . . k}，pi=c（xn），ρ={xn<$→yn}，和ndyn是新的图3。函数式逻辑程序阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔12{}{→ }推导成立：（Γ[x<$→e]，x，S）=（Γ[x<$→e]，e，x：S）（根据规则varexp）=（，v，x：S）（通过前提和归纳假设）=（n [x <$→v]，v，S） （by ruleval）（Val）. 我们有Γ：v<$Γ：v。在这种情况下，（Γ，v，S）= （r，v，S）（通过考虑空序列）（Fun）. 我们有Γ：f（xn）：v。然后，下面的推导成立：（Γ，f（xn），S）=<$（Γ，ρ（e），S）（通过规则fun，其中f（yn）=e∈P且ρ={yn<$→xn}）=（，v，S）（通过前提和归纳。（hyp.）（Let）. 我们有：让 xk= ekinek：v.现在，以下推导成立：（Γ，令{xk =ek}在e，S中）=<$（Γ[yk<$$> →ρ（ek）]，ρ（e），S）（通过规则let，其中ρ={xk<$→yk}）=（，v，S）（通过前提和归纳。（hyp.）此外，我们假设yk是规则Let中使用的相同的新变量，这总是可能的，因为两个推导可以在相应的步骤中使用相同的（或）。 我们有Γ：e1或e2：v。然后，下面的推导成立：（r，e1或e2，S）=<$（Γ，ei，S）（通过规则或，i∈ {1， 2}）=（，v，S）（通过前提和归纳。（hyp.）此外，我们假设ei是在规则Or的前提中选择的同一个参数。（选择）。 我们有r：（f）pkekΘ：v的情形e。然后，以下推导成立：（r，（f）{pk→ek}，S的情形e）=S（r，e，（f）{pk→ek}：S）（根据规则情况）（f）{pk→ek}：S）（通过左前提和归纳法. （hyp.）=（n，ρ（ei），S）（通过规则选择）=（Θ，v，S）（通过右前提和归纳。（hyp.）阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔13{→ }联系我们其中pi= c（xn），且ρ ={xn<$→ yn}。（猜测）。我们有pkekΘ：v的Γ：fcase e。然后，以下推导成立：（Γ，f{pk→ek}，S的情况e）=（Γ，e，f{pk→ek}：S）（按规则情况）=（，x，f{pk→ek}：S）（通过左前提和归纳. （hyp.）=（n [x<$→ρ（pi），yn<$→yn]，ρ（ei），S）（通过引理3.4和规则猜测）=（Θ，v，S）（通过右前提和ind.（hyp.）其中pi=c（xn），ρ=xnyn 和yn是在Guess规则中选择的相同的新变量。✷为了显示小步语义的可靠性，即，它计算的结果不多于自然（大步）语义，我们引入平衡计算的概念定义4.3（平衡计算）（r，e，S）=0 （，eJ，S）如果初始栈和最终栈相同，并且每个中间栈都扩展初始栈，则是平衡的。特别地，每个成功的计算（[]，e，[]）=（Γ，v， []）都是平衡的。定义4.4（迹，平衡迹）计算的迹是计算中使用的转移规则的序列。平衡轨迹是平衡计算的轨迹。有几种可能性可以平衡跟踪。显然，空的轨迹是平衡的。现在，考虑非空跟踪和任意初始堆栈S。非空的平衡跟踪必须以下列规则中的任何一个开始：varcons、varexp、fun、let、or和case。其余的规则不能产生非空的平衡跟踪，因为它们将产生不扩展初始堆栈S的中间堆栈。以varcons开头的跟踪只能包含这一个转换，因为它会产生一个中间堆栈S和一个表达式t，后者应该是一个构造函数根项。唯一可以应用的规则是val和select，但这两个规则都会从堆栈中删除与跟踪的平衡性相矛盾的元素。如果跟踪从varexp开始，产生一个x：S形式的中间堆栈，那么最终必须应用val规则，以便将初始堆栈恢复为S。在这种情况下，派生表达式是以构造函数为根的，因此只能应用规则val和select。然而，由于它们会从堆栈中删除一个元素，这与阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔14›→›→›→{→}计算;因此，跟踪必须具有（varexpbalval）的形式，其中bal代表任意平衡轨迹。以fun开头的跟踪只要fun之后的子跟踪平衡，就平衡。因此，它必须具有形式（funbal）。类似地，迹线（letbal）和（或bal）是平衡的。如果跟踪以case开头，则为 （f）pkek：S被产生。 初始堆栈必须通过应 用 规 则 选 择 或 猜 测 来 恢 复 。 这 样 的 平 衡 轨 迹 必 须 分 别 具 有（casebalselectbal）和（casebalguessbal）的形式总之，所有平衡的痕迹都可以从语法中导出，bal：：= bal|瓦尔孔斯|瓦勒克普巴尔瓦尔| 丰巴尔|让球|或巴尔|箱球选择球|案例球猜测球其中，R1表示空轨迹。每个平衡跟踪对应于大步语义中的一个规则下面的引理形式化了这个陈述的证明。引理4.5（可靠性）如果（Γ 0，e0，S）=（r1，v，S）是平衡的，则r 0：e0 r 1：v.证据证明是通过归纳法的结构平衡的痕迹遵循上述语法。（二）。那么e0必须是一个以构造函数为根的项或逻辑变量。因此，证明遵循应用规则Val。（varcons）. 则e0= x且Γ 0= Γ[x <$→t].因此，（r1，t，S）是导出状态，其中r1 = r [x t]。现在，通过应用VarCons规则进行证明。（varexpbalval）. 则e0=x和r0 = r [x e]（其中e不是构造函数根的，也不是逻辑变量）。应用规则varexp之后的状态必须是（r [x e]，e，x：S），应用规则val之前的状态必须具有（r，v，y：SJ）的形式。由于这些状态之间的轨迹是平衡的，我们有y=x，SJ=S，且Γ[x<$→e]：e∈v.的应 用 规 则 val 后 的 状 态 必 须 是 （ n [x<$→v] ， v ， S ） ， 其 中 Γ1 = n[x<$→v]。因此，使用规则VarExp，我们有Γ[x<$→e]：x∈[x<$→v]：v。（funbal）. 则e0=f（yn），其中f（xn）= e∈P，ρ ={xn<$→yn}.应用规则fun后的状态必须是（Γ0，ρ（e），S）。由于（Γ0，ρ（e），S）=<$$>（Γ1，v，S）是平衡的，所以通过归纳假设我们有Γ0：ρ（e）<$Γ1：v然后，通过应用规则Fun，我们获得了Γ 0：f（yn）<$Γ 1：v。（letbal）. 则e0=令{xk= ek}在e中，ρ ={xk<$→yk}和yk是新变量. 应用规则后的状态必须是e（Γ0[yk<$→ρ（ek）]，ρ（e），S ）. 由于（Γ0[yk<$→ρ（ek）]，ρ（e），S）=（Γ1，v，S）是一个平衡迹，通过归纳定理，我们得到Γ0[yk<$→ρ（ek）]：ρ（e）<$Γ1：v.Ap-阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔15⇓⇓⇓⇓›→›→ ›→⇓应用规则让这个判断具有相同的重命名ρ，我们得到了在e∈Γ1：v中的Γ0：let{xk=ek}。（或bal）。那么 e0= e1或 e2。应用规则或之后的状态必须是（Γ0，ei，S），其中i∈ {1， 2}。由于（Γ0，ei，S）=（Γ1，v，S）是平衡的，所以通过归纳假设我们有Γ0：eiΓ1：v然后，通过应用规则Or，r0：e1或e2r1：v（选择与规则Or应用中相同的参数）进行证明。（casebal选择bal）。 则e0=（f）{pk<$→ ek}的情形e。应用规则case之后的状态必须是（Γ 0，e，（f）{pk→ek}：S），应用规则select之前的状态必须具有形式（r，c（yn），（f）{pk→ ek}：S）。由于这些状态之间的迹是平衡的，我们通过归纳假设得到了Γ 0：e：c（yn）。现在，应用规则选择后的状态必须是（n，ρ（ei），S），其中pi= c（xn）且ρ ={xn<$→yn}。由于从（ε，ρ（ei），S）到（Γ 1，v，S）的迹也是平衡的，所以通过归纳假设我们有ε：ρ（ei）Γ 1：v。最后，通过应用规则Select，Γ 0：（f）{pk→ek}<$Γ 1：v的情形e.（casebalguessbal）. 则e0={pk<$→ek}的fcase e。应用规则情况之后的状态必须是（Γ0，e，f{pk→ek}：S），应用规则猜测之前的状态必须具有形式（Γ [x<$→x]，x，f{pk→ek}：S）。由于这些状态之间的迹是平衡的，我们有Γ 0：e[ x]x]：x通过归纳假设。现在，应用规则猜测后的状态必须是（n [x<$→ρ（pi），yn <$→yn]，ρ（ei），S），其中pi=c（xn）且ρ={xn<$→yn}，和yn是在规则猜测的应用中选择的相同的新变量。由于从（<$[x <$→ρ（pi），yn<$→ yn]，ρ（ei），S）到（Γ 1，v，S）的迹也是平衡的，所以通过归纳假设我们有<$[x ρ（pi），ynyn]，ρ（ei）Γ 1：v.最后，通过应用规则Guess，Γ 0：fcase e of{pk→ek}<$Γ 1：v来进行证明。✷现在，我们可以继续定理4.1的证明证据“如果”部分直接从引理4.2引出。“仅当”部分是引理4.5的推论，并且任何形式的计算（[ ]，e，[ ]）=（，v，[ ]）都是平衡的✷5相关工作在函数式编程领域，Launchbury [17]为纯粹的惰性函数式语言定义了第一它分为两个阶段：第一阶段是将λ演算静态转换为一种形式，在这种形式下，闭包的创建和共享是显式的;然后在闭包级别定义语义。我们的语义是以类似的方式定义的，尽管我们的语言是一阶的，它有逻辑变量和非决定论。再见，塞斯托夫特阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔16[20]从Launchbury的自然语义出发，开发了一个具有惰性求值的λ按需呼叫类似地，我们为函数逻辑程序定义了一个小步骤语义，与以前的自然语义共享我们的小步语义可以被看作是一个扩展的Sestoft的抽象机也考虑逻辑变量和非确定性。Samsom和Peyton Jones [19]从Sestoft的语义学开始，为一种能够测量时间和空间使用的编译的、非严格的、高阶的、纯函数式语言开发了第一个源代码级的profiler。 我们可以以类似的方式用成本信息扩展我们的操作语义，以便为惰性函数逻辑程序开发一个profiler。然而，为了这个目的，我们首先需要一个语义的确定性版本，它可以正确地对搜索策略进行建模。否则，我们只能计算搜索树中每个单一派生的成本，因为一些计算步骤可能由多个派生共享因此，定义小步语义的确定性版本变得至关重要（见[2]）。至于逻辑编程，[16]和[8]包含了Prolog的操作和指称描述，主要强调指定回溯策略和然而，懒惰和分享是不被掩盖的。这同样适用于Büorger[6，7]），它由不同语言结构的各种小步语义组成。至于函数逻辑编程，关于多范式语言Curry的报告仅非正式地涵盖了共享。函数逻辑语言Toy [18]的操作语义基于窄化（共享），但形式定义基于窄化演算[10]，其不考虑特定的模式匹配策略。然而，后者变得重要，例如，如果你想分析计算的成本[15]的方法，最接近我们的工作，包含一个懒惰缩小策略的操作语义，它考虑了共享，非确定性函数，并允许模式中的部分应用。然而，他们没有考虑灵活和严格的情况表达式之间的区别，这对于定义结合窄化和剩余的运算语义是必要的此外，我们提出了我们的操作语义的两个特征：自然风格的高层次描述和更详细的小步语义，并正式证明了它们的等价性。最后，[9，11]通过用某种形式的统一扩展图重写来呈现图缩小关系。图缩小需要一个复杂的机器来表示和操作图。然而，为了建模共享的目的，我们的方法基于let绑定的使用是足够的。阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔176结论和今后的工作提出了一种基于共享和非确定性的惰性求值的函数逻辑语言的操作语义我们分几步开发语义学。首先，我们将程序转换为规范化的形式，以使模式匹配策略，公共子表达式等显式。然后，我们为这些规范化的程序定义了一个自然的语义，包括懒惰，共享和非确定性。最后给出了相应的小步语义，并证明了它与自然语义的等价性据我们所知，这是第一次尝试一个严格的操作描述的功能逻辑语言，包括灵活和严格的情况下表示，基于懒惰的评估与共享和非确定性。我们的最终语义是定义具体函数逻辑语言的适当基础然而，为了获得像Curry这样的实用语言的完整操作描述，必须添加对建模搜索策略和并发性、求解方程约束、评估外部函数和高阶应用的描述。这些扩展与其他操作方面（共享，非确定性）正交，并且它们是正在进行的研究的主题（参见[2]）。事实上，我们正在努力实现Curry的解释器-基于这样一个扩展的操作配置-涵盖所有上述功能[2]。可以使用完整的操作描述，例如，作为定义[1，3，19，21]风格的成本增强语义的基础，开发调试和优化工具（如部分评估器），并检查或导出Curry的新实现（如[20]）。引用[1] E. Albert，S. Antoy和G.维达尔函数逻辑语言中部分求值的有效性度量。在第10届Springer LNCS 2042，2001年。[2] E. Albert，M. Hanus，F. Huch，J.Oliver，and G.维达尔惰性函数逻辑程序的操作语义。在Proc. of Workshop on Reduction Strategies in Rewriting andProgramming（WRS[3] E. Albert和G.维达尔多范式声明性语言的符号轮廓。在Proc. ofSpringerLNCS 2372，2002年。[4] S.安托伊基于构造函数的条件缩窄。在Proc. of the 3rd International ACMSIGPLAN Conference on Principles and Practice of Declarative Programming（PPDP 2001），pages 199-206. ACM Press，2001.阿尔伯特，哈纳斯，胡奇，奥利弗，维达尔18[5] S. Antoy 和 M. 哈 纳 斯 将 多 范 式 声 明 式 程 序 编 译 成 Prolog 。 在 Proc. oftheSpringer LNCS 1794，2000。[6] E. 博格。Full Prolog的逻辑操作语义。 第一部分：选择核心和控制。第三届计算机科学逻辑国际研讨会论文集Springer LNCS 440，1990年。[7] E. 博格。 全Prolog的逻辑操作语义。第II部分：用于数据库操作的内置谓词。计算机科学的数学基础（MFCSSpringer LNCS 452，1990年。[8] S.K. 德 布 雷 和 P. 米 什 拉 。 Prolog 的 指 称 和 操 作 语 义 。 Journal of LogicProgramming（5），pages 61[9] R. Echahed和J.Janodet。可容许的图重写和缩窄。在1998年逻辑编程联合国际会议和研讨会（JICSLP'98）的论文集MIT Press，1998.[10] J.C. G