6
Mathematical Aspects of Logic Programming Semantics
satisfying the property: if y is a fixed point of f , then x [ y. Least pre-fixed
points and least post-fixed points are defined similarly.
The following two theorems are fundamental in handling the semantics of
logic programs.
7 Indeed, the first of them, which is frequently referred to as the
fixed-point theorem, is fundamental in procedural and functional programming
as well.
8
1.1.9 Theorem (Kleene) Let (D, [) denote an ω-complete partial order
and let f : D → D be ω-continuous. Then f has a least fixed point x = f ↑ ω
which is also its least pre-fixed point.
Proof: We sketch the proof of this well-known result.
The sequence (f ↑ n) n∈N is an ω-chain. It therefore has a supremum f ↑ ω =
x, say. By ω-continuity, we have x = f ↑ ω = {f ↑ (n + 1) | n ∈ N} = f ( {f ↑
n | n ∈ N}) = f (x), and so x is a fixed point of f . If y is a pre-fixed point of
f , then ⊥ [ y, and, by monotonicity of f , we obtain f ↑ 1 = f (⊥) [ f (y) [ y.
Inductively, it follows that f ↑ n [ y for all n ∈ N, and hence x = f ↑ ω [ y.
So x is the least pre-fixed point of f and hence also its least fixed point. •
By our earlier observation that a continuous function is ω-continuous, this
theorem applies, of course, to continuous functions on complete partial orders.
Moreover, if the function is not ω-continuous, but is monotonic, the existence
of a least fixed point can still be guaranteed, as we see next.
9
1.1.10 Theorem (Knaster-Tarski) Let (D, [) denote a complete partial
order, let f : D → D be monotonic, and let x ∈ D be such that x [ f (x).
Then f has a least fixed point a above x, meaning x [ a, which is also the
least pre-fixed point of f above x, and there exists a least ordinal α such that
a = f
α (x). In particular, f has a least fixed point a which is also its least
pre-fixed point.
Proof: Again, this theorem is well-known, and we just sketch its proof.
Let γ be an ordinal whose cardinality exceeds that of D, and form the
set {f
β (x) | β ≤ γ}. By cardinality considerations, there must be ordinals
α < β ≤ γ with f
α (x) = f
β (x), and we can assume without loss of generality
that α is least with this property. Since f
α (x) [ f (f
α (x)) [ f
β (x) = f
α (x),
7 Fixed points of certain operators associated with logic programs are of extreme importance in the semantics of logic programs, as we shall see in later chapters.
8 A result similar to Kleene’s theorem, in fact, equivalent to it, is the well-known theorem
due to Tarski and Kantorovitch in which ω-chains are replaced by countable chains, see
[Jachymski, 2001]. Indeed, the collection containing [Jachymski, 2001] is an excellent general
reference to fixed-point theory. As noted in [Lloyd, 1987], the reference [Lassez et al., 1982]
contains an interesting discussion of the history of fixed-point theorems on ordered sets.
9 In attributing Theorem 1.1.10 to Knaster and Tarski, we are noting Proposition 1.1.2
and then following Jachymski in [Jachymski, 2001]. Theorem 1.1.9 is usually attributed to
Kleene, since this theorem is an abstract formulation of the first recursion theorem, and we
are consistent with [Jachymski, 2001] in this respect.
Mathematical Aspects of Logic Programming Semantics
satisfying the property: if y is a fixed point of f , then x [ y. Least pre-fixed
points and least post-fixed points are defined similarly.
The following two theorems are fundamental in handling the semantics of
logic programs.
7 Indeed, the first of them, which is frequently referred to as the
fixed-point theorem, is fundamental in procedural and functional programming
as well.
8
1.1.9 Theorem (Kleene) Let (D, [) denote an ω-complete partial order
and let f : D → D be ω-continuous. Then f has a least fixed point x = f ↑ ω
which is also its least pre-fixed point.
Proof: We sketch the proof of this well-known result.
The sequence (f ↑ n) n∈N is an ω-chain. It therefore has a supremum f ↑ ω =
x, say. By ω-continuity, we have x = f ↑ ω = {f ↑ (n + 1) | n ∈ N} = f ( {f ↑
n | n ∈ N}) = f (x), and so x is a fixed point of f . If y is a pre-fixed point of
f , then ⊥ [ y, and, by monotonicity of f , we obtain f ↑ 1 = f (⊥) [ f (y) [ y.
Inductively, it follows that f ↑ n [ y for all n ∈ N, and hence x = f ↑ ω [ y.
So x is the least pre-fixed point of f and hence also its least fixed point. •
By our earlier observation that a continuous function is ω-continuous, this
theorem applies, of course, to continuous functions on complete partial orders.
Moreover, if the function is not ω-continuous, but is monotonic, the existence
of a least fixed point can still be guaranteed, as we see next.
9
1.1.10 Theorem (Knaster-Tarski) Let (D, [) denote a complete partial
order, let f : D → D be monotonic, and let x ∈ D be such that x [ f (x).
Then f has a least fixed point a above x, meaning x [ a, which is also the
least pre-fixed point of f above x, and there exists a least ordinal α such that
a = f
α (x). In particular, f has a least fixed point a which is also its least
pre-fixed point.
Proof: Again, this theorem is well-known, and we just sketch its proof.
Let γ be an ordinal whose cardinality exceeds that of D, and form the
set {f
β (x) | β ≤ γ}. By cardinality considerations, there must be ordinals
α < β ≤ γ with f
α (x) = f
β (x), and we can assume without loss of generality
that α is least with this property. Since f
α (x) [ f (f
α (x)) [ f
β (x) = f
α (x),
7 Fixed points of certain operators associated with logic programs are of extreme importance in the semantics of logic programs, as we shall see in later chapters.
8 A result similar to Kleene’s theorem, in fact, equivalent to it, is the well-known theorem
due to Tarski and Kantorovitch in which ω-chains are replaced by countable chains, see
[Jachymski, 2001]. Indeed, the collection containing [Jachymski, 2001] is an excellent general
reference to fixed-point theory. As noted in [Lloyd, 1987], the reference [Lassez et al., 1982]
contains an interesting discussion of the history of fixed-point theorems on ordered sets.
9 In attributing Theorem 1.1.10 to Knaster and Tarski, we are noting Proposition 1.1.2
and then following Jachymski in [Jachymski, 2001]. Theorem 1.1.9 is usually attributed to
Kleene, since this theorem is an abstract formulation of the first recursion theorem, and we
are consistent with [Jachymski, 2001] in this respect.