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

Finale Sequenzen-Koalgebra

Eine Sequenzen-Koalgebra über dem Zustandsraum X und dem Alphabet A ist eine Funktion c : X ⟶ (X × A) ⊎ {⊥}. Eine Element x ∈ X ist dann eine Sequenz. Sie ist leer, falls c x = ⊥. Falls jedoch c x = (x′, a) dann ist a das erste Element der Sequenz x und x′ ist die Restsequenz.

Seien c : X ⟶ (X × A) ⊎ {⊥} und d : Y ⟶ (Y × A) ⊎ {⊥} zwei Sequenzen über dem gleichen Alphabet (aber mit möglicherweise verschiedenen Zustandsräumen). Eine Funktion f : X ⟶ Y heißt Sequenzenhomomorphismus von c nach d, falls für alle x ∈ X:

d(f x) = \{ \begin{matrix}⊥ & falls c x = ⊥ \\ (y′, a) & falls c x = (x′, a) ∧ y′ = f x′ \end{matrix}

Eine Sequenzen-Koalgebra d ist final, falls es für jede Sequenzenkoalgebra c genau einen Sequenzenhomomorphismus von c nach d gibt. (Insbesondere muss es auch genau einen Sequenzenhomomorphismus von d nach d geben.)

Aufgabe

1. Formalisieren Sie Sequenzen-Koalgebren, Sequenzenhomomorphismen und den Begriff der finalen Sequenzen-Koalgebra in PVS.

2. Konstruieren Sie die finale Sequenzen-Koalgebra (für ein beliebiges aber festes Alphabet) und beweisen Sie die Finalität in Pvs.

Detaillierte Hinweise

• Es ist zweckmäßig, für den Typ der Sequenzen-Koalgebren einen Typ in Pvs zu definieren. Dabei sind sowohl der Zustandsraum, als auch das Alphabet Typparameter.

• Die Sequenzenhomomorphismen definiert man am besten als Prädikat über dem Funktionsraum X → Y. Dafür braucht man natürlich drei Typparameter.

• Mit diesem Ansatz kann Finalität in Pvs nicht formalisiert werden (weil man nicht über alle Typen quantifizieren kann). Es ist jedoch ausreichend, Finalität in Bezug auf einen (parametrischen) Zustandsraum zu definieren. Dafür braucht man drei Typparameter (Zustandsraum X, Y und Alphabet A). Finalität wird dann als Prädikat über den Koalgebren mit Zustand Y definiert: Eine Koalgebra d ist in diesem Prädikat, falls es für alle Koalgebren c mit dem Zustandsraum X genau einen Sequenzenhomomorphismus gibt.

• Konstruktion und Beweis für die finale Sequenzen-Koalgebra sind in Abschnitt 4.2 des Vorlesungsskriptes [Tew05] skizziert.

Literatur

[JR97] Jacobs, B. and J. Rutten: A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222–259, 1997.

[Tew05] Tews, H.: Koalgebraische Spezifikation und Verfeinerung. Vorlesungsskript., 2005.