76
Mathematical Aspects of Logic Programming Semantics
We close this section with an example which, despite its simplicity, illustrates the main points discussed previously.
3.2.11 Example Consider again the program P of Example 3.2.3.
p(a) ←
p(s(X)) ← p(X)
Let M = ∅, thought of as a two-valued interpretation, and let I n denote
the n-th iterate of T P on M . Then I n = {p(a), p(s(a)), . . . , p(s
n−1 (a))} for
any n ≥ 1. By Part (2) of Example 3.2.7, the sequence (I n ) converges in the
Scott topology to the set I = {p(a), p(s(a)), . . . , p(s
n (a)), . . .} of all natural
numbers. Moreover, I is clearly the greatest limit of the sequence (I n ) and,
hence, by Theorem 3.2.10, is a model for P . Indeed, by the comments immediately prior to this example, I is the least model for P by the results of
[Seda, 1995].
3.3 The Cantor Topology on Spaces of Valuations
As just noted in the previous section, one of the sources of motivation for
studying topology in relation to logic programming is the role of convergence
of sequences of iterates of the immediate consequence operator in relation
to semantics and also, in fact, in relation to termination. We take this discussion further now, but this time in the context of normal programs and the
construction of certain standard models for them, and in more detail in Chapter 5. We also refer the reader to Chapter 5 for details of how convergence
enters into questions concerned with the so-called acceptable programs and
problems concerned with termination, see Corollary 5.2.5, Proposition 5.2.7,
Theorem 5.2.8 and Theorem 5.4.14, for example.
We begin with a result concerning product topologies.
Let X and Y be arbitrary sets, and let [X → Y ] denote the set of all total
functions mapping X into Y . When Y is ordered, perhaps as a set of truth
values T , then so is [X → Y ], and, as we have just seen, important topologies
can be defined on [X → Y ] by quite natural convergence conditions which
make use of the order. However, important topologies can also be defined on
[X → Y ] using natural convergence conditions which do not depend on any
order, as we show next.
12
3.3.1 Theorem Let (s i ) be a net in [X → Y ], and let s ∈ [X → Y ]. Then
the condition
12 Again, see [Seda, 2002].
Précédent

- 107/305

Suivant