A Coalgebraic Theory of Sequences in PVS

Bart Jacobs and Ulrich Hensel

June 1998

[Introduction] [Background] [Theory overview]


We present an axiomatic description of (possibly infinite) sequences in PVS, using (final) coalgebras. Various theories are based on this axiomatisation. You can look at (version 2.0) of the theories and also download the whole dump file. It should run in PVS version 2.414.

(Version 1.0 is still available as gzipped dump file.)

We make this work publicly available, but we appreciate an acknowledgement if you make use of these files in your publications. If you have any comments, or suggestions for additions, please let us know.


A finite or infinite sequence of values from a parameter type A can be seen as generated by a machine or automaton with state space S, a transition function f : [S -> Lift[[A,S]]]---where Lift[X] is the type X augmented with a bottom element---and a start state s in S . This f is a partial function providing either the value bot (for undefined) or an output in A together with a next state in S. The behavior of such a machine is given by consecutively applying f (as long as possible) and observing the emerging output in A. Such a behavior corresponds to a sequence of elements of A.

The above machine with state space S and transition function f is an example of a coalgebra of type Lift[[A,-]]. The collection Seq[A] of sequences of elements of A also carries such a coalgebra structure next: Seq[A] -> Lift[[A,Seq[A]]]. The function next decomposes a sequence into the car and the cdr (head,tail), if these exist (otherwise it produces the value bot). This coalgebra next is very special; it is the final coalgebra of this type: for an arbitrary coalgebra ``struct'' there exists a unique homomorphism ``coreduce(struct)'' to it. This is the content of the (single) axiom that we use for sequences.

The finality axiom provides us with powerful definition schemes and proof mechanisms. In order to define a funtion g taking values in Seq[A] it suffices to describe a coalgebra structure on the domain of g. Uniqueness is used to prove equality of such functions. Bisimulation, invariant, simulation (for prefix order on sequences), and admissability proof methods are developed based on the uniqueness property. The main advantage of this coinductive approach is that it allows us to deal with sequences in a step-by-step manner: we always define and prove by looking at the next step in a sequence. This is similar (but dual, in a suitable sense) to inductive definitions and proofs, where one also only takes single steps.

For more information and references, there is a paper which explains the formalisation in detail. It will appear in the Journal of Logic and Computation. Also, there is a tutorial on (Co)algebras and (Co)induction providing further background information (from: Bulletin of the European Association for Theoretical Computer Science 62 (1997), p.222-259).

Theory overview

We briefly describe the various theories divided into four groups.
[Introduction] [Background] [Theory overview]
Last revised 24 June 1998, Bart Jacobs and Ulrich Hensel