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 set.Fset
  clone export relations.PartialOrder with axiom .

  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 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: 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 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

download ZIP archive

Why3 Proof Results for Project "finite_tarski"

Theory "finite_tarski.Tarski_rec": not fully verified

ObligationsAlt-Ergo 1.30
VC least_fix_point0.10

Theory "finite_tarski.Tarski_while": not fully verified

ObligationsAlt-Ergo 1.30CVC4 1.4
VC least_fix_point------
split_goal_right
VC least_fix_point.10.00---
VC least_fix_point.20.00---
VC least_fix_point.30.01---
VC least_fix_point.40.01---
VC least_fix_point.50.04---
VC least_fix_point.60.02---
VC least_fix_point.70.02---
VC least_fix_point.80.01---
VC least_fix_point.90.01---
VC least_fix_point.10---0.04