26
Mathematical Aspects of Logic Programming Semantics
a binary function whose intended meaning is the list constructor whose first
argument is the head of the list and whose second argument is its tail. Thus,
the program Length is intended to be a recursive definition of the “length of
lists” using the successor notation for natural numbers as in Program 2.1.3.
Length is an example of a definite program.
Thus far, we have specified the syntax of logic programs. We now turn our
attention to dealing with their semantics, and this is based on Definitions 1.2.7
and 1.2.8 of Chapter 1 with some notation peculiar to logic programming.
2.1.5 Definition Let P be a program with underlying language L P , and
let D be a non-empty set. A preinterpretation J for P with domain D is a
preinterpretation J for L P with domain D.
Let J be a preinterpretation for the program P , with domain D, and
let θ be a J-variable assignment. For a typical clause C in P of the form
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k , we let (Cθ)
J denote
(Aθ)
J ← (A 1 θ)
J , . . . , (A n θ)
J , ¬(B 1 θ)
J , . . . , ¬(B k θ)
J .
We call (Cθ)
J a J-ground instance
3 of C. By ground J (P ), we denote the set
of all J-ground instances of clauses in P . We denote by B P,J the set B L P ,J of
all J-ground instances of atoms in L P , that is, the collection of all elements
of the form p(d 1 , . . . , d n ), where p is an n-ary predicate symbol in L P and
d 1 , . . . , d n ∈ D. Usually, we will be working over a fixed, but arbitrary, preinterpretation J. In order to ease notation, we will often omit mention of J if it
causes no confusion, and instead of writing B P,J , ground J (P ), J-ground instance, etc., we will simply write B P , ground(P ), ground instance, etc. We will
frequently abuse notation even further by referring to elements of ground J (P )
as (ground ) clauses and by applying to ground clauses terminology, such as
“definite”, already defined for program clauses.
Of particular interest is the so-called Herbrand preinterpretation of a program. Its importance rests on the fact that, for many purposes, restricting
to Herbrand preinterpretations causes no loss of generality.
4 For example, in
classical first-order logic, a set of clauses has a model if and only if it has a Herbrand model. Indeed, in many cases in the literature on the subject, discussions
of logic programming semantics refer only to Herbrand (pre)interpretations
and Herbrand models.
2.1.6 Definition Given a program P with underlying language L P , the Herbrand universe U P of P is the set of all ground terms in L P . The Herbrand
3 This extends the notion of a J-ground instance of an atom to a J-ground instance of a
clause, see [Lloyd, 1987, Page 12].
4 Nevertheless, we prefer to formulate the basic definitions in complete generality. For one
thing this is at no extra cost, and for another we require quite general preinterpretations in
our treatment of acceptable programs in Chapter 5.
Mathematical Aspects of Logic Programming Semantics
a binary function whose intended meaning is the list constructor whose first
argument is the head of the list and whose second argument is its tail. Thus,
the program Length is intended to be a recursive definition of the “length of
lists” using the successor notation for natural numbers as in Program 2.1.3.
Length is an example of a definite program.
Thus far, we have specified the syntax of logic programs. We now turn our
attention to dealing with their semantics, and this is based on Definitions 1.2.7
and 1.2.8 of Chapter 1 with some notation peculiar to logic programming.
2.1.5 Definition Let P be a program with underlying language L P , and
let D be a non-empty set. A preinterpretation J for P with domain D is a
preinterpretation J for L P with domain D.
Let J be a preinterpretation for the program P , with domain D, and
let θ be a J-variable assignment. For a typical clause C in P of the form
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B k , we let (Cθ)
J denote
(Aθ)
J ← (A 1 θ)
J , . . . , (A n θ)
J , ¬(B 1 θ)
J , . . . , ¬(B k θ)
J .
We call (Cθ)
J a J-ground instance
3 of C. By ground J (P ), we denote the set
of all J-ground instances of clauses in P . We denote by B P,J the set B L P ,J of
all J-ground instances of atoms in L P , that is, the collection of all elements
of the form p(d 1 , . . . , d n ), where p is an n-ary predicate symbol in L P and
d 1 , . . . , d n ∈ D. Usually, we will be working over a fixed, but arbitrary, preinterpretation J. In order to ease notation, we will often omit mention of J if it
causes no confusion, and instead of writing B P,J , ground J (P ), J-ground instance, etc., we will simply write B P , ground(P ), ground instance, etc. We will
frequently abuse notation even further by referring to elements of ground J (P )
as (ground ) clauses and by applying to ground clauses terminology, such as
“definite”, already defined for program clauses.
Of particular interest is the so-called Herbrand preinterpretation of a program. Its importance rests on the fact that, for many purposes, restricting
to Herbrand preinterpretations causes no loss of generality.
4 For example, in
classical first-order logic, a set of clauses has a model if and only if it has a Herbrand model. Indeed, in many cases in the literature on the subject, discussions
of logic programming semantics refer only to Herbrand (pre)interpretations
and Herbrand models.
2.1.6 Definition Given a program P with underlying language L P , the Herbrand universe U P of P is the set of all ground terms in L P . The Herbrand
3 This extends the notion of a J-ground instance of an atom to a J-ground instance of a
clause, see [Lloyd, 1987, Page 12].
4 Nevertheless, we prefer to formulate the basic definitions in complete generality. For one
thing this is at no extra cost, and for another we require quite general preinterpretations in
our treatment of acceptable programs in Chapter 5.