Fixpoint semantics

After [FittingFitting1985] (using the terminology of [Apt and BolApt and Bol1994]), we define $T3_P$, an analogue of $T_P$ which maps interpretations to interpretations. For simplicity, we define it in terms of the model theory ($T_P$ could be defined in the same way -- the inadmissible case would never arise).

Definition 6   $T3_P(M)$ is the interpretation such that an atom $A$ is

1. true, if there is a clause instance $A \leftarrow B$ where $B$ is true in $M$,
2. false, if for all clause instances $A \leftarrow B$, $B$ is false in $M$ and
3. inadmissible, otherwise.

$T3_P$ generalises $T_P$: if there are no inadmissible atoms in $M$ there are none in $T3_P(M)$. Various properties of $T3_P$ are discussed in [Apt and BolApt and Bol1994]. One important result is that a least fixpoint with respect to the information ordering exists.

Another immediate consequence operator, $T3^{+}_P$, which retains the truth value of inadmissible atoms, was introduced in [NaishNaish2000b] (where it was called $C_P^{\prime}$). Essentially, inadmissible atoms are assumed to succeed.

Definition 7   $T3^{+}_P(M)$ is the interpretation such that an atom $A$ is

1. inadmissible, if $A$ is inadmissible in $M$,
2. true, if $A$ is admissible and there is a clause instance $A \leftarrow B$ where $B$ is true or inadmissible in $M$,
3. false, otherwise.

Like $T3_P$, $T3^{+}_P$ generalises $T_P$. If $I$ is empty, $T3^{+}_P$ is equivalent to $T_P$ and thus each fixpoint of $T_P$ corresponds to a fixpoint of $T3^{+}_P$. Fixpoints of $T3_P$ are also fixpoints of $T3^{+}_P$. Generally $T3^{+}_P$ has additional fixpoints as well. It is particularly useful when the set of inadmissible atoms in the intended interpretation is known. Using $T3^{+}_P$, analysis can restrict attention to the behaviour of admissible atoms. If (in)admissibility can be determined from the program, for example, from type/mode declarations, automatic analysis may benefit. In any case it simplifies manual analysis and avoids analysis which can often be non-intuitive.

For example, suppose $M$ is our intended interpretation for merge/3. The inadmissible atoms in $T3^{+}_P(M)$ are the same as those in $M$. To find the true atoms in $T3^{+}_P(M)$ we consider each clause and determine what admissible atoms can be derived in one step from the true and inadmissible atoms in $M$. For the first two clauses we can ignore inadmissible atoms such as merge([],a,a). For the last two clauses it is easy to show that if the clause head is admissible then the recursive call is admissible, so we can ignore inadmissible atoms such as merge([2,3], [2,1], [2,1,2,3]). This ``forward'' reasoning essentially replaces reasoning about inadmissible atoms. Forward reasoning is more procedural in nature [NaishNaish1993] and essential for reasoning about instantiatedness of calls (something logic programmers must consider). It is simple to establish that the true atoms in $T3^{+}_P(M)$ are a subset of those in $M$ (in fact, they are equal). From this we can conclude $M$ is a model (see below).