Angewandte Softwareverifikation mit einem interaktiven Theorembeweiser Version 28. März 2011

Knaster-Tarski Fixpunkttheorem

Ein vollständiger Verband ist eine geordnete Menge in der Infima (größte untere Schranken) und Suprema (kleinste obere Schranken) für beliebige (insbesondere auch unendlich große) Teilmengen existieren. Eine Funktion f auf einem Verband ist monton, wenn aus x ≤ y auch f(x) ≤ f(y) folgt. Ein Fixpunkt ist ein Element x mit f(x) = x.

Das Knaster-Tarski Fixpunkttheorem besagt, dass die Fixpunkte einer beliebigen monotonen Funktion auf einem vollständigen Verband wieder einen vollständigen Verband auf der gleichen (eingeschränkten) Ordnung bilden (das ist die vollständige Version, praktisch interessiert man sich meist nur für den größten oder kleinsten Fixpunkt).

Aufgabe

1. Formalisieren Sie vollständige Verbände, monotone Funktionen und Fixpunkte für beliebige Ordnungsrelationen (auf beliebigen Trägermengen).

2. Beweisen Sie das Knaster-Tarski Fixpunkttheorem in Pvs.