Formal Semantics of

Programming Languages
Florian Zuleger
SS 2023

1
 Denotational Semantics
• In small-step semantic we were interested in how
a While program is executed.
• In contrary, we are just interested in the effect
(i.e. relating input and output) of executing a
program in denotational semantics.
• Additionally, we want to give a semantics to
While that is compositional.

• Big-step semantics is half-way inbetween small-

step and denotational semantics…

2
 How to define the effect of an
command?
We already defined the denotational semantics of
arithmetic and Boolean expressions as functions:
«-¬: Exp ! States ! N
«-¬: Bool ! States ! T = {true, false}

Further we defined semantic (partial) functions for

the big-step and small step semantics:
«-¬S: Com ! States States
» »

«-¬B: Com ! States States

3
 State Transformers
Idea:
We want to directly define a (partial) function
«-¬: Com ! States States

»
using structural induction.

To ease the technical development,

we will define a total function
«-¬: Com ! States ! 2States
that maps an initial state to a set of final states.
This allows to model non-termination (no final state) and
non-determinism (multiple final states).
4
 Determinacy
Then we will show that the denotational
semantics «-¬ of our simple While-language is
deterministic:
|«C¬(s)| · 1 for all commands C and all states s

Further, our definition of «-¬ will indeed result in

partial functions for non-terminating input
states s, identifying «C¬(s) = ; with «C¬(s) = ?.

5
 Assignments
Effect of the command (x := E) relative to state s?

Intuition:
(1) evaluate E relative to state s to some value n = «E¬ s
(2) return the state s with new value n for variable x

State transformer:

«x := E¬(s) = { s[x  «E¬ s] }

6
 The Skip Command
Effect of the command skip relative to state s?

Intuition:
(1) nothing to do
(2) return the state s

State transformer:

«skip¬ = Id, where Id(s) = { s } is the

identity function
7
 Sequential Composition
Effect of the command C1 ; C2 relative to state s?

Intuition:
(1) determine the effect of command C1
(2) determine the effect of command C2
(3) compose the effects of the two commands

State transformer: Well-

defined?

«C1 ; C2¬ = «C2¬ ± «C1¬

8
 Function Lifting
We can easily lift a function f: A ! 2B to accept sets
instead of single elements as input, i.e., we can lift f
to a function f: 2A ! 2B by setting
f(S) = s2S f(s).
Lifting ensures that the function composition
«C2¬ ± «C1¬ is well-typed (consider «C2¬(«C1¬(s)) given
some state s).
Further note that «C2¬ ± «C1¬ is again a function with
type States ! 2States.
Thus «C1 ; C2¬ = «C2¬ ± «C1¬ is well-defined.

9
 Sequential Composition and
Non-termination
Consider the sequential composition C1 ; C2 and
consider some state s that leads to non-termination
in command C1.
This means «C1¬(s) = ;.
Using the definition for sequential composition we
now calculate «C1 ; C2¬(s) = «C2¬ ± «C1¬(s) =
«C2¬(«C1¬(s)) = «C2¬(;) = ;.
This means that C1 ; C2 is also non-terminating for
state s as desired!
10
 Filters
We introduce filter functions
filterP: (States ! T) ! States ! 2States
filterN: (States ! T) ! States ! 2States
by
{s} if b(s)=true,
filterP(b)(s) =
{} if b(s)=false.
{s} if b(s)=false,
filterN(b)(s) = {} if b(s)=true.

filterP(b)/filterN(b) is the identity relation on states for which

the function b returns true/false; states for which b returns
false/true are ‘filtered out’.
11
 If Commands
Effect of command if B then C1 else C2 relative to state s?

Intuition:
(1) determine the effect of Boolean B for the filter functions and
determine the effect of the commands C1 and C2
(2) we compose the filter functions with the effect of C1 and C2
(3) we union both effects from the previous step

State transformer: Meaning of

