1 Introduction
Rule-based reasoning is an important component of artificial intelligence. The definite propositional logic programs considered in this paper can be viewed as Horn theories equipped with least-model semantics (Lloyd Reference Lloyd1987; Apt Reference Apt1990, Reference Apt1997; Hodges Reference Hodges1994; Sterling and Shapiro Reference Sterling and Shapiro1994).
Composition and decomposition of logic programs are not new concerns. Standard approaches decompose programs along the dependency structure of their atoms, for example by stratification or strongly connected components in datalog (Ceri et al. Reference Ceri, Gottlob and Tanca1989, Reference Ceri, Gottlob and Tanca1990), and by splitting sets in the non-monotonic setting of answer set programming (Lifschitz and Turner Reference Lifschitz and Turner1994). These approaches operate primarily at the level of rules or program modules, while the internal structure of individual rule bodies remains unchanged. The present work complements this perspective by studying finer-grained operations that manipulate and decompose rule bodies. To our knowledge, existing algebraic approaches do not directly provide the body-level decompositions and corresponding semantic relationships developed here.
The propositional Horn setting studied in this paper is fundamental to logic programming. Grounding transforms first-order programs into propositional ones, possibly over an infinite alphabet, while function-free programs over finite domains lead to finite propositional programs of the kind considered here. Propositional rule representations obtained by grounding are central to answer set programming (Gelfond and Lifschitz Reference Gelfond and Lifschitz1991; Marek and Truszczyński Reference Marek and Truszczyński1999) (see also Baral (Reference Baral2003); Brewka et al. (Reference Brewka, Eiter and Truszczyński2011); Lifschitz (Reference Lifschitz2019)) and to datalog (Ceri et al. Reference Ceri, Gottlob and Tanca1989, Reference Ceri, Gottlob and Tanca1990). Closely related structures are studied as propositional Horn theories in knowledge representation and reasoning.
The idea of introducing algebraic structure into programming dates back at least to the work of John Backus (Backus Reference Backus1978), who advocated algebraic methods for constructing and reasoning about programs. In logic programming, algebraic and compositional perspectives have been developed extensively in connection with modularity and program composition (O’Keefe Reference O’Keefe1985; Mancarella and Pedreschi Reference Mancarella and Pedreschi1988; Hirani and Subrahmanian Reference Hirani and Subrahmanian1990; Bossi et al. Reference Bossi, Bugliesi, Gabbrielli, Levi and Meo1996; Brogi et al. Reference Brogi, Mancarella, Pedreschi and Turini1990, Reference Brogi, Lamma and Mello1992a, Reference Brogi, Mancarella, Pedreschi and Turini1992b; Dong Reference Dong1988; Gaifman and Shapiro Reference Gaifman and Shapiro1989; Dong and Ginsburg Reference Dong and Ginsburg1990; Ioannidis and Wong Reference Ioannidis and Wong1991; Brogi et al. Reference Brogi, Mancarella, Pedreschi and Turini1994; Bugliesi et al. Reference Bugliesi, Lamma and Mello1994; Hill and Lloyd Reference Hill and Lloyd1994; Brogi and Turini Reference Brogi and Turini1995). The present approach is complementary to this work in that it manipulates the bodies of individual rules directly. The set-like operations introduced below enrich the algebra based on sequential composition (Antić Reference Antić2024d), which is recalled in Section 2.2.3. This paper also forms part of a broader line of work on algebraic methods for logic program synthesis and transformation (Antić Reference Antić2014, Reference Antić2024c, Reference Antić2024d, Reference Antić2025).
We introduce a family of set-like operations on propositional Horn logic programs and study their algebraic laws, their interaction with sequential composition, and their relationship to least-model semantics. A rule has the form
$a\leftarrow B$
, where
$a$
is an atom from a finite alphabet
$A$
and
$B\subseteq A$
is its body. The body may be empty, in which case the rule is a fact. For rules with the same head, the operations introduced in this paper are modeled on the familiar set operations
$\cup$
,
$\cap$
,
${}^c$
,
$-$
,
$\mathrel {\triangle }$
, and
$\mathfrak P$
:
These operations are extended to programs by combining rules with the same head. We refer to them as body-union, body-intersection, body-complement, body-subtraction, body-symmetric-difference, and body-power-set, respectively.
Although these operations are modeled on classical set operations, their behavior at the program level is more subtle. In particular, if a program contains several rules with the same head, body-union and body-intersection need not be idempotent, and familiar distributivity laws may hold only as inclusions, modulo subsumption equivalence, or under additional minimality assumptions. We determine a number of such laws and study how the operations interact with reducts, sequential composition, supported models, and least models. We also show that body-union induces a well-defined operation on subsumption-equivalence classes and yields, together with sequential composition, a seminearring structure on the resulting quotient.
The main technical contribution concerns decomposition into Krom programs, that is, programs whose rules contain at most one body atom. Let
$M$
be a minimalist program, meaning that it contains at most one rule for each rule head, and let
$m=\max \{1,w(M)\}$
, where
$w(M)$
is the maximal number of body atoms occurring in a rule of
$M$
. The Minimalist Decomposition Theorem shows that there are Krom programs
$K_1,\ldots ,K_m\subseteq M^\lor$
such that
\begin{align*} M &= K_1\sqcup \ldots \sqcup K_m \end{align*}
and
\begin{align*} M^\omega &= K_1^\omega \sqcup \ldots \sqcup K_m^\omega = K_1^\omega \cap \ldots \cap K_m^\omega , \end{align*}
where
${}^\omega$
denotes the least-model operator and
$M^\lor$
is the Krom program obtained by replacing each proper rule by its one-atom body components. Thus, both the program and its least model admit compatible representations in terms of Krom components. This is a structural existence and representation result rather than, by itself, an independent algorithm for computing
$M^\omega$
.
For an arbitrary program
$P$
, rules with the same head may interact under body-union and produce additional rules. Exact syntactic and semantic reconstruction can therefore no longer be guaranteed. Nevertheless, the Decomposition Theorem provides Krom programs
$K_1,\ldots ,K_m\subseteq P^\lor$
, where
$m=\max \{1,w(P)\}$
, satisfying
\begin{align*} P &\subseteq K_1\sqcup \ldots \sqcup K_m \end{align*}
and
\begin{align*} P^\omega &\subseteq K_1^\omega \sqcup \ldots \sqcup K_m^\omega = K_1^\omega \cap \ldots \cap K_m^\omega . \end{align*}
The distinction between exact decomposition for minimalist programs and approximation for arbitrary programs reflects the additional combinations created by rules sharing the same head.
Krom programs provide particularly simple components because sequential composition is associative when the left factor is Krom and distributes from the left over program union, whereas these properties fail for arbitrary programs. The decomposition results therefore express complex programs in terms of components with better algebraic behavior and may support further work on compositional reasoning, program transformation, and program construction.
In the final section, we sketch possible applications of the proposed operations to automatic logic programming (Deville and Lau Reference Deville and Lau1994), including inductive logic programming (ILP), learning from interpretation transitions, and analogical logic programming. Further work may investigate extensions to first-order and higher-order programs and to non-monotonic programs under stable-model and answer-set semantics.
2 Preliminaries
In this section, we recall some basic algebraic structures Section 2.1 occurring in the paper, and the syntax and semantics of (propositional Horn) logic programs Section 2.2.
2.1 Algebraic structures
A permutation of a set
$A$
is any mapping
$A\to A$
which is one-to-one and onto.
We denote the composition of two functions
$f:A\to A$
and
$g:A\to A$
by
$f\circ g$
with the usual definition
$(f\circ g)(x)=f(g(x))$
.
We call a binary relation
$\leq$
reflexive if
$x\leq x$
, anti-symmetric if
$x\leq y$
and
$y\leq x$
implies
$x=y$
, and transitive if
$x\leq y$
and
$y\leq z$
implies
$x\leq z$
, for all
$x,y,z$
. A partially ordered set (or poset) is a set
$L$
together with a reflexive, transitive, and anti-symmetric binary relation
$\leq$
on
$L$
. A prefixed point of an operator
$f$
on a poset
$L$
is any element
$x\in L$
such that
$f(x)\leq x$
; moreover, we call any
$x\in L$
a fixed point of
$f$
if
$f(x)=x$
.
We now turn to algebras consisting of a set together with a binary operation (Howie Reference Howie2003). A magma is a set
$M$
together with a binary operation
$\cdot$
on
$M$
. We call
$(M,\cdot ,1)$
a unital magma if it contains a unit element 1 such that
$1a=a1=a$
holds for all
$a\in M$
. A semigroup is a magma
$(S,\cdot )$
in which
$\cdot$
is associative. A monoid is a semigroup containing a unit element.
A left (resp., right) zero is an element
$0$
such that
$0a=0$
(resp.,
$a0=0$
) holds for all
$a$
.
An equivalence relation
$\sim$
on
$S$
is called left (resp., right) compatible with the operation on
$S$
if
$x \sim y$
implies
$zx \sim zy$
(resp.,
$xz \sim yz$
), for all
$x, y, z$
$\in$
$S$
. A left (resp., right) compatible equivalence relation is called a left (resp., right) congruence, and an equivalence relation which is both a left and a right congruence is called a congruence. Given an equivalence relation
$\sim$
, we denote the equivalence class of an element
$a$
with respect to
$\sim$
by
$[a]_\sim$
.
A bimonoid (Droste et al. Reference Droste, Stüber and Vogler2010) is a structure
$(M,+,\cdot ,0,1)$
such that
$(M,+,0)$
and
$(M,\cdot ,1)$
are both monoids. A bimonoid is a strong bimonoid if the operation
$+$
is commutative and
$0$
acts as multiplicative zero, that is,
$a\cdot 0 = 0\cdot a = 0$
for every
$a\in M$
.
A seminearring (van Hoorn and van Rootselaar Reference van Hoorn and van Rootselaar1967; Golan Reference Golan1999) is a set
$S$
together with two binary operations
$+$
and
$\cdot$
on
$S$
, and a constant
$0\in S$
, such that
$(S,+,0)$
is a monoid and
$(S,\cdot )$
is a semigroup satisfying the following laws, for all
$a,b,c\in S$
:
\begin{align} (a+b)\cdot c &= (a\cdot c) + (b\cdot c)\quad \text{(right-distributivity)} \end{align}
\begin{align} 0\cdot a &= 0\quad \text{(left zero).} \end{align}
We say that
$S$
is idempotent if
$a+a=a$
holds for all
$a\in S$
. Typical examples of seminearrings are given by the set of all mappings on a monoid together with composition of mappings, point-wise addition of mappings, and the zero function.
A semiring is a seminearring
$(S,+,\cdot ,0)$
such that
$+$
is commutative and additionally to the laws of a seminearring the following laws are satisfied, for all
$a,b,c\in S$
:
\begin{align*} a\cdot (b+c) &= (a\cdot b) + (a\cdot c)\quad \text{(left-distributivity)}\\ a\cdot 0 &= 0\quad \text{(right zero)}. \end{align*}
For example,
$(\mathbb N,+,\cdot ,0)$
and
$(2^A,\cup ,\cap ,\emptyset )$
are semirings. A characteristic feature of semirings (as opposed to rings) is that addition needs not be invertible.
2.2 Logic programs
We shall now recall the syntax Section 2.2.1 and least model semantics Section 2.2.2 of (propositional Horn) logic programs (Apt Reference Apt1990) and their sequential composition Section 2.2.3.
2.2.1 Syntax
In the rest of the paper,
$A$
denotes a finite alphabet of propositional atoms.
A (propositional Horn logic) program over
$A$
is a finite set of rules of the form
\begin{align} a\leftarrow b_1,\ldots ,b_k,\quad k\geq 0, \end{align}
where
$a,b_1,\ldots ,b_k\in A$
are propositional atoms, and we denote the set of all programs over
$A$
by
$\mathbb P_A$
. With a slight abuse of notation, we will not distinguish between
$a \leftarrow b_1,\ldots ,b_k$
and
$a \leftarrow \{b_1,\ldots ,b_k\}$
, which will allow us to write the rule as
$a \leftarrow B$
with
$B = \{b_1,\ldots ,b_k\}$
, a notation heavily used in the rest of the paper.
The width of a rule
$r$
is the cardinality of its body,
\begin{align*} w(r) := |b(r)|. \end{align*}
The width of a program
$P$
is defined by
\begin{align*} w(P) := \max \bigl (\{w(r)\mid r\in P\}\cup \{0\}\bigr ). \end{align*}
It will be convenient to define, for a rule
$r$
of the form equation (3) the head and body operators
$h$
and
$b$
as
\begin{align*} h(r) := \{a\} \quad \text{and}\quad b(r) := \{b_1,\ldots ,b_k\} \end{align*}
extended to programs rule-wise.
For any programs
$P$
and
$R$
, we have
\begin{align} h(P\cup R) &= h(P)\cup h(R), \end{align}
\begin{align} b(P\cup R) &= b(P)\cup b(R), \end{align}
which means that the head and body operators are homomorphisms with respect to set union.
A fact is a rule with empty body and a proper rule is a rule which is not a fact. We denote the facts and proper rules in
$P$
by
$ f(P)$
and
$ p(P)$
, respectively. We have
\begin{align*} f(P\cup R) &= f(P)\cup f(R),\\ p(P\cup R) &= p(P)\cup p(R), \end{align*}
which means that the facts and proper rules operators are homomorphisms with respect to set union as well.
We call a rule
$r$
of the form equation (3) Krom
Footnote
1
if it has at most one body atom, and we call a program Krom if it contains only Krom rules. We denote the set of all Krom programs over
$A$
by
$\mathbb K_A$
.
A minimalist program contains at most one rule for each rule head and we denote the set of all minimalist programs over
$A$
by
$\mathbb M_A$
. For example, the program
\begin{align*} &a \leftarrow b\\ &a \leftarrow c \end{align*}
implicitly contains a disjunction as it is logically equivalent to the single rule
\begin{align*} a \leftarrow (b\lor c). \end{align*}
Hence, a program is minimalist iff it does not implicitly contain disjunctions of that form.
The unit program over
$A$
is the minimalist Krom program
\begin{align} 1_A := \{a\leftarrow a\mid a\in A\}. \end{align}
2.2.2 Semantics
An interpretation over
$A$
is any set of atoms from
$A$
and we denote the set of all such interpretations by
$\mathbb I_A$
or simply by
$\mathbb I$
in case
$A$
is understood.
We define the entailment relation, for every interpretation
$I$
, inductively as follows: (i) for an atom
$a$
,
$I{\mathrel |\!=} a$
if
$a\in I$
; (ii) for a set of atoms
$B$
,
$I{\mathrel |\!=} B$
if
$B\subseteq I$
; (iii) for a rule
$r$
of the form equation (3),
$I{\mathrel |\!=} r$
if
$I{\mathrel |\!=} b(r)$
implies
$I{\mathrel |\!=} h(r)$
; and, finally, (iv) for a propositional logic program
$P$
,
$I{\mathrel |\!=} P$
if
$I{\mathrel |\!=} r$
holds for each rule
$r\in P$
. In case
$I{\mathrel |\!=} P$
, we call
$I$
a model of
$P$
and we denote the set of all models of
$P$
by
$Mod(P)$
. The set of all models of
$P$
has a least element with respect to set inclusion called the least model of
$P$
and denoted by
$LM(P)$
.
Define the van Emden-Kowalski operator (van Emden and Kowalski Reference van Emden and Kowalski1976)
$T_P : \mathbb I_A\to \mathbb I_A$
of
$P$
, for every interpretation
$I\in \mathbb I_A$
, by
\begin{align*} T_P(I) := \{a\in A \mid a \leftarrow B\in P,\, B\subseteq I\}. \end{align*}
The van Emden-Kowalski operator is at the core of logic programming since the models of
$P$
coincide with the prefixed points of
$T_P$
with respect to the inclusion ordering thus providing an operational characterization of models:
Theorem 1 van Emden and Kowalski (Reference van Emden and Kowalski1976). An interpretation
$I$
is a model of a program
$P$
iff
$T_P(I)\subseteq I$
, that is,
\begin{align*} Mod(P) = \{I\in \mathbb I_A\mid T_P(I)\subseteq I\}. \end{align*}
We call an interpretation
$I$
a supported model of
$P$
if
$I$
is a fixed point of
$T_P$
and we denote the set of all supported models of
$P$
by
$Supp(P)$
.
We say that
$P$
and
$R$
are subsumption equivalent (Maher Reference Maher1988) — denoted by
$P\approx R$
— if
$T_P = T_R$
. Notice that subsumption equivalence implies that
$P$
and
$R$
have the same models.
The van Emden-Kowalski operator is monotone on the set of all interpretations ordered by set inclusion and its least fixed point computation is given by
\begin{align*} &T_P^0 = \emptyset ,\\ &T_P^{n+1} = T_P(T_P^n),\\ &T_P^\infty = \bigcup _{n\geq 0}T_P^n. \end{align*}
The following constructive characterization of least models is due to van Emden and Kowalski (Reference van Emden and Kowalski1976):
Proposition 2. The least model of a program coincides with the least fixed point of its associated van Emden-Kowalski operator, that is, for any program
$P$
we have
\begin{align} LM(P) = T_P^\infty . \end{align}
2.2.3 Sequential composition
We define the (sequential) composition (Antić Reference Antić2024d) of two programs
$P$
and
$R$
as
\begin{align*} P\circ R := \{a \leftarrow (B_1\cup \ldots \cup B_k) \mid a \leftarrow b_1,\ldots ,b_k\in P,\; b_1 \leftarrow B_1,\ldots ,b_k \leftarrow B_k\in R,\, k\geq 0\}, \end{align*}
which we will usually denote simply by
$PR$
.
For example, we have
\begin{align*} \left \{ \begin{array}{l} a\\ b \leftarrow a\\ c \leftarrow a,b \end{array} \right \}\left \{ \begin{array}{l} a\\ b \leftarrow a\\ \end{array} \right \} = \left \{ \begin{array}{l} a\\ b\\ c \leftarrow a \end{array} \right \}. \end{align*}
Composition satisfies the following identities (among others):
\begin{align} P1 &= 1P = P \end{align}
\begin{align} (P\cup R)Q &= PQ\cup RQ \end{align}
\begin{align} P\emptyset &= f(P) \end{align}
\begin{align} h(P) &= PA. \end{align}
Unfortunately, composition is not associative (Antić Reference Antić2024d, Example 10) and does not distribute from the left over union since
\begin{align} \{a \leftarrow b,c\}(\{b\}\cup \{c\}) = \{a\} \quad \text{whereas}\quad \{a \leftarrow b,c\}\{b\}\cup \{a \leftarrow b,c\}\{c\} = \emptyset . \end{align}
However, for minimalist programs
$M$
and
$N$
, composition is associative in the sense that
\begin{align} (PM)N = P(MN) \end{align}
holds for every program
$P$
(Antić Reference Antić2024d, Theorem 11). The same holds true for a Krom program
$K$
and all programs
$P$
and
$R$
(Antić Reference Antić2024d, Theorem 12), that is,
\begin{align} K(PR) = (KP)R. \end{align}
Moreover, in contrast to the general case (see equation (12) above), Krom programs distribute from the left thus satisfying (Antić Reference Antić2024d, Theorem 12)
\begin{align} K(P\cup R) &= KP\cup KR. \end{align}
Together with the corresponding closure properties, this yields the following structural result:
Proposition 3. The structure
$( \mathbb K_A, \cup , \circ , \emptyset , 1_A )$
forms a seminearring with unit
$1_A$
and the structure
$( \mathbb M_A, \circ , 1_A )$
forms a monoid.
Proof. See (Antić Reference Antić2024d, Theorems 11 and 12).
The van Emden-Kowalski operator
$T_P$
can be represented via composition in the sense that
\begin{align} T_P(I) = PI. \end{align}
This correspondence allows us to directly define concepts in terms of programs instead of the van Emden-Kowalski operator:
Fact 4. An interpretation
$I$
is a model of a program
$P$
iff
$PI\subseteq I$
. Moreover,
$I$
is a supported model of
$P$
iff
$PI=I$
.
Fact 5. Two programs
$P$
and
$R$
are subsumption equivalent iff
$PI=RI$
holds for every interpretation
$I$
.
More specifically, we first define
\begin{align*} P\lesssim R \quad :\Leftrightarrow \quad PI\subseteq RI,\quad \text{for every interpretation $I$}, \end{align*}
and
\begin{align*} P\approx R \quad :\Leftrightarrow \quad P\lesssim R \quad \text{and}\quad R\lesssim P. \end{align*}
We clearly have
\begin{align} P\lesssim R \quad \Rightarrow \quad LM(P)\subseteq LM(R). \end{align}
Subsumption equivalence is a congruence with respect to sequential composition and set union as a direct consequence of Antić (Reference Antić2024d, Corollary 36) which means that we can form the factor algebra
\begin{align} [\mathfrak P_A] := \left ([\mathbb P_A], \cup , \circ , [\emptyset ], [1_A]\right ), \end{align}
where
\begin{align*} [\mathbb P_A] := \{[P] \mid P\in \mathbb P_A\}, \end{align*}
and
\begin{align*} [P]\cup [R] := [P\cup R] \quad \text{and}\quad [P]\circ [R] := [P\circ R], \end{align*}
isomorphic to
\begin{align*} \mathfrak T_A := (\mathbb T_{ \mathbb P_A}, \cup , \circ , T_ \emptyset , T_{1_A}), \end{align*}
where
\begin{align*} \mathbb T_{ \mathbb P_A} := \{T_P \mid P\in \mathbb P_A\} \end{align*}
denotes the set of all van Emden–Kowalski operators over
$A$
.
We have the following structural result:
Proposition 6. The isomorphic structures
$\mathfrak T_A$
and
$[\mathfrak P_A]$
are seminearrings.
We now turn to the least model semantics of programs. For this, define the (Kleene) star of a program
$P$
by
\begin{align*} P^\ast := \bigcup _{n\geq 0}P^n, \end{align*}
where (recall that composition is not associative)
\begin{align*} P^0 := 1, \quad P^1 := P, \quad P^{n+1} := P^n P. \end{align*}
Moreover, define the omega of
$P$
by
\begin{align} P^\omega := f(P^\ast ) \stackrel {10}= P^\ast \emptyset . \end{align}
For every interpretation
$I$
, we have
\begin{align} I^\ast &= 1\cup I \end{align}
\begin{align} I^\omega &= I. \end{align}
We have the following algebraic characterization of the least model of a program as shown in Antić (Reference Antić2024d, Theorem 40): the omega of
$P$
coincides with the least model of
$P$
, that is,
\begin{align} P^\omega = LM(P). \end{align}
For an interpretation
$I$
, define the minimalist program
\begin{align*} I^\oplus := \{a\leftarrow (\{a\}\cup I)\mid a\in A\}. \end{align*}
The program
\begin{align*} A^\oplus &= \{a\leftarrow A\mid a\in A\} \end{align*}
will play an important role in this paper as it occurs as the neutral element with respect to body-intersection (see Fact 30).
2.2.4 Reducts
Definition 7. Given an interpretation
$I$
, we define the
$\textit{head-reduct}$
and
$\textit{body-reduct}$
of a program
$P$
with respect to
$I$
respectively byFootnote
2
\begin{align*} ^IP := \{a \leftarrow B\in P \mid a\in I\} \quad \text{and}\quad P^I := \{a \leftarrow B\in P \mid B\subseteq I\}. \end{align*}
We now recollect some basic properties of reducts (see (Antić Reference Antić2024d, Section 4.3)).
For two interpretations
$I$
and
$J$
, we have
\begin{align} I^J &= I \end{align}
\begin{align} {^J}I &= I\cap J. \end{align}
According to Antić (Reference Antić2024d, Proposition 17), the body-reduct operator is an endomorphism on
$(\mathbb P_A,\cup ,\cap ,\emptyset ,A)$
, that is, for any programs
$P,R$
and interpretation
$I$
, we have
\begin{align} (P\cup R)^I &= P^I\cup R^I \end{align}
\begin{align} (P\cap R)^I &= P^I\cap R^I \end{align}
\begin{align} \emptyset ^I &= \emptyset \end{align}
\begin{align} A^I &= A, \end{align}
and the head-reduct operator is an endomorphism on
$(\mathbb P_A,\cup ,\cap ,\emptyset )$
, that is,
\begin{align} {^I}(P\cup R) &= {^I}P\cup {^I}R \end{align}
\begin{align} {^I}(P\cap R) &= {^I}P\cap {^I}R \end{align}
\begin{align} {^I}\emptyset &= \emptyset . \end{align}
Moreover, the left and right reducts can be rewritten in terms of composition as
\begin{align} ^IP &= (1^I)P \end{align}
\begin{align} P^I &= P1^I \end{align}
and
\begin{align} (PR)^I &= PR^I \end{align}
\begin{align} ^I(PR) &= {^I}PR. \end{align}
3 Body-union
The operations introduced in this section and the following ones form a natural family of set-like transformations on rule bodies. While body-union plays a central role in the decomposition results of Section 10, the remaining operations are studied to obtain a more complete picture of the algebraic structure of logic programs and to understand how these operations interact with program semantics.
This section introduces the first set-like operation on logic programs in analogy to the union of sets:
Definition 8. We define the
$\textit{body-union}$
of
$P$
and
$R$
by
\begin{align*} P\sqcup R &:= \{a \leftarrow (B\cup C)\mid a \leftarrow B\in P,\; a \leftarrow C\in R\}. \end{align*}
For example,
\begin{align*} \left \{ \begin{array}{l} a\\ b \leftarrow a\\ b \leftarrow b\\ c \leftarrow a,b \end{array} \right \} \sqcup \left \{ \begin{array}{l} b\\ b \leftarrow c \end{array} \right \} = \left \{ \begin{array}{l} b \leftarrow a\\ b \leftarrow b\\ b \leftarrow a,c\\ b \leftarrow b,c \end{array} \right \}. \end{align*}
We have the following interactions between body-union and some of our basic operations:
\begin{align} h(P\sqcup R) &= h(P)\cap h(R) \end{align}
\begin{align} f(P\sqcup R) &= f(P)\cap f(R) \end{align}
\begin{align} p(P\sqcup R) &= (f(P)\sqcup p(R))\cup (p(P)\sqcup f(R))\cup (p(P)\sqcup p(R)). \end{align}
Notice that the first two identities mean that
$h$
and
$f$
are both homomorphisms from
$( \mathbb P, \sqcup )$
to
$( \mathbb P, \cap )$
.
Recall that the union of sets is idempotent and despite the similarity between body-union and union, we have the following observation (but see Corollary 22 where we will show that body-union is at least idempotent modulo subsumption equivalence):
Observation 9. Body-union is not idempotent even for Krom programs, that is, there is a Krom program
$K$
such that
\begin{align*} K\sqcup K\neq K. \end{align*}
For example, we have
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} \sqcup \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} &= \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c\\ a \leftarrow b,c \end{array} \right \} \end{align*}
However, notice that body-union is idempotent on interpretations as a consequence of the forthcoming equation (48).
Fact 10. The structure
$(\mathbb P_A,\sqcup ,A)$
is a commutative monoid, that is,
\begin{align*} (P\sqcup Q)\sqcup R &= P\sqcup (Q\sqcup R)\\ P\sqcup A &= A\sqcup P = P\\ P\sqcup R &= R\sqcup P \end{align*}
holds for all programs
$P,Q,R\in \mathbb P_A$
.
We now analyze the interaction between body-union and union. Our first observation is the following structural result:
Theorem 11. The structure
$(\mathbb P_A,\cup ,\sqcup ,\emptyset ,A)$
is a commutative idempotent semiring, that is, in addition to
$(\mathbb P_A,\cup ,\emptyset )$
being an idempotent commutative monoid and
$(\mathbb P_A,\sqcup ,A)$
being a commutative monoid (see Fact 10), we have
\begin{align} (P\cup R)\sqcup Q &= (P\sqcup Q)\cup (R\sqcup Q) \end{align}
\begin{align} Q\sqcup (P\cup R) &= (Q\sqcup P)\cup (Q\sqcup R) \end{align}
\begin{align} \emptyset \sqcup P &= P\sqcup \emptyset = \emptyset . \end{align}
Proof. A direct consequence of the rule-wise definition of body-union.
Remark 12. In particular,
$(\mathbb P_A,\cup ,\sqcup ,\emptyset ,A)$
is a strong bimonoid in the sense of Droste et al. (Reference Droste, Stüber and Vogler2010). Notice that the structure with reversed roles
$(\mathbb P_A,\sqcup ,\cup ,A,\emptyset )$
is a bimonoid but not a strong one, since
$P\cup A\neq A$
in general.
The next result shows that
$\cup$
does in general not distribute over
$\sqcup$
(but see Theorem 14 where we show that it distributes modulo subsumption equivalence):
Observation 13. There are an interpretation
$I$
and Krom programs
$K$
and
$L$
such that
\begin{align*} (I\sqcup K)\cup L\neq (I\cup L)\sqcup (K\cup L). \end{align*}
For example, for
\begin{align*} I &:= \{a\} \quad \text{and}\quad K := \{a \leftarrow b\} \quad \text{and}\quad L := \{a \leftarrow c\} \end{align*}
we obtain
\begin{align*} (\{a\}\sqcup \{a \leftarrow b\})\cup \{a \leftarrow c\} &= \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\\ &\neq \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c\\ a \leftarrow b,c \end{array} \right \} = (\{a\}\cup \{a \leftarrow c\})\sqcup (\{a \leftarrow b\}\cup \{a \leftarrow c\}). \end{align*}
Theorem 14. For any programs
$P,Q,R$
, we have
\begin{align*} (P\sqcup R)\cup Q \approx (P\cup Q)\sqcup (R\cup Q). \end{align*}
Proof. For every interpretation
$I$
, we have (the forward references are non-circular and thus harmless)
\begin{align*} [(P\sqcup R)\cup Q]I & \stackrel {9}= (P\sqcup R)I\cup QI\\ & \stackrel {45}= (PI\sqcup RI)\cup QI \end{align*}
\begin{align*} & \stackrel {48}= (PI\cap RI)\cup QI\\ &= (PI\cup QI)\cap (RI\cup QI)\\ & \stackrel {9}= (P\cup Q)I\cap (R\cup Q)I\\ & \stackrel {48}= (P\cup Q)I\sqcup (R\cup Q)I\\ & \stackrel {45}= [(P\cup Q)\sqcup (R\cup Q)]I. \end{align*}
Proposition 15. For any programs
$P,Q,R$
, we have
\begin{align} Q\sqcup (P\cap R)\subseteq (Q\sqcup P)\cap (Q\sqcup R). \end{align}
Proof.
\begin{align*} Q\sqcup (P\cap R) &= \{a \leftarrow (B\cup C) \mid a \leftarrow B\in Q,\; a \leftarrow C\in P\cap R\}\\ &= \{a \leftarrow (B\cup C) \mid a \leftarrow B\in Q,\; a \leftarrow C\in P,\; a \leftarrow C\in R\}\\ &\subseteq \{a \leftarrow (B\cup C) \mid a \leftarrow B\in Q,\; a \leftarrow C\in P\}\\ & \cap \{a \leftarrow (B\cup C)\mid a \leftarrow B\in Q,\; a \leftarrow C\in R\}\\ &= (Q\sqcup P)\cap (Q\sqcup R), \end{align*}
where the inclusion cannot be turned into an identity since a rule occurring in both programs on the right may originate from a rule in
$P$
and a rule in
$R$
which are distinct and hence do not occur in
$P\cap R$
.
Observation 16. For
$Q := \{a \leftarrow b\}$
and
$P := \{a \leftarrow c\}$
and
$R := \{a \leftarrow b,c\}$
, we have
$P\cap R = \emptyset$
and therefore
\begin{align*} Q\sqcup (P\cap R) \stackrel {41}= \emptyset \subsetneq \{a \leftarrow b,c\} = \{a \leftarrow b,c\}\cap \{a \leftarrow b,c\} = (Q\sqcup P)\cap (Q\sqcup R). \end{align*}
We now study the interplay between body-union and the sequential composition of programs which is used to compute the semantic
${}^\omega$
-operator. We first prove that composition distributes from the right over body-union (but not from the left; see Observation 21):
Theorem 17. For any programs
$P,Q,R$
, we have
\begin{align} (P\sqcup R)Q &\subseteq PQ\sqcup RQ, \end{align}
\begin{align} (P\sqcup R)Q &\approx PQ\sqcup RQ, \end{align}
and equality
\begin{align} (P\sqcup R)Q = PQ\sqcup RQ \end{align}
holds in each of the following two cases: (i)
$B\cap C = \emptyset$
for all
$a \leftarrow B\in P$
and
$a \leftarrow C\in R$
; (ii)
$Q\sqcup Q = Q$
.
Proof. Given a set of atoms
$B$
, we call a family
$(C_b)_{b\in B}$
of sets of atoms a
$Q$
-selection for
$B$
if
$b \leftarrow C_b\in Q$
holds for every
$b\in B$
, so that the definition of composition reads as
\begin{align*} PQ = {\left \{a \leftarrow \bigcup _{b\in B}C_b \;\middle |\; a \leftarrow B\in P,\; (C_b)_{b\in B}\ \text{ a }Q\text{-selection for } B\right \}}. \end{align*}
We compute
\begin{align*} &(P\sqcup R)Q\\ &\quad= \{a \leftarrow (B\cup C) \mid a \leftarrow B\in P,\; a \leftarrow C\in R\}Q\\ &\quad= \left \{a \leftarrow \bigcup _{b\in B\cup C}F_b \;\middle |\; a \leftarrow B\in P,\; a \leftarrow C\in R,\; (F_b)_{b\in B\cup C}\ \text{a $Q$-selection for $B\cup C$}\right \}\\ &\quad\subseteq \left \{a \leftarrow \left (\bigcup _{b\in B}D_b\cup \bigcup _{b\in C}E_b\right ) \;\middle |\; a \leftarrow B\in P,\; a \leftarrow C\in R,\; (D_b)_{b\in B},\, (E_b)_{b\in C}\ \text{$Q$-selections}\right \}\\ &\quad= \left \{a \leftarrow \bigcup _{b\in B}D_b \;\middle |\; a \leftarrow B\in P,\; (D_b)_{b\in B}\ \text{a $Q$-selection for $B$}\right \}\\ & \quad\qquad \sqcup \left \{a \leftarrow \bigcup _{b\in C}E_b \;\middle |\; a \leftarrow C\in R,\; (E_b)_{b\in C}\ \text{a $Q$-selection for $C$}\right \}\\ &\quad= PQ\sqcup RQ, \end{align*}
which proves equation (43). The inclusion in the third line holds since the restrictions
$(F_b)_{b\in B}$
and
$(F_b)_{b\in C}$
of a
$Q$
-selection for
$B\cup C$
are
$Q$
-selections for
$B$
and
$C$
satisfying
$\bigcup _{b\in B}F_b\cup \bigcup _{b\in C}F_b = \bigcup _{b\in B\cup C}F_b$
. It is an identity — and hence proves equation (45) — in each of the cases (i) and (ii), since given
$Q$
-selections
$(D_b)_{b\in B}$
and
$(E_b)_{b\in C}$
, the family
\begin{align*} F_b := \begin{cases} D_b & b\in B - C,\\ E_b & b\in C - B,\\ D_b\cup E_b & b\in B\cap C, \end{cases} \end{align*}
is a
$Q$
-selection for
$B\cup C$
satisfying
$\bigcup _{b\in B\cup C}F_b = \bigcup _{b\in B}D_b\cup \bigcup _{b\in C}E_b$
: in case (i) the third line is vacuous as
$B\cap C=\emptyset$
, and in case (ii) we have
$b \leftarrow (D_b\cup E_b)\in Q\sqcup Q = Q$
for every
$b\in B\cap C$
.
Finally, we prove equation (44). Notice first that every interpretation
$J$
satisfies
$J\sqcup J \stackrel {49}= J$
, which means that equation (45) is applicable whenever the right factor is an interpretation. Hence, for every interpretation
$I$
we compute
\begin{align*} [(P\sqcup R)Q]I & \stackrel {Proposition\,6}{\approx } (P\sqcup R)(QI) \stackrel {45}= P(QI)\sqcup R(QI) \stackrel {48}= P(QI)\cap R(QI)\\ & \stackrel {Proposition\,6}{\approx } (PQ)I\cap (RQ)I \stackrel {48}= (PQ)I\sqcup (RQ)I \stackrel {45}= [PQ\sqcup RQ]I, \end{align*}
where we may replace
$\approx$
by
$=$
since all programs occurring in the computation are interpretations and subsumption equivalent interpretations coincide.
Remark 18. Condition (ii) covers the two cases occurring throughout this paper: every interpretation
$I$
satisfies
$I\sqcup I \stackrel {49}= I$
, every minimalist program
$M$
satisfies
$M\sqcup M = M$
, and the program
$A^\ast \stackrel {20}= 1_A\cup A$
used in Proposition 57 satisfies
$A^\ast \sqcup A^\ast = A^\ast$
. On the other hand,
$Q := \{b \leftarrow d,\; b \leftarrow e\}$
satisfies
$Q\sqcup Q = Q\cup \{b \leftarrow d,e\}\neq Q$
, and indeed
$P := \{a \leftarrow b\}$
and
$R := \{a \leftarrow b,c\}$
together with
$Q':=Q\cup \{c \leftarrow c\}$
give
\begin{align*} (P\sqcup R)Q' = \left \{ \begin{array}{l} a \leftarrow c,d\\ a \leftarrow c,e \end{array} \right \} \subsetneq \left \{ \begin{array}{l} a \leftarrow c,d\\ a \leftarrow c,e\\ a \leftarrow c,d,e \end{array} \right \} = PQ'\sqcup RQ', \end{align*}
which shows that the inclusion in equation (43) can in general not be turned into an equality.
Lemma 19. Subsumption equivalence is a congruence with respect to body-union, that is,
$P\approx P'$
and
$R\approx R'$
imply
$P\sqcup R\approx P'\sqcup R'$
, for all programs
$P,P',R,R'$
.
Proof. Since every interpretation
$I$
satisfies
$I\sqcup I \stackrel {49}= I$
, we may apply equation (45) to compute
\begin{align*} (P\sqcup R)I \stackrel {45}= PI\sqcup RI = P'I\sqcup R'I \stackrel {45}= (P'\sqcup R')I, \end{align*}
where the middle identity holds by assumption.
Theorem 20. The structure
$( [\mathbb P_A], \sqcup , \circ , [A], [1_A] )$
forms a seminearring with unit
$[1_A]$
, where
$[P]\sqcup [R] := [P\sqcup R]$
.
Proof. Body-union is well-defined on subsumption equivalence classes by Lemma 19, and
$( [\mathbb P_A], \sqcup , [A] )$
is a monoid since
$( \mathbb P_A, \sqcup , A )$
is one by Fact 10. Composition is associative modulo subsumption equivalence by Proposition 6, right-distributivity is equation (44), and
$[A]$
is a left zero with respect to composition since
\begin{align*} AP = A \end{align*}
holds for every program
$P\in \mathbb P_A$
— indeed,
$A$
consists of facts only, which are left unchanged by composition. Finally,
$[1_A]$
is a unit since
$P1_A = 1_AP = P$
.
Observation 21. Unfortunately, the distributivity law in equation (44) does
$\textit{not}$
hold if composition is computed from the left as there are Krom programs
$K,L,N$
such that
\begin{align*} K(L\sqcup N) \not \approx KL\sqcup KN, \end{align*}
which means that in general we have
\begin{align*} Q(P\sqcup R)\not \approx QP\sqcup QR. \end{align*}
For example, we have
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}(\{b \leftarrow b\}\sqcup \{c \leftarrow c\}) = \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\emptyset = \emptyset \end{align*}
whereas
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\{b \leftarrow b\}\sqcup \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\{c \leftarrow c\} = \{a \leftarrow b\}\sqcup \{a \leftarrow c\} = \{a \leftarrow b,c\} \end{align*}
and the programs
$\emptyset$
and
$\{a \leftarrow b,c\}$
are, of course, not subsumption equivalent.
The next result is analogous to
$P\cup P = P$
:
Corollary 22. Body-union is idempotent modulo subsumption equivalence, that is, for every program
$P$
,
\begin{align*} P\sqcup P\approx P. \end{align*}
Proof. For every interpretation
$I$
,
\begin{align*} (P\sqcup P)I \stackrel {45}= PI\sqcup PI \stackrel {48}= PI. \end{align*}
Theorem 23. Every model of
$P$
is a model of
$P\sqcup R$
, for any programs
$P$
and
$R$
. That is,
\begin{align*} Mod(P)\subseteq Mod(P\sqcup R). \end{align*}
Proof. By Theorem 1, we know that an interpretation
$I$
is a model of
$P$
iff
$T_P(I)\subseteq I$
, which by equation (16) is equivalent to
$PI\subseteq I$
. Now by equation (45), we have
$(P\sqcup R)I=PI\sqcup RI \stackrel {48}= PI\cap RI\subseteq I$
, which means that
$I$
is a model of
$P\sqcup R$
.
Proposition 24. An interpretation
$I$
is a supported model of
$P\sqcup R$
iff
$PI\cap RI=I$
, that is,
\begin{align*} Supp(P\sqcup R) = \{I\in \mathbb I\mid PI\cap RI = I\}. \end{align*}
Proof. By Fact 4, an interpretation
$I$
is a supported model of
$P\sqcup R$
iff
$(P\sqcup R)I \stackrel {45}= PI\sqcup RI \stackrel {48}= PI\cap RI = I$
.
The next result is analogous to
\begin{align*} P\cup R = P \quad \Leftrightarrow \quad R\subseteq P. \end{align*}
Proposition 25. For any programs
$P$
and
$R$
,
\begin{align*} P\sqcup R \approx P \quad \Leftrightarrow \quad P\lesssim R. \end{align*}
Proof.
$(\Rightarrow )$
For any interpretation
$I$
, we have
\begin{align*} PI = (P\sqcup R)I = PI\sqcup RI = PI\cap RI\subseteq RI, \end{align*}
which implies
$P\lesssim R$
.
$(\Leftarrow )$
From the assumption
$PI\subseteq RI$
, for every interpretation
$I$
, we deduce
\begin{align*} (P\sqcup R)I = PI\sqcup RI = PI\cap RI = PI, \end{align*}
which implies
$P\sqcup R \approx P$
.
Reducing a program to a restricted alphabet is a fundamental operation on programs which we will often use in the rest of the paper and in this section we analyze the interactions between body-union and reducts.
We can simplify the computation of the body-union using head-reducts as
\begin{align*} P\sqcup R &= {^{h(R)}}P\sqcup {^{h(P)}}R. \end{align*}
Notice that we have
\begin{align*} {^{f(R)}}P\cup {^{f(P)}}R\subseteq P\sqcup R. \end{align*}
Computing the body of
$P\sqcup R$
is simple using head-reducts:
\begin{align} b(P\sqcup R) &= b({^{h(R)}}P)\cup b({^{h(P)}}R). \end{align}
Interestingly, the left reduct can be represented via body-union as (compare with equation (80))
\begin{align} I\sqcup P &= P\sqcup I = {^I}P. \end{align}
This implies that for any interpretations
$I$
and
$J$
,
\begin{align} I\sqcup J & \stackrel {47}= {^J}I \stackrel {24}= I\cap J, \end{align}
and therefore
\begin{align} I\sqcup I = I. \end{align}
Moreover, it implies that computing the proper rules in
$P\sqcup R$
can be written as
\begin{align} p(P\sqcup R) \stackrel {38, 47}= (p(P)\sqcup p(R))\cup {^{f(R)}}p(P)\cup {^{f(P)}}p(R). \end{align}
Proposition 26. The body-reduct operator is an endomorphism on the monoid
$(\mathbb P_A,\sqcup ,A)$
, that is,
\begin{align*} (P\sqcup R)^I &= P^I\sqcup R^I\\ A^I & \stackrel {23}= A. \end{align*}
Moreover, the head-reduct operator is an endomorphism on the semigroup
$(\mathbb P_A,\sqcup )$
, that is,
\begin{align} ^I(P\sqcup R) = {^I}P\sqcup {^I}R. \end{align}
Proof. The first two identities hold trivially. To prove the third, we compute
\begin{align*} {^I}(P\sqcup R) & \stackrel {47}= I\sqcup P\sqcup R \stackrel {48}= I\sqcup P\sqcup I\sqcup R \stackrel {47}= {^I}P\sqcup {^I}R. \end{align*}
Remark 27. Notice that the head-reduct operator fails to be an endomorphism on the monoid
$(\mathbb P_A,\sqcup ,A)$
since, in case
$I\neq A$
, we have
$^IA \stackrel {24}= I\cap A = I \neq A$
.
Proposition 28. For any programs
$P$
and
$R$
and interpretation
$I$
,
\begin{align} (P\cup I)\sqcup (R\cup I) = I\cup {^I}P\cup {^I}R\cup (P\sqcup R). \end{align}
Proof.
\begin{align*} (P\cup I)\sqcup (R\cup I) &= \{a \leftarrow B\cup C\mid a \leftarrow B\in P\cup I,\;a \leftarrow C\in R\cup I\}\\ &= \{a \mid a\in I\}\cup \{a \leftarrow B\mid a \leftarrow B\in P,\; a\in I\}\\ &\quad \cup \{a \leftarrow C\mid a\in I,\; a \leftarrow C\in R\}\cup \{a \leftarrow B\cup C\mid a \leftarrow B\in P,\;a \leftarrow C\in R\}\\ &= I\cup (I\sqcup P)\cup (I\sqcup R)\cup (P\sqcup R)\\ & \stackrel {47}= I\cup {^I}P\cup {^I}R\cup (P\sqcup R). \end{align*}
4 Body-intersection
We now turn to our next set-like operation which is analogous to set intersection:
Definition 29. Define the
$\textit{body-intersection}$
of
$P$
and
$R$
by
\begin{align*} P\sqcap R &:= \{a \leftarrow (B\cap C)\mid a \leftarrow B\in P,\; a \leftarrow C\in R\}. \end{align*}
Body-intersection is not idempotent even on Krom programs as is witnessed by the following counterexample:
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} \sqcap \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} &= \left \{ \begin{array}{l} a\\ a \leftarrow b\\ a \leftarrow c \end{array} \right \}. \end{align*}
However, body-intersection coincides with intersection on interpretations,
\begin{align} I\sqcap J = I\cap J, \end{align}
which means that it is idempotent on interpretations,
\begin{align*} I\sqcap I & \stackrel {53}= I\cap I = I. \end{align*}
Fact 30. The structure
$(\mathbb P_A,\sqcap ,A^\oplus )$
is a commutative monoid, that is,
\begin{align} (P\sqcap Q)\sqcap R &= P\sqcap (Q\sqcap R) \end{align}
\begin{align} P\sqcap A^\oplus &= A^\oplus \sqcap P = P \end{align}
\begin{align} P\sqcap R &= R\sqcap P. \end{align}
We have the following interactions between body-intersection and and the head operator:
\begin{align*} h(P\sqcap R) &= h(P)\cap h(R). \end{align*}
This means that the head operator
$h$
is a homomorphism from
$( \mathbb P, \sqcap )$
to
$( \mathbb P, \cap )$
.
Unfortunately, computing
$f(P\sqcap R)$
is not as simple as computing
$f(P\sqcup R)$
(see equation (37)) and before we give a formula in equation (57) below, we first introduce the following auxiliary construct:
Definition 31. Define the
$\textit{bowtie}$
of
$P$
and
$R$
by
\begin{align*} P\bowtie R &:= (P\ltimes R)\cup (R\ltimes P). \end{align*}
where
\begin{align*} P\ltimes R &:= \{a \leftarrow B\in P \mid \text{there exists }a \leftarrow C\in R\text{ with } B\cap C = \emptyset \}. \end{align*}
We can now compute the facts in
$P\sqcap R$
as
\begin{align} f(P\sqcap R) = (f(P)\cap f(R))\cup h(P\bowtie R) \stackrel {37}= f(P\sqcup R)\cup h(P\bowtie R). \end{align}
Observation 32. There are Krom programs
$K,L,M$
such that
\begin{align*} M(K\sqcap L) \not \approx MK\sqcap ML, \end{align*}
which means that in general we have
\begin{align*} Q(P\sqcap R) \neq QP\sqcap QR. \end{align*}
This is analogous to what we have encountered in Observation 21 and a similar counterexample works here as well: we have
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}(\{b \leftarrow b\}\sqcap \{c \leftarrow c\}) = \emptyset \end{align*}
whereas
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\{b \leftarrow b\}\sqcap \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\{c \leftarrow c\} = \{a \leftarrow b\}\sqcap \{a \leftarrow c\} = \{a\}. \end{align*}
Moreover, there are minimalist programs
$M,N$
and an interpretation
$I$
such that
\begin{align*} (M\sqcap N)I\neq MI\sqcap NI, \end{align*}
which means that in general we haveFootnote 3
\begin{align*} (P\sqcap R)Q \not \approx PQ\sqcap RQ. \end{align*}
Compare this with the positive result in Theorem 17! To see why, consider the counterexample
\begin{align*} (\{a \leftarrow b,c\}\sqcap \{a \leftarrow c,d\})\{c\} = \{a\} \neq \{a \leftarrow b,c\}\{c\}\sqcap \{a \leftarrow c,d\}\{c\} = \emptyset . \end{align*}
We shall now analyze the interaction between body-intersection and reducts. Our first observation is as follows:
Observation 33. In contrast to Proposition 26, the body-reduct operator is in general
$\textit{not}$
an endomorphism on the monoid
$(\mathbb P_A,\sqcap ,A^\oplus )$
since, in general, we have
\begin{align*} (P\sqcap R)^I \not \subseteq P^I\sqcap R^I \end{align*}
as is witnessed by the following counterexample:
\begin{align*} (\{a \leftarrow b\}\sqcap \{a \leftarrow c\})^{\{b\}} = \{a\}^{\{b\}} \stackrel {23}= \{a\} \end{align*}
whereas
\begin{align*} \{a \leftarrow b\}^{\{b\}}\sqcap \{a \leftarrow c\}^{\{b\}} = \{a \leftarrow b\}\sqcap \emptyset = \emptyset . \end{align*}
However, we do have
\begin{align*} P^I\sqcap R^I\subseteq (P\sqcap R)^I \end{align*}
since
\begin{align*} P^I\sqcap R^I = \{a \leftarrow B\cap C\mid B,C\subseteq I\}\subseteq \{a \leftarrow B\cap C\mid B\cap C\subseteq I\} = (P\sqcap R)^I. \end{align*}
Proposition 34. The head-reduct operator is an endomorphism on the semigroup
$(\mathbb P_A,\sqcap )$
, that is,
\begin{align*} {^I}(P\sqcap R) &= {^I}P\sqcap {^I}R. \end{align*}
Proof. We have
\begin{align*} {^I}(P\sqcap R) & \stackrel {47}= I\sqcup (P\sqcap R) \stackrel {77}= (I\sqcup P)\sqcap (I\sqcup R) \stackrel {47}= {^I}P\sqcap {^I}R, \end{align*}
where the forward reference to equation (77) is non-circular and thus harmless.
Proposition 35. We have the following formula for the computation of the head-reduct:
\begin{align} {^I}P &= {^I}(A^\oplus )\sqcap P. \end{align}
Proof.
\begin{align*} {^I}(A^\oplus )\sqcap P &= \{a \leftarrow A \mid a\in I\}\sqcap P = \{a \leftarrow (B\cap A) \mid a \leftarrow B\in P,\, a\in I\}\\ &= \{a \leftarrow B\in P\mid a\in I\} = {^I}P. \end{align*}
5 Body-complement
In analogy to the complement of sets, we introduce the following unary operation on programs:
Definition 36. We define the
$\textit{body-complement}$
of
$P$
by
\begin{align*} P^{\unicode{x00A9}} := {\left \{a \leftarrow (A- B) \;\middle |\; a \leftarrow B\in P\right \}}. \end{align*}
Example 37. Let
$A := \{a,b,c\}$
. We then have, for instance,
\begin{align*} \emptyset ^{\unicode{x00A9}} = \emptyset ,\qquad \{a\}^{\unicode{x00A9}} = \{a \leftarrow a,b,c\},\qquad \left \{ \begin{array}{l} a\\ b \leftarrow a\\ c \leftarrow a,b \end{array} \right \}^{\unicode{x00A9}} = \left \{ \begin{array}{l} a \leftarrow a,b,c\\ b \leftarrow b,c\\ c \leftarrow c \end{array} \right \}. \end{align*}
Body-complement is involutive,
\begin{align} (P^{\unicode{x00A9}})^{\unicode{x00A9}} = P. \end{align}
Moreover, it satisfies the following identities (among others):
\begin{align} h(P^{\unicode{x00A9}}) &= h(P) \end{align}
\begin{align} b(P^{\unicode{x00A9}}) &= A- \bigcap _{a \leftarrow B\in P} B \end{align}
\begin{align} f(P^{\unicode{x00A9}}) &= h(P\cap A^\oplus ) = \{a\in A\mid a \leftarrow A\in P\} \end{align}
\begin{align} A^{\unicode{x00A9}} &= A^\oplus \end{align}
\begin{align} I^{\unicode{x00A9}} &= {^I}(A^\oplus ). \end{align}
Fact 38. Body-complement is an endomorphism on the boolean algebra
$(\mathbb P_A,\cup ,\cap ,{}^c,\emptyset ,F_A)$
, that is,
\begin{align} (P\cup R)^{\unicode{x00A9}} &= P^{\unicode{x00A9}}\cup R^{\unicode{x00A9}} \end{align}
\begin{align} (P\cap R)^{\unicode{x00A9}} &= P^{\unicode{x00A9}}\cap R^{\unicode{x00A9}} \end{align}
\begin{align} (P^c)^{\unicode{x00A9}} &= (P^{\unicode{x00A9}})^c \end{align}
\begin{align} \emptyset ^{\unicode{x00A9}} &= \emptyset \end{align}
\begin{align} F_A^{\unicode{x00A9}} &= F_A, \end{align}
where
\begin{align} F_A := \{a \leftarrow B \mid a\in A ,\, B\subseteq A\} \end{align}
is the
$\textit{full program}$
over
$A$
consisting of all possible rules and facts that can be formed from
$A$
.
This gives us the following formula for the computation of body-complement:
\begin{align*} P^{\unicode{x00A9}} = (f(P)\cup p(P))^{\unicode{x00A9}} \stackrel {65}= f(P)^{\unicode{x00A9}}\cup p(P)^{\unicode{x00A9}} \stackrel {64}= {^{f(P)}}(A^\oplus )\cup p(P)^{\unicode{x00A9}}. \end{align*}
The next result shows that we can smoothly adapt De Morgan’s laws to body-union, body-intersection, and body-complement as desired:
Proposition 39. For any programs
$P$
and
$R$
,
\begin{align} (P\sqcup R)^{\unicode{x00A9}} & = P^{\unicode{x00A9}}\sqcap R^{\unicode{x00A9}} \end{align}
\begin{align} (P\sqcap R)^{\unicode{x00A9}} & = P^{\unicode{x00A9}}\sqcup R^{\unicode{x00A9}}. \end{align}
Proof. Using De Morgan’s laws, we compute
\begin{align*} (P\sqcup R)^{\unicode{x00A9}} &= \{a \leftarrow (B\cup C) \mid a \leftarrow B\in P,\; a \leftarrow C\in R\}^{\unicode{x00A9}}\\ &= \{a \leftarrow (A- (B\cup C)) \mid a \leftarrow B\in P,\; a \leftarrow C\in R\}\\ &= \{a \leftarrow ((A- B)\cap (A- C)) \mid a \leftarrow B\in P,\; a \leftarrow C\in R\}\\ &= \{a \leftarrow (A- B)\mid a \leftarrow B\in P\}\sqcap \{a \leftarrow (A- C)\mid a \leftarrow C\in R\}\\ &= P^{\unicode{x00A9}}\sqcap R^{\unicode{x00A9}}. \end{align*}
and a similar computation shows the second identity.
The body-complement of a Krom program
$K$
is
\begin{align*} K^{\unicode{x00A9}} = \{a \leftarrow A\mid a\in f(K)\}\cup \{a \leftarrow (A-\{b\}) \mid a \leftarrow b\in p(K)\} \end{align*}
which can be written more compactly as
\begin{align*} K^{\unicode{x00A9}} = {^{f(K)}}(A^\oplus )\cup p(K)^{\unicode{x00A9}}. \end{align*}
The identities
\begin{align*} (P^{\unicode{x00A9}})^I &= \{a \leftarrow (A-B) \mid a \leftarrow B\in P,\; A- B\subseteq I\}\\ (P^I)^{\unicode{x00A9}} &= \{a \leftarrow (A-B) \mid a \leftarrow B\in P,\; B\subseteq I\} \end{align*}
show that in general we have
\begin{align*} (P^{\unicode{x00A9}})^I\neq (P^I)^{\unicode{x00A9}}, \end{align*}
which means that the body-reduct does not commute with body-complement, but see Proposition 40 below where we show that the head-reduct does commute with body-complement. At least we (trivially) have
\begin{align*} (P^{\unicode{x00A9}})^A = (P^A)^{\unicode{x00A9}}. \end{align*}
Proposition 40. Body-complement commutes with head-reducts, that is, for any program
$P$
and interpretation
$I$
,
\begin{align} {^I}(P^{\unicode{x00A9}}) &= ({^I}P)^{\unicode{x00A9}}. \end{align}
Proof. An immediate consequence from the definition of body-complement and head-reducts. To illustrate some of the identities obtained above, we additionally compute
\begin{align*} {^I}(P^{\unicode{x00A9}}) & \stackrel {47}= I\sqcup P^{\unicode{x00A9}} \stackrel {71}= (I^{\unicode{x00A9}}\sqcap P)^{\unicode{x00A9}} \stackrel {64}= ({^I}(A^\oplus )\sqcap P)^{\unicode{x00A9}} \stackrel {58}= ({^I}P)^{\unicode{x00A9}}. \end{align*}
Theorem 41. For all programs
$P,Q,R$
, we have
\begin{align} (P\sqcup R)\sqcap Q &\subseteq (P\sqcap Q)\sqcup (R\sqcap Q) \end{align}
\begin{align} (P\sqcap R)\sqcup Q &\subseteq (P\sqcup Q)\sqcap (R\sqcup Q), \end{align}
and in case
$M$
is a minimalist program, we have the identities
\begin{align} (P\sqcup R)\sqcap M &= (P\sqcap M)\sqcup (R\sqcap M) \end{align}
\begin{align} (P\sqcap R)\sqcup M &= (P\sqcup M)\sqcap (R\sqcup M). \end{align}
Proof. Applying the well-known distributivity laws of the set operations, we compute
\begin{align*} &(P\sqcup R)\sqcap Q\\ &\quad = \{a \leftarrow ((B\cup C)\cap D) \mid a \leftarrow B\in P,\; a \leftarrow C\in R,\; a \leftarrow D\in Q\}\\ &\quad = \{a \leftarrow ((B\cap D)\cup (C\cap D)) \mid a \leftarrow B\in P,\; a \leftarrow C\in R,\; a \leftarrow D\in Q\}\\ &\quad \subseteq \{a \leftarrow ((B\cap D)\cup (C\cap D')) \mid a \leftarrow B\in P,\; a \leftarrow C\in R,\; a \leftarrow D\in Q,\; a \leftarrow D'\in Q\}\\ &\quad = (P\sqcap Q)\sqcup (R\sqcap Q) \end{align*}
and, analogously,
\begin{align*} &(P\sqcap R)\sqcup Q\\ &\quad = \{a \leftarrow ((B\cap C)\cup D) \mid a \leftarrow B\in P,\; a \leftarrow C\in R,\; a \leftarrow D\in Q\}\\ &\quad = \{a \leftarrow ((B\cup D)\cap (C\cup D)) \mid a \leftarrow B\in P,\; a \leftarrow C\in R,\; a \leftarrow D\in Q\}\\ &\quad \subseteq \{a \leftarrow ((B\cup D)\cap (C\cup D')) \mid a \leftarrow B\in P,\; a \leftarrow C\in R,\; a \leftarrow D\in Q,\; a \leftarrow D'\in Q\}\\ &\quad = (P\sqcup Q)\sqcap (R\sqcup Q). \end{align*}
In both computations, the inclusion is an identity in case
$Q$
is minimalist, since then
$D$
and
$D'$
are both the body of the unique rule in
$Q$
with head
$a$
— which proves equations (76) and (77).
Observation 42. The inclusions in equations (74) and (75) can in general not be turned into identities. For example, for the non-minimalist program
$Q := \{a \leftarrow b,\; a \leftarrow c\}$
and
$P := \{a \leftarrow b\}$
and
$R := \{a \leftarrow c\}$
, we have
\begin{align*} (P\sqcup R)\sqcap Q &= (P\sqcap R)\sqcup Q = \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} \subsetneq \left \{ \begin{array}{l} \underline {a}\\ a \leftarrow b\\ a \leftarrow c\\ \underline {a \leftarrow b,c} \end{array} \right \} = (P\sqcap Q)\sqcup (R\sqcap Q)\\ &= (P\sqcup Q)\sqcap (R\sqcup Q). \end{align*}
6 Body-subtraction
In this section, we introduce an operation on programs which mimics set difference:
Definition 43. Define the
$\textit{body-subtraction}$
of
$P$
and
$R$
by
\begin{align*} P\boxminus R &:= \{a \leftarrow (B-C)\mid a \leftarrow B\in P,\; a \leftarrow C\in R\}. \end{align*}
For example, we have
\begin{align*} \left \{ \begin{array}{l} a\\ b \leftarrow a\\ c \leftarrow a,b \end{array} \right \}\boxminus \left \{ \begin{array}{l} b \leftarrow a\\ c \leftarrow a \end{array} \right \} = \left \{ \begin{array}{l} b\\ c \leftarrow b \end{array} \right \}. \end{align*}
This operation satisfies the following identities (among others):
\begin{align*} P\boxminus \emptyset &= \emptyset \boxminus P = \emptyset \\ P\boxminus A &= P\\ P\boxminus A^\oplus &= h(P). \end{align*}
Moreover, we have
\begin{align*} M\boxminus M &= h(M) \end{align*}
for every minimalist program
$M$
. Notice that the identity may fail for non-minimalist programs as is witnessed by the counterexample:
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\boxminus \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} = \left \{ \begin{array}{l} a\\ a \leftarrow b\\ a \leftarrow c \end{array} \right \}. \end{align*}
We thus have
\begin{align*} P\boxminus P\supseteq h(P). \end{align*}
Fact 44. The head operator is a homomorphism
$h:(\mathbb P_A,\boxminus )\to (\mathbb I_A,\cap )$
thus satisfying
\begin{align*} h(P\boxminus R) &= h(P)\cap h(R). \end{align*}
Recall that for sets
$X$
and
$Y$
,
\begin{align*} X- Y = X\cap Y^c. \end{align*}
Analogously, we have:
Proposition 45. For any programs
$P$
and
$R$
,
\begin{align} P\boxminus R = P\sqcap R^{\unicode{x00A9}}. \end{align}
Proof. Using De Morgan’s law, we compute
\begin{align*} P\sqcap R^{\unicode{x00A9}} &= \left \{a \leftarrow (B\cap C) \;\middle |\; a \leftarrow B\in P,\; a \leftarrow C\in R^{\unicode{x00A9}} \right \}\\ &= \left \{a \leftarrow (B\cap C) \;\middle |\; a \leftarrow B\in P,\; a \leftarrow (A- C)\in R \right \}\\ &= \left \{a \leftarrow (B\cap (A- C)) \;\middle |\; a \leftarrow B\in P,\; a \leftarrow C\in R \right \} \end{align*}
\begin{align*} &= \{a \leftarrow (B- C) \mid a \leftarrow B\in P,\; a \leftarrow C\in R\}\\ &= P\boxminus R. \end{align*}
Corollary 46. For any programs
$P,Q,R$
, we have
\begin{align} (P\sqcup R)\boxminus Q \subseteq (P\boxminus Q)\sqcup (R\boxminus Q), \end{align}
with equality in case
$Q$
is minimalist.
Proof. Notice first that
$Q$
is minimalist iff
$Q^{\unicode{x00A9}}$
is minimalist, since body-complement preserves rule heads and neither adds nor removes rules. We can therefore compute
\begin{align*} (P\sqcup R)\boxminus Q \stackrel {78}= (P\sqcup R)\sqcap Q^{\unicode{x00A9}} \stackrel {74}\subseteq (P\sqcap Q^{\unicode{x00A9}})\sqcup (R\sqcap Q^{\unicode{x00A9}}) \stackrel {78}= (P\boxminus Q)\sqcup (R\boxminus Q), \end{align*}
where the inclusion is an identity by equation (76) in case
$Q$
— and hence
$Q^{\unicode{x00A9}}$
— is minimalist.
Observation 47. The inclusion in equation (79) can in general not be turned into an identity, not even modulo subsumption equivalence. For example, for
$P := \{a \leftarrow b\}$
and
$R := \{a \leftarrow c\}$
and the non-minimalist program
$Q := \{a \leftarrow b,\; a \leftarrow c\}$
, we have
\begin{align*} (P\sqcup R)\boxminus Q = \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} \subsetneq \left \{ \begin{array}{l} \underline {a}\\ a \leftarrow b\\ a \leftarrow c\\ \underline {a \leftarrow b,c} \end{array} \right \} = (P\boxminus Q)\sqcup (R\boxminus Q), \end{align*}
and since the program on the right contains the fact
$a$
whereas the program on the left contains no fact at all, Equation (10) yields
\begin{align*} [(P\sqcup R)\boxminus Q]\emptyset = \emptyset \neq \{a\} = [(P\boxminus Q)\sqcup (R\boxminus Q)]\emptyset . \end{align*}
Of course, Equation (79) does imply
\begin{align*} (P\sqcup R)\boxminus Q \lesssim (P\boxminus Q)\sqcup (R\boxminus Q). \end{align*}
Interestingly enough, we can compute the body-complement of
$P$
via body-subtraction according to the formula
\begin{align*} P^{\unicode{x00A9}} = A^\oplus \boxminus P. \end{align*}
We shall now investigate the interaction between reducts and body-subtraction. We can express the head-reduct in terms of body-subtraction as (compare with equation (47))
\begin{align} P\boxminus I &= {^I}P, \end{align}
for every program
$P$
and interpretation
$I$
. Moreover, we can simplify the computation of body-subtraction using left reducts as
\begin{align*} P\boxminus R = {^{h(R)}}P\boxminus {^{h(P)}}R. \end{align*}
Proposition 48. The head-reduct is an endomorphism
${^I}. : (\mathbb P_A,\boxminus )\to (\mathbb P_A,\boxminus )$
for every interpretation
$I$
, that is, for any programs
$P$
and
$R$
,
\begin{align*} {^I}(P\boxminus R) &= {^I}P\boxminus {^I}R. \end{align*}
Proof.
\begin{align*} {^I}(P\boxminus R)& \stackrel {47}= I\sqcup (P\boxminus R) \stackrel {78}= I\sqcup (P\sqcap R^{\unicode{x00A9}}) \stackrel {77}= (I\sqcup P)\sqcap (I\sqcup R^{\unicode{x00A9}}) \stackrel {47}= {^I}P\sqcap {^I}(R^{\unicode{x00A9}})\\& \stackrel {73}= {^I}P\sqcap ({^I}R)^{\unicode{x00A9}} \stackrel {78}= {^I}P\boxminus {^I}R. \end{align*}
We now turn our attention to the interaction between composition and body-subtraction.
Observation 49. There is a minimalist Krom program
$K$
and an interpretation
$I$
such that
\begin{align*} (K\boxminus K)I \not \approx KI\boxminus KI. \end{align*}
For example, we have
\begin{align*} (\{a \leftarrow b\}\boxminus \{a \leftarrow b\}) \emptyset = \{a\} \emptyset = \{a\} \end{align*}
whereas
\begin{align*} \{a \leftarrow b\} \emptyset \boxminus \{a \leftarrow b\} \emptyset = \emptyset \boxminus \emptyset = \emptyset . \end{align*}
Hence, in general we have
\begin{align*} (P\boxminus R)Q \not \approx PQ\boxminus RQ. \end{align*}
Observation 50. There are Krom programs
$K$
and
$L$
and an interpretation
$I$
such that
\begin{align*} K(L\boxminus I)\not \approx KL\boxminus KI. \end{align*}
For example, for
\begin{align*} K := \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \} \quad \text{and}\quad L := \{b \leftarrow b\} \quad \text{and}\quad I := \{c\}, \end{align*}
we have
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}(\{b \leftarrow b\}\boxminus \{c\}) = \emptyset \end{align*}
whereas
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\{b \leftarrow b\}\boxminus \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow c \end{array} \right \}\{c\} = \{a \leftarrow b\}\boxminus \{a\} = \{a \leftarrow b\}. \end{align*}
Hence, in general
\begin{align*} Q(P\boxminus R)\not \approx QP\boxminus QR. \end{align*}
Fact 51. For any programs
$P$
and
$R$
with
$h(P)\subseteq h(R)$
,
\begin{align} P^\omega \subseteq (P\boxminus R)^\omega . \end{align}
7 Body-symmetric-difference
Recall that the set-theoretic symmetric difference of two programs is given by
\begin{align*} P\mathrel {\triangle } R = (P- R)\cup (R- P). \end{align*}
We shall introduce analogous set-like operations on programs in two different ways corresponding to the two sides of the above equation:
Definition 52. Define the
$\textit{body-symmetric-difference}$
of
$P$
and
$R$
by
and define the
$\textit{black-body-symmetric-difference}$
of
$P$
and
$R$
by
The two notions of “symmetric difference” coincide on minimalist programs containing at most one rule for each rule head, that is, for any minimalist programs
$M$
and
$N$
we clearly have
However, for non-minimalist programs, the two notions may differ as is witnessed by the following example:
Example 53. For
\begin{align*} P := \left \{ \begin{array}{l} a \leftarrow b\\[-2pt] a \leftarrow c \end{array} \right \} \quad \text{and}\quad R := \left \{ \begin{array}{l} a \leftarrow b\\[-2pt] a \leftarrow d \end{array} \right \} \end{align*}
we have
whereas
Proposition 54. For any programs
$P$
and
$R$
,
Proof.
8 Body-power-set
This section introduces and studies a set-like operation on programs inspired by the analogous power set operation on sets:
Definition 55. Define the
$\textit{body-power-set}$
of
$P$
by
\begin{align*} P^{ \mathfrak p} := \{a \leftarrow B \mid a \leftarrow C\in P,\; B\subseteq C\}. \end{align*}
For example, we have
\begin{align*} \emptyset ^{ \mathfrak p} = \emptyset ,\quad \{a\}^{ \mathfrak p} = \{a\},\quad \left \{ \begin{array}{l} a\\ b \leftarrow a\\ c \leftarrow a,b \end{array} \right \}^{ \mathfrak p} = \left \{ \begin{array}{l} a\\ b\\ c\\ b \leftarrow a\\ c \leftarrow a\\ c \leftarrow b\\ c \leftarrow a,b \end{array} \right \}. \end{align*}
Interestingly, we have
\begin{align} P^{ \mathfrak p} = P\boxminus F_A, \end{align}
where
$F_A$
is the full program defined in equation (70).
Fact 56. The body-power-set operator is an endomorphism on
$(\mathbb P_A,\cup ,\emptyset )$
Footnote
4
thus satisfying
\begin{align*} (P\cup R)^{ \mathfrak p} &= P^{ \mathfrak p}\cup R^{ \mathfrak p}\\ \emptyset ^{ \mathfrak p} &= \emptyset . \end{align*}
Moreover, we have
\begin{align*} (P\cap R)^{ \mathfrak p} &\subseteq P^{ \mathfrak p}\cap R^{ \mathfrak p}\\ F_A^{ \mathfrak p} &= F_A. \end{align*}
Computing the least model of
$P^{ \mathfrak p}$
is easy as it contains a fact for each rule head of
$P$
and therefore
\begin{align*} (P^{ \mathfrak p})^\omega = h(P). \end{align*}
The body-power-set operator is idempotent and the identity on interpretations, that is,
\begin{align} (P^{ \mathfrak p})^{ \mathfrak p} &= P^{ \mathfrak p} \end{align}
\begin{align} I^{ \mathfrak p} &= I. \end{align}
Moreover, it can be written in terms of composition as
\begin{align} P^{ \mathfrak p} \stackrel {20}= PA^\ast . \end{align}
In particular, for any Krom program
$K$
, we can derive that identity as
\begin{align*} K^{ \mathfrak p} = K\cup h(K) \stackrel {11}= K\cup KA \stackrel {15}= K(1\cup A) \stackrel {20}= KA^\ast . \end{align*}
As a consequence, we have
\begin{align*} (KL)^{ \mathfrak p} \stackrel {85}= (KL)A^\ast \stackrel {14}= K(LA^\ast ) \stackrel {85}= KL^{ \mathfrak p}, \end{align*}
where the second identity follows by the associativity of composition with respect to Krom programs (recall that composition is in general not associative).
Similarly,
\begin{align*} (PR)^{ \mathfrak p} \stackrel {85}= (PR)A^\ast \approx P(RA^\ast ) \stackrel {85}= PR^{ \mathfrak p}, \end{align*}
where we have to invoke Proposition 6 instead of equation (14) as for Krom programs above since composition is in general associative only modulo subsumption equivalence.
An interesting identity is
\begin{align*} 1_A^{ \mathfrak p} = A^\ast . \end{align*}
For the program
$A^\oplus$
, neutral to body-intersection (55), we have
\begin{align*} (A^\oplus )^{ \mathfrak p} = F_A. \end{align*}
Hence, as a consequence of equation (82),
\begin{align*} P^{ \mathfrak p } = P\boxminus (A^\oplus )^{ \mathfrak p}. \end{align*}
We now analyze the body-power-set operator in combination with body-union. The next result shows that the body-power-set operator is a homomorphism for body-union:
Proposition 57. The body-power-set operator is an endomorphism on the monoid
$(\mathbb P_A,\sqcup ,A)$
, that is,
\begin{align*} (P\sqcup R)^{ \mathfrak p} &= P^{ \mathfrak p}\sqcup R^{ \mathfrak p}\\ A^{ \mathfrak p} & \stackrel {84}= A. \end{align*}
Proof. Since
\begin{align*} A^\ast \sqcup A^\ast \stackrel {20}= (1_A\cup A)\sqcup (1_A\cup A) = 1_A\cup A \stackrel {20}= A^\ast , \end{align*}
we may apply equation (45) and compute
\begin{align*} (P\sqcup R)^{ \mathfrak p} \stackrel {85}= (P\sqcup R)A^\ast \stackrel {45}= PA^\ast \sqcup RA^\ast \stackrel {85}= P^{ \mathfrak p}\sqcup R^{ \mathfrak p}. \end{align*}
9 Homomorphisms
This section is concerned with homomorphisms, which are structure-preserving mappings between algebras.
First, we state that interpretations under the usual set operations can be embedded into programs under the set-like operations as follows:
Proposition 58. The mapping
${}^\square :\mathbb I_A\to \mathbb P_A$
given by
\begin{align*} I^\square := \{a \leftarrow I \mid a\in A\} \end{align*}
is a monomorphism
$(\mathbb I_A,\cup ,\cap ,{}^c,\emptyset ,A)\to (\mathbb M_A,\sqcup ,\sqcap ,{}^{\unicode{x00A9}},A,A^\oplus )$
, that is,
${}^\square$
maps every interpretation
$I\in \mathbb I_A$
to a minimalist program
$I^\square \in \mathbb M_A$
such that
\begin{align} (I\cup J)^\square &= I^\square \sqcup J^\square \end{align}
\begin{align} (I\cap J)^\square &= I^\square \sqcap J^\square \end{align}
\begin{align} (I^c)^\square &= (I^\square )^{\unicode{x00A9}} \end{align}
\begin{align} \emptyset ^\square &= A \end{align}
\begin{align} A^\square &= A^\oplus . \end{align}
Proof. Follows immediately from the definitions.
Remark 59. Equations (89) and (90) mean that
$\emptyset ^\square$
and
$A^\square$
are the neutral elements
$A$
and
$A^\oplus$
with respect to
$\sqcup$
and
$\sqcap$
, respectively.
The following theorem gives us a way to construct homomorphisms bottom-up from single-element interpretations representing single atoms:
Theorem 60. Let
$A$
and
$A'$
be alphabets and let
${}^\bullet :\mathbb I_A\to \mathbb I_{A'}$
be a mapping on interpretations satisfying
\begin{align} I^\bullet &= \bigcup _{a\in I}\{a\}^\bullet , \end{align}
\begin{align} \{a\}^\bullet &\neq \emptyset ,\quad \text{for every $a\in A$}, \end{align}
\begin{align} \{a\}^\bullet \cap \{b\}^\bullet &= \emptyset ,\quad \text{for all $a,b\in A$ with $a\neq b$}. \end{align}
We extend
${}^\bullet$
to a mapping
$\mathbb P_A\to \mathbb P_{A'}$
on programs as
\begin{align*} P^\bullet := {\left \{a' \leftarrow B^\bullet \;\middle |\; a \leftarrow B\in P,\, a'\in \{a\}^\bullet \right \}}. \end{align*}
Then
\begin{align*} {}^\bullet : (\mathbb P_A,\cup ,\sqcup , \emptyset )\to (\mathbb P_{A'},\cup ,\sqcup , \emptyset ) \end{align*}
is a homomorphism satisfying
\begin{align*} P\in \mathbb I_A \quad \Leftrightarrow \quad P^\bullet \in \mathbb I_{A'}, \end{align*}
that is, a program
$P\in \mathbb P_A$
is an interpretation iff
$P^\bullet \in \mathbb P_{A'}$
is an interpretation.
Proof. Instantiating equation (91) with
$I=\emptyset$
yields
$\emptyset ^\bullet = \emptyset$
, and
${}^\bullet$
is a homomorphism with respect to
$\cup$
since
\begin{align*} (P\cup R)^\bullet &= \left \{a' \leftarrow B^\bullet \;\middle |\; a \leftarrow B\in P\cup R,\; a'\in \{a\}^\bullet \right \}\\[4pt] &= \left \{a' \leftarrow B^\bullet \;\middle |\; a \leftarrow B\in P,\; a'\in \{a\}^\bullet \right \}\cup \left \{a' \leftarrow B^\bullet \;\middle |\; a \leftarrow B\in R,\; a'\in \{a\}^\bullet \right \}\\[4pt] &= P^\bullet \cup R^\bullet . \end{align*}
To show that
${}^\bullet$
is a homomorphism with respect to
$\sqcup$
, we compute
\begin{align*} (P\sqcup R)^\bullet &= \{a \leftarrow (B\cup C) \mid a \leftarrow B\in P,\; a \leftarrow C\in R\}^\bullet \\[4pt] &= \left \{a' \leftarrow (B\cup C)^\bullet \;\middle |\; a \leftarrow B\in P,\; a \leftarrow C\in R,\; a'\in \{a\}^\bullet \right \}\\[4pt] & \stackrel {91}= {\left \{a' \leftarrow (B^\bullet \cup C^\bullet ) \;\middle |\; a \leftarrow B\in P,\; a \leftarrow C\in R,\; a'\in \{a\}^\bullet \right \}}\\[4pt] & \stackrel {93}= P^\bullet \sqcup R^\bullet , \end{align*}
where the last identity holds since
$P^\bullet \sqcup R^\bullet$
consists of all rules
$a' \leftarrow (D\cup E)$
with
$a' \leftarrow D\in P^\bullet$
and
$a' \leftarrow E\in R^\bullet$
: the inclusion from left to right is immediate from the definition of
${}^\bullet$
, and for the inclusion from right to left notice that by equation (93) the head
$a'$
determines the unique atom
$a$
satisfying
$a'\in \{a\}^\bullet$
, which means that
$D=B^\bullet$
and
$E=C^\bullet$
for rules
$a \leftarrow B\in P$
and
$a \leftarrow C\in R$
with one and the same head
$a$
.
It remains to prove the stated equivalence. Every interpretation
$I\in \mathbb I_A$
is a program consisting of facts only, which by equation (91) gives
\begin{align*} \{a \leftarrow \emptyset \mid a\in I\}^\bullet = {\left \{a' \leftarrow \emptyset ^\bullet \;\middle |\; a\in I,\; a'\in \{a\}^\bullet \right \}} = {\left \{a' \leftarrow \emptyset \;\middle |\; a'\in \bigcup _{a\in I}\{a\}^\bullet \right \}} \stackrel {91}= I^\bullet , \end{align*}
which shows that the extension of
${}^\bullet$
to programs is consistent with the given mapping on interpretations and, in particular, that
$P^\bullet$
is an interpretation whenever
$P$
is one. For the other direction, assume that
$P$
is not an interpretation and pick a proper rule
$a \leftarrow B\in p(P)$
together with an atom
$b\in B$
. By equation (92), we can pick atoms
$a'\in \{a\}^\bullet$
and
$b'\in \{b\}^\bullet$
, and equation (91) yields
$b'\in B^\bullet$
. Hence,
$a' \leftarrow B^\bullet$
is a proper rule in
$P^\bullet$
and therefore
$P^\bullet$
is not an interpretation.
Example 61. Let
$A := \{a,b\}$
and
$A' := \{a',b',c'\}$
. Define the mapping
${}^\bullet$
on interpretations in
$\mathbb I_A$
by
\begin{align*} \emptyset ^\bullet &:= \emptyset \\ \{a\}^\bullet &:= \{a',c'\}\\ \{b\}^\bullet &:= \{b'\}. \end{align*}
This forces us to put
\begin{align*} \{a,b\}^\bullet := \{a\}^\bullet \cup \{b\}^\bullet = \{a',b',c'\}. \end{align*}
Informally speaking,
${}^\bullet$
“blows up” the atom
$a$
to
$a',c'$
and leaves the atom
$b$
“unchanged”. By Theorem 60, extending
${}^\bullet$
to programs as described above we automatically get a homomorphism satisfying, for example,
\begin{align*} \left (\left \{ \begin{array}{l} a\\ b \leftarrow a \end{array} \right \}\sqcup \left \{ \begin{array}{l} a\\ b \leftarrow b \end{array} \right \}\right )^\bullet &= \left \{ \begin{array}{l} a\\ b \leftarrow a,b \end{array} \right \}^\bullet \\[5pt] &= \left \{ \begin{array}{l} a'\\ c'\\ b' \leftarrow a',b',c' \end{array} \right \}\\[5pt] &= \left \{ \begin{array}{l} a'\\ c'\\ b' \leftarrow a',c' \end{array} \right \}\sqcup \left \{ \begin{array}{l} a'\\ c'\\ b' \leftarrow b' \end{array} \right \}\\[5pt] &= \left \{ \begin{array}{l} a\\ b \leftarrow a \end{array} \right \}^\bullet \sqcup \left \{ \begin{array}{l} a\\ b \leftarrow b \end{array} \right \}^\bullet . \end{align*}
10 Decomposition
This section is concerned with syntactic and semantic decompositions of programs.
Our first observation is as follows:
Fact 62. We can syntactically decompose every program
$P$
into single-rule Krom programs as
\begin{align} P = f(P)\cup \bigcup _{a \leftarrow B\in p(P)}\bigsqcup _{b\in B}\{a \leftarrow b\}. \end{align}
For example,
\begin{align*} \left \{ \begin{array}{l} a\\ b \leftarrow a,b\\ c \leftarrow a,b,c \end{array} \right \} = \{a\}\cup (\{b \leftarrow a\}\sqcup \{b \leftarrow b\})\cup (\{c \leftarrow a\}\sqcup \{c \leftarrow b\}\sqcup \{c \leftarrow c\}). \end{align*}
In what follows, we are interested in decomposing programs with respect to body-union.
We shall now show that composition can be represented via
$\sqcup$
,
$\cup$
,
$f$
, and
$p$
which is useful given that
$\sqcup$
and
$\cup$
satisfy nice algebraic laws (see Theorems 11 and 14):
Theorem 63. For any programs
$P$
and
$R$
,
\begin{align} PR = f(P)\cup \bigcup _{a \leftarrow B\in p(P)}\bigsqcup _{b\in B}\bigcup _{b \leftarrow C\in R}\bigsqcup _{c\in C}\{a \leftarrow c\}, \end{align}
where we use the convention
$\bigsqcup _{c\in C}\{a \leftarrow c\} = \{a \leftarrow C\}$
for every atom
$a$
and every set of atoms
$C$
, so that the empty body-union of rules with head
$a$
is the fact
$a$
.
Proof.
\begin{align*} PR &= f(P)\cup \bigcup _{a \leftarrow B\in p(P)}\{a \leftarrow B\}R\\[5pt] &= f(P)\cup \bigcup _{a \leftarrow B\in p(P)}\bigsqcup _{b\in B}\{a \leftarrow b\}R\\[5pt] & \stackrel {15}= f(P)\cup \bigcup _{a \leftarrow B\in p(P)}\bigsqcup _{b\in B}\bigcup _{c \leftarrow C\in R}\{a \leftarrow b\}\{c \leftarrow C\}\\[5pt] &= f(P)\cup \bigcup _{a \leftarrow B\in p(P)}\bigsqcup _{b\in B}\bigcup _{b \leftarrow C\in R}\{a \leftarrow C\}\\[5pt] &= f(P)\cup \bigcup _{a \leftarrow B\in p(P)}\bigsqcup _{b\in B}\bigcup _{b \leftarrow C\in R}\bigsqcup _{c\in C}\{a \leftarrow c\}, \end{align*}
where the first identity uses
$f(P)R=f(P)$
together with equation (9). For the second identity, we first write
$\{a\leftarrow B\}=\bigsqcup _{b\in B}\{a\leftarrow b\}$
and then apply equation (45) iteratively. This is legitimate since the bodies
$\{b\}$
,
$b\in B$
, are pairwise disjoint and therefore satisfy case (i).
Recall from equation (15) that Krom programs have the nice property that composition distributes over union from both sides which is not the case in general (see equation (12)). Decomposing programs into Krom programs is thus desirable. We shall now prove the main results of the paper showing that every program can be
$\sqcup$
-decomposed into Krom programs (Theorems 66 and 68), but before we can give the formal proofs we first introduce some auxiliary notions and then illustrate the main idea with an example:
Definition 64. Define the
$\textit{body-or}$
of
$P$
as
\begin{align*} P^\lor := f(P)\cup \{a \leftarrow b \mid a \leftarrow B\in p(P),\; b\in B\}. \end{align*}
Notice that the body-or of a program is always a Krom program consisting only of rules with at most one body atom. For example, we have
\begin{align*} \left \{ \begin{array}{l} a\\ a \leftarrow b,c \end{array} \right \}^\lor = \left \{ \begin{array}{l} a\\ a \leftarrow b\\ a \leftarrow c \end{array} \right \}. \end{align*}
Example 65. Now consider the minimalist program
\begin{align*} M := \left \{ \begin{array}{l} a\\ b\\ c \leftarrow a,b\\ d \leftarrow a,b,d \end{array} \right \}. \end{align*}
We show that we can decompose
$M$
with width
$w(M)=3$
into three Krom programs
$K_1,K_2,K_3$
, where
\begin{align*} K_1,K_2,K_3\subseteq M^\lor = \left \{ \begin{array}{l} a\\ b\\ c \leftarrow a\\ c \leftarrow b\\ d \leftarrow a\\ d \leftarrow b\\ d \leftarrow d \end{array} \right \}, \end{align*}
such that
\begin{align} M = K_1\sqcup K_2\sqcup K_3 \end{align}
and
\begin{align*} M^\omega = K_1^\omega \sqcup K_2^\omega \sqcup K_3^\omega . \end{align*}
For this, define
\begin{align*} K_1 := \left \{ \begin{array}{l} a\\ b\\ c \leftarrow a\\ d \leftarrow a \end{array} \right \},\quad K_2 := \left \{ \begin{array}{l} a\\ b\\ c \leftarrow b\\ d \leftarrow b \end{array} \right \},\quad K_3 := \left \{ \begin{array}{l} a\\ b\\ c \leftarrow b\\ d \leftarrow d \end{array} \right \}. \end{align*}
We have equation (96) and
\begin{align*} M^\omega = \{a,b,c\} = \{a,b,c,d\}\cap \{a,b,c,d\}\cap \{a,b,c\} = K_1^\omega \cap K_2^\omega \cap K_3^\omega \stackrel {48}=K_1^\omega \sqcup K_2^\omega \sqcup K_3^\omega . \end{align*}
We are now ready to prove the following decomposition theorem for minimalist programs containing at most one rule for each rule head by generalizing the reasoning in Example 65:
Theorem 66 (Minimalist decomposition theorem). Let
$M$
be a minimalist program and put
\begin{align*} m := \max \{1,w(M)\}. \end{align*}
Then there are Krom programs
\begin{align*} K_1,\ldots ,K_m\subseteq M^\lor \end{align*}
such that
\begin{align} M = K_1\sqcup \ldots \sqcup K_m \end{align}
and
\begin{align} M^\omega = K_1^\omega \sqcup \ldots \sqcup K_m^\omega \stackrel {48}= K_1^\omega \cap \cdots \cap K_m^\omega . \end{align}
Proof. Since
$M$
is minimalist, for every
$a\in h(M)$
there is a unique rule
\begin{align*} r_a = a\leftarrow B_a \end{align*}
in
$M$
.
We first choose, for every non-empty body
$B_a$
, a distinguished atom
$b_a^\ast \in B_a$
. If
$a\notin M^\omega$
, choose
\begin{align*} b_a^\ast \in B_a- M^\omega . \end{align*}
Such an atom exists. Indeed, if
$B_a\subseteq M^\omega$
, then
\begin{align*} a\in MM^\omega = M^\omega , \end{align*}
contrary to
$a\notin M^\omega$
. If
$a\in M^\omega$
, choose
$b_a^\ast$
arbitrarily from
$B_a$
.
Since
$|B_a|\leq m$
, for every non-empty
$B_a$
we can choose atoms
\begin{align*} b_{a,1},\ldots ,b_{a,m}\in B_a \end{align*}
such that
\begin{align*} b_{a,1}=b_a^\ast \quad \text{and}\quad B_a=\{b_{a,1},\ldots ,b_{a,m}\}. \end{align*}
If
$|B_a|\lt m$
, the remaining positions are filled by repeating arbitrary atoms of
$B_a$
.
For
$1\leq i\leq m$
, define
\begin{align*} K_i := f(M)\cup \{a\leftarrow b_{a,i} \mid a\leftarrow B_a\in p(M)\}. \end{align*}
Every
$K_i$
is a Krom program. Moreover, every rule
$a\leftarrow b_{a,i}$
belongs to
$M^\lor$
, and hence
\begin{align*} K_i\subseteq M^\lor . \end{align*}
For every
$a\in h(M)$
, the unique rules with head
$a$
in the programs
$K_1,\ldots ,K_m$
have bodies whose union is
$B_a$
. Consequently,
\begin{align*} K_1\sqcup \ldots \sqcup K_m = \{a\leftarrow B_a\mid a\in h(M)\} = M. \end{align*}
This proves equation (97).
We next compare the least models. For every interpretation
$I$
and every
$i$
, we have
\begin{align*} MI\subseteq K_i I. \end{align*}
Indeed, whenever
$B_a\subseteq I$
, we also have
$b_{a,i}\in I$
. Facts are present in both
$M$
and
$K_i$
. By induction on the iterations of the immediate consequence operators, it follows that
\begin{align*} M^\omega \subseteq K_i^\omega \qquad (1\leq i\leq m). \end{align*}
It remains to show that the first component introduces no new atoms. We claim that
$M^\omega$
is a model of
$K_1$
. Consider a rule in
$K_1$
. If it is a fact, then its head belongs to
$f(M)\subseteq M^\omega$
. Otherwise, it has the form
\begin{align*} a\leftarrow b_{a,1}. \end{align*}
If
$a\in M^\omega$
, this rule is satisfied by
$M^\omega$
. If
$a\notin M^\omega$
, then the construction of
$b_{a,1}$
gives
\begin{align*} b_{a,1}=b_a^\ast \notin M^\omega , \end{align*}
so the body of the rule is false in
$M^\omega$
. Thus every rule of
$K_1$
is satisfied by
$M^\omega$
, and therefore
\begin{align*} K_1^\omega \subseteq M^\omega . \end{align*}
Together with the opposite inclusion proved above, this yields
\begin{align*} K_1^\omega =M^\omega . \end{align*}
Finally,
\begin{align*} M^\omega =K_1^\omega \subseteq K_i^\omega \qquad (1\leq i\leq m), \end{align*}
and hence
\begin{align*} K_1^\omega \cap \ldots \cap K_m^\omega =M^\omega . \end{align*}
Since body-union coincides with intersection on interpretations by equation (48), we obtain
\begin{align*} K_1^\omega \sqcup \ldots \sqcup K_m^\omega = K_1^\omega \cap \ldots \cap K_m^\omega = M^\omega . \end{align*}
This proves equation (98).
Remark 67. The decomposition in equation (97) is not unique. The condition in equation (97) is essential since without it, we can simply choose
$M^\omega$
— which is an interpretation and thus trivially Krom — as our “decomposition.”
Theorem 68 (Decomposition theorem). Let
$P$
be a program and put
\begin{align*} m := \max \{1,w(P)\}. \end{align*}
Then there are Krom programs
\begin{align*} K_1,\ldots ,K_m\subseteq P^\lor \end{align*}
such that
\begin{align} P &\subseteq K_1\sqcup \cdots \sqcup K_m \end{align}
and
\begin{align} P^\omega &\subseteq K_1^\omega \sqcup \cdots \sqcup K_m^\omega \stackrel {48}= K_1^\omega \cap \cdots \cap K_m^\omega . \end{align}
Proof. Since
$|B|\leq m$
holds for every rule
$a \leftarrow B\in p(P)$
, we can choose for every such rule
$r = a \leftarrow B$
atoms
\begin{align*} b_{r,1},\ldots ,b_{r,m}\in B \quad \text{such that}\quad B = \{b_{r,1},\ldots ,b_{r,m}\}, \end{align*}
where in case
$|B|\lt m$
the remaining positions are filled by repeating arbitrary atoms of
$B$
. For
$1\leq i\leq m$
, define
\begin{align*} K_i := f(P)\cup \{a \leftarrow b_{r,i} \mid r = a \leftarrow B\in p(P)\}. \end{align*}
Every
$K_i$
is a Krom program and every one of its rules occurs in
$P^\lor$
, which gives
$K_i\subseteq P^\lor$
.
We first prove equation (99). Let
$a \leftarrow B\in P$
. In case
$B=\emptyset$
, we have
$a\in f(P)\subseteq K_i$
for every
$i$
and hence
$a\in K_1\sqcup \cdots \sqcup K_m$
. In case
$r = a \leftarrow B\in p(P)$
, the rule
$a \leftarrow b_{r,i}$
belongs to
$K_i$
for every
$i$
, and the body-union of these
$m$
rules is
\begin{align*} a \leftarrow (\{b_{r,1}\}\cup \ldots \cup \{b_{r,m}\}) = a \leftarrow B, \end{align*}
which shows
$a \leftarrow B\in K_1\sqcup \cdots \sqcup K_m$
. Notice that in contrast to Theorem 66 we cannot expect equality here, since the body-union also combines rules originating from different rules of
$P$
with the same head, thus producing rules not occurring in
$P$
(see Example 69).
We now prove equation (100). Let
$I$
be an arbitrary interpretation and let
$a\in PI$
, that is, there is a rule
$a \leftarrow B\in P$
with
$B\subseteq I$
. In case
$B=\emptyset$
, we have
$a\in f(P)\subseteq K_i$
and hence
$a\in K_iI$
; and in case
$r = a \leftarrow B\in p(P)$
, we have
$b_{r,i}\in B\subseteq I$
and therefore
$a\in K_iI$
as well. This shows
\begin{align*} P\lesssim K_i \quad (1\leq i\leq m), \end{align*}
which by equations (17) and (22) yields
$P^\omega \subseteq K_i^\omega$
for every
$i$
and hence
\begin{align*} P^\omega \subseteq K_1^\omega \cap \cdots \cap K_m^\omega \stackrel {48}= K_1^\omega \sqcup \cdots \sqcup K_m^\omega . \end{align*}
The next example provides an intuition why we cannot turn the inclusion in Theorem 68 into an equality:
Example 69. The non-minimalist program
\begin{align*} P := \left \{ \begin{array}{l} a \leftarrow b,c\\ a \leftarrow d,e \end{array} \right \} \end{align*}
cannot be
$\sqcup$
-decomposed into Krom programs. Consider, for instance,
\begin{align*} \left \{ \begin{array}{l} a \leftarrow b\\ a \leftarrow d \end{array} \right \}\sqcup \left \{ \begin{array}{l} a \leftarrow c\\ a \leftarrow e \end{array} \right \} = \left \{ \begin{array}{l} a \leftarrow b,c\\ a \leftarrow \underline {b,e}\\ a \leftarrow \underline {d,c}\\ a \leftarrow d,e \end{array} \right \}, \end{align*}
where the body-union produces the two underlined rules not occurring in
$P$
. This is not an artifact of the particular choice. Suppose
$P = K_1\sqcup \ldots \sqcup K_n$
for Krom programs
$K_1,\ldots ,K_n$
. Since every rule in
$P$
has head
$a$
, each
$K_i$
contains at least one rule with head
$a$
, and by the definition of body-union there are bodies
$B_1,\ldots ,B_n$
and
$C_1,\ldots ,C_n$
of rules with head
$a$
in
$K_1,\ldots ,K_n$
satisfying
\begin{align*} B_1\cup \ldots \cup B_n = \{b,c\} \quad \text{and}\quad C_1\cup \ldots \cup C_n = \{d,e\}. \end{align*}
As each
$B_i$
contains at most one atom, we have
$B_i = \{b\}$
for some
$i$
, and replacing
$C_i$
by
$B_i$
in the second selection yields a rule in
$K_1\sqcup \ldots \sqcup K_n = P$
whose body contains
$b$
and is contained in
$\{b,d,e\}$
— contradicting the fact that the only rule in
$P$
with
$b$
occurring in its body is
$a \leftarrow b,c$
.
11 Towards applications to automatic logic programming
Automatic logic programming studies the construction of logic programs from specifications and background knowledge (Deville and Lau Reference Deville and Lau1994). A key challenge in this setting is to provide principled mechanisms for combining and transforming programs while preserving their semantics.
In this section, we sketch how the set-like operations introduced in this paper can contribute to this goal by enabling structured manipulations of programs and supporting decomposition-based approaches to program construction.
Beyond these examples, algebraic operations on logic programs are also relevant to program transformation and optimization (Fuchs and Fromherz Reference Fuchs and Fromherz1992; Partsch and Steinbrüggen Reference Partsch and Steinbrüggen1983).
11.1 Algebraic semantics
A central requirement for algebraic reasoning about logic programs is the ability to decompose complex programs into simpler components in such a way that their semantics can be derived from the semantics of these components.
Theorems 66 and 68 provide two related structural results: minimalist programs admit exact representations in terms of Krom components, whereas arbitrary programs admit corresponding syntactic and semantic upper approximations. In the minimalist case, the least model is the intersection of the least models of the components.
Krom programs satisfy algebraic laws such as associativity equation (14) and left-distributivity equation (15), which fail for arbitrary programs. The decomposition results therefore provide structural representations in terms of algebraically simpler components. Since the construction used in Theorem 66 depends on the least model of the original program, however, the theorem does not by itself yield an algorithmic reduction of reasoning to the components.
11.2 Schema-based transformation
Program schemes provide a common mechanism for representing reusable program fragments that can be instantiated to obtain concrete programs (Greibach Reference Greibach1975; Flener Reference Flener1995; Fuchs and Fromherz Reference Fuchs and Fromherz1992).
Within an algebraic setting, such schemes can be naturally understood as terms (or polynomials) over logic programs, where programs act as constants, algebraic operations as function symbols, and program variables as placeholders (see e.g. Burris and Sankappanavar (Reference Burris and Sankappanavar1981), Section II.1). For example, the term
$\{a \leftarrow b\}\sqcup X$
defines a schema that can be instantiated with a program
$P$
to yield
$\{a \leftarrow b\}\sqcup P$
, thus inducing a transformation on programs.
Crucially, the expressive power of such schemes depends on the underlying algebra of programs. Introducing new algebraic operations expands the space of definable transformations. In particular, the set-like operations considered in this paper enable schemes that are not expressible in a natural way without them, such as those based on body-union.
11.3 Inductive logic programming
In ILP (Shapiro Reference Shapiro1981; Muggleton Reference Muggleton1991; Nienhuys-Cheng and de Wolf Reference Nienhuys-Cheng and de Wolf1997; Cropper and Dumančić Reference Cropper and Dumančić2022), (partial) specifications consist of sets of positive and negative examples in the form of interpretations
$I_+$
and
$I_-$
, respectively, and the task is, given some background program
$R$
, to find a program
$P$
such that
\begin{align*} I_+\subseteq (P\cup R)^\omega \quad \text{and}\quad I_-\cap (P\cup R)^\omega = \emptyset . \end{align*}
From an algebraic perspective, this task amounts to searching the space of programs under the least model operator and its interaction with program composition. A key difficulty is that this search space is typically large and poorly structured.
Algebraic operations on programs provide a way to impose structure on this space. In particular, the decomposition results established in Theorems 66 and 68 allow one to reduce the search for a solution to reasoning about simpler components, since they make explicit how the behavior of a program emerges from the behavior of its parts.
11.4 Learning from interpretation transitions
Closely related to ILP Section 11.3 is the following learning setting introduced in Inoue et al. (Reference Inoue, Ribeiro and Sakama2014).
Every logic program
$P$
is a state transition system that maps, via its immediate consequence van Emden-Kowalski operator
$T_P$
, every state of the world represented as an interpretation
$I$
to a next state
$T_P(I)$
(Inoue Reference Inoue2011; Inoue and Sakama Reference Inoue and Sakama2012).
The learning setting now is as follows. The positive examples are given by pairs of interpretations
$(I,J)$
and the task is to find a program
$P$
such that
$T_P(I) = J$
holds for each such pair. Notice that by equation (16), this is equivalent to finding a program
$P$
satisfying
$PI = J$
via sequential composition of
$P$
with
$I$
.
We are thus interested in the transition behavior of programs with respect to the composition with interpretations and in this paper, we have derived numerous results in that direction. In fact, every result showing identities (modulo subsumption equivalence) between programs can be instantiated with interpretations to yield results concerning the behavior of programs with respect to interpretations. For example, Theorem 17 shows
\begin{align*} (P\sqcup R)I = PI\sqcup RI \stackrel {48}= PI\cap RI, \end{align*}
which means that if we have programs
$P$
and
$R$
, then
$P\sqcup R$
is a solution to the state transition
$(I,PI\cap RI)$
. Here the benefit of representing the solution program as the body-union of its two factors
$P$
and
$R$
is that it provides a better understanding of the inner workings of the program.
11.5 Analogical logic programming
In analogical logic programming — recently introduced in Antić (Reference Antić2025) — the task is as follows.
Given a proportional equation of the form
$P:Q::R:X$
— read as “
$P$
is to
$Q$
what
$R$
is to
$X$
” — where
$P,Q,R$
are programs and
$X$
is a program variable, we wish to find solutions
$S_1,S_2,\ldots$
such that
$P:Q::R:S_i$
for all
$i$
, in which case we say that
$P,Q,R,S_i$
are in an analogical proportion.Footnote
5
That is, we generate novel programs from “known” ones via analogical transfer instead of starting with a partial specification as in ILP Section 11.3.
Analogical proportions formalize the idea that analogy-making is the task of transforming different objects from the source to the target domain in “the same way” (which is why “copycat” is the name of a prominent model of analogy-making (Hofstadter and Mitchell Reference Hofstadter and Mitchell1995); and see Correa et al. (Reference Correa, Prade and Richard2012)).
At the formal level, we instantiate a recently introduced abstract algebraic framework of analogical proportions (Antić Reference Antić2022) in our setting of logic programming, where we will restrict ourselves to the functorial fragment (Antić Reference Antić2025):Footnote 6
Definition 70 (Logic program proportions). Let
$P,Q,R,S$
be programs. We say that
$P$
$\textit{transforms into}$
$Q$
$\textit{as}$
$R$
$\textit{transforms into}$
$S$
— in symbols,
$P\to Q :: R\to S$
— if there is a schema
$\textbf {F}(X)$
such that
$Q = \textbf {F}(P)$
and
$S = \textbf {F}(R)$
, in which case we call
$\textbf {F}$
a
$\textit{justification}$
of
$P\to Q :: R\to S$
. We call an expression of the form
$P\to Q :: R\to S$
an
$\textit{arrow proportion}$
.
We now say that
$P$
$\textit{is to}$
$Q$
$\textit{as}$
$R$
$\textit{is to}$
$S$
— in symbols,
$P:Q::R:S$
— if
$P\to Q :: R\to S$
and
$Q\to P :: S\to R$
, that is, if there are schemes
$\textbf {F}$
and
$\textbf {G}$
such that
$Q = \textbf {F}(P)$
,
$S = \textbf {F}(R)$
,
$P = \textbf {G}(Q)$
, and
$R = \textbf {G}(S)$
, in which case we call the pair
$(\textbf {F},\textbf {G})$
a
$\textit{justification}$
of
$P:Q::R:S$
. We call an expression of the form
$P:Q::R:S$
a
$\textit{(logic program) proportion}$
.
Since Definition 70 uses program schemes, the underlying algebra of programs is essential and, importantly, the set-like operations introduced in this paper allow us to derive (plausible) proportions which would otherwise not be expressible.
We shall now illustrate logic program proportions with some simple examples:
Example 71. We have the proportion
\begin{align*} \{a\} : \{a,b\} :: \{c\} : \{c,b\} \end{align*}
between interpretations as justified by the schemes
\begin{align*} \textbf {F}(X) := X\cup \{b\} \quad \text{and}\quad \textbf {G}(X) := X- \{b\}. \end{align*}
Example 72. The proportion
\begin{align*} \{a\} : \{a,b\} :: \{c\} : \{c\} \end{align*}
is justified by
\begin{align*} \textbf {F}(X) := \left \{ \begin{array}{l} a \leftarrow a\\ b \leftarrow a\\ c \leftarrow c \end{array} \right \}X \quad \text{and}\quad \textbf {G}(X) := \left \{ \begin{array}{l} a \leftarrow a\\ a \leftarrow b\\ c \leftarrow c \end{array} \right \}X. \end{align*}
Proposition 73. For any programs
$P$
and
$R$
,
\begin{align} P : P^{\unicode{x00A9}} :: R : R^{\unicode{x00A9}}. \end{align}
Proof. An immediate consequence of equation (59).
Example 74. Let
$A := \{a,b,c\}$
. As a consequence of equation (101) we have, for example,
\begin{align} \left \{ \begin{array}{l} a \leftarrow b\\ b \leftarrow a\\ c \leftarrow c \end{array} \right \} : \left \{ \begin{array}{l} a \leftarrow a,c\\ b \leftarrow b,c\\ c \leftarrow a,b \end{array} \right \} :: \left \{ \begin{array}{l} a \leftarrow a\\ b \leftarrow b\\ c \leftarrow c \end{array} \right \} : \left \{ \begin{array}{l} a \leftarrow b,c\\ b \leftarrow a,c\\ c \leftarrow a,b \end{array} \right \} \end{align}
which can be written more concisely as follows.
Every permutation
$\pi$
of
$A$
gives rise to a
$\textit{permutation program}$
over
$A$
— again denoted by
$\pi$
— via
\begin{align} \pi := \{\pi (a) \leftarrow a \mid a\in A\}. \end{align}
We will use the well-known cycle notation.Footnote
7
For example, the permutation
$\pi _{(a\,b\,c)}$
, which is defined as the mapping
$a\mapsto b$
,
$b\mapsto c$
,
$c\mapsto a$
, gives rise to the permutation program
\begin{align*} \pi _{(a\,b\,c)} = \left \{ \begin{array}{l} b \leftarrow a\\ c \leftarrow b\\ a \leftarrow c \end{array} \right \}. \end{align*}
Notice that every permutation program is minimalist and Krom. In the cycle notation used below, cycles of length one are included, so that the atoms occurring in the notation are exactly the elements of the underlying alphabet.
Moreover, define the
$\textit{diagonal program}$
over
$A$
as the minimalist program
\begin{align} \Delta _A := \{a \leftarrow (A- \{a\}) \mid a\in A\}. \end{align}
For example, we have
\begin{align*} \Delta _{\{a\}} = \{a\},\quad \Delta _{\{a,b\}} = \pi _{(a\,b)},\quad \Delta _{\{a,b,c\}} = \left \{ \begin{array}{l} a \leftarrow \quad b,c\\ b \leftarrow a,\quad c\\ c \leftarrow a,b \end{array} \right \}. \end{align*}
We can now rewrite equation (102) more compactly as
\begin{align*} \pi _{(a\,b)(c)} : \pi _{(a\,b)(c)}^{\unicode{x00A9}} :: 1_A : \Delta _A, \end{align*}
where
$\pi _{(a\,b)(c)}$
is a permutation program,
$1_A$
is a unit program defined in equation (6), and
$\Delta _A$
is a diagonal program.
Proposition 75. Let
$P,Q,R$
be programs such that
$Q$
is minimalist and
-
(i)
$B\cap C = \emptyset$
, for all
$a \leftarrow B\in P$
and
$a \leftarrow C\in Q$
; -
(ii)
$D\cap C = \emptyset$
, for all
$a \leftarrow D\in R$
and
$a \leftarrow C\in Q$
; -
(iii)
$h(P)\cup h(R)\subseteq h(Q)$
.
Then
\begin{align*} P : P\sqcup Q :: R : R\sqcup Q. \end{align*}
Proof. Since
$Q$
is minimalist, for every
$a\in h(Q)$
there is a unique rule
$a \leftarrow C_a\in Q$
. We show
$(P\sqcup Q)\boxminus Q = P$
; the identity
$(R\sqcup Q)\boxminus Q = R$
is proved analogously using (ii) instead of (i). By (iii), every rule head of
$P$
occurs in
$Q$
, which by minimalism of
$Q$
gives
\begin{align*} P\sqcup Q = \{a \leftarrow (B\cup C_a) \mid a \leftarrow B\in P\} \end{align*}
and therefore, again by minimalism of
$Q$
,
\begin{align*} (P\sqcup Q)\boxminus Q = \{a \leftarrow ((B\cup C_a) - C_a) \mid a \leftarrow B\in P\} = \{a \leftarrow (B - C_a) \mid a \leftarrow B\in P\} = P, \end{align*}
where the last identity holds by (i). Consequently, the schemes
\begin{align*} \textbf {F}(X) := X\sqcup Q \quad \text{and}\quad \textbf {G}(X) := X\boxminus Q \end{align*}
satisfy
$\textbf {F}(P) = P\sqcup Q$
,
$\textbf {F}(R) = R\sqcup Q$
,
$\textbf {G}(P\sqcup Q) = P$
, and
$\textbf {G}(R\sqcup Q) = R$
, which by Definition 70 means that
$(\textbf {F},\textbf {G})$
is a justification of the stated proportion.
Example 76. As a consequence of Proposition 75, we have
\begin{align*} \{a\} : \{a \leftarrow c\} :: \{b\} : \{b \leftarrow c\}, \end{align*}
justified by
\begin{align*} \textbf {F}(X) := X\sqcup \left \{ \begin{array}{l} a \leftarrow c\\ b \leftarrow c \end{array} \right \} \quad \text{and}\quad \textbf {G}(X) := X\boxminus \left \{ \begin{array}{l} a \leftarrow c\\ b \leftarrow c \end{array} \right \}. \end{align*}
12 Conclusion
In this paper, we introduced a family of algebraic operations on propositional Horn logic programs that generalize classical set-theoretic constructions, including union, intersection, complement, subtraction, symmetric difference, and power set (see Sections 3–8). While inspired by set theory, these operations exhibit fundamentally different behavior due to the rule-based structure of logic programs, in particular through non-idempotence and non-trivial interactions between rules sharing the same head.
These operations provide a structured means of decomposing and recomposing logic programs, which allowed us to establish the Decomposition Theorems 66 and 68. As illustrated in Section 11, they offer a basis for approaching problems in automatic logic programming from an algebraic perspective, including program construction, transformation, and analysis.
A natural direction for future work is the extension of this framework beyond the propositional Horn setting. In particular, lifting these operations to first-order and higher-order logic programs (Lloyd Reference Lloyd1987; Apt Reference Apt1990; Chen et al. Reference Chen, Kifer and Warren1993; Miller and Nadathur Reference Miller and Nadathur2012), as well as to answer set programs with negation as failure (Gelfond and Lifschitz Reference Gelfond and Lifschitz1991; Marek and Truszczyński Reference Marek and Truszczyński1999; Brewka et al. Reference Brewka, Eiter and Truszczyński2011; Lifschitz Reference Lifschitz2019), raises substantial technical challenges. For instance, the definition of a body-complement operation in the first-order setting is non-trivial, as rule bodies are required to be finite, preventing a direct generalization of the propositional case. Developing suitable generalizations that preserve the algebraic structure identified in this paper remains an open problem.
More broadly, the results highlight an algebraic structure of the class of logic programs considered here: minimalist programs can be decomposed into and constructed from Krom components while preserving their least-model semantics, whereas arbitrary programs admit corresponding syntactic and semantic approximations. In this respect, the results complement earlier algebraic approaches to logic programming and may support the further development of compositional methods for program synthesis and transformation.
Data availability statement
The manuscript has no data associated.
Competing interests
The author declares none.
Use of artificial intelligence tools
OpenAI Codex (GPT-5, accessed on 4 August 2026, https://openai.com/codex/) was used to analyze an earlier proof of the Minimalist Decomposition Theorem 66, identify a gap in that argument, and assist in drafting a corrected proof.
Anthropic’s Claude (Opus 5, accessed on 7 August 2026, https://claude.ai) was subsequently used to check the manuscript for mathematical and expository errors. It assisted in testing algebraic identities, identifying counterexamples, missing hypotheses, and an omitted empty-body case, and in drafting and verifying corrected statements, proofs, and examples. This included the results on distributivity and subsumption equivalence in Theorems 17, 41, and Lemma 19, as well as the Decomposition Theorems 66 and 68.
Both systems also assisted in revising the abstract and the introduction. The author reviewed and independently verified all resulting statements and arguments and takes full responsibility for the correctness and content of the manuscript.
Open access
