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

Endliche Mengen: Interne Charakterisierung

Ein algebraisches Modell für endliche Mengen enthält eine Konstante nil : set und eine Operation add : set × A ⟶ set. Ein Modell endlicher Mengen kann in folgenden Schritten konstruiert werden:

1. Zuerst bildet man den absolut freien Datentyp T mit den beiden Konstruktoren nil und add.

2. Auf diesem Datentyp betrachtet man die kleinste Kongruenzrelation R, für die folgendes gilt:

∀t ∈ T, a ∈ A . add(add(t, a), a) R add(t, a)
∀t ∈ T a, b ∈ A . add(add(t, a), b) R add(add(t, b), a)

3. Jede Äquivalenzklasse von R beschreibt genau eine endliche Menge. Man erhält deshalb das Modell der endlichen Mengen durch eine Faktorisierung: T/R.

Aufgabe

1. Konstruieren Sie den Quotienten T/R in PVS!

2. Konstruieren Sie eine bijektive Abbildung zwischen den in PVS eingebauten endlichen Mengen und T/R!