声明式多范式语言的操作语义模型及搜索策略明确确定和扩展实现 - 深入分析与应用

62网址：http://www.elsevier.nl/locate/entcs/volume70.html22页一种声明式多范式语言的操作语义？埃尔韦拉·阿尔伯特1迈克尔·哈努斯2弗兰克·胡赫2哈维尔·奥利弗3德国人维达尔31DSIP，UCM，Avda.Computense s/n，E-28040 Madrid，Spainelvira@fdi.ucm.es2 Institut furInformatik，CAUKiel，Olshausenstr. 40，D-24098Kiel，Germanyfmh，fhuinformatik.uni-kiel.de3DSIC，UPV，Camino de Vera s/n，E-46022Valencia，Spainffjoliver，gvidaldsic.upv.es摘要实用的声明式多范式语言结合了函数、逻辑和并发编程的主要特征（例如，懒惰、共享、高阶、逻辑变量、非确定性、搜索策略）。通常，这些语言还包括外部函数和约束求解器的接口在这项工作中，我们介绍了第一次正式描述的操作语义现实的多范式语言，涵盖了所有上述功能，在一个精确的和可理解的方式。我们还提供了一个确定性版本的操作语义模型的搜索策略明确。这种确定性的语义成为必不可少的开发语言特定的工具，如程序跟踪器，prolers，优化器等。最后，我们扩展了确定性的语义，以模拟并发计算。已经实施了完整的操作语义。1介绍现代声明式多范式语言结合了函数式、逻辑和并发编程的最佳特性。为这些语言定义精确的操作语义并不是一件容易的事情，因为必须涵盖共享、逻辑变量、非确定性、搜索策略、并发等概念，以及它们之间的相互作用最近，一位...？ 这项工作得到了CICYT TIC 2001-2705-C 03 -01，MCYT在资助HA 2001 -0059、HU 2001 -0019和HI 2000 -0161下，以及DFG在资助Ha 2457/1-2下的部分支持。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。63对惰性函数逻辑语言的一个重要描述[2]。这项工作定义了一个严格的操作描述的功能逻辑语言的基础上懒惰的评估与共享和非确定性。 进一步给出了操作语义的两个刻画：自然风格的高层描述和更详细的小步语义。文中还证明了这两种刻画的等价性然而，为了获得实用语言（如Curry [14]或Toy [18]）的完整操作语义，必须添加用于建模搜索策略和并发性的描述，用于求解等式约束，评估外部函数和高阶特征。这些扩展与其他操作方面（共享，非确定性）正交，尚未正式描述。 本文的目的是提供一个操作描述声明性多范式语言涵盖所有上述功能，在一个精确和可理解的方式。本工作的出发点是[2]的（非确定性的）\“小步”操作语义。首先，我们提出了这种语义的扩展，以便覆盖诸如整数和浮点数、外部函数（例如，算术运算符）、预定义约束（union）和高阶函数。然后，我们提供了一个确定性版本的小步语义，使搜索策略明确。这种决定性的描述构成了推理程序的面向实现的方面的正式基础，例如，开发适当的跟踪、分析和调试工具。例如，可以对该语义进行仪器化，以便计算与特定计算相关联的成本（时间/空间）（类似于，例如，[1，4，21，24]）。这对于正式量化具体程序优化所实现的改进以及比较不同的搜索策略是有用的注意，通过考虑非确定性语义，这种方法将是不可能的，因为它不能正确地描述与特定搜索策略相关联的计算路径。最后，我们考虑使用线程来建模并发计算，并相应地扩展以前的语义。因此，我们获得了一个完整的确定性语义，支持多线程与通信的逻辑变量。据我们所知，这项工作是第一次尝试正式去-一个像Curry这样的现实多范式语言的完整操作语义这种语义的实施已经进行。它可以用于测试语言扩展、检查程序优化或通过设计插装版本来派生编程工具。本文的组织结构如下。在下一节中，我们简要描述所考虑的语言。第3节回顾了[2]的小步语义。这在第4节中进行了扩展，以涵盖声明式多范式语言的其他特性。第5节介绍了语义的确定性版本，第6节添加了并发性，以便nal语义涵盖所有重要功能。在第7节中，我们描述了我们的语义的实现，并在第8节中与相关工作进行了比较642语言正如我们已经提到的，这项工作的主要动机是为开发编程工具（如prolers，tracers，optimizers等）提供基础。声明性多范式语言的。为了具体起见，我们将Curry [12，14]作为我们的源语言。Curry是一种现代多范式语言，它以无缝的方式融合了函数式、逻辑和并发编程中最重要的特性。基本上，一个Curry程序是一组函数定义（和数据定义，为了打字，我们在这里忽略 每个函数都由形式为\ft1： tn规则定义 其中f是一个函数，t1; ：;tn 是数据（或构造器）项（即， 没有出现指定的函数），左手边ft1： tn 是线性的（即， 没有变量的多次出现），并且e是well-formedexpression。1 例如，从构造函数0、1和BO（binary over ow）构建的二进制数的加法可以通过以下规则来定义：addB 0 y =yaddB 1 0 = 1addB 1 1 = BO(data构造函数通常以大写字母开头，函数应用用并置表示如果规则的左侧与当前应用程序匹配，则该规则适用 函数是惰性求值的，因此Curry的操作语义是惰性函数式编程的保守扩展。为了提供一个可理解的操作描述，我们假设程序被翻译成一个“at”的形式，这是一个方便的标准表示的功能逻辑程序。at形式通过使用case表达式使模式匹配策略显式化，这对于操作描述很重要;此外，Curry程序可以自动转换为这种at形式[13]。中程序的语法表1中总结我们用P来表示一个程序，D是一个函数，定义，p表示模式，e2表示任意表达式.程序P由一系列函数定义D组成，使得左边有两两不同的变量参数。 右侧是由来自Var =f x;y; z;：g的变量组成的表达式e，数据构造器（例如，a，b，c，.）、功能符号（例如，f，g，h，.）、格表达式、析取（例如，表示非确定性或集值函数），并让绑定，其中本地变量x1; ：;xn 仅在e1中可见; ： ：;en;e。的情况1 虽然Curry允许有条件的规则，但为了简单起见，我们只考虑无条件规则。这不是一个真正的限制，因为条件规则可以通过引入辅助函数转换为无条件规则，参见[5]。65Xn我K1nP：：=D1： DmD：：=f（x1; ：;xn）=ee：：= x（变量）jc（e1; ：;en）（构造函数应用程序）J f（e1; ：;en）（函数应用）J fp1的case e！ e1;：;pn！恩（刚性情况）J f p 1的fcasee！ e1;：;pn！恩（灵活的情况下）J e1 或E2（disjunction）jletx1=e1; ： ： ：;xn=enine（letbinding）p：：=c（x1; ： ： ：;xn）Fig. 1. 程序的平面表示表达式具有以下形式：2（f）fc1（xn1）的情况e！e1;：;ck（xn ）！ekg其中e是一个表达式，c1; ：;ck 是直接构造函数，而e1; ： ： ：;ek是表达。模式变量是本地引入和绑定的子表达式ei的相应变量。 case和fcase之间的区别在参数e是自由变量时表现出来：case是待定的，而fcase非确定性地将该变量绑定到case表达式的分支中的模式，并继续进行适当的分支。作为一个例子，我们展示了函数\addB“到at形式的转换：addB（x;y）=f0的情况x！y; 1！f 0的情况y！1; 1！ BOGG原则上，翻译Curry程序不需要Let绑定，它们便于表达子项的共享而不使用复杂的图结构（例如，[8，11]）。在操作上，让绑定在内存中引入新的结构，这些结构在计算后更新，这在惰性计算和非确定性函数中是必不可少的我们还假设所有额外的变量（即，在函数的右手侧中的变量，其不出现在左手侧中）通过直接循环let绑定被显式地引入AT程序中例如，如果右侧e包含一个额外的变量x，则表示为let x=x in e。在本文中，我们称这些变量为逻辑变量。我们对逻辑变量的表示并不排除使用其他循环数据结构，如letx=1：xin：Curry还包括一些实用功能，将在本节的其余部分进行描述。特别是，库里扩展了最佳的2 我们写对于对象序列o ;：;o及（f）case为fcase或case。on66[6]的评价策略的并发编程功能。这些由&约束条件上的 并发合 取运算符支持（即， 例如内置类型Success）。例如，形式为\c1通过&同时求解两个约束C1和C2来估计C2“。埃尔-其他约束是成功，它总是满足的，以及等式约束e1=：=e2两个表情之间的区别。如果两个表达式都可约简为相同的基构造函数项（即，我们认为所谓的严格平等[9，19]）。在操作上，等式约束e1=：=e2 通过评估e1来求解 和e2 到uniableconstructorterms.Curry中的高阶特性包括部分函数应用和lambda抽象。在我们的（一阶）at表示中，高阶函数被转换为辅助函数apply的应用[25]。这个特殊的函数可以很容易地用普通的程序规则来定义（见4.3节的讨论）。但是，不允许对包含自由变量作为函数的高阶应用进行求值（即，这些应用被暂停以避免使用更高阶的union [13]）。此外，Curry还允许使用用户程序中未定义的函数（外部函数），如算术运算符，基本输入/输出设施等。让我们用一个例子来说明上面的一些特征考虑下面的规则，定义一个函数来连接两个列表（其中[]表示空列表，z：zs表示具有第一个元素z和尾部zs的列表）：conc（xs; ys）= f []的case xs！ys;（z：zs）！z：浓度（zs; ys）g现在，等式约束\conc（p，s）=：=[1，2，3]“通过将变量p和s实例化到列表中来解决，使得它们的连接产生列表[1，2，3]。因此，我们可以定义一个约束，如果p是列表xs的前x，则该约束满足如下：前缀（p，xs）=让s=sin conc（p，s）=：=xs为了示出高阶编程的示例，我们定义了高阶约束satisfyAll，其将一元约束c和列表xs作为输入;如果xs的所有元素满足约束c，则满足：satisfyAll（c，zs）= f []的case zs ！成功;（x：xs）！apply（c，x）&matifyAll（c，xs）g这里我们用apply来表示函数的应用。现在，我们可以将这个定义与前面的前缀定义结合起来，以计算一个字符串列表的公共前缀x（字符串被认为是字符列表commonPrefix （ p ， xs ）=matisfyAll （ prefix（p），xs）67k k kk1 2 121k k kkn1n例如，约束commonPrefix（p，[“abc”，“abda”，“abab”]）是变量p的实例化“”、“a”或“ab”。3小步操作语义在本节中，我们回顾了[2]中提出的惰性函数逻辑程序这种语义涵盖了懒惰、共享和非决定论等概念它分为两个独立的阶段进行描述。在第一阶段，应用规范化过程以确保函数和构造函数的参数始终是变量。这些变量将被解释为表达共享的参考，并且不需要成对不同。定义3.1表达式e的规范化通过映射e涉及函数（或构造器）应用程序的所有参数，映射e归纳定义如下：x=x'（x; ：; x） ='（x; ：; x）'（x; ：; x;e;e;：;e）= letx=e in'（x; ：; x;x;e;：;e ）的方式1i 1i i+1nii1I1i i+1n其中e i不是变量，x i是新鲜的（令fx=e g in e）= letfx=e g in e（e）或（e） = e或e（（f）f p的情况e！eg）=（f）fp 7的情况e！eg这里，'表示构造函数或函数符号。将这个规范化过程扩展到程序是很简单的。规范化为函数（或构造函数）应用程序的每个非变量参数引入了一个新的let构造显然，这可以修改，以便为所有不可变参数生成一个具有绑定的let对于小步语义的定义，假设要评估的程序和表达式都已预先规范化。状态转换语义可以在图2中找到。规则遵循以下命名约定：2He ap =Var！Expv2Vvalue：：=xjc（en）堆是从变量到表达式的部分映射。 空堆 表示为[]。 与堆中变量x关联的值表示为[x]。【X7！e]表示具有[x] =e的堆，即，我们将使用这个符号作为堆上的一个条件或作为的一个修改。 逻辑变量68统治varconsVareXPVal有趣让或情况选择猜堆控制堆栈【X7！t]xS=）[x7！t]tS【X7！ e]xS=）[x7！e]ex：Sv x：S=）[x7！v]vSf（xn）S（e）S设fxk=ek gin e S=）[yk7！（ek）]e1或e2S=）eiS（f）f p k的情况e！ e kgS=）e（f）fpk！ekg：Sc（y n）（f）f p k！ ekg：S=）（ei）【X7！ x]xffpk！ekg：S=）[x7！ （pi）;yn7！[yn]（ei）S其中在varcons中：t是构造函数根的varexp：e不是构造函数根的，e6=xval：v是构造函数根的或者是一个变量，[v]= vfun：f（y n）= e 2 P and =f y n7！xng让：=f x k7！ykg和或：i2 f1; 2g是新鲜选择：p i= c（x n）和=f x n7！银银i= c（x n）;=f x n7！yng，以及是新鲜图二. 函数式逻辑程序ykyn69x表示在堆中 通过形式[x] =x的循环绑定，即，x不是w.r.t.实例化的。. 值是一个以构造函数为根的项或逻辑变量（w.r.t.关联的堆）。小步长语义定义在（; e; S）形式的状态（或目标）上，其中是当前堆，e是要计算的表达式（通常称为小步长语义的控制），S是表示当前上下文的堆栈对于堆栈S2Stack，我们使用与列表相同的符号Goal表示域堆控制堆栈。让我们简单描述一下小步语义的转换规则varcons：此规则用于评估绑定（在堆中）到构造函数根项的变量。在这种情况下，它只是返回这个术语。varexp：它用于计算绑定到表达式e的变量x（既不是构造函数根变量，也不是逻辑变量）。它首先计算e，然后将对变量x的引用添加到堆栈中。val：当在堆栈顶部发现变量x时，此规则使用绑定x7更新一旦计算出值vfun：它执行函数应用程序的展开。这里，程序P是微积分的全局参数。let：这个规则用于减少let构造，方法是将关联的（重新命名的）绑定添加到堆中，并继续计算let的主参数。or：它用于通过计算第一个参数或第二个参数来非确定性地计算orcase：此规则通过评估case表达式并推送alternati ves（f）fpk来启动case表达式的评估！ 例如，在stack上。select：如果我们到达一个以构造函数为根的项，那么这个规则用于选择case表达式的适当分支，并继续对这个分支进行求值。guess：如果我们到达一个逻辑变量，那么这个规则用于非确定性地选择一个替代方案，并继续对所选分支进行评估。为了避免变量名冲突，模式变量的重命名也是必要的。此外，堆会使用模式的（重命名的）逻辑变量进行更新。为了计算表达式e，我们构造一个形式为（[];e;[]）的初始目标，并应用图2 的 规 则 。 Wedenoteby=）的 环 的 exi vee 和 transiti vee 闭 包 。Aderivation（[];e;[]）=） （;e0;S）是成功的，如果e0 是头部正常形式（计算值），S是电磁场。计算的答案可以从通过解引用初始目标e的变量。例3.2考虑由函数\addB“组成的程序，定义如下：70有趣或有趣有趣情况Val选择情况瓦尔孔斯选择（[ ];letx1=bitinfoo（x1）;[]）让=）（[x27！int[] ;foo（int[ ]）=）（[x27！bits];addB（x2;x2）;[]）=）（[x27！ bit];casex2off0！ x2;1！ casesx2off0！1;1！BOgg;[]）=）（[x27！ bit];x2;[f0！ x2;1！ casesx2off0！1;1！BOgg]）varexp=）（[x27！ 位];位;[x2;f0！ x2;1！ casesx2off0！ 1;1！BOgg]）=）（[x27！ 位];0或1;[x2;f0！ x2;1！ casesx2off0！1;1！BOgg]）=）（[x27！ 位];1;[x2;f0！ x2;1！ casesx2off0！ 1;1！BOgg]）=）（[x27！ 1];1;[f0！ x2;1！ casesx2off0！ 1;1！BOgg]）=）（[x27！ 1];casex2off0！ 1;1！BOg;[]）=）（[x27！ 1];x2;[f0！ 1;1！BOg]）=）（[x27！ 1];1;[f0！ 1;1！BOg]）=）（[x27！1];BO;[]）图三. 第2节中的\letx1=bitinfoo（x1）”的求值，以及以下函数：foo（ x）= addB（ x; x）bit=0或 1图3详细描述了在上述程序的一个可能的（非确定性的）推导中执行的 计 算 步 骤 ， 以 及 目 标 \foo （ bit ） “ （ 以 规 范 化 的 形 式 写 为\letx1=bitinfoo（x1）”在每一步中，我们指出已经应用的转换规则。这个例子是从[2]中借来的，它被用来说明一个大步语义的共享行为。类似地，我们也可以在小步长语义中观察到共享的效果，其中共享子项“bit“仅被评估一次。 注意，nal目标中的堆，[x27！1]，does不包含初始表达式的变量x1这对应于计算出的答案是空替换的事实。4语言扩展到目前为止，我们描述了函数逻辑语言内核的操作语义在本节中，我们扩展了小步长操作语义，以涵盖整数和浮点数、外部函数、预定义约束（union）和高阶函数等扩展。714.1平等逻辑语言的一个重要特征是它们以高效的方式执行约束求解的能力对于项之间的等式约束，这是通过union来实现的，其中变量之间的等式通过绑定这些变量来求解（而不是将它们实例化为所有可能的值）。类似地，函数逻辑语言在包含定义函数的表达式之间提供等式约束由于这样的函数可以表示无穷项，因此等式约束被解释为严格等式[9，19]：如果两个构造函数e1和e2可以被简化为可统一的构造函数项（即，没有出现指定函数的表达式通常，这是通过递归计算头范式的参数，然后将两个参数与逻辑变量的可能实例化进行比较来实现的为了提供上述操作行为的通用定义，我们需要一种方法来评估任意表达式的头范式。 在图1所示的基本语言中，强制表达式求值为head范式的唯一方法是使用case表达式。这导致了大集合的困难（或者甚至是像数字这样的构造函数的集合，见下）。因此，我们引入了一个新的预测函数hnf（e1;e2），第一次评估的结果1 在返回e2之前， 作为结果. 为了在我们的小步长操作语义中正式地描述这种行为，我们首先对当前表达式e1进行了评估 并在STA上推送包含E2的HNF文本。当第一个元素是头部范式时，此元素将从堆栈中弹出。因此，hnf的操作语义由以下规则正式定义：规则堆控制堆栈hnf1=）的文件hnf（x1;x2）X1Shnf（x2）：Shnf2vhnf（x）：S=）xS其中v是构造函数根项或变量y，其中[y] =y。通过使用函数hnf，可以将任意表达式求值为头范式。这个事实在下面的严格相等的定义中得到了利用（注意，这个定义需要像任何其他程序规则一样规范化）：x1=：=x2 =hn f（x1;hnf（x2;hnconstrE q（x1;x2）这个定义确保了x1 和x2 被简化为头部正常形式，即，一个以构造函数为根的项或逻辑变量。原始函数Eq递归地下降其两个参数，并重新启动小-72Xnyn12N3N4nn规则堆控制堆叠Eq1=）[x0Eq（ x; y）S成功SEq2Eq（ x; y）S=）[x7！c（x）;0n n七！x]n（x=：=y&>：&> x11n =：=y）nSEq3Eq（ x; y）S=）[y7！ c（y）;y7！y]0n n n（x=：=y&>：&> x11n =：=y）nSEq4=）Eq（ x; y）（x1=：=y1&>：&>xn=：=yn）SS通过将新的表达式放入控件中，为子表达式添加步骤操作语义在成功union的情况下，它会产生一个修改的堆和结果Success（一个表示成功解决约束的内部构造函数）。由于不一致性，对微分方程行为的精确定义引起了新的复杂性由于逻辑变量并不总是实例化为构造函数根项（如在规则猜测中），但也可以绑定到其他逻辑变量，因此在堆中可能会出现绑定链例如，如果我们将变量x统一为y，然后将y统一为常数0，那么x并不直接绑定到0，我们有一个堆，其中[x] =y，[y] = 0。这个属性要求在我们访问堆变量之前取消对它们的引用我们用一个定义如下的函数来表示：（x）=（y）if [x] =yandx6=y：[x]否则注意，（x）=y意味着y是逻辑变量（即， [y] =y）。 在下面的规则中，我们将只应用于已经被求值为头范式的变量x（x）总是一个值。现在，我们可以定义Eq的小步语义如下：其中，在等式中：（x）=x0 且（y）=y0Eq ：（ x） =x0;（ y ） =c（ y） ;和 Eq ：（x）=c（x）;（y）=y0;和Eq：（x）=c（x）和（y）=c（y）新鲜新鲜在上面的规则中，等式约束是通过表达式的交错惰性计算和变量的绑定以增量方式解决的。73Xn12n21nn规则堆控制堆叠布尔方程1=）BubbleEq（ x; y）（x1==y1 ：xn ==yn）boolEq（x; y）SS布尔方程2=）S假S建造师术语特别地，当等式约束的两个参数x和y在堆中绑定到逻辑变量时， 和y0，规则返回Success并通过绑定x0更新堆的日期 你0。在规则Eq中，变量x与逻辑变量x0 但是变量y被绑定到构造器应用c（y）。在这种情况下，我们绑定x 到构造函数应用程序的形式c（xn），其中是新鲜的变量名称，并检查构造函数参数的约束相等性。由于必须递归比较的参数的数量取决于构造函数c的arity，我们在控件上放置一个包含顺序合取运算符\&>“的新表达式（以规范化形式）在这里，我们认为一个空合取（n = 0）等价于成功。约束上的运算符\&>“定义如下：x1&>x2 =casesx1 F成功！x2g规则10.Eq3以类似的方式进行最后，如果两个参数x和y都绑定到同一个构造函数应用程序，则规则Eq4继续比较构造函数参数（不修改堆）。为了简单起见，我们省略了规则Eq2和Eq3中的发生检查。例如，在规则Eq2中，发生检查必须确保变量x0 d不符合yy表示的值（如果x0 而y是不同的）。这里，y表示的值是y递归引用的表达式的一部分（根据当前堆），不考虑函数应用（更多细节见[14，附录D.4]）。我们也可以定义布尔测试相等函数\==“，以类似的方式测试两个表达式的严格相等与\=：=“相反，函数\==“仅定义在基础构造函数项上（即，它在存在逻辑变量时挂起）并返回True（相应地，如果两个条件相同，则为False。Dierent）。函数\==“可以定义如下：x1==x2 =hnf（x1;hnf（x2;xboolEq（x1;x2）其中，xboolEq递归地检查其两个参数是否相等：在boolEq中：（x）=c（x），（y）=c（y）布尔方程：（x）=c（：）; （y）=d（：），且c6= d在规则布尔公式1中 操作者&& 表示布尔合取，741212一定义如下：x1x2 =casesx1 F是真的！ x2;False！此外，我们认为空合取（n = 0）等价于真。4.2外部函数每一种实际的编程语言都必须支持许多在同一种编程语言中无法实现的函数。例如，让我们从概念上讲，整数或浮点数的集合可以被解释为常数的集合（0元构造函数）。在下文中，我们将这些常量称为文字。文字可以出现在程序中的任何地方，包括case表达式的模式例如，我们还可以解释用整数计算的算术函数（例如，整数上的加法），如由程序规则的一个集合所定义的。由于case表达式只有nite数量的分支，我们不能在我们的内核语言中表示这样的nite集。这就需要对语言进行扩展，以便包括外部定义的功能，即，程序规则没有明确定义的函数。这些函数称为外部函数。在一种简单的方法中，可以尝试扩展我们的操作语义，以使用以下通用规则来覆盖外部函数：h;F （ en） ;Si=）的文件h;FA（en）;S我其中每个预定义函数F的语义通过解释FA来表示。然而，一般来说，这是不够的，因为F的参数是表达式，需要在我们用FA解释它们之前将它们评估为文字。因此，我们必须确保这些表达式在应用函数FA类似于等式约束，我们使用原始hnf来解决这个问题。例如，我们通过使用外部函数+来定义两个整数的加法，x1+x2 =hnf（x1; hnf（x2; n+（x1; x2））由于原始函数+总是应用于已经被评估为文字（或逻辑变量，见下文）的参数，我们将其小步语义定义如下：规则+堆控制堆栈+（x; y）S=）l1+Al2S哪里（x）=l，（y）=l，l;l是字面量，+表示算术和。注意，这个定义意味着，如果其中一个变量是逻辑变量，则对+的求值将挂起（=中没有后继变量）。75对于像Curry这样的语言的其余基本功能的规则的定义可以很容易地以类似的方式完成4.3高阶特征根据图1的语法，at程序被限制为第一阶。原则上，这是足够的，因为它是众所周知的（例如，[25])典型函数（逻辑）语言的高阶特征可以被翻译成一个特殊函数apply的应用，该函数apply可以由一组一阶规则例如，像\（f a）b“这样的表达式可以被翻译成intoapply（apply（f; a）; b）其中apply的定义包含二元函数f的以下规则：apply （ f;x ） =f（x ） apply （f（ x）; y）=f（ x;y）为了避免为程序的所有函数生成这些规则我们提供了一个基于原始函数apply的apply定义，它假设rst参数是head范式;注意，只有apply的rst参数必须被评估为head范式。因此，我们必须遵守以下规则：apply （ x1;x2 ） =hnf （ x1;hnapply（x1;x2））小步长语义然后扩展如下：规则应用堆控制堆栈push（x; y）S=）'（xk;y）S其中（x）='（xk）并且'是构造函数sy mbo l或'（yn）=e2P，其中kSUSP，如果e=x; S=fpSUCC，如果e=v且S= []一个小步操作语义（包括搜索），它计算第一片叶子在枯萎的树上w.r.t. 一个sear ch函数\n\n可以被定义为最小关系！目标目标满足（评价）g=）GgG0 ！GG0其中g2目标和G; G2的进球评估从初始目标g0开始=（[];e0;[]）其中e0是要计算的表达式。关系！是确定性的，它可以达到四种nal状态：溶液在这种情况下，序列中的第一个目标具有（; v;[]）的形式，其中v是计算值。此外，通过解引用初始表达式e 0的变量，可以提取计算出的答案。悬浮液然后，序列中的第一个目标的表达式应该是在参数位置具有逻辑变量的严格情况表达式，或者是应用于某些逻辑变量的原始函数。注意，在后一种情况下，并非所有的原语函数都在逻辑变量上挂起，例如，在这种情况下，Eq执行union这种情况代表一个暂停的目标，将在下一节中更详细地讨论失败这里，序列的第一个目标应该是参数不匹配任何模式的case表达式，或者是不成功的原始函数的应用，例如，Eq应用于具有不同最外层构造函数的值。没有更多的目标：这种情况发生在序列中的所有目标都已经被探索过的时候。为了区分不同的可能性，我们给关系！它对搜索树的叶子进行分类。标签是通过以下函数类型计算的。 对于不是原始函数应用的表达式e（即，e6=f（xn）），定义如下：Kg：S0;且[x]=x！eKtype（; e; S）=FAILife=c（yn ）;S=（f）fpk！杨永g：S0;且8i= 1;：; k：pi 6=c（：）>：>COMP否则对于原始函数，它是通过使用表示其行为的函数primType来type（;f（xn）;S）=Type（;f（xn）;S）函数primType表示任何原始函数的行为。特别地，对于某些G，证明了ω Ty pe（;ωf（xn）;S）=COMPi（;ωf（xn）;S）=）G。例如，对于外部函数+，它被定义为0780KKprimType（; x+（x; y）; S）=k knCOMP如下所示：SUSP如果（x）=z或（y）= zCOMP否则其中z是逻辑变量。类似的定义可以提供给其余的原始函数。特别是，对于约束相等，挂起不是可能的行为。此外，约束相等在应用于不同的构造函数时可能会失败：primType（;n= 0）失败如果（x）= c（y=COMP否则）的情况下;（y）= d（z），且c6=d通过使用函数类型，我们现在可以定义 表达式如下：g=）G（评价）GG0 ！GG0G（弃用）gG0=6）类型（g）！的g0（g2目标和G;G0 2G oal）规则Discard的（可判定）条件g=6）意味着没有规则for=）match. 在这种情况下，！do不执行COMP步骤，如以下引理所述：3引理5.1如果g！ gG0 且g=6），则类型e（g）证明。关于g=（; e; S）的案例分析：e是一个值。 我们区分两种情况：(i) e=c（xn）：如果S=x：S0，则val是适用的，并且g=）G。COMP.如果S=（f）fp！ 例如：S0，则e=c（y）或e=x，其中[x]=x。在第一种情况下，rule select是适用的或者type（g）= FAIL;在第二种情况下，我们可以应用rule guess或者type（g）= SUSP。如果S= [ ]，则没有规则适用，并且type（g）= SUCC。(ii) e=x：如果S6 =[]且S6 =fp！ 例如：S0，则规则v arcons、v arexp或guess都是适用的，type（g）= SUCC，或type（g）= FAIL。e=f（x n）。函数primType在=）产生后继的情况下产生COMP类型。e是任何其他表达式。然后，对于所有可能的表达式，存在独立于和S适用的规则。2nM793 我们写作！的自反和传递闭包的集合。包括所有标签。80SUCC0（评价）（;e;S）=）（1;e1;S1）：（n;en;Sn）COMP（;T（e;S））：G（叉）！（1; T（e1;S1）） ：（n; T（en;Sn））GCOMP（成功1）（; T（e1e2;S））：Gtype（; e; S）=SUCCCOMP！（; T（e1;S）（e2;S））→G（成功2）（;T（e;S））：G！（;T）βG（;;）：G！G（未通过）type（; e; S）=未通过失败（僵局）8（e; S）2T：类型（; e;S）=SUSPSUSP（;T（e; S））：G！G（;T）：G！ G图五. 多范式程序关系！ 包含计算的所有信息。人们可以很容易地从（可能在夜间）推导中提取感兴趣的部分例如，所有解的集合可以用以下方式定义溶液（g）= fgjg！GgSUCC！Gg：6添加并发性像Curry这样的现代声明式多范式语言支持并发性，这使得在共享逻辑变量上进行通信的多线程成为可能。最简单的并发语义是交织，它通常定义在小步操作语义的级别上。 的定义并发的自然语义将更加复杂，因为交织的附加的无关非确定性。在本节中，我们将展示我们的确定性语义！可以自然地扩展到对并发进行建模。为了简单起见，我们通过要求初始表达式总是约束来限制所考虑的并发程序main是成功的类型）。对于并发的形式化（参见图5），我们将目标中的表达式和堆栈扩展为表达式和堆栈的集合，即，目标=堆P （对照Stack）。 P的每个元素（对照堆栈）表示一个线程，这些线程可以非确定性地执行操作（这是交织语义的思想）。作为不交并T]f（e; S）g的缩写，我们写T（e;S）。通过将新线程添加到集合（Fork），使用并发合取运算符\“创建新线程。堆是目标中所有线程的全局实体。因此，线程通过这个全局堆中081的变量绑定相互在我们的并发操作语义中，以下可能性为dis-