选言逻辑规划与线性逻辑规划的比较和属性的研究

理论计算机科学电子笔记48（2001）网址： http://www.elsevier.nl/locate/entcs/volume48.htmlpp. 1- 2 5 岁关于选言逻辑规划与线性逻辑规划马尔科·博扎诺1乔治·德尔扎诺2毛里齐奥·马尔泰利3Dipartimento di Informatica e scienze dell16146热那亚，意大利摘要本文研究了文[13]中定义的选言逻辑程序与线性逻辑的一个子集，即对应于Andreoli和Pareschi的LO [3]的Lin-Log [2]片段我们从自上而下的操作角度和自下而上的语义角度分析了这两种语言从证明理论的角度来看，我们表明，模之间的经典和线性连接词的简单映射，LO可以被视为一个子结构片段的DLP中的规则的收缩是禁止在右手边的序列。 我们还证明了LO是严格的表达比DLP的命题的情况下。 从语义的角度来看，在回顾了我们在以前的工作[5]中给出的LO的自底向上定点语义的定义之后，我们表明DLP定点语义可以被视为相应LO语义的抽象，定义在合适的抽象域上。 我们证明了[6，8]意义下的抽象是正确的和完备的。最后，我们表明，以前的属性的语义是严格相关的证明理论的经典和线性逻辑片段的DLP和LO的属性。1介绍析取逻辑编程（DLP）[13]和线性逻辑编程（LLP）[11]是霍恩逻辑的经典理论的更有趣的扩展，底层语言如Prolog。引入这两种范式背后的动机一方面，析取逻辑程序设计已被引入，以表示不确定的信念。另一方面，线性逻辑编程已经被引入，以增加基于状态的计算纯Prolog程序。仔细1电子邮件地址：bozzano@disi.unige.it2电子邮件地址：giorgio@disi.unige.it3电子邮件地址：martelli@disi.unige.it2001年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。博扎诺，德扎诺和马尔泰利2然而，看看它们的正式定义，就会发现非常有趣的联系。让我们专注于线性逻辑编程语言LO [3]（Linear Ob-Prolog），它是LinLog [2]的一个片段，可能是Prolog [11]的“线性”扩展的第一个建议DLP和LO程序都扩展了Horn程序，允许子句具有多个头部：在DLP中，子句的头部由原子公式的经典 原子公式的乘法析取（见[9]）。通过考察两种语言的操作语义，可以清楚地看出经典连接词和线性连接词的意义差异在DLP中，扩展了解析步骤，以便处理正子句（原子的集合/析取）。隐式收缩步骤应用于所选子句。相反，在禁止收缩的子结构逻辑中，LO分解具有与多集重写（应用于原子公式的集合）相同的效果基于这种直觉，在本文中，我们将调查的观点，LO作为一个子结构制定的DLP，正式比较的优势和劣势的两种语言。作为数学工具，我们将使用证明理论和抽象解释。证明理论允许我们比较在统一设置中工作的两种范式的自上而下的语义（即在有或没有结构规则的可证明性）。抽象解释允许我们将比较扩展到自下而上的程序评估。更具体地说，通过展示DLP和LO的语义域之间的伽罗瓦连接，我们将把DLP程序的语义描述为LO程序的语义的抽象此外，使用抽象解释理论和完备性概念[6，8]，我们将讨论所得到的抽象的质量。这一步基于我们在最近的工作中定义的LO的新定点语义[4，5]。最后，我们将讨论证明理论属性（规则的可置换性）和抽象属性（完备性）之间的关系。DLP作为LO的抽象的观点有几个原因。首先，它打开了使用DLP技术分析LO程序的可能性。此外，它表明DLP的范式可能具有意想不到的应用程序，作为一个框架来推理Petri网的属性，Petri网是一种着名的并发计算形式[10]，如[5]中所讨论的。1.1文件计划在第2节中介绍了一些概念之后，在第3节中，我们回顾了析取逻辑编程的主要概念，并在一个逻辑演算的上下文中重新表述了它的操作语义在第4节中，我们介绍语言LO，而在第5节中，我们比较DLP和LO证明理论。在第六节中，我们通过抽象解释研究了DLP和LO之间的关系，并讨论了由此产生的抽象的性质节中博扎诺，德扎诺和马尔泰利3n←7.讨论了抽象解释中的完备性概念与证明论之间的联系最后，在第8节中，我们讨论了结论和未来的工作。2预赛在本文中，我们将广泛使用多集运算我们将考虑一个固定的签名，它定义了一组有限的对象常量、函数符号和谓词符号。在T上的基项的集合将被表示为T，而T上的原子集记为A。A上的多重集在下文中称为事实，并象征性地记为A，B，C，.。. . 一个多重集，（可能是 重复的）元素A1，...， An∈ An将被简单地 表示为{A1，. 一个n}，重载集 合 的常用符号。一个多重集A由映射Occ：A→N唯一确定，使得OccA（A）是A在A中出现的次数。多集是根据多集包含关系 空的多重集记为，并且使得对于每个A∈A，Occ（A）= 0，对于任何A，Occ（A）=多集并集A，B（当'，'是二义性的时，也写作A+B）是这样的：对于每个A ∈ A <$，我们还定义了一个特殊的运算·来计算两个相对于“的多集的最小上界也就是说， A·B满足对任意A∈A <$，OccA·B（A）=max（OccA（A），OccB（A））.最后，我们将使用符号A，其中n是自然数，以表示A +. +A（n次）。在本文的其余部分，我们将使用θ，Θ，. 来表示可能的复合公式的多集合。给定两个多集<$和Θ，<$，Θ表示多集并，如前所述，并且<$，{G}简单地写为<$，G。最后，设T：I→I是定义在完备格我是说， 我们定义T↑0=.其中，t是h。e底元素nt，T↑k+1=T（T↑k）对所有k≥0，T↑ω=k∞=0T↑k，其中是最小上界wrt. ±。此外，我们使用lfp（T）来表示T的最小定点。3选言逻辑程序设计[13]中定义的选言逻辑程序是一组有限的子句一个100... A n← B1 你好，其中n≥1，m≥0，Ai和Bi为原子式。 分离目标 的形式为C1，...，Cn，其中Ci是肯定分句（即析取原子式），对于i：1，.，n.为了使语言对称，在本文中，我们将考虑以下形式一个100... A n← C1 C m博扎诺，德扎诺和马尔泰利4PPPP在正文中包含肯定分句在[13]之后，我们将通过考虑程序子句的基实例集来处理一阶程序给定一个程序P，我们将使用符号Gnd（P）来表示P中子句的基础实例的集合。此外，我们将用原子集合来识别肯定分句为了定义DLP的操作和指称语义，我们需要以下定义。定义3.1（析取Herbrand基）程序P的析取Herbrand基（英语：DisjunctiveHerbrandBase），简称DHBP，是由任意数量的不同基原子构成的所有正子句的集合定义3.2（析取解释）析取Herbrand基DHBP的子集I称为析取Herbrand解释。定义3.3（Ground SLO-推导）设P是一个DLP程序。从P得到的地面目标G的SLO推导由目标G0= G，G1，. 使得对于所有i≥ 0，从Gi= ←（ C1，.，Cm，...，Ck）如下：• C←D1. Dq是P中的子句的基例，使得C包含在Cm中（选择子句）;• Gi+1是目标←（C1，.，Cm−1，D1<$Cm，.，Dq<$Cm，Cm+1，.，Ck）。注意，当程序子句的主体为空时，Gi+1等于←（C1，.，Cm−1，Cm+1，.，Ck）。定义3.4（SLO-反驳）设P是一个DLP程序。从P到地面目标G的SLO-返回是SLO-导出G0，G1，.，GKS. T. Gk只包含空子句SLO分辨作为Horn程序的SLD分辨，为DLP程序提供了一种过程性的解释操作语义定义如下：Odlp={C |C ∈ DHBP，<$C有SLO-反驳}。对于Horn程序，可以通过以下运算符定义定点语义。定义3.5（Tdlp运算符）给定DLP程序P和IdlpDHBP，Tdlp（I）={Cj∈ C1∈. C n|CJ← D1. n∈ Gnd（P），Di<$Ci∈I， i：1，.，n}请注意，在前面的定义中，我们已经隐含地将肯定分句视为原子的集合算子Tdlp在wrt序解释格上是单调连续的集合包含。基于此属性，博扎诺，德扎诺和马尔泰利5⊆⊆± ∈∈PPPPPPPPP定点语义定义为Fdlp=lfp（Tdlp）=Tdlp↑ω。 如图所示在[13]中，定点语义相对于操作语义是完备的，即对于所有C∈Odlp，存在CJ∈Fdlps. t。 CJ蕴涵C。注意对于两个基本子句C和CJ，C蕴涵CJ当且仅当CCJ。这表明，解释也可以按文字顺序排列。子集包含对于它们的元素，即， 我J当且仅当对所有A I存在B J使得B A（B蕴涵A）。在本文的其余部分，我们将考虑后者的排序。例3.6考虑析取程序P={r（a），p（X）<$q（X）<$r（X）}和辅助谓词t。然后，DHBP={r（a），p（a），q（a），t（a），p（a）<$r（a），p（a）<$q（a）<$r（a），. . }。此外，目标G0=←（p（a）<$q（a）<$t（a））有反驳G0，G1=<$（p（a）<$q（a）<$t（a）<$r（a）），G2其中G2只包含空子句。 P的定点语义是DLPP={{r（a）}，{p（a），q（a）}}。注意，{p（a），q（a）}包含在{p（a），q（a），t（a）}（即p（a）<$q（a）蕴涵p（a）<$q（a）<$t（a））。Tdlp算子的定义可以这样重新表述，即它的输入和输出域包含多重集而不是原子集（即我们可以考虑原子多重集的集合事实上，我们总是可以将一个多重集映射到它的基础集，即包含重数大于零的元素的集合，反之亦然，一个集合可以被看作是一个多重集，其中每个元素的重数都等于1。基于多重集的公式将使与LO定点算子（见第6节）的比较更容易，因为后者是在这种域上定义析取Herbrand基和Tdlp算子定义可以重新表述如下（在下文中，我们将始终引用这些定义）。定义3.7（析取Herbrand基）程序P的析取Herbrand基（英语：DisjunctiveHerbrandBase），简称DHBP，是由任意数量的基原子构成的所有多重集的集合，每个原子的重数至多为1。定义3.8（α映射）设α是多原子集上的下列函数给定一个多重集A，α（A）是这样的多重集，使得对于每个A∈A∈A，如果OccA（A）= 0，则Occα（A）（A）=0，否则Occα （A ）（A）= 1（即我们用相应的集合抽象一个多重集）。我们顺便注意到，α定义与[13]中给出的子句的最小因子定义3.9（Tdlp运算符）给定DLP程序P和IdlpDHBP，Td lp（I）={α（C1）+C1+. . +Cn）|C J←D1.. . n∈Gnd（P），D^i+ Ci∈I，i：1， .， n}F博扎诺，德扎诺和马尔泰利6^∨·^一⇒·∨∨ ∨←←普利特 TTRPA1，.，A n，PA1. ∨An,∆∨PC1，H^，A. . . PCm，H^，APH^，A条件是H ← C1<$... 图1. DLP的证明系统前面定义中的符号用于正式映射肯定子句（即，- 原子的析取）到原子的多集合（而在定义3.5中，从子句到原子集合的映射是隐式的）。在不失一般性的情况下，从现在开始，我们将进一步假设，像A1的条款... A n← C1 Ai都是不同的Cj由不同的原子组成这将简化DLP条款的嵌入线性逻辑（见定义5.1）。3.1DLP的一个证明系统我们现在将给出一个基于微积分的DLP证明理论演示它的公式与SLO推导的定义直接相关（见定义3.3）。 为了简化与LO的比较，我们引入了一个显式的常数tt来表示真，并使用语法A1. Antt. 上一节中给出的定义可以用一种简单的方式加以修改生成的语言可以用以下语法描述：H：：= A1mm... AnD：：= H←G| D ∧ DG：：= H1... Hn|TT其中Ai是原子式。DLP程序P是D-子句，而DLP目标被表示（模"DLP的证明系统如图1所示（同样，我们使用符号将原子的-析取映射到多集）。在这里，在一个P是一个DLP程序，而DLP是一组目标。此外，表示原子公式的集合，而H表示H-公式。在不失一般性的情况下，我们将最高目标仅限于正子句（作为子句的合取的目标的执行可以通过引入一个ficatom并向程序中添加一个子句来模拟）。读者应该说服自己，图1中的系统是RBC博扎诺，德扎诺和马尔泰利7←一A.∨ ∨←A.A.普利特TTRPA1，.，A n，PA1. ∨An,∆∨PA，A，APA， A中央广播电台PC1，A.. .PC m，APH^，A条件是H ← C1<$... 图2.改进的DLP打样系统。直接模拟SLO可证明性。计算的状态，在DLP中是由合取目标C1，...，Ck，在递归的上下文中- culus由派生树表示，其边界（开放的叶子）是仍待证明的目标（C1，...，Ck）。规则bc对反向链接步骤进行建模，并且对应于SLO推导的步骤;仅当当前上下文仅由原子公式组成时才可以应用它规则r形式化了肯定分句是原子集合的直觉（即它允许在序列的右侧交换格式为a1... ant在DLP中扮演与unit子句相同的角色，事实上，在这样的子句上的反向链接步骤导致独立于当前上下文的成功，如以下方案所示：TTRPTT，BCPA1，.，An，A如果A1…n←tt∈Gnd（P）这一观察使我们得出以下性质，即弱化规则在DLP中是允许的命题3.10（DLP中弱化规则的可容许性）给定DLP程序P和两组目标，使得如果P是，则P是。证据通过简单的归纳介绍了DLP样张的结构.✷为了比较DLP和LO，我们现在将在图1中展示系统的微小变化。这个新系统可以证明与前一个系统等价，并且与我们将在第5节中介绍的LO系统直接相关在这里，序列的右边是一个多目标集合，并明确添加了收缩该系统如图2所示。添加压缩规则使得规则bc的稍微修改成为可能，在规则bc中，相关程序子句的头部中的原子在上面的序列中排出这两个系统的等价性可以通过对导子结构的简单归纳得到证明RBC博扎诺，德扎诺和马尔泰利8⇒AAP◦−.在系统中证明需要表明，收缩和削弱规则在第一个系统中是可接受的我们有以下结果。命题3.11给定DLP程序P和目标G，存在G从P的SLO-反驳当且仅当P∈G在系统中可证明 当且仅当P G在图2的系统中是可证明的。证据 为了清楚起见，让我们分别使用符号E1和E2来区分图1和图2中系统的可证明性。我们还使用符号bc1和bc2表示相应的反向链接规则。SLO-反驳和1可证明性之间的等价性是通过定义（见定义3.3和3.4）。注意，交换规则（即，肯定子句和原子集合）隐含在定义3.3中。此外，规则ttr可以从定义3.3中推导出具有空主体的子句（即单位子句）的特殊情况。可以通过证明ctrr r和bc2规则在第一个系统中是可容许的，而bc1在第二个系统中是可容许的来证明bq1和bq2之间的等价性• 在第一个系统中ctrr r的可容许性来自于集合A，A，等于A的事实（换句话说，收缩隐含在选择的集合中）;• bc2 在 第 一 个 系 统 中 是可容许的：假设H ← C1≠...... <$Cm∈ Gnd（P）;如果P<$1C1，A，.，P<$1Cm，A，那么由命题3.10我们得到P<$1C1，H^，A， .P<$1Cm，H^，A，因此P<$1H^，A;• bc1在第二个系统中是可容许的：假设H ← C1 . <$Cm∈ Gnd（P）;如果P<$2C1，H^，A， . ， P=2Cm，H^，A，则P=2H^，H^，A;由此可见，通过对H^中的每个元素应用ct，P=2Cm，H^，A。✷作为一个推论，给定一个肯定子句C = A1... 我们有P<$C是可证的当且仅当存在CJ∈Fdlp使得Cj<$C。4线性逻辑程序设计语言LO线性逻辑[9]可以被看作是经典逻辑的一种改进，其中弱化和收缩的使用只允许用于特殊模态范围内的公式（指数和这样，公式（没有模态）可以被视为在可能的应用中，线性逻辑被证明是扩展逻辑编程的自然基础，具有状态的概念（在这种设置中，是有限使用公式的集合）。LO [3]是一种基于线性逻辑的逻辑编程语言。它的数学基础在于线性逻辑的一个片段的证明理论表示，称为LinLog [2]，并包括线性连接词（线性. . . .（附加连词），&（附加连词）。. . （乘法分离），常数T（加法恒等式）。 在命题的情况下，LO由博扎诺，德扎诺和马尔泰利9.►一^^不.....►一PG1，G2，PT r.. ... . ... .RPG1，PG2，P G 3，P G4，P G5，P G 6，P G 7，P G 8，P G 9，&PT，PG1. . .G2，PG1G2，&PG，BCPH^，A条件是 H−G ∈Gnd（P）图3.第三章。LO的验证系统以下公式类：D：：=A1. ... .............. . An−G | D &DG：：=G. . . G|G&G|一|不这里A1，...，An和A都是从一个固定的符号n开始的命题符号。G-公式对应于给定程序中要评估的目标。D-公式对应于多头程序子句。 LO程序是一个D-公式.设P为程序C1&. &Cn. G-公式G1，...，Gk在P中对应于双边LO的目标驱动证明P 第一个，...， Gk.LOP-G1，.，Gk是以下双边线性逻辑的缩写：！C1，...，！Cn→G1，...， Gk.公式！F在图的左边表示F可以在证明中使用任意次数。这意味着LO计划也可以被视为一组可重复使用的子句。根据这种观点，LO的操作语义通过图3中定义的统一（目标驱动）证明系统给出在图3中，P是一组蕴涵子句，表示原子公式的多重集合，而G表示G-公式的多重集合。一个公理是可证明的，如果它的证明树的所有分支都以r公理的实例终止图3的证明系统是更一般的线性逻辑统一证明系统的特殊化，如Andreoli[2] 论坛[12]规则bc表示反向链接（解析）步骤。注意，我们重载了符号（在定义3.9中，它被用来将原子的双析取映射到多集）来表示的映射。. . . - 将原子分离成多集。还要注意，只有当当前LO表达式的右侧由原子公式组成时，才可以执行bc因此，LO子句的行为类似于多集重写规则。格式为a1的LO条款..... ...... ... . an−T扮演着与DLP计划的单位条款事实上，在这样一个条款上的后链步骤.....R博扎诺，德扎诺和马尔泰利10.. C................ C............不独立于当前上下文A导致成功，就像DLP中一样：PT，ATrBCP A1，.，An，A提供了A1..... . .... ... . An∈Gnd（P）一个类似于命题3.10的结果成立。因此，LO可以被看作是线性逻辑的一个简单注意，弱化和收缩在LO序列的左侧（即在程序部分）都是允许的。命题4.1（弱化规则在LO中的可容许性）给定一个LO规划P和两个多目标集，使得 P然后PJ。证据通过简单的归纳，对LO证明的结构进行了分析。✷例4.2设P是由以下子句1. a-b二、 b −（d. . .. . .. . .. . . . （e）&f3. C4. e5. C. . . d − T. . . . e − b. . . . f −T. . . .. . .并考虑初始目标e，e。这个目标的证明如图4所示，其中我们用bc（i）表示反向链接规则在P的子句号i上的应用。证明过程如下。使用条款4.，证明e，e我们必须证明b. . . . c，其中，通过LO. . . . r规则，简化为证明b，c. 在这个. . .我们可以在第2条上进行反向链接，我们得到新的目标（D）。. e）f、c.. . . .通过应用&r规则，我们得到两个独立的目标d. . . e，c和f，c。 第一，. . .在减少通孔之 后 。. . r规则，可通过子句（公理）3证明，而后者可由子句（公理）5直接证明。 注意 在左分支中的非空上下文（即包含e）中成功。一个类似的证明表明，目标a也可以从P证明。5证明理论视角：从DLP到LO现在让我们回到析取逻辑编程。在第3节中，我们已经证明了DLP的操作（自顶向下）语义可以用一个具有显式收缩规则的证明系统来表示此外，弱化规则在DLP中是可接受的一个自然的问题出现了：..博扎诺，德扎诺和马尔泰利11►不...[·|. ...[·|一一P e，Trbc（3）TrPd，e，c. .. . .....RPTBC（5）Pd. . .e、c. ..菲律宾f，c&P（d. . . e）&f、cBC（2）巴基斯坦b，c. .. . . .. . . RPb. . . CBC（4）Pe，e图四、例4.2程序中目标e的LO证明如果我们禁止在DLP中使用结构化规则呢结果语言是否我们将分两步回答这些问题。我们将首先通过以下映射将DLP嵌入线性逻辑定义5.1（[·|映射）从DLP公式到线性逻辑（LO）公式的映射通过对DLP结构的归纳来定义. . . .公式如下：[F|=[F|[F|−[G|，[tt|=T。.. [G|，[F]G|=[F|&[G|、[F←G|为基于这个映射，D-和G-公式的文法可以重写如下：H：：=A1..... ...... . . .. . .nD：：= H−G | D &DG：：=H1& ... & Hn|不其中Ai是原子式。通过DLP程序的定义，的映像返回一类LO程序，其中主体中的头和析取符都没有相同原子的重复出现。从句法上讲，所得到的语言是在[3]中提出的语言LO的真子集。. . .第4节，除了前面的公式，连接词。. 和&可以在LO目标中任意嵌套。这两种语言的操作语义之间的关系有待分析专门针对所考虑的片段的LO的操作语义通过图5中定义的证明系统给出，其中表示原子公式的多集，H表示H-公式，并且序列的右侧是目标的多集图5的证明系统和前面一样，只有当当前LO表达式的右侧由原子公式组成时，才可以执行bc规则，并且如果它的证明树的所有分支....R博扎诺，德扎诺和马尔泰利12. ... .. .►►|·|.. 一个一个一.一|..PA1，.，A n，. . . ..PT，PTrP A。......这是什么？A，1N. . RPC1，A.. .PC m，APH^，A条件是 H − C1&. &Cm∈Gnd（P）图五、LO片段的专用证明系统终止于Tr公理的实例。DLP和LO证明系统之间的比较现在是直截了当的。通过观察图2中的DLP系统和图5中的LO系统，我们可以看到，将经典连接词直接编码为线性连接词取模，通过添加压缩的结构规则，从LO获得DLP。等价地，LO可以被看作是DLP的一个子结构逻辑，其中禁止收缩我们注意到，弱化规则，相反，在DLP和LO中都允许。通过用c表示语言LO中的可证明性，用类似于以下的压缩规则扩充：图2中的，并在线性逻辑中的LL可证明性，我们可以说下面的命题。注意指数！然后呢？在最后一个例子中，需要用弱化和收缩来增强线性逻辑的可证明性（在例子的两侧）。命题5.2给定一个DLP程序P，P ∈ G在DLP中可证当且仅当[P|C[G|在LO中是可行的，当且仅当！[P|我？[G|是可行在LL。5.1命题DLP与命题LO作为迄今为止进行的证明理论分析的结果，我们现在提出一些关于DLP和LO的命题片段的简单结果这些结果表明，在命题的情况下，LO是严格的表达比DLP。命题5.3不存在从命题LO程序和目标的类到命题DLP的类的转换，这保留了可证明性，即 使得对于任何P和G，P ∈ G是可证明的 当且仅当|P |⇒|G|是可以证明的证据（略）在命题的情况下，逻辑上不同的子句的集合是有限的（即，aaa等）。所以是析取Herbrand基地。让我们. .. .考虑LO目标a，a的. . . .. .......... ... . . a等从. . . .根据上面的观察，存在n > m，使得 a. . . ... （n次）.... . . .. . . .. . 一|在逻辑上等同于（DLP）|a. . . ......这是什么？（m倍）.. . 一|. 还有待展示一个区分LO中两个目标的程序P。我们将P定义为.BC博扎诺，德扎诺和马尔泰利13. .. ......||.|·|[·||[||[|∪[ |a. . . ......这是什么？n次.... . . a ← T. 显然，第一个目标可以从LO中的P证明而后者不是。无论我们给出P的任何平移P，我们都会得到两个目标的平移（重合）在DLP中是可证明的，或者它们都是不可证明的。✷另一方面，从DLP到LO的转换是简单的。我们有以下建议。命题5.4存在从命题DLP程序和目标的类到命题LO的类的翻译，其保持可证明性，即 使得对于任何P和G，P ∈ G是可证明的当且仅当|P |►|G|是可以证明的证据 采取以下措施就足够了|G = G|得双曲正弦值. P =PP中心，其中 P是通过将翻译（见定义5.1）. . . .P中的每个子句，Pctr是子句ai− ai的 有 限 集 合 。. . ai，一个代表一个语言中的命题符号这些分句给出了紧缩的直接✷6基于语义的比较在我们最近的工作[4，5]中，我们已经证明了LO程序服从定点语义，该语义表征了可证明的LO目标集。作为Horn和析取程序的相应语义，在命题情况下，LO的定点语义可以在有限的步骤中计算LO的定点语义使我们能够更深入地研究LO和DLP之间的关系为此，我们可以使用抽象解释提供的数学工具[6]，特别是可以用来估计抽象精确度的完备性非正式地，LO和DLP定点语义之间的比较是基于将多集映射到原子公式集（肯定子句）的抽象。这种抽象导致DLP和LO的语义域之间的伽罗瓦连接我们证明了在DLP中的LO程序的翻译的定点语义是原始LO程序的定点语义的正确抽象。此外，我们表明，这种抽象是不完全完整的LO语义。在一个完全完全的抽象中，抽象定点算子的应用与抽象α交错的结果与具体定点算子的抽象相一致。对于一个完整的抽象，一个类似的关系适用于定点，即，抽象运算符的定点与具体运算符的定点的抽象一致。我们将证明这种较弱的完备性对整个LO程序类的抽象都成立，从而推广了[5]中的结果，该结果仅限于体中没有合取的LO程序类。博扎诺，德扎诺和马尔泰利14PPP⟨I±⟩P{A}{}↑AA{B |AB}联系我们A B A·BP联系我们·让我们首先给出一些用于介绍LO定点振动的定义（详细介绍见[5]）。定义6.1（LO Herbrand基）在A上的一个比例LO程序P的Herbrand基HBP是A上所有基原子的多重集的集合。前面的定义与定义3.7相同，唯一的区别是元素的重数不要求最多为1。给定一个多重集我们用[A]表示的向上封闭，即“[[a，b]] =a，b，a，a，b，a，b，b，a，b，c，.. . ）. 以下定义形式化的直觉，解释总是隐含地认为向上封闭集。因此，向上闭包相等的解释被认为是等价的。这是由prop。4.1（削弱效力规则的可定义6.2（LO Herbrand解释）LO Herbrand解释的格定义如下：• I=P（HBP）/↑其中I↑J当且仅当[[I]]=[[J]];• [I]±[J]当且仅当对所有B ∈I存在A ∈J使得A• 底元是空集<$1，顶元是单点{<$1}的↑-等价类（<$1=空多集，<$• 最小上界IHJ是IHJ的↑-等价类。等价性允许我们推理模冗余。例如，any在，中是多余的，，实际上等价于。为了便于标记，在本文的其余部分，我们将用它的类[I]来标识解释I。对于我们在本文中考虑的LO程序的子类（即没有连接词的嵌套），定点Tlo运算符的定义可以具体如下：定义6.3（Tlo运算符）给定一个LO程序P和一个解释I，运算符Tlo定义如下：T10（I）={H2+（C1）.. . . ·Cn）|H−D1&.. . Dn∈Gnd（P），1， . ，n，D^i+Ci∈I}<$ {H^|H<$−T∈P}这个定义与定义3.9相似。这里，我们有两个不同的操作，它们都是由定义3.9中的多集并建模的：多集并（+）和多集的最小上界 比如说，甲乙丙+ 和218c= a，b，b，c，而甲乙丙和218c=a，b，c. 注意，这两个运算在α下是等价的（见定义3.8），即α（+）=α（）.还要注意，单位子句的情况在定义3.9中是隐式的。证明了算子Tlo在上是单调连续的，博扎诺，德扎诺和马尔泰利15±ωP.....P→PHerbrand解释的格（有序wrt.）.因此，LO程序P的定点语义可以定义为：Flo=.T lo↑i.P Pi=0时操作语义和定点语义之间的关系可以表述如下。命题6.4（完备性[5]）设P是LO规划，A ∈HBP，则P <$A是可证的当且仅当存在AJ∈ F los. t. AJ“A。例6.5考虑LO程序P={r（a）<$− T，p（X）. . . p（X）. . . .. .q（X）<$−r（X）}和辅助谓词t。然后，Herbrand基HBP定义如下{{r（a）}，{p（a）}，{q（a）}，{t（a）}，{p（a），r（a）}，{p（a），p（a），r（a）}}，。. . }。L0中的p∈p（a），p（a），q（a），t（a）在L0中是可证明的。实际上，通过应用反向链接步骤，我们获得了PARP_r（a），t（a）。现在，我们可以应用事实r（a）<$− T，并得到公理Tr的一个实例。P的定点语义如下：Flo={{r（a）}，{p（a），p（a），q（a）}}。注意，{p（a），p（a），q（a）}我们注意到，如[5]中所证明的，命题LO程序的定点语义可以在有限多个步骤中计算。虽然Herbrand基总是无限的（它包含A上所有可能的多重集，因此它是如果一个人是有限的，那么这个属性是由良好的准序保证的[5]《易经》的解释在下文中，我们将使用前面的语义学和抽象解释的框架来给出另一种自下而上的解释，即DLP和LO之间的关系。首先，我们将对与抽象解释理论相关的一些概念进行简要的概述。6.1抽象解释抽象解释[6，7]是一个经典的语义近似框架，用于构建基于语义的程序分析算法。给定一个语义和语言构造器和标准数据的抽象，抽象解释确定了语言的抽象这种新的表示使得能够在有限时间内计算抽象语义，尽管它意味着一些精度损失我们在这里回顾一下抽象解释中的一些关键概念，读者可以在[6，7，8]中找到。给定一个具体的语义C，TP，由一个具体的域（完全格）C和一个（单调）定点算子TP：C C指定，抽象语义可以由一个抽象域A和一个抽象定点算子T#指定。 在本文中，程序语义由lfp（TP）给出，并且.博扎诺，德扎诺和马尔泰利16PPP≤→→P⟨ ⟩ ⟨⟩◦≤◦⟨⟩P◦◦⊆我我我我± ∈∈P我我P它抽象为lfp（T#）。 具体和抽象语义S=C，TP和S#=A，T#通过Galois连接α，C，A，γ联系起来，其中α：CA和γ：AC分别称为抽象和具体化函数.称 S#是S 的 一个 可靠抽象，如果对所有P，α（lfp （TP））Alfp（T#）。这个条件是由全可靠性的最强性质所隐含的，它要求α TPAT #α. 完备性和完全完备性的概念与可靠性的概念是对偶的。也就是说，S#是S的（完全）完全抽象，如果对所有P，（T#<$α≤Aα <$TP）lfp （T#）≤Aα（lfp（TP））。很多时候，假设完整性的概念包括可靠性（即，我们强加在前面的等式中的“=”）。众所周知[7]，抽象域A诱导TP的最佳正确逼近，由α TPγ给出，并且可以定义（完全）完备抽象算子T#当且仅当最佳正确逼近是（完全）完备的。可以证明，对于固定的具体语义，抽象解释的（完全）完备性只取决于抽象域的选择。[8]中研究了从正确的抽象解释开始，通过精炼或简化抽象域来实现（完全）完整的抽象解释的问题我们通过观察得出结论，抽象解释的等价表示是基于闭包运算符[7]，即。从一个具体的域C到它自身的函数是单调的、幂等的和可拓的。这种方法提供了与抽象域对象的具体表示的独立性我们现在处于连接LO（具体）语义和DLP（抽象）语义的位置6.2DLP作为LO我们将通过闭包运算符来定义抽象解释。根据这一观点，我们可以将抽象解释定义为格上的闭包算子，即定义6.2的LO解释的域。事实上，我们可以把析取解释看作是包含所有集合的子类（即元素重数至多为1的所有多集合）。换句话说，选言解释类是一个抽象域。我们记得，在解释的顺序定义如下：J当且仅当对于所有B存在AJ，使得A是B的子集（即，对于选言解释，A B）。我们给出以下定义。定义6.6（从LO到DLP的抽象解释）抽象解释由闭包算子α：I → I定义，使得对于每个I∈I，α（I）={α（A）|A∈I}。请注意，我们重载了定义3.8中的运算符α，博扎诺，德扎诺和马尔泰利17PP◦PPPP·PPPPPPPPPPPP延伸到解释。定义6.7（抽象语义）抽象定点语义由p（T#）给出，其中操作符T#的抽象定点被定义为（αf）P PTlo）。根据[7]，对于固定抽象α，α Tlo是具体定点算子Tlo的最佳正确逼近。抽象α通过遗忘原子的多次出现将多集变换为集合T#算子确实是定义3.9的析取逻辑程序的Tdlp算子（为此，我们在包含多集的域上定义了它在换句话说，Tdlp输入域对应于由闭包算子α的定点集（即图像）给出的抽象域。在Tlo的定义中使用的运算（多集的最小上界）和+（多集并）是可互换的，正如前面已经指出的，因为随后应用了运算符α，并且两者都对应于Tdlp定义中的多集并。此外，单位子句的情况在Tdlp的定义中是隐含的。我们有以下结果。命题6.8（DLP是LO的抽象）给定DLP程序P和选言解释I，Tdlp（I）=T#（一）P[P|证据 根据定义。✷命题6.9（DLP是LO的可靠抽象）对于每个LO程序P，抽象语义是具体语义的完全可靠抽象，即对于每个解释I ，α（ T1o（I ））±T# （α（I））。是的。当T#=α<$T10，I±α（I）时，该命题遵循单调性的T#。✷前面的结果意味着soundnes s，即。α（lfp（T1o））±lfp（T#）。 的完全完备性的强性质不适用于抽象。看到为什么，作为一个反例，单个子句a-b和解释I单复数{b，b}。那么，α（T10（I））={{a，b}}，T#（α（I））={{a}}，P P和T#（α（I））/±α（T10（I））。在[5]中我们证明了一个初步结果，即对于其子句在程序体中最多包含一个合取（即禁止合取）的LO程序子类，抽象是完全的。这个子类特别有趣，如[5]中所讨论的，以及在7.2节中提到的，因为它可以用来编码Petri网。我们现在解决证明整个LO程序类的抽象的完整性的问题我们将根据完备性概念和证明论之间的联系，给出这一事实的间接证明。证明将在第7.1节中给出。博扎诺，德扎诺和马尔泰利18PP∨∨P◦PPP普利特 TTRPA，A，APA， A中央广播电台PC^1，A. . . PCm，APH^，A条件是H ← C1<$... 图6. DLP的等效证明系统7完备性的证明理论解释在本节中，我们讨论抽象的完备性概念和规则的可置换性的证明论概念之间的关系，从而在3.1节和5.1节与6.2节之间建立了一座桥梁。首先，让我们重新定义图2中所示的DLP证明系统。新系统如图6所示。在这里，我们直接将规则blog插入到反向链接规则中。由此产生的系统可以很容易地证明在以下意义上是等价的：原子的析取A1.. .An在第一个系统中是可证明的，当且仅当多重集A1，...，在第二种情况下，n是可证明的。这个新的证明系统更直接地对应于Tlo算子的公式化。特别地，如果我们考虑仅包括图6中的规则ttr和bc的系统（即没有收缩），我们得到，模经典和线性连接词之间的通常映射，LO的证明系统此外，Tdlp算子定义中的α步骤类似于图6中证明系统中的压缩规则（准确地说，α对应于ctrr的多次应用）。为了完成这个循环，现在让我们考虑完备性的性质即α（lfp（Tlo））=lfp（α<$Tlo）。第一个表达式α（lfp（Tlo））表示抽象的一组目标，可以证明从证明系统的LO（没有收缩），即。可以使用压缩规则仅在证明树的根处证明的目标的集合第二个表达式lfp（α Tlo）表示可以通过自由使用压缩规则来证明的目标集（准确地说，bc的应用后面是ctrr的每一个可能的应用）。因此，在这种观点中，