# safe_inductions_an_algebraic_study__7000d3be.pdf Safe Inductions: An Algebraic Study Bart Bogaerts and Joost Vennekens and Marc Denecker KU Leuven, Department of Computer Science Celestijnenlaan 200A, Leuven, Belgium In many knowledge representation formalisms, a constructive semantics is defined based on sequential applications of rules or of a semantic operator. These constructions often share the property that rule applications must be delayed until it is safe to do so: until it is known that the condition that triggers the rule will remain to hold. This intuition occurs for instance in the well-founded semantics of logic programs and in autoepistemic logic. In this paper, we formally define the safety criterion algebraically. We study properties of so-called safe inductions and apply our theory to logic programming and autoepistemic logic. For the latter, we show that safe inductions manage to capture the intended meaning of a class of theories on which all classical constructive semantics fail. 1 Introduction In many fields of computational logic, natural forms of induction show up. Such an induction can be seen as a sequence of semantic structures obtained by iterative applications of rules or a semantic operator. For instance, in logic programming, it is natural to think of sequences of interpretations where at each stage a number of rules whose bodies are satisfied are triggered (i.e., their head is added to the current interpretation). For positive logic programs, all such sequences converge to the minimal model. For non-positive programs, this strategy may yield meaningless results. For instance, for the program P = {a, b a}, one such sequence is , {b}, {b, a}, the limit of which is not even a supported model of the logic program. Intuitively, what is wrong here is that the rule b a is applied before the value of a is established. For stratified programs, like P, this problem has been resolved [Apt et al., 1988]. For the general case, the well-founded semantics [Van Gelder et al., 1991] offers a solution that uses three-valued interpretations instead of twovalued interpretations. In recent work, the notions of natural and safe inductions for inductive definitions were introduced [Denecker and Vennekens, 2014; Denecker et al., 2017]. It was argued that this Bart Bogaerts is a postdoctoral fellow of the Research Foundation Flanders (FWO). kind of processes forms the essence of our understanding of inductive definitions. In this paper, we lift those ideas to a more general setting: we provide a principled study of inductions in approximation fixpoint theory (AFT) (Denecker, Marek and Truszczy nski (DMT) 2000), an algebraic theory that provides a unifying framework of semantics of nonmonotonic logics. We show convergence of safe inductions in general and study the relationship between safe inductions and various fixpoints defined in approximation fixpoint theory. By presenting our theory in AFT, our results are broadly applicable. DMT [2000] originally developed AFT to unify semantics of logic programs, autoepistemic logic and default logic. Later, it was also used to define semantics of extensions of logic programs, such as HEX logic programs [Antic et al., 2013] and an integration of logic programs with description logics [Liu et al., 2016]. Strass [2013] showed that many semantics from Dung s argumentation frameworks (AFs) [Dung, 1995] and abstract dialectical frameworks (ADFs) [Brewka et al., 2013] can be obtained by direct applications of AFT. Cruz-Filipe [2016] and Bogaerts and Cruz-Filipe [2017] showed that AFT has applications in database theory, for defining semantics of active integrity constraints [Flesca et al., 2004]. The theory we present in this paper induces for each of the above logics notions of (safe) inductions and a safe semantics. Our complexity results are obtained for general operators and hence can also be transfered to various logics of interest. Throughout the paper, we give examples from logic programming; in Section 6, we apply our theory to autoepistemic logic. There, we show that safe inductions induce a constructive semantics that captures the intended semantics of a class of theories for which classical constructive semantics fail. This failure was recently exposed and solved using a notion of set-inductions which is based on sets of lattice elements instead of intervals (which are standard in AFT) [Bogaerts et al., 2016]. We show that safe inductions provide an alternative solution to this problem. Our solution is more direct: in contrast to set-inductions or well-founded inductions [Denecker and Vennekens, 2007], safe inductions do not require any form of approximation; they are sequences in the original lattice. For logic programming, this means that they are sequences of interpretations such that some atoms are derived in each step. For AEL, this means that they are Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) sequences of possible world structures such that additional knowledge is derived in each step. 2 Preliminaries: Lattices and Operators A partially ordered set (poset) L, is a set L equipped with a partial order , i.e., a reflexive, antisymmetric, transitive relation. We write x < y for x y x = y. We call L, a complete lattice if every subset S of L has a least upper bound W S and a greatest lower bound V S. A complete lattice has a least element and a greatest element . We use notations x y = W({x, y}) and x y = V({x, y}). An operator O : L L is monotone if x y implies that O(x) O(y). An element x L is a prefixpoint, a fixpoint, a postfixpoint of O if O(x) x, respectively O(x) = x, x O(x). Every monotone operator O in a complete lattice has a least fixpoint [Tarski, 1955], denoted lfp(O), which is also O s least prefixpoint and the limit of any monotone induction, i.e., of any increasing sequence (xi)i 0 satisfying x0 = , xi xi+1 O(xi), for successor ordinals i + 1, xλ = W({xi | i < λ}), for limit ordinals λ. Logic Programming Let Σ be an alphabet, i.e., a collection of symbols which are called atoms. A logic program P is a set of rules r of the form h ϕ, where h is an atom called the head of r, denoted head(r), and ϕ is a conjunction of literals called the body of r, denoted body(r). An interpretation I of Σ is a subset of Σ. The set of interpretations 2Σ forms a lattice equipped with the order . The truth value (t or f) of a propositional formula ϕ in a structure I, denoted ϕI, is defined as usual. With a logic program P, we associate an immediate consequence operator TP [van Emden and Kowalski, 1976] that maps a structure I to the structure {p Σ | r P : head(r) = p body(r)I = t}. This is an operator on the lattice 2Σ, . 3 Safe Inductions Let L be a lattice and O an operator on L, fixed throughout the rest of this paper. Definition 3.1. We call y L derivable from x L if x y x O(x). Definition 3.2. Let x be an element of L. An O-induction in x is a sequence (xi)i β such that x0 = x, xi+1 is derivable from xi for each i < β, xλ = W({xi | i < λ}), for limit ordinals λ β. Intuitively, we view O as an operator that constructs certain lattice points. An O-induction is the associated construction process. Intuitively, if we are at a stage xi, O(xi) represents what can be concluded from this given stage. Therefore, the next step xi+1 in the induction is at least xi (xi+1 xi) and at most the combination of xi and what can be concluded from it (xi+1 xi O(xi)). In the context of a powerset lattice (a lattice of the form 2S, ), this means that xi+1 xi O(xi), i.e., xi+1 only contains elements that were already in xi or such that O concludes them from xi. Definition 3.3. Let N = (xi)i β and N = (yi)i α be two O-inductions. We say that N extends N if α β and xi = yi for all i β. The extension is strict if yα = xβ. Definition 3.4. An O-induction is terminal if there exists no O-induction that strictly extends it. Proposition 3.5. An O-induction (xi)i β is terminal if and only if xβ is a prefixpoint of O. Proposition 3.6. If O is monotone, all monotone inductions are O-inductions in and vice versa. Corollary 3.7. If O is monotone, all terminal O-inductions in converge to lfp(O). There is a high degree of non-determinism in O-inductions. For monotone operators O, despite this non-determinism, all O-inductions converge to the same point. As such, Oinductions provide (if O is monotone) a way to construct an intended lattice point (lfp O). For non-monotone operators, the situation is quite different: O-inductions might not converge to a single point. Example 3.8. Let P be the logic program This is a simple, stratified logic program [Apt et al., 1988; Przymusinski, 1988]. Its intended fixpoint (its so-called perfect model) is {p}. Let TP denote its immediate consequence operator. The following are the three terminal strict TPinductions in = . N1 = ( , {q}, {p, q}) N2 = ( , {p, q}) N3 = ( , {p}) In Example 3.8 it can be seen that certain derivations in an O-induction happen prematurely. For instance, in N1 and N2, q is derived by the non-monotonic rule q p. As soon as p is derived, this rule no longer applies: q TP({p, q}) = {p}. In this sequence, the rule was applied when it was not safe to do so. Below, we define a notion of safety to avoid such premature derivations, i.e., to only derive facts that remain derivable, regardless of what other derivations are made further on in the induction process. Definition 3.9. Let x be derivable from x. We say that x is safely derivable from x if for each O-induction (xi)i β in x, it holds that x x O(xβ). An O-induction (xi)i β is safe if xi+1 is safely derivable from xi for each i < β. In words, x is safely derivable from x if no matter what other derivations we make (ending up in xβ), x consists at most of what we have in x combined with what O concludes from xβ, i.e., x x O(xβ). An induction is terminal if it cannot be extended into a strictly larger induction. We define a similar concept for safe inductions. Definition 3.10. A safe O-induction N is safe-terminal if there exists no strict extension N of N that is safe. In Example 3.8, we showed that not all terminal Oinductions converge to the same lattice point. Luckily, the safety criterion warrants a better situation. Theorem 3.11. For each x L, all safe-terminal Oinductions in x converge to the same lattice point. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) In order to prove this theorem, we use the following result. Lemma 3.12. Let N = (xi)i β, N = (yi)i γ be two safe O-inductions with x0 = y0. For every i β, j γ it holds that if i+1 β then xi+1 yj is safely derivable from xi yj and if j+1 γ then xi yj+1 is safely derivable from xi yj. Proof of Theorem 3.11. Let N = (xi)i β and N = (yi)i γ be two safe-terminal O-inductions. Consider the sequence (zi)i β+γ where zi = xi if i β and zβ+i = xβ yi if i γ. By Lemma 3.12, this sequence is a safe O-induction. Since N is safe-terminal, this sequence cannot be a strict extension of N and hence xβ yγ = zβ+γ = xβ, i.e., yγ xβ. A symmetric argument shows that xβ yγ, hence xβ = yγ, as desired. Definition 3.13. The safely defined point by O, denoted safe(O) is the limit of all safe-terminal O-inductions in . By Theorem 3.11, the safely defined point is well-defined. We now study some properties of the safely defined point. Proposition 3.14. For any operator O, safe(O) is a postfixpoint of O, i.e., safe(O) O(safe(O)). Example 3.15. Consider a lattice { , } with two elements and an operator O that maps to and to . The safely defined point by O is , since is not safely derivable ( O( )). Here, the O-induction N = ( ) is safe-terminal, but not terminal. Definition 3.16. We call an operator O complete if the safely defined point by O is a fixpoint of O, i.e., if O(safe(O)) = safe(O). We will be mostly interested in complete operators O, as they uniquely determine a fixpoint of interest of O. Proposition 3.17. An operator O is complete if and only if every safe-terminal O-induction in is terminal. Proposition 3.18. If O is a monotone operator, then O is complete and safe(O) = lfp(O). Theorem 3.11 shows that safe O-inductions, despite their non-determinism, uniquely determine a lattice point of interest. Furthermore, if O is monotone, this point is the least fixpoint of O. The question now arises: what if O is nonmonotone? How does the safely defined point by O relate to other points of interest? In particular, how does it relate to fixpoints defined in approximation fixpoint theory? We study this in Section 5. First, we study complexity. Complexity The height of a finite lattice L is the length n of the longest sequence = x0 < x1 < < = xn in L. We call y L a direct successor of x L if x < y and there is no z such that x < z < y. The branching width of a finite L is the maximum over x L of the number of direct successors of x. All complexity results presented below are in terms of the sum of the branching width and the height of the input lattice. This means that we use the sum of the branching width and the height as the measure of our input. In this section, we assume that a class C = { L, O } of pairs of a finite lattice L and an operator O : L L is given. Let FC denote the function problem: given one of the L, O in C and p, p L, compute (1) O(p), (2) p p , and (3) {x | x is a direct successor of p}. We assume that FC can be solved in polynomial time. The kind of setting used here is not so unusual: it is an algebraic variant of data complexity. For instance, in logic programming, each non-ground program P determines a class of lattices and associated operators (immediate consequence operators of the groundings of P with respect to a given domain). The height and branching width of the lattice are then polynomial in terms of the domain size. In this setting, the problem FCP is indeed polynomially solvable. Theorem 3.19. Let C be a class as above. The decision problem given Li C, x, y Li, is y safely derivable from x by Oi? is in co-NP. Sketch of the proof. To prove this, we build a program that nondeterministically traverses an O-induction from x. To determine that y is not safely derivable from x, it suffices to find one run of the algorithm such that y x O(s) with s a state in in the O-induction. Such algorithm runs in polynomial time in the height of the lattice. Theorem 3.20. Let C be a class as above. The decision problem given L, O C, s L, is safe(O) s? is in ( P 2 ). For some classes C, this problem is co-NP-hard. Sketch of the proof. Containment follows from Theorem 3.19. Hardness follows from Theorem 6.10 of Denecker et al. [2017]. 4 Preliminaries: AFT Given a lattice L, approximation fixpoint theory makes use of the lattice L2. We define projections for pairs as usual: (x, y)1 = x and (x, y)2 = y. Pairs (x, y) L2 are used to approximate all elements in the interval [x, y] = {z | x z z y}. We call (x, y) L2 consistent if x y. We use Lc to denote the set of consistent elements. Elements (x, x) Lc are called exact. We sometimes use the tuple (x, y) and the interval [x, y] interchangeably. The precision ordering on L2 is defined as (x, y) p (u, v) if x u and v y. In case (u, v) is consistent, this means that (x, y) approximates all elements approximated by (u, v), or in other words that [u, v] [x, y]. If L is a complete lattice, then L2, p is also a complete lattice. AFT studies fixpoints of lattice operators O : L L through operators approximating O. An operator A : L2 L2 is an approximator of O if it is p-monotone, and O(x) A(x, x) for all x L. Approximators map Lc into Lc. As usual, we restrict our attention to symmetric approximators: approximators A such that for all x and y, A(x, y)1 = A(y, x)2. DMT [2004] showed that the consistent fixpoints of interest (defined below) are uniquely determined by an approximator s restriction to Lc, hence, sometimes we only define approximators on Lc. AFT studies fixpoints of O using fixpoints of A. The AKripke-Kleene fixpoint is the p-least fixpoint of A and has the property that it approximates all fixpoints of O. A partial A-stable fixpoint is a pair (x, y) such that x = lfp(A( , y)1) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) and y = lfp(A(x, )2), where A( , y)1 denotes the operator L L : x 7 A(x, y)1 and analogously for A(x, )2. The A-well-founded fixpoint is the least precise partial A-stable fixpoint. An A-stable fixpoint of O is a fixpoint x of O such that (x, x) is a partial A-stable fixpoint. This is equivalent to the condition that x = lfp(A( , x)1). A-stable fixpoints are minimal fixpoints of O. The A-Kripke-Kleene fixpoint of O can be constructed by iterative applications of A, starting from ( , ). For the A-well-founded fixpoint, a similar constructive characterization has been worked out. Definition 4.1. An A-refinement of (x, y) is a pair (x , y ) L2 satisfying one of the following two conditions: (x, y) p (x , y ) p A(x, y), or x = x and A(x, y )2 y y. An A-refinement is strict if (x, y) = (x , y ). Definition 4.2. A well-founded induction of A is a sequence (xi, yi)i β with β an ordinal such that (x0, y0) = ( , ); (xi+1, yi+1) is an A-refinement of (xi, yi), for all i < β; (xλ, yλ)= W p{(xi, yi)|i < λ} for limit ordinals λ β. A well-founded induction is terminal if its limit (xβ, yβ) has no strict A-refinements. Denecker and Vennekens [2007] showed that all terminal A-inductions converge to the A-well-founded fixpoint of O. Logic Programming For logic programming, DMT showed that Fitting s immediate consequence operator ΨP [Fitting, 2002] is an approximator of TP, that the ΨP-wellfounded fixpoint is the well-founded model of P [Van Gelder et al., 1991] and that ΨP-stable fixpoints are the stable models of P [Gelfond and Lifschitz, 1988]. 5 Safe Inductions and AFT In this section, we study how (safe) O-inductions relate to the fixpoints studied in AFT. Theorem 5.1. Let O be an operator and A an approximator of O. The A-well-founded fixpoint approximates the safely defined point by O. The proof makes use of the following proposition. Proposition 5.2. Let O be an operator and A an approximator of O. Let (xi, yi)i β be an A-well-founded induction. The following claims hold: (1) (xi)i β is a safe O-induction, and (2) for each i β and each O-induction N = (zj)j α with z0 = xi, it holds that zα yβ Proof of Theorem 5.1. Let z denote the safely defined point of O and let (xβ, yβ) denote the A-well-founded fixpoint of O. For any terminal A-well-founded induction (xi, yi)i β, it holds that xβ z by the first point of Proposition 5.2. Furthermore, by the second point of Proposition 5.2 it holds that any O-induction stays under yβ; hence z yβ. Theorem 5.1 has several consequences. Corollary 5.3. If the A-well-founded fixpoint of O is exact, i.e., equal to (x, x) for some x L, then O is complete and safe(O) = x. Corollary 5.4. Let O be an operator and A an approximator of O. The A-Kripke-Kleene fixpoint of O approximates the safely defined point by O. Corollary 5.5. If the A-Kripke-Kleene fixpoint of O is exact, i.e., equal to (x, x) for some x L, then O is complete and safe(O) = x. Safe O-inductions identify a unique lattice point of interest. Since an operator can have multiple stable fixpoints, we cannot expect a strong link between the safely defined point and stable fixpoints. However, we do find the following relation between stable fixpoints and O-inductions. Theorem 5.6. Let A be an approximator of O. If x is an A-stable fixpoint of O, then x is the limit of a terminal Oinduction. Sketch of the proof. If x is an A-stable fixpoint of O, then x = lfp(A( , x)1). The clue to proving this proposition is to show that monotone inductions of A( , x)1 are O-inductions. The result then easily follows. Example 5.7. Consider the logic program P = { p q, q p } It holds that {p} is a stable model of P (a ΨP-stable fixpoint of TP). Also, {p} is the limit of the TP-induction ( , {p}). This induction is not safe since ( , {q}) is also a TP-induction and {p} TP({q}) = {q}. The limit of a terminal O induction is not always a stable fixpoint of O (for some approximator A), as we show below. Example 5.8. Consider the logic program P = p p, p q, q p, q q In this case ( , {q}, {q, p}) is the unique terminal TPinduction. It can be verified that this is a safe induction and that TP is complete. The safely defined point is a nonminimal fixpoint of TP, hence it is also non-grounded (see [Bogaerts et al., 2015]) and not an A-stable fixpoint for any approximator A of TP. In the well-founded model of P, all atoms are unknown. 6 Safe Inductions and Autoepistemic Logic Recently Bogaerts et al. [2016] exposed a problem in several semantics of autoepistemic logic (AEL). They showed that for very simple, stratified theories, the well-founded and other semantics fail to identify the intended model. They solved this problem by defining, algebraically, a new constructive semantics that is based on a refined notion of approximations of a lattice point (more refined than intervals, i.e., elements of L2). In this section, we show that safe inductions provide a direct solution to the aforementioned problem without the need for any approximation. First, we recall some background on AEL. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) 6.1 AFT and Autoepistemic Logic AEL is a non-monotonic logic for modeling the beliefs or knowledge of a rational agent with perfect introspection capabilities [Moore, 1985]. Let L be the language of propositional logic based on a set of atoms Σ. Extending this language with a modal operator K, which is read I (the agent) know 1, yields a language LK of modal propositional logic. An autoepistemic theory is a set of formulas in LK. A crucial assumption about such theories that distinguishes this logic from the standard modal logic S5 is that all of the agent s knowledge is encoded in the theory: it either belongs to the theory, or can be derived from it. Levesque [1990] called this the all I know assumption . A modal formula is a formula of the form Kψ; an objective formula is a formula without modal subformulas. If ϕ is a formula, At(ϕ) denotes the set of all atoms that occur in ϕ and At O(ϕ) the set of all atoms that occur objectively in ϕ, i.e., outside of the scope of an operator K. An interpretation is a subset of Σ. A possible world structure is a set of interpretations. A possible world structure can be seen as a Kripke structure in which the accessibility relation is total. The set of all possible world structures is denoted WΣ; it forms a lattice with the knowledge order k such that Q k Q iff Q Q . A possible world structure Q is a mathematical object to represent all situations that are possible according to the agent: interpretations q Q represent possible states of affairs, i.e., states of affairs consistent with the agent s knowledge, and interpretations q Q represent impossible states of affairs, i.e., states of affairs that violate the agent s knowledge. If ϕ is a formula in LK, Q is a possible world structure and I is an interpretation, satisfaction of ϕ with respect to Q and I (denoted Q, I |= ϕ) is defined as in the modal logic S5 by the standard recursive rules of propositional satisfaction augmented with one additional rule: Q, I |= Kϕ if Q, I |= ϕ for every I Q. In this formula, Q represents the belief of the agent and I represents the actual state of the world. Modal formulas are evaluated with respect to the agent s belief, while objective formulas are evaluated with respect to the state of the actual world. We furthermore define Q |= Kϕ (ϕ is known in Q) if Q, I |= ϕ for every I Q. Moore [1985] associated with every theory T an operator DT on WΣ as follows: DT (Q) = {I WΣ | Q, I |= T }. The intuition behind this operator is that DT (Q) is a revision of Q consisting of all worlds that are consistent with the agent s current beliefs (Q) and the constraints in T . DMT [2003] defined approximators for DT and showed that AFT induces all main and some new semantics for AFT. Monotonically Stratified AEL Theories Following Vennekens et al. [2006], we call an autoepistemic theory T stratifiable2 w.r.t. a partition (Σi)0 i n of its alphabet if 1Or, following DMT [2011] My knowledge entails . 2As mentioned in the introduction, we restrict to finite stratifications here. there exists a partition (Ti)0 i n of T such that for each i, At O(Ti) Σi and At(Ti) S 0 j i Σj. This notion of stratification significantly extends the notion from Marek and Truszczy nski [1991]. A stratification is modally separated if for every modal subformula Kψ of Ti, either At(ψ) Σi or At(ψ) S 0 j