samples of final coalgebras

It's about the first example of algebras/coalgebras from http://okmij.org/ftp/tagless-final/course/lecture.pdf


So, we have a theory, or, rather a language (free theory, that is), looking e.g. like this:

<expr> :::= add(<expr>, <expr>)
<expr> := neg(<expr>)
<expr> := 1

As a functor, it is T(A) = {1} + A + A×A, so that an algebra is T(A) -> A, consisting of i: {1} -> A, f: A->A, m: A×A->A.

A free algebra for such a theory, aka "initial algebra", "least fixpoint" is the "set" of all possible expressions (that is, sentences in this language).
Or, not expressions, but their syntax trees, for some reason called "abstract" (AST).

Since Kiselyov had suggested a "biggest fixpoint", aka "final coalgebra", there is some kind of interest, how does that thing look like?

Suppose we did not have the binary operation m. Then the theory would consist of two constants and a unary operation; algebras would consist of i: {1} -> A and f: A->A. An initial algebra would be ℕ, with component-wise transitions, f₀ and f₁. You can find all the details in wikipedia, since we are essentially talking about the functor 1+A.
For that functor, the terminal coalgebra ("final") is ℕ^~, where ℕ^~ is the set of natural numbers with a point added, so that transition goes back, 1->0, 2->1, etc, while the new point, ω, remains intact. For an arbitrary coalgebra A -> T(A), consisting of a partial endomorphism f, an element x of A maps to such n that fⁿ(x) == 1. We can call such an n a degree of x.

Now let's throw in the binary operation m: A×A->A. Initial algebra is still a set of expressions of our language. But a final coalgebra?

It is an infinite binary tree with  ℕ^~ at all nodes. An arbitrary coalgebra consists of two partial functions (with domains not intersecting): f': A⇸A, m': A⇸A×A. So for such a coalgebra, elements of A map to the following:

  - to number n if f' is defined on x and f'ⁿ(x) == 1;

 - to the pair of trees built for m'(x)∈A×A;

 - to number 0 if x == 1

The story behind these coalgebras being final fixpoints goes back to the category of adjoint pairs, but that's not important.

If you see how this thing works, you can, I guess, build all kind of final coalgebras for finite free theories (aka languages). All this, I think, is covered in the chapter "Model Theory" of Johnstone.

I'll be glad if you point out that something is not clear here and needs a clarification.