Information Technology Reference
In-Depth Information
we obtain that
f
(
{
x
,
y
}
=
{
f
(
x
),
f
(
y
)
f
(
y
).
With continuity and cocontinuity we can construct, in a more tractable way, the least
and greatest fixed point, respectively.
)
=
f
(
y
)
}
, which means
f
(
x
)
Proposition 2.1
Let X be a complete lattice.
1. Every continuous function f on X has a least fixed point, given by
n
≥
0
f
n
(
↥
)
,
is the bottom element of the lattice, and f
n
(
where
↥
↥
)
is the nth iteration of f
: f
0
(
and f
n
+
1
(
f
(
f
n
(
0
.
2. Every cocontinuous function f on X has a greatest fixed point,
on
↥
↥
):
=↥
↥
):
=
↥
))
for n
≥
given by
n
≥
0
f
n
(
)
, where
is the top element of the lattice.
Proof
We only prove the first clause, since the second one is dual.
We notice that
↥
f
(
↥
), and then monotonicity of
f
yields an increasing
sequence:
f
2
(
↥
f
(
↥
)
↥
)
...
By continuity of
f
we have,
f
(
n
≥
0
f
n
(
=
n
≥
0
f
n
+
1
(
↥
))
↥
) and the latter is
equal to
n
≥
0
f
n
(
).
And in fact that limit is the least fixed point: for if some other
x
were also a fixed
point, then we have
↥
x
and moreover
f
n
(
↥
↥
)
x
for all
n
by induction. So
x
is
an upper bound of all
f
n
(
↥
).
) be a partially ordered set. We say
X
is a
complete partially ordered
set
(CPO) if it has suprema for all increasing chains. A CPO with
bottom
is a CPO
with a least element
Let (
X
,
↥
. The least fixed point of a continuous function
f
on the CPO
can be characterised in the same way as in Proposition
2.1
(1), namely
n
≥
0
f
n
(
↥
).
2.2
Induction and Coinduction
We observe that Theorem
2.1
provides two proof principles: the
induction principle
says that, to show
lfp
(
f
)
x
it is enough to prove
f
(
x
)
x
; the
coinduction
principle
says that, to show
x
gfp
(
f
) it suffices to prove
x
f
(
x
). Those are two
important proof principles in concurrency theory. In this section, we briefly introduce
inductive and coinductive definitions by rules and their associated proof techniques.
For more detailed accounts, we refer the reader to [
1
,
2
].
Given a set
X
,a
ground rule
on
X
is a pair (
S
,
x
)
X
, meaning that,
from the premises
S
we can derive the conclusion
x
. Usually, we write the rule (
S
,
x
)
as
∈
P
(
X
)
×
, and as
x
1
,
...
,
x
n
x
if
S
=∅
if
X
={
x
1
,
...
,
x
n
}
.
(2.1)
x
∅
A rule without any premise, i.e. in the form (
,
x
), is said to be an
axiom
.
Quite often we define a set of objectives by rules. For example, let
Var
be a set
of variables ranged over by
x
. In the lambda calculus the set
ʛ
of all lambda terms
can be expressed by a BNF (Backus-Naur Form) grammar:
Search WWH ::
Custom Search