85
Topology and Logic Programming
and v i → v in Q. Let x ∈ X be arbitrary. Then there exist i 1 and i 2 such
that u i (x) = u(x) whenever i ≥ i 1 and v i (x) = v(x) whenever i ≥ i 2 . By
directedness, there is i 3 such that, for i ≥ i 3 , we have both u i (x) = u(x) and
v i (x) = v(x). Therefore, whenever i ≥ i 3 , we have u i (x) ∨ v i (x) = u(x) ∨ v(x)
and u i (x) ∧ v i (x) = u(x) ∧ v(x). Therefore, u i ∨ v i → u ∨ v and u i ∧ v i → u ∧ v,
as required.
•
There are several interesting topics relating to topology and logic programming semantics which are examined in the literature on the subject,
but are not pursued here. These include, among other things, the consistency of program completions and of the union of program completions, see
[Batarekh and Subrahmanian, 1989b]; compactness of spaces of models for a
program; and continuity in Q of T P for a normal program P at the point
T P ↓ ω and the coincidence of T P ↓ ω with the greatest fixed point of T P . For
further discussion of all these points and others, see [Seda, 1995].
In conclusion, we note that order is a very satisfactory foundation for the
semantics of procedural and imperative programming languages as exemplified through the denotational semantics approach to programming language
theory. On the other hand, order is not an entirely satisfactory foundation
for the semantics of logic programming languages in the presence of negation,
and yet negation is a natural part of most logics. However, our treatment here
and in later chapters shows that one can consider convergence instead as a
foundation for a unified approach by which one can recover conventional ordertheoretic semantics and at the same time display some important standard
models in logic programming languages as limits of a sequence of iterates.
In addition, convergence conditions involving nets arise very naturally in a
number of areas within theoretical computer science and are simple to state
and to comprehend. Moreover, nets usually give short and technically simple
proofs, as demonstrated in several places in this chapter.
Topology and Logic Programming
and v i → v in Q. Let x ∈ X be arbitrary. Then there exist i 1 and i 2 such
that u i (x) = u(x) whenever i ≥ i 1 and v i (x) = v(x) whenever i ≥ i 2 . By
directedness, there is i 3 such that, for i ≥ i 3 , we have both u i (x) = u(x) and
v i (x) = v(x). Therefore, whenever i ≥ i 3 , we have u i (x) ∨ v i (x) = u(x) ∨ v(x)
and u i (x) ∧ v i (x) = u(x) ∧ v(x). Therefore, u i ∨ v i → u ∨ v and u i ∧ v i → u ∧ v,
as required.
•
There are several interesting topics relating to topology and logic programming semantics which are examined in the literature on the subject,
but are not pursued here. These include, among other things, the consistency of program completions and of the union of program completions, see
[Batarekh and Subrahmanian, 1989b]; compactness of spaces of models for a
program; and continuity in Q of T P for a normal program P at the point
T P ↓ ω and the coincidence of T P ↓ ω with the greatest fixed point of T P . For
further discussion of all these points and others, see [Seda, 1995].
In conclusion, we note that order is a very satisfactory foundation for the
semantics of procedural and imperative programming languages as exemplified through the denotational semantics approach to programming language
theory. On the other hand, order is not an entirely satisfactory foundation
for the semantics of logic programming languages in the presence of negation,
and yet negation is a natural part of most logics. However, our treatment here
and in later chapters shows that one can consider convergence instead as a
foundation for a unified approach by which one can recover conventional ordertheoretic semantics and at the same time display some important standard
models in logic programming languages as limits of a sequence of iterates.
In addition, convergence conditions involving nets arise very naturally in a
number of areas within theoretical computer science and are simple to state
and to comprehend. Moreover, nets usually give short and technically simple
proofs, as demonstrated in several places in this chapter.