回溯计算的新模型：易于表示回溯，具有模块化属性和紧凑的实现状态

理论计算机科学电子笔记128（2005）39-59www.elsevier.com/locate/entcs回溯计算的概念MarijaKulas1FBInformatik，FernUniversita？tHagen，Hagen，Germany摘要本文提出了一个新的纯Prolog执行的数学定义，以结构化操作语义中的公理的形式。 该模型的主要优点是其易于表示回溯，由于转换关系及其逆的功能。因此，向前和向后推导步骤是可能的。引入了一个新的阶段概念相对于传统的堆栈的堆栈方法的优点是模块化属性。最后，该模型结合了传统的“伯德盒”隐喻的直觉与执行状态的紧凑表示，使其可行的制定和证明定理的模型。 在本文中，我们介绍了该模型，并陈述了一些有用的性质。保留字：回溯，Prolog，操作语义1动机、目标和结果本文介绍了一种新的纯Prolog运算语义S1：PP，并建立了一些有用的性质，旨在对Prolog计算概念在路上，我们得到了一些新的概念，用于表征回溯，但也可能有用的对象，随着时间的推移演变。这样的对象在逻辑编程中是目标，在它的动态意义上目标是逻辑编程的一个基本概念，但即使在纯Prolog的情况下，也很难以形式化的方式掌握1电子邮件：marija. fernuni-hagen.de1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.02640M. 《理论计算机科学电子笔记》128（2005）39问题是，在非确定性过程的情况下，通过稍微不同的身份，“那个”目标可能会演变。例如，假设我们向Prolog程序提出以下查询：p（X，Y），q（Y），fail。假设p（X，Y）有两个答案，比如p（a，Z）和p（b，3）。在静态意义上，我们只有一个目标q（Y），但动态地我们可以有两个不同的目标：第一个q（Z），如果q（Z），失败终止，那么q（3）。这两个目标都有自己的创建、向前和向后执行的生命周期以及可能的到期时间。 在这些对象之间区分回溯的操作语义是至关重要的。此外，假设q/1是递归的。在计算E。G.对于目标q（Z），我们还需要注意q/1的所有递归调用，以便准确地知道失败后该去哪里。它们是否也都被认为是不同的对象，与上面的两个q（Z）和q（3）是同一类型的，以及如何管理它们？在本文的其余部分，我们继续如下。首先定义一个谓词的规范形式，原始的纯Prolog程序将被转换成它。然后，在第3节中，纯Prolog的一个新的操作语义被定义，在结构化的操作方式。在整个第4节至这显然也包括以某种方式定义目标的（动态）概念。 我们通过阶段的方式解决了这个问题，初始事件（代表目标的创建）在计算过程中通过这些阶段。阶段可以被看作是范式思想的一般化，在这个意义上，阶段独立于计算的上下文，如第7节所示，但由宏转换组织。从模型中给定的各个过渡开始，构建简单的派生（向前和向后），这是简单刀路的基础，简单刀路聚合为组合刀路。最后，我们将在第8中展示组合传递如何对Prolog计算进行建模我们的方法可以被看作是一个形式化的原始伯德模型。但有一个重要的细节：我们扩展了端口的概念，最初设想由伯德选定的原子，一般的目标公式。将注意力从原子转移到一般目标公式被证明是一个关键思想，并使一个非常简单的模型成为可能。该模型的第一个版本称为S：PP，在[18]中提出。但变量的处理结果是困难的。新型号S1：PP对此进行了改进。2预赛在我们的模型中解释它之前，原始的Prolog程序必须转换为规范形式，即常见的单子句表示。M. 《理论计算机科学电子笔记》128（2005）3941−这种表示法可以说与原始程序“足够接近”，唯一的区别在于中心统一定义2.1 [完全规范形式]我们说一个谓词P/n是完全规范形式的，如果它在给定程序中的定义由单个子句P（X1，...，X n）：−Bs. 这里X1，.，X n是不同的变量，Bs是分支的析取（可能为空，对应于失败）。每个分支的形式为 X1=T1，.，Xn = Tn，Gs，其中Gs是目标公式的合取（可能为空，对应于真）。没有X i可以出现在任何T1，. T n，G。这里，目标公式可以是六种：用户定义的原子P（T1，.， T n），特殊术语真和失败，等式T 1= T 2，目标公式转换成完全标准形式可以如下进行：首先重新命名P/n的子句，获得子句P（T1，...，T n）：−G. (For事实，将G设为真。）选择不同的变量X1，...，X n不出现在任何T1中，...，Tn，G.对于每个物体G，组装一个新的物体X1 = T1，.，Xn= Tn，G.最后，对新的物体作一个析取，保持它们出现的顺序，给出标准形的物体。头应该是P（X1，.，X n）。例如，以下程序p（a，Z）。p（b，3）.q（0）。q（s（N））：−q（N）。将被规范地表示为p（X，Y）：−X=a，Y=Z，true; X=b，Y=3，true。q（Z）：−Z=0，true; Z=s（N），q（N）.简单地说，p（X，Y）：−X=a; X=b，Y=3. q（Z）：−Z=0; Z=s（N），q（N）.为了本文的目的，一个较弱的概念是足够的：定义2.2[规范形式]我们说一个谓词P/n是规范形式的，如果它在给定程序中的定义由一个子句组成 P（X1，.，X n）：G. 这里X1，.，Xn是独立变量，G是任意目标公式.42M. 《理论计算机科学电子笔记》128（2005）39DDDDD无无D在D的图中。 我们说E可以从E0到达。 推导+Π无Π无无3语义S1：PP我们提出的模型S1为了便于参考，该模型定义在两个文件中，Subsection 3.2（语法）和Subsection 3.3（规则）。请注意，转换规则，所以微积分只包含公理。定义3.1[事件]一个事件是一个四元组（Port，Goal，A-stack，B-stack），由3.2小节中的语法给出。直观地说，事件是Prolog计算的一种状态，在我们的模型中，它由四个参数决定：• 目标：当前计算的焦点或“目标”（通用目标公式）• port：标记当前目标的进展（调用、退出、失败或重做）• A-stack：当前目标的历史（祖先的堆栈）• B-stack：当前环境（赌注的堆栈）定义3.2[transition]设Prolog是一个规范形式的纯Prolog程序，如3.2小节和定义2.2所定义。转移关系的定义见3.3小节。逆关系应表示为：- 是的 如果E1= 我们说E1导致E. 换句话说，我们说E1是E的前趋，而E是E1的后继。如果某个事件导致事件E，则可以输入如果事件E导致某个事件，则它可以被留下转换规则的左侧是相互不相交的，即。e. 没有关键对，所以我们有引理3.3（跃迁是确定性的）e.对于每个事件E，最多可以有一个事件E1，使得E ≥ E1。注3.4[逆关系]转换关系的逆关系是不起作用的，因为可能有一个以上的事件导致相同活动例如，我们有call T 1= T 2 nil Dfail T 1= T 2 nil，以及重做T1=T2<$σ·nil<$d失败T1=T2<$nil <$。再往下，就会发现，对于合法的事件，相反的关系是功能性的。 在我们的例子中，重做T1=T2<$σ·nil<$不是一个法律事件。定义3.5[推导]设E0，E是事件。 E的一个n-推导，k步的E0，记为E0kE，是从E0到E的长度为k的路径非零长度用EE∗ E.0天E，以及任何长度的推导，0天M. 《理论计算机科学电子笔记》128（2005）3943无DDDD无ΣΠΠΠ示例：调用G<$σ·nil<$D，redo Gnon-initial），并重做pnilD（不能左，但不合法，p是无ΠΠ （不能输入，定义3.6 [初始事件]初始事件对于任何Q都称为Q nil。直觉上，初始事件的目标Q在Prolog中对应于顶级目标（查询）.定义3.7[法律推导，法律事件]如果存在一个目标Q，对于一个QnilE0E，本文认为E0E是一个代数导子，而E是一个合法的事件。定义3.8[最终事件]一个合法的事件E是一个最终事件，如果没有过渡EE1。记法1（不可能事件）为了便于记法，所有不是最终的，也不会导致任何进一步事件的事件都被描述为导致不可能事件，记为“不可能事件”。 类似地，非初始事件，无法输入。特别是，对于任何错误，都要执行redofailD命令和exitfaild命令。 一些更UΠ原子目标）。最后一个例子可能不太明显，它是从引理4.1和（S1：atom：2）.3.1关于微积分的(i) 在S1：PP中，goal一词有两种通常的含义：作为语法域，意思是(ii) SLD-分辨率是对选定的原子进行操作，而S1：PP是对整个当前目标进行操作。(iii) 对于3.2小节中没有定义的语法域，我们参考[14]（替换），[21]（逻辑编程）和[12]（Prolog）。(iv) 最一般的单位元σ应选择为幂等的，即σ（σ（T））=σ（T）。这总是可能的。(v) 分辨率由（S1：atom：1）建模，并且它是实际上依赖于k的唯一规则。如果原子目标的谓词有一个定义，归结将成功，因为规范形式。(vi) 注意在（S1：atom：1）中的要求σ（GA）=GA。由于子句是规范形式的，因此将子句的头部与目标统一起来可能不会产生任何效果。而不是重新命名目标。我们希望多边集团只对该条款进行操作。(vii) 一个新的变量，在派生的某个点上，由44M. 《理论计算机科学电子笔记》128（2005）39.最后进球+.·3.2活动语言B栈定义。}atom：− goal push|突然呼叫|重做出口|失败真正|失败|原子|术语=术语|目标|目标，目标原子|目标|标签/目的，目的1 |2BY（目标）|OR（tag）mgu|备忘录无|祖先·A栈无|bet·B栈元变量E：事件程序Γ： port，Push ：push，Pop： 流行U、V： A-stack，a，b，G^ ： 一个控制器， 编号： tag、Θ、 B-stack，α ： 打赌σ：替代A、B、C、G、H：目标GA： 原子T：术语大元功能[1/A，B<$：=A，[2/A，B<$：=B，类似地用于析取σ（T）=σ对T的应用mgu（T1，T2）=T1和T2的subst（）=当前替代=来自的所有mgu的组成;（1）（2）（3）（4）（5）（6）（7）（8）（9）（10）nil（T）：= 不α（T）：=α（（T）），如果α是mgu（T），如果α是memo按其通常意义上所取的域term（在Prolog意义上，作为目标的超集）; atom（逻辑编程中用户定义的谓词）; substitution，renaming，mgu。事件：：=程序：：=定义：：=端口：：=推：：=M. 《理论计算机科学电子笔记》128（2005）3945结合呼叫A，BΣUA出口不及格B出口Σ1 /A、B·U⟩⟩⟩⟩⟩⟩DΣΠ1/A，B·U打电话给A1 /A、B·UDΣΠ 呼叫B2 /A、B·U⟩⟩DΣΠ 失败A、BU2/A，B·U2 /A、B·UΣDΠ A、B出口U失败BΣDΣΠredo A，BΣUDΠredoAredoB1 /A、B·U2/A，B·U⟩⟩（S1：conj：1）（S1：conj：2）（S1：conj：3）（S1：（S1：conj：6）析取呼叫A;BΣUΣ失败BΣ2 /A;B·UC出口重做A;B真实与失败无/无;无U⟩⟩⟩⟩⟩DΠ 打电话给A1 /A;B·U不及格B1/A;B·UDΣΠ 呼叫B2 /A;B·U⟩⟩DΣΠ 失败A;B失败UDΠ A出口;B出口OR（N）·N2U与C…OR（N）·NDΠ redoC无/无;无与C…2（S1：disj：1）（S1：disj：2）（S1：disj：3）（S1：disj：5）调用真函数重做真实的ΣUUU⟩⟩⟩DΣΠ 退出真值UDΣΠDfailtrue错误UΠ fail失败ΣU（S1：true：1）（S1：true：2）（S1：失败）平等调用T=T1 2ΣU.退出T=T1 2⟨ ⟩σU• Σ、如果我...3否则redo T=T1 2U⟩⟩DΠ失败T=TΣ（S1：unif：1）1 2但是，Uσ·ΣDΣΠ 失败T=T1 2U（S1：unif：2）用户定义原子GA呼叫G一 ΣU.Σ一⟩⟩⟩⟩D调用σ（B）Π失败的G，Σ⟨ ⟩GA·U、一个U如果H：−B...4否则（S1：原子：1）B出口ΣG·美国DΠ G出口一 BY（B）·U⟩失败BΣG·美国redo GA BY（B）·UDΣΠ一失败G一 UDΣΠ redoBG·美国一（S1：原子：2）（S1：原子：3）（S1：原子：4）2，其中C =[N/A;B]。3.当mgu（ψ（T1），ψ（T2））= σ.4 如果H：−B是一个具有线性关系的线性映射，且dσ=m gu（GAJ，H），其中hGAJ：=m gu（GA）且dσ（GAJ）=GAJ.3.3纯Prolog的操作语义S1：PP46M. 《理论计算机科学电子笔记》128（2005）39对于事件的两个堆栈，我们表示为，其中，DDU+VU+VVULemma4. 1（pendant）如果calllGnilDfailHθ，则无WW无W事件，是一个变量没有出现在前面的推导过程中，由目标和事件的A-堆栈表示。3.4辅助记法除了3.2小节中给出的语言之外，这里还有一些辅助符号，它们将在定理中使用：(i) 匿名元变量：如果事件的某些部分与当前主题无关，则应使用下划线““将其抽象化。(ii) 要导航祖先X，使用两个函数：[X]，它是X的选定一半，如子节3.2中定义的，以及[X|，即X（不带标记）：[N/A，B|：= A，B，[不适用; B|：= A; B，[G A|：= G A.(iii) 堆栈加法和减法：堆栈右侧的连接我们用+表示，如果U + V = W，则W-V：= U。连接-U VΓG+，和Γ G + g：= Γ G。(iv) 栈序：如果存在W使得U=W+V，那么我们说U≥V。(v) σ |T表示仅限于T项变量的代换σ。¢ ¢(vi) 宏转换将在第5中定义，第6.符号2（区分两个级别）对象级别术语（i. e.实际的Pro-log术语）以无衬线体显示，如true。元级术语（i.e. 微积分中的任何其他东西）都用斜体表示，比如call，α。符号3（dropping）在下面我们通常会删除任何对的引用，因为纯Prolog中的程序在推导过程中不能改变。 然而，一个固定的程序总是被假定的。 注意，本文中所有建立在转移关系上的新关系也隐含地依赖于转移关系。4单一索赔首先，我们陈述一个有用的性质，我们称之为悬垂引理。观察到该公式是非确定性的，因为我们只声称存在一个悬垂事件（具有相同的B堆栈），但不知道它是否是唯一的一个。零Wcal llGnildcallHθdfailHθ。如果CallGnildredoH θ，那么，M. 《理论计算机科学电子笔记》128（2005）3947V无DD−→nWW无无Cal llGnildexitHθdredoHθ.悬垂引理使我们能够证明微积分的一个重要性质：给定事件只能有一个后继事件，而且，对于一个法律事件只能有一个前驱事件。定理4.2（合法变迁是唯一的）如果E是合法事件，则E只能有一个合法的前趋者，也只能有一个后继者。 如果E是非初始的，则只有一个合法的前身。 如果E是非最终的，则恰好有一个后继者。在建立了转移关系及其逆关系的功能性之后，我们可以从它的每个端点展开一个法律推导。首先，让我们看看我们可以通过过渡从初始事件走多远引理4.3（祖先）如果ΓG是合法事件，则存在Push和J这样，Push [a|吉吉a·VD+ΓG阿吉亚五世是一个合法的派生词。引理4.4（标记父事件）如果ΓG是合法事件，且a=N/A，B或a= N/A; B，则G=[a]。a·V引理4.5（final event）如果E是一个合法的pop事件，且A栈为非空，则总有一个变迁EDE1。无WW无引理4.6如果调用GnilD+Γ Hθ和Γ HθPop，则对于某个V，W= V+ G^·nil，且一个A_nG^使得[G^|=G.Lemma4. 7若callGnilPopHp，则nH=G.上述引理表明，波普·尼克尔事件是自然结束的形式，衍生点基于这个原因，我们发展了一个围绕这类事件的衍生概念我们从简单推导的概念开始。5简单的派生和子事件在本节中，我们将通过将整个过渡步骤序列折叠成一个大步骤，来定义一些新的“宏观”过渡关系。可以说，非法派生在这种情况下没有多大意义，因此我们排除它们：符号4（仅合法推导）在过渡关系中，¢ ¢从现在开始定义，即，=，总是假设，衍生品是合法的。48M. 《理论计算机科学电子笔记》128（2005）39UUDDUUU¢WU埃克塞特UUDUDWW给我5分。4（endpoint）IfPushGD<$弹出Hθ Θ θ，则H =G。UUUU的PushG。第5.1节[向前或向后简单推导]考虑一个法律推导，vationPushGD+E，使得在该导数内没有Pop。UU蒂翁岛e. 不允许按G键+Pop键+E键。 这样的衍生物-我们称一个相对于U的前向导子，记为推G的前向导子E. 类 似 地，一个法律推导Pop G+E使得没有在这个推导，推U是相对于U的向后推导，附注dbyPopGd E. 一个前向或一个后向的发展相对于U是相对于U的简单求导。向前推导产生子事件：定义5.2[subevent]IfPushGd rHθnrHθ是一个子事件引理4.6和引理4.7可以被推广以提供任意推送事件和任意A栈的情况，并且以与原始引理相同的方式被证明：定理5.3（子事件性质）如果推G的子事件为H且WU当W=V+G^·U时，对于某个V和一个A，G^suchthat[G^|=G.UU显然，每个推转换都是一个向前推导。一些前向导数也可以组合这是从子事件属性中得出的。推论5.5如果推1UG推式HΘTMa·UE，然后按1GΣ¢E. 此外，如果按G键， EDEwith thEPoPouches，thenPushGouches1U UE1.给我5分。6（前一遍）如果PopG按G键来做一些推和推。下一个语句来自subevent属性。与pop和push交换位置类似的声明，由于简单的传递引理而成立引理5.7（no pop no push）令Push 0 GUE为合法推导，使得在推导内不存在Pop U。 那么在推导中也没有Push_U_n。这同样适用于形式EPush 0G U。考虑到前向导子的合成，我们可以证明祖先引理的更强版本新版本的优势在于M. 《理论计算机科学电子笔记》128（2005）3949−→WVDa·VWWWWWWW¢是的。此外，如果重做H <$θ<$是一个合法事件，则重做H <$θ<$←−退出H<$θ<$。确定性，我。e.在派生中只有一个地方可以放置父事件：Push [ a]形式的最近过去事件|你好。引理5.8（祖先，更强）如果ΓG是一个合法事件，则有J，a·V是Push和PushJ，使得Push [a| ⟨ Σ ⟩ DΓ G ⟨ Σ ⟩ is a legal derivation.引理5.9（子事件，逆事件）如果对于一个法律事件，W = V + a·U，则Γ H<$Θ<$是Push [ a]的子事件|为一些推，W U还有一点...正如我们所看到的，具有相同A栈和相同目标的事件之间的向前或向后推导在微积分中扮演着特殊的角色。我们将这些推导抽象为一个新的概念：¢定义5.10[向前或向后简单传递]A向前推导PushGU我们称之为相对于G和U的向前传球。类似地，背-向后推导PopGUDPushGU我们称向后传递相对G和U。 从E1到E2的向前或向后传递是简单的传递，用E1E2表示。事件E1，E2被称为阶段.为了表示阶段，我们可以使用固定的部分（目标和A栈）作为上标，像这样：EG，U。6复合导子有了有用的结果，如pendant和forward pass引理，我们现在能够证明更强的结果。与祖先引理的更强版本一样，其优势在于对过去相关事件的确定性具体化。例如，对于一个失败事件，我们现在知道它的挂起调用（具有相同的B堆栈）是最近的调用事件，具有相同的目标和相同的A堆栈。定理6.1（pendant，stronger）设失败H为法律事件。然后如果HθD不符合Hθ，则Hθ D不符合导数，引理6.2（B-栈）如果调用G −→ Γ Hj，则J≥。U U引理6.3（no call no fail）如果EPopGU是合法推导，并且callG U不在此推导内，则fail G U也不在此推导内推导从引理5.6和定理6.1中我们知道，合法的流行事件可以经历一系列过去的阶段，如退出<$U<$−重做<$U<$−退出<$U <$<$−。... 由于逆导子的有限性和引理5.6，D50M. 《理论计算机科学电子笔记》128（2005）39D21⟨ ⟩DU·UUUUUUUUUUΣ一定会出现。 因此，我们最终必须重建一个派生出口U调用U，其中没有调用U形式的事件介入。失败事件也是定义6.4[组成 通过]考虑一 序列的 简单孔型EG，U−→+E G，U使得没有呼叫G在这个序列中，i。e.1G、U12−→+调用G−→+EG，UU是不允许的。 这样的序列称为可组合的，或相对于G和U的组合通道，并表示为EG，U=EG，U.可以看出，调用GU不能出现在相对于G和U的合成通道内，即使被视为派生，即。e.既不是在简单传球的阶段之间，也不是在两者之间。一个重要的问题是-mains：特定阶段的B堆栈如何相互关联？这是我们下一个主张（引理5.6的同伴）的主要关注点。定理6.5（合成遍数）以下两个关系成立：如果失败G合法，则失败G =调用G。（一）如果退出G合法，则退出G =调用G，其中≥（二）因为（2）进一步成立：如果G是一个析取，那么对于某个N，从OR（N）开始，对于一个统一或一个原子目标，也是类似的。我们已经知道，对于合法的重做事件holdredoG←−exitG，U U这增加了更多的关系，如果失败G=重做Gj，则J≥（3）如果redoG合法，则redoG=调用G，其中≥（4）作为副产品，可以得到引理4.5的以下补充，从而得出结论，唯一的最终事件是具有空A栈的合法弹出事件：引理6.6（非最终事件）如果E是合法的推事件，则总是有一个转移E E1。7独立性与模块性注7.1[最新呼吁]铭记子句，以及我们模型中mgus的幂等性，可以从规则（S1：atom：1）中看出，对于任何法律事件调用σ（B），σ（B）成立：（σ（B））=σGAU（B）. 换句话说，这样一个事件的目标部分是最新的相对于B-stack。E2UM. 《理论计算机科学电子笔记》128（2005）3951⟨ ⟩D D DD1nPop G流行音乐 U和U，U无UUU≥UU1UnUU无UU无UUUUredoGJ−DE1Jgd. DEnJgDPopGJ−。U+V1VnVU+V联系我们定理7.2（添加堆栈）设G为nilE.E无是一个合法的衍生物。 则对于每个G，调用G是一个合法事件，并且（G）= G，成立：打电话给GdE你好 DE ⟨ Σ⟩ DPop G ◦ ⟨ Ω + Σ⟩也是一种法律衍生。这里，如果E i= Γ H <$θ，则Ei= Γ H <$θ，其中VV（H定理7.3（减去栈）设G为E1D. DEnDPop G是一个合法的推导，并且Ei=PopGJ：=（G）成立：你代表每一个我。 那么对于CallGjnilDE1Jgd. DEnJgDPopGJ−也是一种法律衍生。这里，如果E i= Γ H j <$θ，则EiJ= Γ H J<$θ，其中V VJH（H）= HJ和V（V）= V J。前面的两个声明表明，以调用事件开始的简单传递堆栈表示当前目标的计算上下文看看类似的属性是否适用于以重做事件开始的简单过程，这将是一件有趣的事情。首先注意，如果重做G是合法事件，则根据定理6.1，重做G← −退出G。我们-通过定理6.5，我们进一步得到重做G=调用G，其中没关系这给了我们一个提示，我们可以削减多少的堆栈。请注意，与调用事件相反，我们不一定通过添加或减去堆栈来达到合法的重做事件。(For例如，无法到达具有空A堆栈的重做事件但如果我们这样做，那么我们可能知道它的下一个阶段，由于以下主张：引理7.4（从redo开始）Let redo GDE1D. DEnDUUPopG是一个合法导子，对每一个i，E i/= Pop G。进一步让重做G =调用G。 则对于G J：=（G）和EiJ类似于在U U定理7.3成立：无UU无此外，对于Θ（G）= G和Ei，与定理7.2类似：重做G + θ DE θ d.。 DE θDPop G+ θ。我们的下一个目标是证明：即使在回溯时，目标也总是通过相同的阶段，与堆栈的起始内容无关52M. 《理论计算机科学电子笔记》128（2005）39无无UUUUVVVVU1MV1我U我VΠ引理7.5（向后独立性）考虑序列callG−→exitGJ−→redoGJ−→exitG调用H<$Θj −→退出H<$ΘJ<$−→重做H<$Θ j<$−→退出H<$θj <$−其中Θ（H）= θ（G）。 则ΘJ= θJ−θ + Θ和=换句话说，第二次推导是从不同的背景开始的，但从同一个目标开始，它经过了与第一次推导相同的阶段。注意回溯的存在。这个结果可以推广到任意组合刀路。记住，由于引理6.3，在组合过程中只能出现一次失败阶段，我们得出了对推导上下文的独立性的一般要求。定理7.6（独立性）设下列序列是可合成的，其中m，k≥ 1，且令Θ（H）= θ（G）。调用G −→ E G，U− →. −→ E G，U调用H <$Θ<$−→ E H，V−→... −→ E则对于任何i in common（i≤m，k）成立：如果E G，U：= Γ G <$$> J<$ $ > ，则E H，V= Γ H <$Θ j <$$>，使得ΘJ=<$j− θ +Θ。独立于推导的上下文，与合取和析取的组合性以及转换到更大步骤的聚合一起，在S1：PP中建立了一种模块性在第8节末尾有一个插图。在剩下的技术部分中，我们定义了一个计算的概念，旨在模仿Prolog风格的SLD-归结，即。e.具有最左侧选择和顺序的从左到右深度优先搜索的SLD分辨率。为了简洁起见，这样受限的SLD-解析应该被称为Prolog计算。8建模纯Prolog计算基于阶段的概念，可以以简洁的方式表示Prolog计算。在这一节中，再次表示规范形式的纯Prolog程序，如3.2小节和定义2.2中所定义的。定理8.1（存在终止，成功，失败）目标G相对于目标G的Prolog计算存在终止，如果存在简单的传递呼叫Gnil− →PopGH、VKM. 《理论计算机科学电子笔记》128（2005）3953无无|⟨⟩−→⟨⟩⟨ ⟩ ⇒⟨⟩UΣ无UUUU-|UUΠ1无ΠUΠ如果Pop = exit，则G的Prolog计算成功，否则失败。定理8.2（第一个计算出的答案）如果callGnil−→exit Gnil，则subst（n）G是相对于n的G的第一个计算出的答案替换在Prolog中。定理8.3（所有计算的答案，通用终止）在可合成序列调用Gnil1/G，失败·零2k−1出口G1/G，失败·零是subst（）|G是Prolog中相对于G的第k个计算答案替换。此外，G相对于G是泛终止的，如果调用Gnil=1/G，失败·零失败Gnil1/G，失败·零实际上，我们可以更精确一点，将目标G视为其他目标的子目标 回想一下，如果调用G是合法的，并且U = a n·. ·a1·nil，则callGD脓h[a|好吧在其余的世界里，卡尔·格奥尔基是一个被他所取代的人。最近推送[a1|你好此外，由于具有空A的推送事件堆栈不能到达，我们知道我们的事件必须是派生的最老事件，形式为call[a1|你好 类似于Prolog中的子目标，让我们定义两个新概念：定 义 8.4[S1-superergoal ，S1-ssubgoal]LetcallG 可 编 程 逻 辑 。IfU=an·. ·a1·nil，我们是一个[a1|是Gj的S1-超代数，且GJ是[a1]的S1-超代数|，其中GJ：=θ（G）. 在U=nil的情况下，我们定义Gj为它自己的 S1-超目标。定理8.5（超目标）设G为一个合法事件。 考虑最大可合成序列称为G。然后持有：subst（S_i）G_J是G_j相对于Prolog中的S_i的第k个也是最后一个计算的答案替换，其中G_J：= S_i（G），Prolog填充的查询是G_j的S_1-supergaL。最后，我们展示了一个模块化推导的例子。假设退出A、B的行为是一个法律事件。它是如何衍生出来的？幸运的是，逆向转换对于法律事件是确定性的（唯一性属性），所以我们可以从任何一个看起来更有希望的端点展开法律推导该指数54M. 《理论计算机科学电子笔记》128（2005）39U⇐⟨⇐⟨DU⟨⟩ ⇐⟨⟩⟨D出口B2/A，B·U，by（S1：conj：4）⟩ ⇐⟨D出口A 1/A，B·U，by（S1：conj：2）⟩Σ将省略，因为以下对任何程序都适用A、B出口=打电话给B2 /A、B·UΣ◦定理6.5。（2），其中，=打电话给A小姐1/A、B·UΣ◦◦定理6.5。（2），其中，调用A，B，通过（S1：conj：1）此外，可以看出，整个推导是一个可组合序列。所以我们得到引理8.6（合取）设退出A，B为合法事件。 那就来吧，来吧存在，其中n≥n ≥n，使得退出A，Bn=调用A，Bn，并且B出口2 /A、B·U=打电话给B2/A、B·UU从A出口离开1 /A、B·UU打电话给阿杰。1 /A、B·U以类似的方式，我们可以展开一个析取和一个原子目标，从而模拟S1：PP中的vanilla元解释器。9相关工作纯Prolog执行的最早且仍然权威的模型是SLD-推导[3]。在这个模型中没有显式的析取信息，所以回溯根本没有形式化。这个问题在另一个流行的模型SLD-tree[3]中得到解决。两者都有一个缺点是缺乏组合性：不可能表达e。G.一个合取的SLD树通过合取的SLD树。许多进一步的工作受到传统的四端口盒子隐喻的启发，称为Byrd模型[9]，旨在表示Prolog中过程调用的演变。伯德模型是控制流中的一项开创性工作，但它被证明很难形式化，并且变量处理在原始工作中根本没有解决。 Tobermann和Beckstein在[24]伯德的图遍历思想，将执行轨迹（给定查询相对于给定程序的执行轨迹）的中心概念定义为轨迹图中的路径。端口被清晰地定义为这样一个图的层次节点。但是，跟踪图不是很容易管理。Cheng等人[10]提出了另一种称为SLD-contour的图形模型，它是SLD-tree的变体，但其遍历应该更好地对应于执行轨迹。 这个想法SLD-轮廓的结果是可扩展的合取和析取目标，给出了可能是纯Prolog表达式的第一个组合模型。从本质上讲，他们将伯德盒的概念M. 《理论计算机科学电子笔记》128（2005）3955公式，因此在我们自己的研究之前。另一种形式化的方法体现了Byrdmodel的精神，它是一种基于约束的方法，由J.A.、D. U. C.S.和D. Ridoux [16]提出。在我们早期的工作[ 19 ]中，也有人试图定义伯德盒，但它本质上与其他跟踪规范相同，从[ 9 ]的跟踪中断/ 1开始：在这些方法中，生成Prolog执行的跟踪，但是不支持关于执行结构的推理，因此跟踪生成必须伴随着通过一些其他设备的跟踪分析。还有其他各种纯（甚至完全）Prolog执行的模型。与我们的工作相媲美的是基于标准的方法。Staürkgivesin[23]是一个简单的问题，是纯逻辑编程的一个简单的执行状态是帧堆栈的堆栈。Jones和Mycroft的开创性论文[17]是第一个提出堆栈执行模型的论文，适用于添加了cut的纯Prolog。栈的栈的思想反映了Prolog实现的通常内存管理，并且通常不可能抽象执行的部分。10总结这项工作的动机是能够证明，在调试中使用的某种程序转换不会以任何“严重”的方式影响原始程序。很快就变得很明显，即使是制定这样的属性也不是一件容易的事情，并且需要一个相当强大的Prolog执行模型该模型需要能够充分详细地表示Prolog执行，另一方面，支持关于它的形式化推理（这意味着一些抽象方法，如模块化）。除了这两个至关重要的要求之外，为了自身的发展和实际相关性，模型应该有助于有效的实现（这意味着纯粹的象征性表示和较小的开销）。因此，一个相当简单的演算S1：PP定义了纯Prolog执行。由于合取与析取的组合性，以及转换聚合成更大的步骤，一种模-实现了larity。Prolog的前向和后向计算被统一处理，使得该模型适合于表示回溯。 这个想法能在多大程度上延伸到定义完整的标准Prolog还有待观察。此外，指定其他类型的可逆计算的潜力似乎值得研究。56M. 《理论计算机科学电子笔记》128（2005）39确认非常感谢C.贝尔乐和匿名裁判。引用[1] J. H.安德鲁斯逻辑程序设计：操作语义学和证明理论。剑桥大学出版社，1992年。[2] J. H.安德鲁斯Prolog割的见证属性和语义。 逻辑程序设计理论与实践，3（1）：1[3] K. R. Apt和M. H.范·埃姆登。对逻辑程序设计理论的贡献。J. of the ACM，29：841[4] B. Arbab和D. M.贝瑞Prolog的操作和指称语义。J. of Logic Programming，4（4）：309[5] M.博迪内Prolog程序的终止性证明：一种语义方法。J. of Logic Programming，14：1[6] M.比约Prolog的简单操作和指称语义。Theoretical Computer Science，71（2）：193[7] M.比约 回溯的公理化。 在Proc. of the STACS，第71-82页，1992中。[8] E. BéorgerandD. 我是说，我的意思是，我的意思是， Amathematitinof u llProlog. 计算机程序设计科学，24（3）：249[9] Lawr e n ceByrd。以及Pr ologpr ams的连续记录。InS. A. Ta？nlund，编辑，Proc. of the1980 Logic Programming Workshop，pages 127也是D. A. I.研究论文编号151.[10] M. H. M. Cheng，M.中国植物志H.范埃姆登河N. Horspool和M.利维Prolog程序的组合操作语义。J. New Generation Computing，，10（3）：315[11] E. P. de Vink. Prolog与cut的比较语义。Science of Computer Programming，13（1）：237[12] P. Deransart ， A. Ed-Dbali 和 L. Cervoni Prolog ： The Standard （ Reference Manual ） .Springer-Verlag，1996.[13] P. Deransart和G.费朗Prolog的一种操作形式化定义：一种具体化方法及其应用。J. NewGeneration Computing，10：121[14] E.艾德 置换和unifiations的性质。 J. Symbolic Computation，1：31[15] B.易卜勒深度优先逻辑程序的说明性语义. J. of Logic Programming，41：27[16] E. 是的，M. 你知道的。 Ri d oux.使用约束语义指定Byr d的模块化。 在proc 的WLPE'99 ， LasCruces ， NM ， ENTCS 的 第 30 卷 。 爱 思 唯 尔 ， 2000 年 。http://www.elsevier.com/locate/entcs/的网站。[17] N. D. Jones和A.迈克罗夫逐步开发Prolog的操作和指称语义。 在proc ISLP'84 ，第281-288页，大西洋城，1984。[18] M. Kulas. Purr