Al Vilcius asks:
concatenation of lists and streams from an alphabet A: - formally given by the unique arrow to a terminal coalgebra - heuristically it is supposed to be thought of as "erasing the comma" between a pair of streams (a,b)
But how is this to be understood computationally? eg. write down all the +ve odd integers and then all the even ones in reverse order to get a stream (1, 3, 5, .........., 6, 4, 2) can this be made into a stream specification? ie. what is the behaviour of the "dots" in the middle?
I don't have the Rutten paper. However, if it says what I expect then the idea is this. A coalgebra X -> 1 + AxX says how an element of X is either empty or can have an atom (from A) pulled off it on the left - in other words, it is a "cons" of a head atom and a tail sequence. Hence an element of X can either have just finitely many atoms pulled off it before it's exhausted, or it can supply infinitely many atoms. This gives the map from X to a final coalgebra A* comprising the finite and countably infinite sequences. The infinite sequences are infinite on the right, not the left, so 1, 3, 5, ... is one, but not ..., 6, 4, 2. The map A*xA* -> 1 + Ax(A*xA*) shows how to pull a head off a pair (s,t) of sequences. If s is non-empty, then take its head. If s is empty, take the head of t. If both are empty then there is no head (so map to the element of 1). The concatenation map A*xA* -> A* therefore acts as follows: if s is finite, then (s,t) maps to (elements of s followed by elements of t) - you pull all the elements of s off, and then when you've finished you start on t. if s is infinite, then (s,t) maps to s. You never finish taking the elements off s. Thus the concatenation question has a simple but boring answer. 1, 3, 5, ... concatenated with anything is just 1, 3, 5, ... again. And this is exactly what will happen if you compute the answer in a lazy programming language with lists, such as Haskell. Steve Vickers Department of Pure Maths Faculty of Maths and Computing The Open University ----------- Tel: 01908-653144 Fax: 01908-652140 Web: http://mcs.open.ac.uk/sjv22 10-Dec-2002 20:57:12 -0400,1055;000000000000-00000000