142
Mathematical Aspects of Logic Programming Semantics
Certainly, ExistsEven is somewhat pointless as a program. However, it exhibits the basic idea underlying the generate-and-test programming scheme.
If Prolog is called with the query
?- existsEven.
then the interpreter successively generates all instantiations of nat(X) and
tests for each instance of X whether or not it falls under the predicate even.
Obviously, the generator nat and the test even could be replaced by something
much more sophisticated.
In ExistsEven, the subprogram consisting of the first four clauses is acyclic
A
A
bb
A
A
bb
with respect to the level mapping l with l even s
k (0) = l nat s
k (0) = k
for all k ∈ N, and we notice that any level mapping with respect to which
this subprogram is acyclic must have an infinite codomain. Consequently,
ExistsEven is not acyclic, but it is locally hierarchical, as can be seen by
extending the level mapping by setting l(existsEven) = ω.
We want to apply generalized metric fixed-point theorems from Chapter 4
to acyclic and locally hierarchical programs, that is, we would like to construct
a (generalized) metric on the set of all interpretations of a program such that
the immediate consequence operator of the program satisfies a corresponding
contractivity property. We follow the construction of Section 4.8.2 with a
minor modification to suit our present purposes.
5.1.3 Definition Let P be a normal logic program, and let l : B P → γ be a
level mapping for P . We consider symbols 2
−α for ordinals α, and, essentially
as in Section 4.8.2, define Γ l = {2
−α | α ≤ γ}. The set Γ l is again ordered by
2
−α < 2
−β if and only if β < α, and we denote 2
−γ by 0.
In Sections 4.8.2 and 4.8.3, we used this construction for gums with ordinal
distances, and with the notation established there we have Γ l = Γ γ+1 , where
l : B P → γ.
Finally, define a mapping d l : I P ×I P → Γ l by setting d l (I, J) = 0 if I = J,
and, when I = J, by setting d l (I, J) = 2
−α , where I and J differ on some
ground atom of level α, but agree on all ground atoms β satisfying β < α.
In case γ = ω, we can identify each 2
−n ∈ Γ l with the corresponding
1
negative power of two, that is, 2
−n =
∈ R and 2
−ω = 0, and then d l takes
2 n
values in the set of real numbers.
5.1.4 Proposition Suppose that P is a normal logic program, and that l is
a level mapping. Then the following statements hold.
(a) If P is locally hierarchical with respect to l, then d l is a spherically complete generalized ultrametric.
(b) If P is acyclic with respect to l, then d l is a complete ultrametric.
Mathematical Aspects of Logic Programming Semantics
Certainly, ExistsEven is somewhat pointless as a program. However, it exhibits the basic idea underlying the generate-and-test programming scheme.
If Prolog is called with the query
?- existsEven.
then the interpreter successively generates all instantiations of nat(X) and
tests for each instance of X whether or not it falls under the predicate even.
Obviously, the generator nat and the test even could be replaced by something
much more sophisticated.
In ExistsEven, the subprogram consisting of the first four clauses is acyclic
A
A
bb
A
A
bb
with respect to the level mapping l with l even s
k (0) = l nat s
k (0) = k
for all k ∈ N, and we notice that any level mapping with respect to which
this subprogram is acyclic must have an infinite codomain. Consequently,
ExistsEven is not acyclic, but it is locally hierarchical, as can be seen by
extending the level mapping by setting l(existsEven) = ω.
We want to apply generalized metric fixed-point theorems from Chapter 4
to acyclic and locally hierarchical programs, that is, we would like to construct
a (generalized) metric on the set of all interpretations of a program such that
the immediate consequence operator of the program satisfies a corresponding
contractivity property. We follow the construction of Section 4.8.2 with a
minor modification to suit our present purposes.
5.1.3 Definition Let P be a normal logic program, and let l : B P → γ be a
level mapping for P . We consider symbols 2
−α for ordinals α, and, essentially
as in Section 4.8.2, define Γ l = {2
−α | α ≤ γ}. The set Γ l is again ordered by
2
−α < 2
−β if and only if β < α, and we denote 2
−γ by 0.
In Sections 4.8.2 and 4.8.3, we used this construction for gums with ordinal
distances, and with the notation established there we have Γ l = Γ γ+1 , where
l : B P → γ.
Finally, define a mapping d l : I P ×I P → Γ l by setting d l (I, J) = 0 if I = J,
and, when I = J, by setting d l (I, J) = 2
−α , where I and J differ on some
ground atom of level α, but agree on all ground atoms β satisfying β < α.
In case γ = ω, we can identify each 2
−n ∈ Γ l with the corresponding
1
negative power of two, that is, 2
−n =
∈ R and 2
−ω = 0, and then d l takes
2 n
values in the set of real numbers.
5.1.4 Proposition Suppose that P is a normal logic program, and that l is
a level mapping. Then the following statements hold.
(a) If P is locally hierarchical with respect to l, then d l is a spherically complete generalized ultrametric.
(b) If P is acyclic with respect to l, then d l is a complete ultrametric.