© 1999 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Coalgebraic theories of sequences in PVS
A1 Institut für Theoretische Informatik, TU Dresden, D-01062 Dresden, Germany E-mail: hensel@tcs.inf.tu-dresden.de A Department of Computer Science, University of Nijmegen, PO Box 9010, 6500 GL Nijmegen, The Netherlands E-mail: bart@cs.kun.nl
The paper explains the setting of an extensive formalization of the theory of sequences (finite and infinite lists of elements of some data type) in the Prototype Verification System PVS. This formalization is based on the characterization of sequences as a final coalgebra, which is used as an axiom. The resulting theories comprise standard operations on sequences like composition (or concatenation), filtering, flattening, and their properties. They also involve the prefix ordering and proofs that sequences form an algebraic complete partial order. The finality axiom gives rise to various reasoning principles, like bisimulation, invariance, and induction for admissible predicates. Most of the proofs of equality statements are based on bisimulations, and most of the proofs of prefix order statements use simulations. Some significant aspects of these theories are described in detail. This coalgebraic formalization of sequences is presented as a concrete example that shows the importance and usefulness of coalgebraic modelling and reasoning. Hopefully, it will help to convey the view that coalgebraic data types should form an intrinsic part of (future) languages for programming and reasoning. Therefore, some suggestions for an appropriate syntax for coalgebraic datatypes are included. The use of sequences as a final coalgebra is demonstrated in two (standard) applications: a refinement result for automata involving sequences of actions, and a coalgebraic definition plus correctness proof for an insert operation on ordered sequences.
Keywords: Datatype, coinduction, theorem proving