A semantics for definite programs

The results in this section are based on [NaishNaish2000b]. However, some definitions are changed slightly to make the subsequent treatment of negation simpler. We don't consider our semantics for definite programs particularly useful for programmers in its own right. However, this section introduces several things used in our semantics for normal programs and is useful for comparison purposes and any work on analysis of definite programs. We use a variant of definite clauses which we call disjunctive definite clauses (disjunctions only appear in the body, not the head), primarily so conjunction and disjunction can be treated more uniformly in the logic, though it also eases the transition to semantics for normal programs, as does our use of an equality predicate rather than head unification. We also use the constraint view of equality at some points, rather than substitutions. This avoids some technicalities and would make adding a ``not equals'' primitive simpler (something definitely worth doing if negation is supported).

Definition 1   A disjunctive definite program is a collection of predicate definitions, each a single clause $H \leftarrow (B_1 \vee B_2 \vee \ldots \vee B_n)$, where each $B_i$ is a conjunction of atoms. $H$ is an atom $p(V_1 , V_2 , \ldots V_n )$ where the $V_i$ are distinct variables and each $B_j$ is prefixed by a sequence of calls to a built-in equality predicate/constraint $V_i = T_i$, where $T_i$ is a term, for each variable $V_i$. Other atoms in the $B_j$ are user-defined. The $V_i$ are called head variables; others are called local variables. A head instance of a clause is an instance where head variables are replaced by terms and body variables are replaced by (new) distinct variables.

Disjunctive definite programs can be mapped to definite clause programs trivially: each disjunct leads to a clause $p(T_1 , T_2 , \ldots T_n ) \leftarrow B_j'$, where $B_j'$ is $B_j$ without the initial calls to $= / 2$. Definite clause programs can easily be mapped to disjunctive definite programs by renaming variables, converting head unification into calls to the equality predicate and combining all clauses for a predicate into a single disjunctive clause. This is similar to the completion of a program [ClarkClark1978]. We use these equivalences implicitly when relating properties of disjunctive programs and their Horn clause counterparts.

An intended interpretation associates each ground atom with one of three truth values: true, false or inadmissible. We sometimes abbreviate these to $\textbf{T}$, $\textbf{F}$ and $\textbf{I}$ (bold font). We also use these letters in italics to refer to sets of user-defined atoms assigned that truth value. When describing interpretations we use the notation $\langle I,T\rangle$ for the interpretation which maps the (ground) atoms in $I$ to inadmissible, those in $T$ to true and other user-defined atoms to false. Equality has a fixed interpretation. $E$ is the set of all ground equality atoms of the form $X = X$. These equality atoms are considered true; others are considered false. This essentially restricts interpretations to be Herbrand interpretations.

Programmers do need to consider the fact that their programs manipulate Herbrand terms. It can also be useful to think at a higher level, where terms may represent values in some other domain and two terms may represent the same value. However, Prolog does not respect this form of equality. Only syntactic equality is supported and programmers must write explicit equality predicates or convert terms into canonical form and be very careful with input-output modes. Although results for arbitrary models hold for definite programs, they typically do not hold when negation is introduced and arbitrary models are not very useful for programmers.

Inadmissible atoms may succeed or fail according to the procedural semantics but this distinction is not made in the declarative semantics. Our semantics is thus less precise than the traditional semantics, to reflect the lack of precision of programmers. If we consider calls to merge/3 where the first two arguments are sorted lists then programmers typically know which ones should succeed. For other (inadmissible) calls to merge/3, programmers typically don't know and don't care precisely which calls succeed. Our semantics aims at providing tools to reason about program correctness without the need for additional precision and without unnecessary restrictions on programming style. We define operational, model theoretic and fixpoint semantics then discuss the relationships between them.