44
Mathematical Aspects of Logic Programming Semantics
recursion in certain situations, and the most convenient way of expressing
these conditions is again by the use of level mappings. For example, the alternative characterization of the Fitting model in Definition 2.4.8 and Theorem
2.4.9 can be viewed from this standpoint, and we will return to this point later
on in this section and in Section 2.6.
The approach which we present in this section is based on the following
idea: the introduction of negation, and in particular the possibility of allowing recursive dependencies between negated atoms, causes ambiguity from a
declarative point of view. However, if recursion is only allowed through positive atoms, a standard model, namely, the least model, can be obtained. So it
seems natural to disallow recursion through negative dependencies, while at
the same time allowing recursion through positive ones. This idea is captured
in the following definition.
2.5.1 Definition A program P is called locally stratified
11 if there exists a
level mapping l : B P → α such that for each clause
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m
in ground(P ) the following hold.
(S1) l(A) ≥ l(A i ) for i = 1, . . . , n.
(S2) l(A) > l(B j ) for j = 1, . . . , m.
Furthermore, P is called stratified if it is locally stratified, and for all atoms
A, B ∈ B P with the same predicate symbol, we have l(A) = l(B).
Note that for stratified programs the image of the level mapping involved
is finite, in contrast to locally stratified programs. Stratified programs are
particularly interesting from the procedural point of view. Nevertheless, we
will concentrate here on the more general locally stratified programs.
Along with the introduction of locally stratified programs, a semantics was
developed called the perfect model semantics. We will discuss this semantics
only in passing in this chapter. Indeed, we will focus here on the more general
weakly perfect semantics, which is introduced later in this section and is also
defined for locally stratified programs. However, we will consider the perfect
model semantics in some detail in Section 6.3.
2.5.2 Definition Let P be a locally stratified program, and let l denote the
associated level mapping. Given two distinct models M and N for P , we say
that N is preferable to M if, for every ground atom A in N \ M , there is a
ground atom B in M \ N such that l(A) > l(B). A model M for P is called
perfect if there are no models for P preferable to M .
11 The notion of local stratification and the perfect model semantics were introduced in
the paper [Przymusinski, 1988]. Stratified programs and certain procedural apects of them
were studied in [Apt et al., 1988].
Mathematical Aspects of Logic Programming Semantics
recursion in certain situations, and the most convenient way of expressing
these conditions is again by the use of level mappings. For example, the alternative characterization of the Fitting model in Definition 2.4.8 and Theorem
2.4.9 can be viewed from this standpoint, and we will return to this point later
on in this section and in Section 2.6.
The approach which we present in this section is based on the following
idea: the introduction of negation, and in particular the possibility of allowing recursive dependencies between negated atoms, causes ambiguity from a
declarative point of view. However, if recursion is only allowed through positive atoms, a standard model, namely, the least model, can be obtained. So it
seems natural to disallow recursion through negative dependencies, while at
the same time allowing recursion through positive ones. This idea is captured
in the following definition.
2.5.1 Definition A program P is called locally stratified
11 if there exists a
level mapping l : B P → α such that for each clause
A ← A 1 , . . . , A n , ¬B 1 , . . . , ¬B m
in ground(P ) the following hold.
(S1) l(A) ≥ l(A i ) for i = 1, . . . , n.
(S2) l(A) > l(B j ) for j = 1, . . . , m.
Furthermore, P is called stratified if it is locally stratified, and for all atoms
A, B ∈ B P with the same predicate symbol, we have l(A) = l(B).
Note that for stratified programs the image of the level mapping involved
is finite, in contrast to locally stratified programs. Stratified programs are
particularly interesting from the procedural point of view. Nevertheless, we
will concentrate here on the more general locally stratified programs.
Along with the introduction of locally stratified programs, a semantics was
developed called the perfect model semantics. We will discuss this semantics
only in passing in this chapter. Indeed, we will focus here on the more general
weakly perfect semantics, which is introduced later in this section and is also
defined for locally stratified programs. However, we will consider the perfect
model semantics in some detail in Section 6.3.
2.5.2 Definition Let P be a locally stratified program, and let l denote the
associated level mapping. Given two distinct models M and N for P , we say
that N is preferable to M if, for every ground atom A in N \ M , there is a
ground atom B in M \ N such that l(A) > l(B). A model M for P is called
perfect if there are no models for P preferable to M .
11 The notion of local stratification and the perfect model semantics were introduced in
the paper [Przymusinski, 1988]. Stratified programs and certain procedural apects of them
were studied in [Apt et al., 1988].