union
«if B then C1 else C2¬ = operator?
«C1¬ ± filterP(«B¬) [ «C2¬ ± filterN(«B¬)
12
 Union of Functions
Let f,g be two functions with f,g 2 States ! 2States.

We define the union of f and g to be the function

f [ g = ¸s. f(s) [ g(s),
where the lambda expression is to be interpreted
as (f [ g)(s) = f(s) [ g(s) for all s 2 States.

Example: We have filterP(b) [ filterN(b) = Id.

13
 While Commands
So far we succeeded in giving compositional
definitions to the commands in While.

Can we also give a compositional definition for the

command while B do C?

Our big-step semantic definition for while B do C

wasn’t compositional…

hC,si  s1 hwhile B do C,s1i  s’

B-WHILE.T «B¬ s = true
hwhile B do C,si  s’
14
 Denotational Semantics for
While Commands
Executing the loop corresponds to repeating the loop body
either 0 times, or 1 time, 2 times, …, i times, … and then
leaving the loop:

«while B do C¬(s) =
filterN(«B¬) (s)
[ filterN(«B¬) ± «C¬ ± filterP(«B¬) (s)
[ filterN(«B¬) ± «C¬ ± filterP(«B¬) ± «C¬ ± filterP(«B¬) (s)
[ … [ filterN(«B¬) ± («C¬ ± filterP(«B¬))i (s) [ …
= i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i(s)
15
 A Remark on Non-terminating Loops
Let us assume while B do C does not terminate for
some state s.

Then executing the loop results in the empty set:

«while B do C¬(s) =
= i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i(s)
=;

16
Denotational Semantics of while
From the two previous slides we get the following
semantics for while:

«while B do C¬ =
filterN(«B¬)
[ filterN(«B¬) ± «C¬ ± filterP(«B¬)
[ filterN(«B¬) ± «C¬ ± filterP(«B¬) ± «C¬ ± filterP(«B¬)
[ … [ filterN(«B¬) ± («C¬ ± filterP(«B¬))i [ …
= i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i
17
 An equation for while
We already know
«while B do C¬B =
«if B then (C;while B do C) else skip¬B.

We want to have the same property in

denotational semantics, so do we have
«while B do C¬ =
«if B then (C;while B do C) else skip¬?

18
 Fixed Point Equation
«while B do C¬ =
«if B then (C;while B do C)Any solution
else for f =in such
skip¬
an equation
«C;while B do C¬ ± filterP(«B¬) [ «skip¬is ±called a
filterN(«B¬) =
fixed point!
«while B do C¬ ± «C¬ ± filterP(«B¬) [ filterN(«B¬)

Does «while B do C¬ satisfy the equation

f=Ff
where
F f = f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)
with
F: (States ! 2States) ! (States ! 2States).

19
 «while B do C¬ is Fixed Point
Indeed, F «while B do C¬ =
= ( i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i ) ± «C¬ ± filterP(«B¬) [
filterN(«B¬)
= i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i ± «C¬ ± filterP(«B¬) [
filterN(«B¬)
= i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i+1 [ filterN(«B¬)
= i¸1 filterN(«B¬) ± («C¬ ± filterP(«B¬))i [ filterN(«B¬)
= i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i = «while B do C¬,

where F f = f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)

with F: (States ! 2States) ! (States ! 2States).
20
 Definition of «while B do C¬
as a Fixed Point
Idea: Use fixed points of F for a definition of
«while B do C¬.

Is there a always a fixed point?

Yes.
Is there a always a unique fixed point?
No…, but we will make it unique by
requiring an additional property.
21
 No Unique Fixed Point
We consider the command
C = while true do skip.

We have
F f = f ± «skip¬ ± filterP(«true¬) [ filterN(«true¬) =
= f ± Id ± Id [ ; = f.

Thus, every function f is a fixed point of F!

22
 Order of Functions
We define an order on functions States ! 2States.

Let f,g be two functions

with f,g 2 States ! 2States.

We say that f is smaller than g, in signs f µ g, iff

f(s) µ g(s) for all s 2 States.

23
 Comparison with other Fixed Points?
Let f be a pre-fixed point of F, i.e.,
f ± «C¬ ± filterP(«B¬) [ filterN(«B¬) = F f µ f.
How does f compare to
i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i ?

We have filterN(«B¬) µ f.
Thus filterN(«B¬) ± «C¬ ± filterP(«B¬) µ f.
By induction filterN(«B¬) ± («C¬ ± filterP(«B¬))i µ f for all i.
Therefore i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i µ f.

Because fixed points are also pre fixed points we have that
i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i is the least fixed point of F with
regard to the order µ.

24
 Notation
We use the lambda expressions
¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)
as an abbreviation for the functional F defined by
F f = f ± «C¬ ± filterP(«B¬) [ filterN(«B¬).

We denote by
lfp ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)
the least fixed point of the functional F.
25
 While Commands
Effect of command while B do C?

Intuition:
(1) determine the effect of Boolean B for the filter functions and
determine the effect of the command C
(2) we compose the filter function with the effect of C
(3) we determine the least fixed point of the functional that
represents iterating the loop

State transformer:
«while B do C¬ =
lfp ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)
26
 Denotational Semantics
«x := E¬(s) = { s[x  «E¬ s] }
«skip¬ = Id
«C1 ; C2¬ = «C2¬ ± «C1¬
«if B then C1 else C2¬ =
«C1¬ ± filterP(«B¬) [ «C2¬ ± filterN(«B¬)
«while B do C¬ =
lfp ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)

27
 Example
«y := 1; while : (x=1) do (y := y * x; x := x – 1)¬
= «while : (x=1) do (y := y * x; x := x – 1)¬ ± «y := 1¬
= i¸0 filterN(«: (x=1)¬) ± («y := y * x; x := x – 1¬ ±
filterP(«: (x=1)¬))i ± «y := 1¬
= i¸0 filterP(«(x=1)¬) ± («x := x – 1¬ ± «y := y * x¬±
filterN(«(x=1) ¬))i ± «y := 1¬
= i¸0 ¸s. filterP(«(x=1)¬) ± («x := x – 1¬ ± «y := y * x¬±
filterN(«(x=1) ¬))i ± «y := 1¬(s)

{s[x  1] [y  i!] } if s(x)=i,

= i¸0 ¸s.
{} otherwise.

28
 Example
«y := 1; while : (x=1) do (y := y * x; x := x – 1)¬
= «while : (x=1) do (y := y * x; x := x – 1)¬ ± «y := 1¬
= i¸0 filterN(«: (x=1)¬) ± («y := y * x; x := x – 1¬ ±
filterP(«: (x=1)¬))i ± «y := 1¬
= i¸0 filterP(«(x=1)¬) ± («x := x – 1¬ ± «y := y * x¬±
filterN(«(x=1) ¬))i ± «y := 1¬
= i¸0 ¸s. filterP(«(x=1)¬) ± («x := x – 1¬ ± «y := y * x¬±
filterN(«(x=1) ¬))i ± «y := 1¬(s)

{s[x  1] [y  i!] } if s(x)=i,

= i¸0 ¸s.
{} otherwise.

29
 Determinism
Lemma
We have |«C¬(s)| · 1 for all commands C and all
states s.

Proof
By structural induction on the commands C.

Case x := E and skip: trivial.

30
 Determinism
Case C1 ; C2 :
By definition we have «C1 ; C2¬ = «C2¬ ± «C1¬.
By induction assumption we have |«C1¬(s)| · 1 and
|«C2¬(s)| · 1 for all states s.
Let s be an arbitrary state.
We have «C2¬ ± «C1¬(s) = «C2¬(«C1¬(s)).
Thus either «C1¬(s) = ; or «C1¬(s) = {t} for some state t.
In the first case we get |«C2¬(«C1¬(s))| = |«C2¬(;)| = |;| = 0.
In the second case we get |«C2¬(«C1¬(s))| = |«C2¬(t)| · 1.
In both cases |«C2¬ ± «C1¬(s)| = |«C2¬(«C1¬(s))| · 1.
31
 Determinism
Case if B then C1 else C2:
By definition we have «if B then C1 else C2¬ =
«C1¬ ± filterP(«B¬) [ «C2¬ ± filterN(«B¬).
By induction assumption we have |«C1¬(s)| · 1 and
|«C2¬(s)| · 1 for all states s (*).
Let s be an arbitrary state.
We either have «B¬(s) = true or «B¬(s) = false.
Hence, either (s,s) 2 filterP(«B¬) or (s,s) 2 filterN(«B¬).
Thus «C1¬ ± filterP(«B¬) [ «C2¬ ± filterN(«B¬)(s) is either
«C1¬(s) or «C2¬(s).
Therefore the conclusion follows from (*).

32
 Determinism
Case while B do C:
We have «while B do C¬ = lfp ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)
= i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i.
By induction assumption we have |«C¬(s)| · 1 for all states s.
Thus |filterN(«B¬) ± («C¬ ± filterP(«B¬))i(s)| · 1 for all states s.
We observe that there is at most one i with
|filterN(«B¬) ± («C¬ ± filterP(«B¬))i(s)| = 1
for all states s.
Hence,
| i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i(s)| · 1
for all states s.

33
 Contexts: Commands with Holes
C 2 Com ::= - | x := E | if B then C else C |
C ; C | skip | while B do C

Example:
for the context
C[-] = - ; while B do -
we have
C[x := x + 1] = x := x + 1 ; while B do x := x + 1

34
 Contextual Equivalence
Definition
Commands C1 and C2 are contextually equivalent
with respect to the small-step semantics, if for all
contexts C[−] and states s,s’

C[C1] s !* s’ iff C[C2] s !* s’.

Note: Very hard to reason about because of the

quantification over C!

35
 Denotational Semantics
Frege’s principle of compositionality:
“The meaning of a composite phrase can be defined in
terms of the meanings of its parts”

«x := E¬(s) = { s[x  «E¬ s] }

«skip¬ = Id
«C1 ; C2¬ = «C2¬ ± «C1¬
«if B then C1 else C2¬ =
«C1¬ ± filterP(«B¬) [ «C2¬ ± filterN(«B¬)
«while B do C¬ =
lfp ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)
36
 Compositionality and Contextual
Equivalence
Each context determines a “function between
meanings”, i.e., for each C[−] there is a function
fC: (States ! 2States) ! (States ! 2States) such
that
«C[C’]¬ = fC(«C’¬)
for any command C’.

37
 Compositionality and Contextual
Equivalence
A consequence of such a function
fC: (States ! 2States) ! (States ! 2States) for a
context C[−] is that
if «C1¬ = «C2¬ then
«C[C1]¬ = fC(«C1¬) = fC(«C2¬) = «C[C2]¬!

It remains to relate the structural and the

denotational semantics, i.e., we want to establish
that «C¬S = «C¬ for all commands C!

38
 An Equivalence Result
Theorem
For all commands C we have «C¬ = «C¬S.

Proof
We split the proof into the two lemmas for the cases
«C¬S µ «C¬.
and
«C¬S ¶ «C¬.
39
 «C¬S µ «C¬
It is sufficient to prove that for all states s and s’
hC,si !* s’ implies «C¬(s) = s’.

Note that we now make use of the determinacy of «-¬ and

simply write «C¬(s) = s’ instead of s’ 2 «C¬(s).

To do so we will prove by structural induction on C that

hC,si ! s’ implies «C¬(s) = s’
hC,si ! hC’,s’i implies «C¬(s) = «C’¬s’

The claim then follows by an induction on the length k of the

derivation hC,si !k s’.

40
 hC,si ! s’ implies «C¬(s) = s’
Case S-ASS:
We have hx := E,si ! s[x  «E¬ s].
Since «x := E¬(s) = s[x  «E¬ s] the claim follows.

Case S-SKIP: trivial

41
 hC,si ! s’ implies «C¬(s) = s’
Case S-SEQ.FINAL:
We assume hC1 ; C2,si ! hC2,s’i.
The rule hypothesis gives us hC1,si ! s’.
We can apply the induction assumption to this
transition and get «C1¬(s) = s’.
Thus «C1 ; C2¬(s) = «C2¬ ± «C1¬(s) =
«C2¬(«C1¬(s)) = «C2¬(s’).

42
 hC,si ! hC’,s’i implies «C¬(s) = «C’¬s’

Case S-SEQ.STEP:
We assume hC1 ; C2,si ! hC1’ ; C2,s’i.
The rule hypothesis gives us hC1,si ! hC1’,s’i.
We can apply the induction assumption to this
transition and get «C1¬(s) = «C1’¬(s’).
Thus «C1 ; C2¬(s) = «C2¬ ± «C1¬(s) = «C2¬(«C1¬(s)) =
«C2¬(«C1’¬(s’)) = «C2¬ ± «C1’¬(s’) = «C1‘ ; C2¬(s’).

43
 hC,si ! hC’,s’i implies «C¬(s) = «C’¬s’
Case S-IF.T:
We assume «B¬ s = true.
Then, hif B then C1 else C2,si ! hC1,si.
Hence, «if B then C1 else C2¬(s) =
(«C1¬ ± filterP(«B¬) [ «C2¬ ± filterN(«B¬))(s) =
«C1¬ ± filterP(«B¬)(s) [ «C2¬ ± filterN(«B¬)(s) =
«C1¬(s) [ «C2¬ ± ; = «C1¬(s).

Case S-IF.F: Analogous.

44
 hC,si ! hC’,s’i implies «C¬(s) = «C’¬s’
Case S-WHILE:
We assume hwhile B do C,si !
hif B then C;while B do C else skip,si.
We have «while B do C¬ =
lfp ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬) =
«while B do C¬ ± «C¬ ± filterP(«B¬) [ filterN(«B¬) =
«C ; while B do C¬ ± filterP(«B¬) [ Id ± filterN(«B¬) =
«if B then C ; while B do C else skip¬

45
 «C¬S ¶ «C¬
We proceed by structural induction on the
command C.

Case x := E:
We have «x := E¬(s) = s[x  «E¬ s].
We get hx := E,si ! s[x  «E¬ s] from rule S-ASS.

Case skip: analogous.

46
 «C¬S ¶ «C¬
Case C1 ; C2 :
By induction assumption we have «C1¬ µ «C1¬S
and «C2¬ µ «C2¬S.
Thus, we have «C1 ; C2¬ = «C2¬ ± «C1¬ µ «C2¬S ± «C1¬S.
From lecture 2 slide 38 we know that
If hC1,si !k s’ then hC1;C2,si !k hC2,s’i.
This gives us «C2¬S ± «C1¬S µ «C1 ; C2¬S.
The property then follows from the transitivity of
µ.
47
 «C¬S ¶ «C¬
Case if B then C1 else C2:
By induction assumption we have «C1¬ µ «C1¬S
and «C2¬ µ «C2¬S.
We have «if B then C1 else C2¬
= «C1¬ ± filterP(«B¬) [ «C2¬ ± filterN(«B¬)
µ «C1¬S ± filterP(«B¬) [ «C2¬S ± filterN(«B¬)
= «if B then C1 else C2¬S.

48
 «C¬S ¶ «C¬
Case while B do C:
By induction assumption we have «C¬ µ «C¬S.
We have «while B do C¬S =
«C ; while B do C¬S ± filterP(«B¬) [ «skip¬S ± filterN(«B¬)
¶ «while B do C¬S ± «C¬S ± filterP(«B¬) [ filterN(«B¬)
¶ «while B do C¬S ± «C¬ ± filterP(«B¬) [ filterN(«B¬)

Thus «while B do C¬S is a pre-fixed point of F,

where F f = f ± «C¬ ± filterP(«B¬) [ filterN(«B¬).
Using the property on slide 24 we have
«while B do C¬ = lfp ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬) =
i¸0 filterN(«B¬) ± («C¬ ± filterP(«B¬))i µ «while B do C¬S.
49
 Partial Order
(L,v) is a partial order, if the binary relation
v µ L £ L satisfies:

• reflexifity: 8 x 2 L. x v x
• transitivity: 8 x,y,z 2 L. x v y Æ y v z ! x v z
• anti-symmetry: 8 x,y 2 L. x v y Æ y v x ! y = x
 Upper and Lower Bounds
Let (L,v) be a partial order and X µ L some subset.
For y 2 L we define:
X v y :, ∀ x 2 X. x v y “y is an upper bound for X”
y v X :, ∀ x 2 X. y v x “y is a lower bound for X”
tX is a least upper bound for X if:
X v tX and ∀y 2 L. X v y ⇒ tX v y
uX is a greatest lower bound X if:
uX v X and ∀y 2 L. y v X ⇒ y v uX
Note that tX and uX do not always exist. If they exist, they
are unique.
 Lattice
For X = {x,y} we also write x t y instead of t{x,y}
and x u y instead of u{x,y} .

A lattice is a partial order (L,v) where:

x t y and x u y exist for all x,y 2 L
We also write (L,t,u) to acknowledge that (L,v)
is a lattice.

Note that for lattices we have:

xv y,xu y=x,xt y=y
These Partial Orders Are Lattices
These Partial Orders Are Not Lattices

Why?
These Partial Orders Are Not Lattices
 Literature
"Introduction to lattices and order", B. A. Davey
and H. A. Priestley is a good introduction to
lattice theory

56
 Lattice Properties
Let (L,t,u) be a lattice.

For all x,y,z 2 L we have:

xv y)xt zv y t z
xv y)xu zv y u z
xt y=yt x
xu y=yu x
(x u z) t (y u z) v (x t y) u z
(x u y) t z v (x t z) u (y t z)

57
 Top and Bottom Elements
If L has a largest element, i.e., if tL exists,
> := tL is called the top element of L.

If L has a smallest element, i.e., if uL exists,

? := uL is called the bottom element of L.

We also write (L,t,u,>,?), if > and ? exist.

 The Subset Lattice
Every finite set A defines a lattice (2A,µ), where:
–?=;
–>=A
–xty=x[y E.g. A = {a,b,c}
–xuy=xÅy {a,b,c}

{a,b} {a,c} {b,c}

{a} {b} {c}

;
 Complete Lattices
A lattice (L,t,u) is complete,
if tX and uX exist for all X µ L.

Note that for a complete lattice there is always a

smallest and largest element.

Fact:
Every finite lattice is complete.
Why?
 Complete Lattices
A lattice (L,t,u) is complete,
if tX and uX exist for all X v L.
Note that for a complete lattice there is always a
smallest and largest element.
Fact:
Every finite lattice is complete.
Show that tX and uX exist by induction on |X|
(the number of elements in X).
 Map Lattice
Given a set A and a lattice L we define the map lattice A ! L by point-
wise operations.

For f,g 2 A ! L we define

f v g iff f(a) v g(a) for all a
f t g = ¸a. f(a) t g(a)
f u g = ¸a. f(a) u g(a)

Example:
Consider the map lattice States ! 2States,
where f µ g for f,g 2 States ! 2States iff f(s) µ g(s) for all s 2 States.

We have that A ! L is complete iff L is complete (exercise).

 Monotone Functions
• A function f: L → L is monotone when:
∀x,y ∈ L: x v y ⇒ f(x) v f(y)
• Monotone functions are closed under
composition (exercise)
• t and u are monotone in both arguments:
x v x’ Æ y v y’ ! x t y v x’ t y’
x v x’ Æ y v y’ ! x u y v x’ u y’
 Monotone Functions
Let (L,t,u) be a lattice.
We consider the map lattice L ! L.

Function concatenation
± : (L ! L) ! (L ! L)
is montone in its first argument, i.e.,
f1 v f2 ) f1 ± g v f2 ± g for all f1,f2,g 2 L ! L,
and montone in its second argument
f1 v f2 ) g ± f1 v g ± f2 for all f1,f2 2 L ! L
if g 2 L ! L is a monotone function.
64
 Example
We consider the complete lattice
(States,[,Å,>,?) and the corresponding map
lattice States ! 2States, which is also complete.

By the properties on the two previous slides we

have that
¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)
is a monotone function on States ! 2States.
65
 Fixed-Points
Given a function f: L → L, we say x is a fixed
point of f, if
x = f(x).
A fixed point x is the least fixed point of f, if
y = f(y) ) x v y for all y 2 L.

Similarly we define the greatest fixed point.

 Basic Fixed-Point Theorem
Let (L,t,u,>,?) be a finite lattice.
Then every monotone function f has a unique
least fixed-point:
lfp(f) = ti¸0 fi(?)
Moreover for every pre fixed point x,
i.e., f(x) v x, we have lfp(f) v x.
A dual theorem holds for the greatest fixed
point: gfp(f) = ui¸0 fi(>)
 Proof of Existence
Clearly, ? v f(?).
Since f is monotone, we also have f(?) v f2(?).
By induction, fi(?) v fi+1(?).
This means that
? v f(?) v f1(?) v... Fi(?) ...
is an increasing chain.
Since L is finite we have fk(?) = fk+1(?) for some k.
) lfp(f) = fk (?) is a fixed point.
 Proof of Unique Least
Let x be some pre fixed point, i.e., f(x) v x.
Clearly, ? v x.
By induction, fi(?) v fi(x) v x.
In particular, lfp(f) = fk(?) v x.

Because every fixed point is also a pre fixed point

we get that lfp(f) is a least fixed point of f.

The uniqueness of lfp(f) follows from the anti-

symmetry of the partial order v.
 Continuity
Let (L,t,u,>,?) be a complete lattice.
A function f: L → L is continuous, iff
f(t i¸0 xi) = t i¸0 f(xi)
for all sequences (xi)i¸0.

Example: ¸f. f ± «C¬ ± filterP(«B¬) [ filterN(«B¬)

is continuous (exercise)

Theorem
Every continuous function f has a unique least fixed-point:
lfp(f) = ti¸0 fi(?)
Moreover for every pre fixed point x, i.e., f(x) v x,
we have lfp(f) v x.
70