7

If I understand correctly, we can model inductive data types as initial F-algebras and co-inductive data types as final F-coalgebras (for an appropriate endofunctor F) [1]. I understand that according to Lambek's lemma the initial algebras (and final coalgebras) are fixed point solutions of the isomorphism T ≅ F T, but I don't see why the initial algebra is the least fixed point, while the final coalgebra is the greatest fixed point. (Is it obvious that the isomorphism T ≅ F T has a solution?)

Also I'm not really clear on how are inductive and co-inductive data types defined in type theory. Are there any recommended resources on this topic and maybe their relationship to category theory?

Thank you!

3
  • 4
    In a poset category, an initial object is the bottom ("least"), and a final one is the top ("greatest"). So, by extension, it makes sense to call the initial algebra the least fixed point, etc. even if that's a little abuse, I think.
    – chi
    Aug 22, 2018 at 13:29
  • 1
    @chi Thanks for the comment! Just to make sure I understand this correctly. One object is initial and the other is terminal, but they are leaving in different categories, right? The first one is initial in F-Alg(C), the second one is terminal in F-Coalg(C). I guess we cannot "compare" them, or it just doesn't matter? Aug 22, 2018 at 13:49
  • 3
    Both are isomorphisms, though. We have a: FA->A and b: B->FB. So, in particular, a^-1 : A->FA is also a coalgebra and b^-1: FB->B is an algebra. Hence, we get an algebra-morphism A->B and a coalgebra morphism A->B. (They might be the same ones if we think of them as C-morphisms). So, we could say that A is "less" than B since there's a morphism between them in C. It is not a proper comparison since C is a category, not a poset, but there is some analogy. In a sense, a category is an extension of a preorder.
    – chi
    Aug 22, 2018 at 14:03

1 Answer 1

4

My understanding is that, in principle, there may be many solutions to the fixed point equation T ≅ F T. By Lambek's lemma, the initial algebra, if it exists, is one of those fixed points. In fact it's the least fixed point.

There is a universal condition that defines the least fixed point, along the lines of there being a unique morphism to any other fixed point that satisfy certain commutation conditions.

In other words, not every fixed point defines the initial algebra.

The same argument applies to final coalgebras and greatest fixed points.

See, for instance, Least Fixed Point of a Functor .

2
  • 1
    Thank you for the answer and for the reference – I'll check it out! If I understood correctly, the definition of "least fixed point" from category theory generalizes the notion from order theory. I would also like to make the connection with data types: where does the interpretation of recursive data types as least fixed points come from? Is it from domain theory? (I'm sorry, but my background in type theory and semantics is very weak.) Aug 23, 2018 at 15:24
  • 2
    Adamek gives an interesting example of the identity functor, for which every object is a fixed point, but there is only one least fixed point (up to isomorphism)--the initial object. Aug 24, 2018 at 17:47

Your Answer

Reminder: Answers generated by Artificial Intelligence tools are not allowed on Stack Overflow. Learn more

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.