A connection between the Cantor-Bendixson derivative and the well-founded semantics of finite logic programs (Q1926591)

From MaRDI portal
scientific article
Language Label Description Also known as
English
A connection between the Cantor-Bendixson derivative and the well-founded semantics of finite logic programs
scientific article

    Statements

    A connection between the Cantor-Bendixson derivative and the well-founded semantics of finite logic programs (English)
    0 references
    0 references
    0 references
    28 December 2012
    0 references
    Amongst the possible definitions of the well-founded semantics of a finite logic program \(P\) (a finite set of formulas of the form \(B\rightarrow\alpha\) where \(B\) is a conjunction of literals and \(\alpha\) is an atom), the one given by Van Gelder is most relevant to this paper, and goes as follows. Given a subset \(M\) of the set \(H(P)\) of all ground instances of atoms occurring in \(P\), \(GL_M(P)\), the Gelfond-Lifschitz reduct of the set \(ground(P)\) of closed instances of the members of \(P\) by \(M\), is the Horn program obtained by keeping only the members of \(ground(P)\) whose bodies do not contain the negation of a member of \(M\), and deleting in them all negated atoms (which are all true in \(M\)). A Horn program \(P\) has a least model \(LM(P)\), which is the set of closed atoms that are logical consequences of \(P\). Inductively define two sets \(\mathbb F_\alpha(P)\) and \(\mathbb T_\alpha(P)\) of atoms, for all ordinals \(\alpha\), as follows. Set \(\mathbb F_0(P)=\varnothing\) and \(\mathbb T_0(P)=LM(GL_{H(P)}(P))\). For all ordinals \(\alpha\), set \(\mathbb F_{\alpha+1}(P)=\overline{\mathbb T_\alpha(P)}\) and \(\mathbb T_{\alpha+1}(P)=LM(GL_{\overline{\mathbb F_\alpha(P)}}(P))\). For all limit ordinals \(\lambda\), set \(\mathbb F_\lambda(P)=\bigcup_{\alpha<\lambda,\alpha\text{ even}}\mathbb F_\alpha(P)\) and \(\mathbb T_\lambda(P)=LM(GL_{\overline{\mathbb T_\lambda(P)}}(P))\). Then the (3-valued) well-founded model of \(P\) consists of the negations of the atoms in \(\mathbb F_\alpha(P)\) and the atoms in \(\mathbb T_\alpha(P)\) where \(\alpha\) is the least ordinal with \(\mathbb F_\alpha(P)=\mathbb F_{\alpha+1}(P)\). The Cantor-Bendixson derivative of a subset \(Q\) of the Baire space \(2^\omega\) is defined as the set \(D(Q)\) of non-isolated members of \(Q\), that is, the set of members \(x\) of \(Q\) such that for all open sets \(U\) (for the topology over \(2^\omega\) generated by the sets of the form \(I[\tau]\) consisting of all members of \(2^\omega\) that extend \(\tau\) where \(\tau\) belongs to the set \(\{0,1\}^\ast\) of finite sequences of 0's and 1's), \(Q\cap U\neq\{x\}\). The perfect kernel of \(Q\) is defined as the intersection of all sets \(D^\alpha(Q)\), for all ordinals \(\alpha\), inductively defined as follows. Set \(D^0(Q)=Q\). For all ordinals \(\alpha\), set \(D^{\alpha+1}(Q)=D(D^\alpha(Q))\). For all limit ordinals \(\lambda\), set \(D^\lambda(Q)=\bigcap_{\alpha<\lambda}D^\alpha(Q)\). The paper establishes a relationship between the well-founded semantics of finite logic programs and the Cantor-Bendixson derivative as follows. Consider an effective enumeration \((T_e)_{e\in\mathbb N}\) of all primitive recursive trees over \(2^\omega\) (that is, subsets of \(\{0,1\}^\ast\) closed under subsequences), which defines an effective enumeration of all \(\Pi^0_1\) classes over \(2^\omega\), with \(T_e\) being associated with the \(\Pi^0_1\) set \([T_e]\) of all members \(x\) of \(2^\omega\) such that for all \(n\in\mathbb N\), the restriction of \(x\) to \(\{0,\dots,n\}\) belongs to \(T_e\). Then for all \(e\in\mathbb N\), a finite logic program \(P_e\) is defined such that for all non-successor ordinals \(\lambda\) and for all \(n\in\mathbb N\), \[ \mathbb T_{\lambda+2n}(P_e)=\bigl\{\sigma\in\{0,1\}^\ast\mid I[\tau]\cap D^{\lambda+n}([T_e])\bigr\}=\varnothing. \] As a consequence of this relationship, some complexity results about the well-founded semantics are derived, and in particular the following. Let \((PE_e)_{e\in\mathbb N}\) be an effective enumeration of all finite logic programs. Then: {\parindent=6mm \begin{itemize}\item[-] The set of all \(e\in\mathbb N\) such that the well-founded model of \(P_e\) contains no atom is \(\Pi^0_2\) complete; \item[-] the set of all \(e\in\mathbb N\) such that the well-founded model of \(P_e\) contains no negated atom is \(\Pi^0_3\) complete; \item[-] the set of all \(e\in\mathbb N\) such that the well-founded model of \(P_e\) is equal to the least model of its Horn part (hence contains nothing but non-negated atom) is \(\Pi^0_2\) complete. \end{itemize}}
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    logic program
    0 references
    well founded semantics
    0 references
    Cantor-Bendixon derivative
    0 references
    0 references