Wiki Agenda Contact Version française

Tarski fixed point theorem

existence of a least fixed point (for finite sets)


Authors: Léon Gondelman / Martin Clochard

Topics: Mathematics

Tools: 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 import set.Fset
  clone export relations.PartialOrder

  constant a : set 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 import set.Fset
  clone export Tarski

  let lemma least_fix_point () : unit
   ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
   = let rec aux (x: t) (b: set 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 import set.Fset
  clone export Tarski
  use import 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


download ZIP archive

Why3 Proof Results for Project "finite_tarski"

Theory "finite_tarski.Tarski_rec": fully verified in 0.15 s

ObligationsCVC3 (2.4.1)
VC for least_fix_point0.15

Theory "finite_tarski.Tarski_while": fully verified in 0.19 s

ObligationsCVC3 (2.4.1)
VC for least_fix_point0.19