[Notes] Domain and Fixed Point

此篇大量參考 FLOLAC 08' 的 Denotational Semantics 講義。

A poset(partially ordered set) is a set D with a binary relation ⊑ s.t. the following properties hold:

1. reflexive: x ⊑ x 
2. anti-symmetric: x ⊑ y and y ⊑ x -> x ≡ y 
3. transitive: x ⊑ y and y ⊑ z -> x ⊑ z 

For a poset D, a set X ⊆ D is directed if:

1. X ≠ { } 
2. ∀ x,y ∈ X, ∃ z ∈ X s.t. x ⊑ z and y ⊑ z 

For a poset D, D is a cpo(complete partial order) if:

1. ∃ ⊥ ∈ D s.t. ∀ x ∈ X, ⊥ ⊑ x
2. Every directed set X ⊆ D has a least upper bound denoted as ⨆X

A cpo D is called domain as well.

---

Let D be a poset with ⊑ and f be a total function from D to D.

• x ∈ D is a fixed point of f iff f x = x
• x ∈ D is a least fixed point of f iff x is a fixed point of f and for every fixed point y of f, x ⊑ y.

**The Least Fixed Point Theorem**

Let D be a domain.

• ∀ f : D -> D, ∃ a least fixed point 
• ∃ fix : (D -> D) -> D, s.t. ∀ f : D -> D, fix f is the least fixed point of f.

For a function f : (D -> D), we can define a directed set Xf ⊆ D by

• Xf = {⊥,f ⊥,ff ⊥,fff ⊥,...}.

By the continuity of f,

f ⨆Xf
= f ⨆{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆f{Xf}
= ⨆f{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆{⊥, f ⊥, ff ⊥, fff ⊥, ...}
= ⨆Xf.

Thus, for any function f : D -> D, there exist a fixed point ⨆Xf of f. For least, we can support x is a fixed point as well. Then

⊥ ⊑ x,
f ⊥ ⊑ f x,
ff ⊥ ⊑ ff x,
...
fn ⊥ ⊑ fn x, (we write fn for applying f n times)
...

Because x is a fixed point of f, fd x will be x obviously. Collecting both sides as set we will obtain

{⊥,f ⊥,ff ⊥,fff ⊥,...} and {x},

then taking least upper bound of both set, 

⨆Xf ⊑ x

Thus, for any function f : D -> D, there exist a least fixed point ⨆Xf of f. Finally, we can define fix by 

fix f = ⨆Xf

for any function f : D -> D.

---

Relevance to (denotational) semantics:

The semantics of program g is a function g. For example, a program can be defined as follow:

g args = h (g args') : A -> B

This is not a simple case that we can find a corresponding g easily. However we can define another program/function f/f that can help us to define g. For example, we define

f : (A -> B) -> (A -> B),
f g = \args -> h (g args') = g.

Obviously, g is the least fixed point of f and the ⨆Xf as well. In this case, the domain D = (A -> B).