Supported Model Semantics
141
We notice that the sequence of iterates is alternating in a certain sense. The
iterates with ev
model M =
successively delete
atoms are generated
en num
A bers
b successiv ely generate the atoms in the supported
even s
2n (0) | n ∈ N , while the iterates with odd numbers
those atoms which are not in M . The order in which the
or deleted is such that atoms with more occurrences of
the function symbol s are generated or deleted later. This corresponds to the
structure of the Even program, whose rules reflect this in the sense that the
atom in the head of a ground instance of the second program clause always
contains one more function symbol than the corresponding body atom.
The following definition abstracts from this and draws on the observation
made in the previous paragraph that iterates of the immediate consequence
operator can in some sense be controlled if there is a strong dependency between heads of clauses and their corresponding body atoms. This is a theme
which will dominate the discussion of this chapter, and the reader may have
already noticed that it is related to the characterizations of semantics using
level mappings given in Chapter 2. The precise relationship between these two
themes will be made more explicit in Section 5.2.
5.1.1 Definition A normal logic program P is called locally hierarchical
1 if
there exists a level mapping l : B P → α, for some ordinal α, such that for
each clause A ← L 1 , . . . , L n in ground(P ) and for all i = 1, . . . , n we have
l(A) > l(L i ). If α can be chosen here to be ω, then P is called acyclic.
2
A The
A Even
bb program is acyclic, as can be seen by defining l : B P → α by
l even s
k (0) = k for all k ∈ N.
5.1.2 Program (ExistsEven) Consider the following program, which extends Even. We call it ExistsEven because intuitively, and also when run
under Prolog, it is a generate-and-test program which tests whether or not
there exists an even number.
nat(0) ←
nat(s(X)) ← nat(X)
even(0) ←
even(s(X)) ← ¬even(X)
existsEven ← nat(X), even(X)
1 Locally hierarchical programs were studied in [Cavedon, 1989]. It was shown in
[Seda and Hitzler, 1999a] that it is possible to compute all partial recursive functions with
locally hierarchical programs under SLDNF-resolution if the use of the meta-logical cut is
allowed.
2 Acyclic programs were studied in [Cavedon, 1989, Cavedon, 1991] under the name of
ω-locally hierarchical programs. The notion of acyclicity was introduced in [Bezem, 1989],
and further studies of it concerning termination properties were undertaken in [Bezem, 1989,
Apt and Bezem, 1990].
141
We notice that the sequence of iterates is alternating in a certain sense. The
iterates with ev
model M =
successively delete
atoms are generated
en num
A bers
b successiv ely generate the atoms in the supported
even s
2n (0) | n ∈ N , while the iterates with odd numbers
those atoms which are not in M . The order in which the
or deleted is such that atoms with more occurrences of
the function symbol s are generated or deleted later. This corresponds to the
structure of the Even program, whose rules reflect this in the sense that the
atom in the head of a ground instance of the second program clause always
contains one more function symbol than the corresponding body atom.
The following definition abstracts from this and draws on the observation
made in the previous paragraph that iterates of the immediate consequence
operator can in some sense be controlled if there is a strong dependency between heads of clauses and their corresponding body atoms. This is a theme
which will dominate the discussion of this chapter, and the reader may have
already noticed that it is related to the characterizations of semantics using
level mappings given in Chapter 2. The precise relationship between these two
themes will be made more explicit in Section 5.2.
5.1.1 Definition A normal logic program P is called locally hierarchical
1 if
there exists a level mapping l : B P → α, for some ordinal α, such that for
each clause A ← L 1 , . . . , L n in ground(P ) and for all i = 1, . . . , n we have
l(A) > l(L i ). If α can be chosen here to be ω, then P is called acyclic.
2
A The
A Even
bb program is acyclic, as can be seen by defining l : B P → α by
l even s
k (0) = k for all k ∈ N.
5.1.2 Program (ExistsEven) Consider the following program, which extends Even. We call it ExistsEven because intuitively, and also when run
under Prolog, it is a generate-and-test program which tests whether or not
there exists an even number.
nat(0) ←
nat(s(X)) ← nat(X)
even(0) ←
even(s(X)) ← ¬even(X)
existsEven ← nat(X), even(X)
1 Locally hierarchical programs were studied in [Cavedon, 1989]. It was shown in
[Seda and Hitzler, 1999a] that it is possible to compute all partial recursive functions with
locally hierarchical programs under SLDNF-resolution if the use of the meta-logical cut is
allowed.
2 Acyclic programs were studied in [Cavedon, 1989, Cavedon, 1991] under the name of
ω-locally hierarchical programs. The notion of acyclicity was introduced in [Bezem, 1989],
and further studies of it concerning termination properties were undertaken in [Bezem, 1989,
Apt and Bezem, 1990].