144
Mathematical Aspects of Logic Programming Semantics
with l(A) ≤ α. Then there is a clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in
ground(P ), where k 1 , l 1 ≥ 0, such that for all k, j we have A k ∈ I 1 and
B j ∈ I 1 . Since P is locally hierarchical and I 1 , I 2 agree on all atoms of level
less than α, it follows that for all k, j we have A k ∈ I 2 and B j ∈ I 2 . Therefore,
A ∈ T P (I 2 ). By the same argument, if A ∈ T P (I 2 ) with l(A) ≤ α, then
A ∈ T P (I 1 ). Hence, we have that T P (I 1 ) and T P (I 2 ) agree on all atoms of
level less than or equal to α, and it follows that
d l (T P (I 1 ), T P (I 2 )) ≤ 2
−(α+1) < 2
−α = d l (I 1 , I 2 ),
as required.
Thus, T P is strictly contracting, and Theorem 4.3.6 yields that T P has a
unique fixed point and therefore that P has a unique supported model.
The proof just given is easily adapted to establish (b). The operator T P
turns out to be contractive with contractivity factor
1
2 , and then Theorem
4.2.3 is applied instead of Theorem 4.3.6.
•
5.1.7 Example Consider the program Tweety1 from Examples 2.1.2 and
2.2.7. Tweety1 is acyclic with level mapping l(penguin(X)) = 0, l(bird(X)) =
1 and l(flies(X)) = 2 for X ∈ {bob, tweety}. For I 0 = {bird(tweety)}, we
obtain
I 1 = T Tweety1 (I 0 ) = {penguin(tweety), bird(bob), flies(tweety)},
I 2 = T Tweety1 (I 1 ) = {penguin(tweety), bird(bob), bird(tweety),
flies(bob)}, and
I 3 = T Tweety1 (I 2 ) = I 2 .
Another example is given by the program Even (Program 2.1.3), as discussed at the beginning of Section 5.1.1.
5.1.2 Acceptable Programs
Historically, acyclic programs were introduced in attempts to capture
procedural properties, such as termination, under SLDNF-resolution, see
[Bezem, 1989, Apt and Bezem, 1990, Cavedon, 1991]. The basic idea behind
acyclic programs was extended to take into account the fact that logic programming systems, such as Prolog, evaluate clause bodies from left to right,
and this led to the acceptable programs
3 studied in this section. We will focus
on declarative aspects of acceptable programs here, generalizing the approach
of Section 5.1.1.
3 Acceptable programs were introduced by Apt and Pedreschi in AP94. For further reading concerning termination in resolution-based logic programming, see [Marchiori, 1996,
Apt, 1997, Pedreschi et al., 2002].
Mathematical Aspects of Logic Programming Semantics
with l(A) ≤ α. Then there is a clause A ← A 1 , . . . , A k1 , ¬B 1 , . . . , ¬B l1 in
ground(P ), where k 1 , l 1 ≥ 0, such that for all k, j we have A k ∈ I 1 and
B j ∈ I 1 . Since P is locally hierarchical and I 1 , I 2 agree on all atoms of level
less than α, it follows that for all k, j we have A k ∈ I 2 and B j ∈ I 2 . Therefore,
A ∈ T P (I 2 ). By the same argument, if A ∈ T P (I 2 ) with l(A) ≤ α, then
A ∈ T P (I 1 ). Hence, we have that T P (I 1 ) and T P (I 2 ) agree on all atoms of
level less than or equal to α, and it follows that
d l (T P (I 1 ), T P (I 2 )) ≤ 2
−(α+1) < 2
−α = d l (I 1 , I 2 ),
as required.
Thus, T P is strictly contracting, and Theorem 4.3.6 yields that T P has a
unique fixed point and therefore that P has a unique supported model.
The proof just given is easily adapted to establish (b). The operator T P
turns out to be contractive with contractivity factor
1
2 , and then Theorem
4.2.3 is applied instead of Theorem 4.3.6.
•
5.1.7 Example Consider the program Tweety1 from Examples 2.1.2 and
2.2.7. Tweety1 is acyclic with level mapping l(penguin(X)) = 0, l(bird(X)) =
1 and l(flies(X)) = 2 for X ∈ {bob, tweety}. For I 0 = {bird(tweety)}, we
obtain
I 1 = T Tweety1 (I 0 ) = {penguin(tweety), bird(bob), flies(tweety)},
I 2 = T Tweety1 (I 1 ) = {penguin(tweety), bird(bob), bird(tweety),
flies(bob)}, and
I 3 = T Tweety1 (I 2 ) = I 2 .
Another example is given by the program Even (Program 2.1.3), as discussed at the beginning of Section 5.1.1.
5.1.2 Acceptable Programs
Historically, acyclic programs were introduced in attempts to capture
procedural properties, such as termination, under SLDNF-resolution, see
[Bezem, 1989, Apt and Bezem, 1990, Cavedon, 1991]. The basic idea behind
acyclic programs was extended to take into account the fact that logic programming systems, such as Prolog, evaluate clause bodies from left to right,
and this led to the acceptable programs
3 studied in this section. We will focus
on declarative aspects of acceptable programs here, generalizing the approach
of Section 5.1.1.
3 Acceptable programs were introduced by Apt and Pedreschi in AP94. For further reading concerning termination in resolution-based logic programming, see [Marchiori, 1996,
Apt, 1997, Pedreschi et al., 2002].