200
Mathematical Aspects of Logic Programming Semantics
and not just for d l , but this suffices for what we want to say here. Now, given
a level n, we form the subset P n of ground(P ) containing all those clauses
whose heads have level ≤ n. Then, for all A ∈ B P with l(A) ≤ n and for all
I ∈ I P , we have A ∈ T Pn (I) if and only if A ∈ T P (I), or equivalently, by
definition of d l , we have d l (T Pn (I), T P (I)) ≤ 2
−(n+1) for all I ∈ I P . Hence,
λ(T Pn , T P ) ≤ 2
−(n+1) . Now suppose that ε > 0 is given. Choose n ∈ N so
o
large that
b
−i < ε, and form P n . Then for all I ∈ I P , T Pn (I) and T P (I)
i>n
agree on all atoms A with l(A) ≤ n. Therefore, the expansions ι(T Pn (I)) and
ι(T P (I)) agree in their first n terms. Hence, for all I ∈ I P we have, from
Figure 7.5, that
|f Pn (ι(I)) − f P (ι(I))| = |ι(T Pn (I)) − ι(T P (I))| < ε.
In other words, given any ε > 0, we obtain the approximation |f Pn − f P | < ε
provided n is sufficiently large. In addition, approximation can be thought of in
terms of d l and λ at the level of interpretations and of T P itself independently
of the embedding ι chosen. We refer to this process of working with P n as
approximating T P up to level n, and we will see shortly that it can be used to
show that approximating networks exist for T P for certain programs P . Indeed,
in this terminology the estimates just made show that T Pn approximates T P
up to ε provided T Pn approximates T P up to level n for large enough n.
Unfortunately, the subsets P n of ground(P ) which, as we have just seen,
are appropriate for approximation can be infinitely large. For example, there
are infinitely many ground instances of the clause a ← p(X). Therefore, we
consider only so-called covered logic programs in the rest of this section, excluding Section 7.5.6, and we define the notion of a covered program next.
7.5.4 Definition A logic program is called covered if it has no local variables,
that is, if every variable symbol occurring in the body of a clause also occurs
in the head of the same clause.
7.5.5 Proposition Let P be a covered logic program, let l be a bijective level
mapping from B P to ω, and let n ∈ ω be fixed. Then the program P n defined
above by
P n := {C | C ∈ ground(P ) with l(H) ≤ n, where H is the head of C}
is finite.
Proof: The finiteness of P n follows directly from the fact that, for a given
level m, there is at most one ground clause C whose head has level m.
•
Using this finiteness property, we can directly obtain the following theorem
showing the existence of approximating networks for a given covered logic
program.
Mathematical Aspects of Logic Programming Semantics
and not just for d l , but this suffices for what we want to say here. Now, given
a level n, we form the subset P n of ground(P ) containing all those clauses
whose heads have level ≤ n. Then, for all A ∈ B P with l(A) ≤ n and for all
I ∈ I P , we have A ∈ T Pn (I) if and only if A ∈ T P (I), or equivalently, by
definition of d l , we have d l (T Pn (I), T P (I)) ≤ 2
−(n+1) for all I ∈ I P . Hence,
λ(T Pn , T P ) ≤ 2
−(n+1) . Now suppose that ε > 0 is given. Choose n ∈ N so
o
large that
b
−i < ε, and form P n . Then for all I ∈ I P , T Pn (I) and T P (I)
i>n
agree on all atoms A with l(A) ≤ n. Therefore, the expansions ι(T Pn (I)) and
ι(T P (I)) agree in their first n terms. Hence, for all I ∈ I P we have, from
Figure 7.5, that
|f Pn (ι(I)) − f P (ι(I))| = |ι(T Pn (I)) − ι(T P (I))| < ε.
In other words, given any ε > 0, we obtain the approximation |f Pn − f P | < ε
provided n is sufficiently large. In addition, approximation can be thought of in
terms of d l and λ at the level of interpretations and of T P itself independently
of the embedding ι chosen. We refer to this process of working with P n as
approximating T P up to level n, and we will see shortly that it can be used to
show that approximating networks exist for T P for certain programs P . Indeed,
in this terminology the estimates just made show that T Pn approximates T P
up to ε provided T Pn approximates T P up to level n for large enough n.
Unfortunately, the subsets P n of ground(P ) which, as we have just seen,
are appropriate for approximation can be infinitely large. For example, there
are infinitely many ground instances of the clause a ← p(X). Therefore, we
consider only so-called covered logic programs in the rest of this section, excluding Section 7.5.6, and we define the notion of a covered program next.
7.5.4 Definition A logic program is called covered if it has no local variables,
that is, if every variable symbol occurring in the body of a clause also occurs
in the head of the same clause.
7.5.5 Proposition Let P be a covered logic program, let l be a bijective level
mapping from B P to ω, and let n ∈ ω be fixed. Then the program P n defined
above by
P n := {C | C ∈ ground(P ) with l(H) ≤ n, where H is the head of C}
is finite.
Proof: The finiteness of P n follows directly from the fact that, for a given
level m, there is at most one ground clause C whose head has level m.
•
Using this finiteness property, we can directly obtain the following theorem
showing the existence of approximating networks for a given covered logic
program.