- Source: Kleene fixed-point theorem
In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following:
Kleene Fixed-Point Theorem. Suppose
(
L
,
⊑
)
{\displaystyle (L,\sqsubseteq )}
is a directed-complete partial order (dcpo) with a least element, and let
f
:
L
→
L
{\displaystyle f:L\to L}
be a Scott-continuous (and therefore monotone) function. Then
f
{\displaystyle f}
has a least fixed point, which is the supremum of the ascending Kleene chain of
f
.
{\displaystyle f.}
The ascending Kleene chain of f is the chain
⊥
⊑
f
(
⊥
)
⊑
f
(
f
(
⊥
)
)
⊑
⋯
⊑
f
n
(
⊥
)
⊑
⋯
{\displaystyle \bot \sqsubseteq f(\bot )\sqsubseteq f(f(\bot ))\sqsubseteq \cdots \sqsubseteq f^{n}(\bot )\sqsubseteq \cdots }
obtained by iterating f on the least element ⊥ of L. Expressed in a formula, the theorem states that
lfp
(
f
)
=
sup
(
{
f
n
(
⊥
)
∣
n
∈
N
}
)
{\displaystyle {\textrm {lfp}}(f)=\sup \left(\left\{f^{n}(\bot )\mid n\in \mathbb {N} \right\}\right)}
where
lfp
{\displaystyle {\textrm {lfp}}}
denotes the least fixed point.
Although Tarski's fixed point theorem
does not consider how fixed points can be computed by iterating f from some seed (also, it pertains to monotone functions on complete lattices), this result is often attributed to Alfred Tarski who proves it for additive functions. Moreover, Kleene Fixed-Point Theorem can be extended to monotone functions using transfinite iterations.
Proof
Source:
We first have to show that the ascending Kleene chain of
f
{\displaystyle f}
exists in
L
{\displaystyle L}
. To show that, we prove the following:
Lemma. If
L
{\displaystyle L}
is a dcpo with a least element, and
f
:
L
→
L
{\displaystyle f:L\to L}
is Scott-continuous, then
f
n
(
⊥
)
⊑
f
n
+
1
(
⊥
)
,
n
∈
N
0
{\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot ),n\in \mathbb {N} _{0}}
Proof. We use induction:
Assume n = 0. Then
f
0
(
⊥
)
=
⊥
⊑
f
1
(
⊥
)
,
{\displaystyle f^{0}(\bot )=\bot \sqsubseteq f^{1}(\bot ),}
since
⊥
{\displaystyle \bot }
is the least element.
Assume n > 0. Then we have to show that
f
n
(
⊥
)
⊑
f
n
+
1
(
⊥
)
{\displaystyle f^{n}(\bot )\sqsubseteq f^{n+1}(\bot )}
. By rearranging we get
f
(
f
n
−
1
(
⊥
)
)
⊑
f
(
f
n
(
⊥
)
)
{\displaystyle f(f^{n-1}(\bot ))\sqsubseteq f(f^{n}(\bot ))}
. By inductive assumption, we know that
f
n
−
1
(
⊥
)
⊑
f
n
(
⊥
)
{\displaystyle f^{n-1}(\bot )\sqsubseteq f^{n}(\bot )}
holds, and because f is monotone (property of Scott-continuous functions), the result holds as well.
As a corollary of the Lemma we have the following directed ω-chain:
M
=
{
⊥
,
f
(
⊥
)
,
f
(
f
(
⊥
)
)
,
…
}
.
{\displaystyle \mathbb {M} =\{\bot ,f(\bot ),f(f(\bot )),\ldots \}.}
From the definition of a dcpo it follows that
M
{\displaystyle \mathbb {M} }
has a supremum, call it
m
.
{\displaystyle m.}
What remains now is to show that
m
{\displaystyle m}
is the least fixed-point.
First, we show that
m
{\displaystyle m}
is a fixed point, i.e. that
f
(
m
)
=
m
{\displaystyle f(m)=m}
. Because
f
{\displaystyle f}
is Scott-continuous,
f
(
sup
(
M
)
)
=
sup
(
f
(
M
)
)
{\displaystyle f(\sup(\mathbb {M} ))=\sup(f(\mathbb {M} ))}
, that is
f
(
m
)
=
sup
(
f
(
M
)
)
{\displaystyle f(m)=\sup(f(\mathbb {M} ))}
. Also, since
M
=
f
(
M
)
∪
{
⊥
}
{\displaystyle \mathbb {M} =f(\mathbb {M} )\cup \{\bot \}}
and because
⊥
{\displaystyle \bot }
has no influence in determining the supremum we have:
sup
(
f
(
M
)
)
=
sup
(
M
)
{\displaystyle \sup(f(\mathbb {M} ))=\sup(\mathbb {M} )}
. It follows that
f
(
m
)
=
m
{\displaystyle f(m)=m}
, making
m
{\displaystyle m}
a fixed-point of
f
{\displaystyle f}
.
The proof that
m
{\displaystyle m}
is in fact the least fixed point can be done by showing that any element in
M
{\displaystyle \mathbb {M} }
is smaller than any fixed-point of
f
{\displaystyle f}
(because by property of supremum, if all elements of a set
D
⊆
L
{\displaystyle D\subseteq L}
are smaller than an element of
L
{\displaystyle L}
then also
sup
(
D
)
{\displaystyle \sup(D)}
is smaller than that same element of
L
{\displaystyle L}
). This is done by induction: Assume
k
{\displaystyle k}
is some fixed-point of
f
{\displaystyle f}
. We now prove by induction over
i
{\displaystyle i}
that
∀
i
∈
N
:
f
i
(
⊥
)
⊑
k
{\displaystyle \forall i\in \mathbb {N} :f^{i}(\bot )\sqsubseteq k}
. The base of the induction
(
i
=
0
)
{\displaystyle (i=0)}
obviously holds:
f
0
(
⊥
)
=
⊥
⊑
k
,
{\displaystyle f^{0}(\bot )=\bot \sqsubseteq k,}
since
⊥
{\displaystyle \bot }
is the least element of
L
{\displaystyle L}
. As the induction hypothesis, we may assume that
f
i
(
⊥
)
⊑
k
{\displaystyle f^{i}(\bot )\sqsubseteq k}
. We now do the induction step: From the induction hypothesis and the monotonicity of
f
{\displaystyle f}
(again, implied by the Scott-continuity of
f
{\displaystyle f}
), we may conclude the following:
f
i
(
⊥
)
⊑
k
⟹
f
i
+
1
(
⊥
)
⊑
f
(
k
)
.
{\displaystyle f^{i}(\bot )\sqsubseteq k~\implies ~f^{i+1}(\bot )\sqsubseteq f(k).}
Now, by the assumption that
k
{\displaystyle k}
is a fixed-point of
f
,
{\displaystyle f,}
we know that
f
(
k
)
=
k
,
{\displaystyle f(k)=k,}
and from that we get
f
i
+
1
(
⊥
)
⊑
k
.
{\displaystyle f^{i+1}(\bot )\sqsubseteq k.}
See also
Other fixed-point theorems
References
Kata Kunci Pencarian:
- Kleene fixed-point theorem
- Fixed-point theorem
- Kleene's recursion theorem
- Stephen Cole Kleene
- Least fixed point
- Knaster–Tarski theorem
- Bourbaki–Witt theorem
- Tarski's theorem
- List of theorems
- Complete partial order
