逻辑程序非基有限失败的语义
摘要
逻辑程序始于上世纪70年代初，来源于定理机器证明与人工智能的研究。在逻辑程序30年的发展中，它已经成为了人工智能领域中重要的一个方向，在众多人工智能领域展示着它的价值。逻辑程序语义的研究中重要的一个方面就是否定的处理。处理否定最基本的两种方法是闭世界假定(closed world assumption)和失败即否定原则(negation as failure)。本文所论述的非基有限失败语义，是对于失败即否定原则的研究。在对非基有限失败语义的研究中，抽象解释(abstract interpretation)方法被用于不动点语义的推导。
抽象解释方法是一种用于近似程序语义的通用方法。其核心思想在于构建和联系程序的两个不用的语义：具体语义(concrete semantics)和抽象语义(abstract semantics)，抽象语义是具体语义的近似。抽象解释方法与逻辑程序有着紧密的联系，在逻辑程序语义的研究中有着重要的作用。
有限失败是失败即否定原则中重要的概念，它是指求解一个目标所得到的SLD树是有限且每个分支都是失败的。最先在文献中介绍的用来描述有限失败的语义是(基)有限失败集FF_p(程序P有限失败的基原子集合)，
FF_p={A|A是基原子，←A有一棵公平的有限失败SLD树}。
然而这个语义并不能正确描述有限失败。如果我们考虑≈FF，程序之间关于相同有限失败目标集的等价，我们可以看出FF_p不足以区分不等价的程序。即两个程序有相同的基有限失败集，但某个目标在两个程序中关于有限失败的行为并不相同。
因此，一个新的有限失败语义被提出：非基有限失败集合NGFF_p，
NGFF_p={A|←A有一棵公平的有限失败SLD树}。
NGFF_p被证明对于有限失败是正确的。接下来一个重要的问题是给出关于非基有限失败的不动点语义。
为了描述有限失败，首先应该尽可能详尽地表达推导过程中得到的SLD树，为此本文首先介绍了Comini提出了一个语义框架：SLD推导语义，这个语义可以对有限SLD推导进行推理。SLD推导语义的基本概念是合式推导集合，合式推导集合是部分SLD树的形式化表示。语义域是collection的构成的完备格，collection是将目标映射到合式推导集合的部分函数，可以看作是一个目标在推导过程中得到的部分SLD树。在此基础上，本文介绍了SLD推导语义中推导的联接、实例化、合取，collection的和、积、实例化、组合、扩展等基本运算符，以及应用这些运算符定义的指称语义、操作语义。然后叙述了语义的几个性质：指称语义和操作语义的等价，自顶向下与自底向上指称的等价，指称的正确性及最小性，指称的AND组合性。
接下来本文介绍了在此基础上发展出来的可观察行为理论。可观察行为在这个框架中被形式化为具体域和抽象域之间的Galois嵌入。其中具体域描述SLD树，抽象域描述我们感兴趣的行为。由可观察行为的概念可定义理想的抽象运算符，当我们用理想的抽象运算符来代替相应的具体运算符，就可以从具体的语义得到相应的抽象的语义。然后介绍了两类重要的可观察行为，它们是满足一定充分条件的可观察行为，
摘要
并且介绍了它们的性质。第一类可观察行为是标准(perfect)可观察行为，它是一种抽
象的操作语义和指称语义都精确的可观察行为。另一类可观察行为是指称
(denotational)可观察行为，其中理想条件被放宽。
因为这个可观察行为理论框架只关注有限推导，而为了研究有限失败的性质，我
们需要区分有限失败的推导和无限推导的部分答案，因此它不能被用作描述有限失败
的性质。为了将可观察行为理论用于处理有限失败，接下来本文介绍了Gori扩展了的
SLD推导语义和可观察行为，扩展了的框架可处理无限推导。他将无限推导分为永久
无限推导和非永久无限推导两类，给出了与有限失败经典的向下封闭性质相对应的向
上封闭性质。在此基础上，得出了用于分析非基有限失败的可观察行为，并且证明它
满足一定的充分条件，这些充分条件可以保证抽象语义是精确的。这个语义可以作为
一个共连续算子的最大不动点计算出。
本文的工作是对Gori框架中可观察行为的抽象域进行重构。基于有限失败的向一下
封闭性质，本文提出了最小生成集的概念，应用最小生成集来表示非基有限失败的原
子集。首先给出了最小生成集的定义，用最小生成集对抽象域进行了重构，并且重新
定义了其上的序关系。然后本文给出了基于最小生成集的非基有限失败可观察行为，
证明了它满足Gori框架中的充分条件，由此得到用最小生成集表示非基有限失败原子
集的不动点语义。
Logic programming began in the early 1970's as the outgrowth of earlier work in automated theorem proving and artificial intelligence. Logic programming has become an important area in artificial intelligence in its thirty years' development. And it shows its value in various areas in artificial intelligence. One of the most valuable research fields in logic programs is deducing negative information. There are two basic rules to negation, closed world assumption and negation as failure. Non-ground finite failure semantics, which is studied in this thesis, is toward negation as failure. In the analysis, abstract interpretation techniques are used to derive a fixpoint semantics.
Abstract interpretation is a general method to approximate semantics of programs, the guiding idea of which is to construct and relate different semantics of a program, concrete semantics and abstract semantics. Abstract semantics is approximation of concrete semantics. Abstract interpretation is related to logic programming closely, and it plays an important role in the study of semantics of logic programs.
Finite failure is the essential concept in negation as failure. It denotes that the SLD-tree for a goal is finite and all branches of the tree fail. The first semantics appeared in literatures is ground finite failure set FFp (the set of ground atoms which finitely failed in P), FFp={A |A is a ground atom and -A has a fair finitely failed SLD-tree }.
However, the semantics does not correctly model finite failure. If we consider FF, the equivalence relation induced on programs by having the same set of finite failure goals, we can find FFp is to weak to distinguish certain programs which are not equivalent. Namely, There are two programs having the same ground finite failure set, but a certain goal has different behaviors with respect to finite failure in the two programs.
Therefore, a new semantics for finite failure was introduced, non-ground finite failure set NGFFp,
NGFFp={A | -A has a fair finitely failed SLD-tree } .
NGFFp has been proved correct. Next, we need to derive a fixpoint semantics for non-ground finite failure.
In order to model finite failure, we should first model SLD-trees that are formed in derivation in detail. Hence this thesis introduces a semantics framework by Comini, SLD derivation semantics, which can be used to reason on finite SLD derivation. The basic concept in SLD derivation semantics is the well-formed derivation set. A well-formed derivation set is a formal denotation of a partial SLD-tree. Semantics domain is a complete lattice of collections which are partial functions mapping goals to well-formed derivation sets. A collection can be viewed as partial SLD trees for goals in derivation. Based on these, this thesis introduces some basic operators, such as concatenation, instantiation and
conjunction of derivations, sum, product, instantiation, composition and extension of collections. This thesis also introduces denotational and operational semantics defined by these operators. And then some properties of the semantics are stated, such as equivalence between denotational and operational semantics, equivalence between top-down and bottom-up semantics, correctness and minimality of the denotation, AND-compositionality of the denotation.
Then the thesis presents the theory of observables, which is based on SLD derivation semantics. In this framework, observables are formalized into Galois insertion between concrete domain and abstract domain where concrete domain models SLD-tree and abstract domain models the behaviors we are interested in. We can define optimal abstract operators from observables. When we replace concrete operators with their abstract corresponding ones, we can derive abstract semantics from concrete semantics. Then the thesis presents two classes of observables, which satisfy certain sufficient conditions. The properties of the two classes of observables are also stated. The first class is perfect observables, the denotational and operational semantics of which are precise. The ot
抽象解释方法是一种用于近似程序语义的通用方法。其核心思想在于构建和联系程序的两个不用的语义：具体语义(concrete semantics)和抽象语义(abstract semantics)，抽象语义是具体语义的近似。抽象解释方法与逻辑程序有着紧密的联系，在逻辑程序语义的研究中有着重要的作用。
有限失败是失败即否定原则中重要的概念，它是指求解一个目标所得到的SLD树是有限且每个分支都是失败的。最先在文献中介绍的用来描述有限失败的语义是(基)有限失败集FF_p(程序P有限失败的基原子集合)，
FF_p={A|A是基原子，←A有一棵公平的有限失败SLD树}。
然而这个语义并不能正确描述有限失败。如果我们考虑≈FF，程序之间关于相同有限失败目标集的等价，我们可以看出FF_p不足以区分不等价的程序。即两个程序有相同的基有限失败集，但某个目标在两个程序中关于有限失败的行为并不相同。
因此，一个新的有限失败语义被提出：非基有限失败集合NGFF_p，
NGFF_p={A|←A有一棵公平的有限失败SLD树}。
NGFF_p被证明对于有限失败是正确的。接下来一个重要的问题是给出关于非基有限失败的不动点语义。
为了描述有限失败，首先应该尽可能详尽地表达推导过程中得到的SLD树，为此本文首先介绍了Comini提出了一个语义框架：SLD推导语义，这个语义可以对有限SLD推导进行推理。SLD推导语义的基本概念是合式推导集合，合式推导集合是部分SLD树的形式化表示。语义域是collection的构成的完备格，collection是将目标映射到合式推导集合的部分函数，可以看作是一个目标在推导过程中得到的部分SLD树。在此基础上，本文介绍了SLD推导语义中推导的联接、实例化、合取，collection的和、积、实例化、组合、扩展等基本运算符，以及应用这些运算符定义的指称语义、操作语义。然后叙述了语义的几个性质：指称语义和操作语义的等价，自顶向下与自底向上指称的等价，指称的正确性及最小性，指称的AND组合性。
接下来本文介绍了在此基础上发展出来的可观察行为理论。可观察行为在这个框架中被形式化为具体域和抽象域之间的Galois嵌入。其中具体域描述SLD树，抽象域描述我们感兴趣的行为。由可观察行为的概念可定义理想的抽象运算符，当我们用理想的抽象运算符来代替相应的具体运算符，就可以从具体的语义得到相应的抽象的语义。然后介绍了两类重要的可观察行为，它们是满足一定充分条件的可观察行为，
摘要
并且介绍了它们的性质。第一类可观察行为是标准(perfect)可观察行为，它是一种抽
象的操作语义和指称语义都精确的可观察行为。另一类可观察行为是指称
(denotational)可观察行为，其中理想条件被放宽。
因为这个可观察行为理论框架只关注有限推导，而为了研究有限失败的性质，我
们需要区分有限失败的推导和无限推导的部分答案，因此它不能被用作描述有限失败
的性质。为了将可观察行为理论用于处理有限失败，接下来本文介绍了Gori扩展了的
SLD推导语义和可观察行为，扩展了的框架可处理无限推导。他将无限推导分为永久
无限推导和非永久无限推导两类，给出了与有限失败经典的向下封闭性质相对应的向
上封闭性质。在此基础上，得出了用于分析非基有限失败的可观察行为，并且证明它
满足一定的充分条件，这些充分条件可以保证抽象语义是精确的。这个语义可以作为
一个共连续算子的最大不动点计算出。
本文的工作是对Gori框架中可观察行为的抽象域进行重构。基于有限失败的向一下
封闭性质，本文提出了最小生成集的概念，应用最小生成集来表示非基有限失败的原
子集。首先给出了最小生成集的定义，用最小生成集对抽象域进行了重构，并且重新
定义了其上的序关系。然后本文给出了基于最小生成集的非基有限失败可观察行为，
证明了它满足Gori框架中的充分条件，由此得到用最小生成集表示非基有限失败原子
集的不动点语义。
Logic programming began in the early 1970's as the outgrowth of earlier work in automated theorem proving and artificial intelligence. Logic programming has become an important area in artificial intelligence in its thirty years' development. And it shows its value in various areas in artificial intelligence. One of the most valuable research fields in logic programs is deducing negative information. There are two basic rules to negation, closed world assumption and negation as failure. Non-ground finite failure semantics, which is studied in this thesis, is toward negation as failure. In the analysis, abstract interpretation techniques are used to derive a fixpoint semantics.
Abstract interpretation is a general method to approximate semantics of programs, the guiding idea of which is to construct and relate different semantics of a program, concrete semantics and abstract semantics. Abstract semantics is approximation of concrete semantics. Abstract interpretation is related to logic programming closely, and it plays an important role in the study of semantics of logic programs.
Finite failure is the essential concept in negation as failure. It denotes that the SLD-tree for a goal is finite and all branches of the tree fail. The first semantics appeared in literatures is ground finite failure set FFp (the set of ground atoms which finitely failed in P), FFp={A |A is a ground atom and -A has a fair finitely failed SLD-tree }.
However, the semantics does not correctly model finite failure. If we consider FF, the equivalence relation induced on programs by having the same set of finite failure goals, we can find FFp is to weak to distinguish certain programs which are not equivalent. Namely, There are two programs having the same ground finite failure set, but a certain goal has different behaviors with respect to finite failure in the two programs.
Therefore, a new semantics for finite failure was introduced, non-ground finite failure set NGFFp,
NGFFp={A | -A has a fair finitely failed SLD-tree } .
NGFFp has been proved correct. Next, we need to derive a fixpoint semantics for non-ground finite failure.
In order to model finite failure, we should first model SLD-trees that are formed in derivation in detail. Hence this thesis introduces a semantics framework by Comini, SLD derivation semantics, which can be used to reason on finite SLD derivation. The basic concept in SLD derivation semantics is the well-formed derivation set. A well-formed derivation set is a formal denotation of a partial SLD-tree. Semantics domain is a complete lattice of collections which are partial functions mapping goals to well-formed derivation sets. A collection can be viewed as partial SLD trees for goals in derivation. Based on these, this thesis introduces some basic operators, such as concatenation, instantiation and
conjunction of derivations, sum, product, instantiation, composition and extension of collections. This thesis also introduces denotational and operational semantics defined by these operators. And then some properties of the semantics are stated, such as equivalence between denotational and operational semantics, equivalence between top-down and bottom-up semantics, correctness and minimality of the denotation, AND-compositionality of the denotation.
Then the thesis presents the theory of observables, which is based on SLD derivation semantics. In this framework, observables are formalized into Galois insertion between concrete domain and abstract domain where concrete domain models SLD-tree and abstract domain models the behaviors we are interested in. We can define optimal abstract operators from observables. When we replace concrete operators with their abstract corresponding ones, we can derive abstract semantics from concrete semantics. Then the thesis presents two classes of observables, which satisfy certain sufficient conditions. The properties of the two classes of observables are also stated. The first class is perfect observables, the denotational and operational semantics of which are precise. The ot
引文
[1] K.R. Apt, M.H. van Emden, Contributions to the theory of logic programming, J. ACM 29(3), 1982, pp. 841-862.
[2] K.R. Apt, Introduction to logic programming, Vol. B: Formal Models and Semantics of Handbook of Theoretical Computer Science, Elsevier and The MIT Press, Amsterdam, Cambridge, MA, 1990, pp. 495-574.
[3] K.R. Apt, R. Bol, Logic programming and negation: A survey, Journal of Logic Programming 19-20, 1994, pp. 9-71.
[4] M. Comini, M.C. Meo, Compositionality properties of SLD-derivations, Theoretical Computer Science 211(1-2), 1999, pp. 275-309.
[5] M. Comini, G. Levi, M.C. Meo, A theory of observables for logic programs, Information and Computation 169, 2001, pp. 23-80.
[6] P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proc. 4th ACM Symp. Principles of Programming Languages, 1977, pp.238-252.
[7] P. Cousot, R. Cousot, Systematic design of program analysis frameworks, in: Proc. 6th ACM Symp. Principles of Programming Languages, 1979, pp.269-282.
[8] P. Cousot, R. Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, 13(2-3), 1992, pp. 103-179.
[9] P. Cousot, R. Cousot, Inductive definitions, semantics and abstract interpretation, in: Proc. 19th Annu. ACM Symp. Principles of Programming Languages, 1992, pp. 83-94.
[10] G. File, R. Giacobazzi, F. Ranzato, A unifying view on abstract domain design, ACM Computing Surveys 28(2), 1996, pp. 333-336.
[11] M. Gelfond, V. Lifschitz, The stable model semantics for logic programming, in: Proc. Fifth Int'l Conf. and Symp. Logic Programming, 1988, pp. 1070-1080.
[12] R. Gori, G. Levi, Finite failure is and-compositional, Journal of Logic and Computation 7(6), 1997, pp. 753-776.
[13] R. Gori, G. Levi, On the verification of finite failure, in: Proc. Internat. Conf. Principles and Practice of Declarative Programming, Lecture Notes in Computer Science 1702, Springer, Berlin, 1999, pp. 311-327.
[14] R. Gori, An abstract interpretation approach to termination of logic programs, in: Proc. 7th Internat. Conf. on Logic for Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, Vol. 1955, Springer, Berlin, 2000, pp. 362-380.
[15] R. Gori, An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations, Theoretical Computer Science 290, 2003, pp. 863-936.
[16] J. Jaffar, M. J. Mather, Constraint logic programming: A survey, Journal of Logic
Programming 19-20, 1994, pp. 503-582.
[17] N. Lavarac, S. Dzeroski, Inductive Logic Programming: Techniques and Applications, Ellis Horwood, 1993.
[18] J.W. Lloyd, Foundations of Logic Programming, 2nd Edition, Springer, Berlin, 1987.
[19] S. Muggleton, Inductive logic programming, New Generation Computing 8(4), 1991, pp. 295-318.
[20] A. Van Gelder, K. Ross, J. Schlipf, Well-founded semantics for general logic programs, J.ACM 38(3), 1991, pp. 620-650.
[2] K.R. Apt, Introduction to logic programming, Vol. B: Formal Models and Semantics of Handbook of Theoretical Computer Science, Elsevier and The MIT Press, Amsterdam, Cambridge, MA, 1990, pp. 495-574.
[3] K.R. Apt, R. Bol, Logic programming and negation: A survey, Journal of Logic Programming 19-20, 1994, pp. 9-71.
[4] M. Comini, M.C. Meo, Compositionality properties of SLD-derivations, Theoretical Computer Science 211(1-2), 1999, pp. 275-309.
[5] M. Comini, G. Levi, M.C. Meo, A theory of observables for logic programs, Information and Computation 169, 2001, pp. 23-80.
[6] P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proc. 4th ACM Symp. Principles of Programming Languages, 1977, pp.238-252.
[7] P. Cousot, R. Cousot, Systematic design of program analysis frameworks, in: Proc. 6th ACM Symp. Principles of Programming Languages, 1979, pp.269-282.
[8] P. Cousot, R. Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, 13(2-3), 1992, pp. 103-179.
[9] P. Cousot, R. Cousot, Inductive definitions, semantics and abstract interpretation, in: Proc. 19th Annu. ACM Symp. Principles of Programming Languages, 1992, pp. 83-94.
[10] G. File, R. Giacobazzi, F. Ranzato, A unifying view on abstract domain design, ACM Computing Surveys 28(2), 1996, pp. 333-336.
[11] M. Gelfond, V. Lifschitz, The stable model semantics for logic programming, in: Proc. Fifth Int'l Conf. and Symp. Logic Programming, 1988, pp. 1070-1080.
[12] R. Gori, G. Levi, Finite failure is and-compositional, Journal of Logic and Computation 7(6), 1997, pp. 753-776.
[13] R. Gori, G. Levi, On the verification of finite failure, in: Proc. Internat. Conf. Principles and Practice of Declarative Programming, Lecture Notes in Computer Science 1702, Springer, Berlin, 1999, pp. 311-327.
[14] R. Gori, An abstract interpretation approach to termination of logic programs, in: Proc. 7th Internat. Conf. on Logic for Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, Vol. 1955, Springer, Berlin, 2000, pp. 362-380.
[15] R. Gori, An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations, Theoretical Computer Science 290, 2003, pp. 863-936.
[16] J. Jaffar, M. J. Mather, Constraint logic programming: A survey, Journal of Logic
Programming 19-20, 1994, pp. 503-582.
[17] N. Lavarac, S. Dzeroski, Inductive Logic Programming: Techniques and Applications, Ellis Horwood, 1993.
[18] J.W. Lloyd, Foundations of Logic Programming, 2nd Edition, Springer, Berlin, 1987.
[19] S. Muggleton, Inductive logic programming, New Generation Computing 8(4), 1991, pp. 295-318.
[20] A. Van Gelder, K. Ross, J. Schlipf, Well-founded semantics for general logic programs, J.ACM 38(3), 1991, pp. 620-650.