Tarski fixed point theorem

existence of a least fixed point (for finite sets)

Auteurs: Léon Gondelman / Martin Clochard

Catégories: Mathematics

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

Proof of Tarski fixed point theorem (existence of least fixed point) for finite sets, using lemma functions.

Authors: Martin Clochard Léon Gondelman

```module Tarski

use set.Fset
clone export relations.PartialOrder with axiom .

constant a : fset t

constant e : t
axiom minimality: mem e a /\ forall x. mem x a -> rel e x

function f t : t
axiom range: forall x. mem x a -> mem (f x) a
axiom monotone: forall x y. mem x a -> mem y a -> rel x y -> rel (f x) (f y)

predicate fixpoint (x:t) = mem x a /\ f x = x

end

module Tarski_rec
use set.Fset
clone export Tarski with axiom .

let lemma least_fix_point () : unit
ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
= let rec ghost aux (x: t) (b: fset t) : t
requires { mem x a /\ subset b a }
requires { forall y. mem y a -> rel x y -> mem y b }
requires { forall y. fixpoint y -> rel x y }
requires { rel x (f x) }
ensures  { fixpoint result /\ forall x. fixpoint x -> rel result x }
variant  { cardinal b }
= let y = f x in if x = y then x else aux y (remove x b)
in let _witness = aux e a in ()
end

module Tarski_while
use set.Fset
clone export Tarski with axiom .
use ref.Ref

let lemma least_fix_point () : unit
ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
=
let x = ref e in
let b = ref a in
while (f !x) <> !x do
invariant { mem !x a /\ subset !b a}
invariant { forall y. mem y a -> rel !x y -> mem y !b }
invariant { forall y. fixpoint y -> rel !x y }
invariant { rel !x (f !x) }
variant   { cardinal !b }
b := remove !x !b;
x := f !x
done

end
```