Vaughan Pratt <pratt@cs.stanford.edu> writes:

1. Is there a variety embedding coinduction?

Jesse Hughes distinguishes induction from recursion in terms of natural numbers. For him induction is Peano's mathematical induction, while recursion is the uniqueness of the map from the (unique up to a unique isomorphism) initial algebra to an arbitrary algebra.

This doesn't look like what I had in mind, exactly. Peano's mathematical induction was meant as an example of induction, not the whole meaning of induction. I stated induction in terms of natural numbers only to continue Dusko's example. I'm afraid that I was a bit vague in what exactly induction is in my previous post. I say that a G-algebra A satisfies the principle of induction just in case every mono G-homomorphism into A is an isomorphism. If our base category has equalizers, then A satisfies the principle of induction just in case, for every algebra B, there is at most one homomorphism A -> B. So induction is the uniqueness part of initiality. What's recursion, then? As far as I'm concerned, recursion is just initiality. I.e., an algebra A satisfies the principle of definition by recursion just in case it is the initial algebra. (Why not take recursion to be just the existence part? I haven't seen much use for just the existence part and it also doesn't fit well with conventional usage.) Clearly, on this view, the principle of recursion implies the principle of induction, but the converse is not the case. I hope that my idea of induction is a bit clearer. I really must learn to write more precisely. -- Jesse Hughes "Such behaviour is exclusively confined to functions invented by mathematicians for the sake of causing trouble." -Albert Eagle's _A Practical Treatise on Fourier's Theorem_