I'm afraid that I've never quite understood the notion of guarded equations, so I cannot comment on much of what you wrote below without some more time and more thought. Let me make a few introductory comments and perhaps I can say more later. Dusko Pavlovic <dusko@kestrel.edu> writes:
Al Vilcius asks:
can anyone explain coinduction? in what sense it dual to induction?
and most people reply along the lines of:
The principle of induction says that initial algebras have no non-trivial subalgebras.
Coinduction says, dually, that the final coalgebra has no non-trivial quotients.
but wouldn't it be nice to keep the standard definition of induction, which says that the equations
f(0) = c f(n+1) = g(f(n))
determine a unique f, given c and g? this is the definition that most first year students study, and many programmers use every day, usually without the slightest idea about subalgebras, or triviality. do we really gain anything by replacing this simple scheme by the higher-order statement about all subalgebras? ok, we do get the appearance of symmetry between induction and coinduction. but is the higher-order statement about quotients really the friendliest form of coinduction, suitable to be taken as the definition?
I have always considered the statement regarding existence of a unique function f to be the principle of recursion. The principle of induction is, in my mind, the weaker principle that says that if a property holds of 0 and is closed under successor, then it holds of N. I identify "properties" with subobjects here. In terms of homomorphisms, this is equivalent to the "uniqueness part" of initiality (assuming that our category has some epi-mono factorization property, I suppose). One may question whether it's appropriate to take the principle of induction to apply to all properties or only those properties which are definable in some sense -- I guess you've done as much when you refer to the "higher-order statement" above. I'm not sure to what extent my use of all subalgebras differs from your quantification over all g and c in the statement of recursion above, however. When we separate the properties of induction and recursion in the way I mention above, by the way, then (conceptually) induction is a property of those algebras A in which each element is picked out by a (not necessarily unique) term of our language. I.e., those A for which there is an epi from the initial algebra to A. Hence, induction in my sense is weaker than recursion (induction in your sense). Regarding whether a statement about quotients is really the "friendliest form" of coinduction, I'll have to agree that it is not, if one's aim is to describe coinduction as it is commonly used. I chose to describe it in the terms above because these terms make clear the "co" in "coinduction". I did gloss over details that ensure the equivalence of the "familiar principle" of coinduction and the principle regarding quotients. If the base category has kernel pairs of coequalizers and G preserves weak pullbacks, then a G-coalgebra A has no non-trivial quotients iff the equality relation is the largest coalgebraic relation on A (I hope I've got that right). Inasmuch as the principle I called coinduction is not always equivalent to the familiar principle, I was being a bit misleading. However, I think it is the right approach if one's goal is to explain the relationship between induction and coinduction. I'm not sure that the principle regarding the equality relation is what you'd call coinduction, however. I think that the principle you have in mind is what I'd call "corecursion". Analogous to the distinction between recursion and induction, I omit the existence part of finality in what I call "coinduction" and I use the uniqueness part.
and then, moving from coalgebraic theories to comonads, like from algebraic theories to monads, should presumably yield an HSP-like characterization for the categories of (comonad) coalgebras. but coalgebras for a comonad over a topos usually form just another topos.
But, there *are* such characterizations of categories of coalgebras, if I understand your point. Namely, a full subcategory of coalgebras is closed under coproducts, codomains of epis and domains of regular monos iff it is the class of coalgebras satisfying a "coequation" -- given, here, some boundedness conditions on the functor so that things work out well. For brevity's sake, and because you're likely familiar with this result, I'll omit details on what a coequation is and how it's satisfied. By the way, about that last statement regarding coalgebras "usually" forming a topos: Doesn't one need that the endofunctor preserve pullbacks, or am I missing something? -- Jesse Hughes "The only "intuitive" interface is the nipple. After that, it's all learned." -Bruce Ediger on X interfaces "Nipples are intuitive, my ass!" -Quincy Prescott Hughes
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. To me induction is on the one hand a slightly more general notion, yet on the other sufficiently tractable that it can be axiomatized equationally when suitably expressed, as I'll now describe. In particular there exists a variety embedding induction, meaning one in which an induction principle holds. Whether the additional generality makes induction equal to recursion is another story. The context in which all this arose, namely answers to Al Vilcius' question about coinduction, naturally prompts the question, is there a variety embedding coinduction, to which I'll return at the end. 2. Nature of Induction Suppose, somewhere out there in the universe, a world exists where kicking a nonworking TV set always leaves it in its nonworking state. Then in that world (certainly not ours), it is surely the case that repeated kicking can do no better. The general principle here is that if performing a certain action on a system cannot under any circumstance destroy a certain property of that system, then neither can _repeatedly_ performing that action on that system. I submit that this is the essence of induction, of which mathematical induction is just an instance. This principle may be expressed more logically as PQ |- P ------- (IND) PQ* |- P The premise is that Q preserves P. That is, if first P and then afterwards Q, it follows that P. The conclusion is that Q* preserves P. That is, if first P and then afterwards Q repeatedly, it follows that P. Here we understand Q* as the reflexive transitive closure of Q, in the spirit of Kleene's regular expressions, which we take to denote the performance of Q zero or more times. By itself (IND) serves only to bound Q* from above, which would allow us to satisfy (IND) with Q* = 0 for all Q. We may bound Q* from below by adding that Q* is a closure of Q, namely Q <= Q*, and is transitive --- Q*Q* <= Q* --- and reflexive --- 1 <= Q*. These additional conditions make Q* the least reflexive transitive element greater or equal to Q (proved below), thereby uniquely determining it. 3. Equational Expression of Induction The earliest description to my knowledge of a finitely based variety embedding an induction principle is Tarski and Ng's RAT [1] (1977). (The second is DALG, dynamic algebras, which I described two years later [2] (1979), independently of [1], which I did not learn about until 1989.) The following, based on [3] (1990), generalizes the Boolean setting for RAT to residuated semirings. Others who have worked on finitely based varieties embedding induction include Kozen, Bloom, and Esik, to name just a few. Take as the ambient variety that of semirings with unit. The signature is 2-2-0-0, notated (X, ., +, 0, 1). The equations are: 1. (X,+,0) is a semilattice with unit: + is associative (1), commutative (2), and idempotent (3), with identity 0 (4). 2. (X,.,1) is a monoid: . is associative (5), with identity 1 (6,7). 3. Distributivity: x.(y+z) = x.y + x.y (8) (x+y).z = x.z + y.z (9) (Distributivity could be weakened to monotonicity for our purposes, but since (RR) and (LR) below force it anyway we may as well put it in here to justify calling this a semiring.) We make the following abbreviations. xy for x.y x <= y for x+y = y (inequations are expressible equationally) x |- y for x <= y (i.e. for x+y = y), to look more logical The induction principle IND may then be understood as being about such a semiring expanded with a unary operation *. Thus far the signature has constants 0 and 1, binary operations + and ., and a unary operation *, amounting to Kleene's language of regular expressions. The addition of two further binary operations, suitably axiomatized equationally, permits a purely equational expression of the foregoing. The desired language expansion adds right and left residuation, x\y and x/y (of which just the first suffices for our immediate purposes). PQ <= R iff Q <= P\R (right residuation) (RR) iff P <= R/Q (left residuation) (LR) These axioms, recognizable in this forum of course as making P\ and /P the polarities of a Galois connection or posetal adjunction, serve to define P\Q and Q/P uniquely in terms of the semiring operations. In particular they force P\Q (resp. Q/P) to be the greatest, i.e. weakest, element satisfying P(P\Q) <= Q (resp. (Q/P)P <= Q). If we interpret PQ logically as a noncommutative conjunction P _then_ Q, then P\Q, or P -> Q, may be understood logically as "if previously P, then R". Similarly Q/P, or Q <- P, becomes "Q provided eventually P". One way of looking at this is that we are furnishing the signature with internal conditionals in order to express the external conditionals in (IND), (RR), and (LR) purely equationally. (RR) and (LR) serve not merely to axiomatize residuation but to define it, in the sense that for any given semiring there exists at most one interpretation of right residuation satisfying (RR). Hence (RR) serves (a) to pick out those semirings having exactly one such interpretation, and (b) to enforce that interpretation. Similarly for (LR). The nonequational definition of residuation given by (RR) and (LR) has the following equipollent equational expression (exercise): P\(Q+R) = P\Q + P\R (10) P(P\Q) <= Q <= P\(PQ) (11) (P+Q)/R = P/R + Q/R (12) (Q/P)P <= Q <= (QP)/P (13) (Actually (10) and (12) are overkill, it suffices to state that P\Q and Q/P are monotone in Q, viz. P\Q <= P\(Q+R) and similarly for Q/P. Also left residuation along with (LR), (12), and (13) are redundant for the purposes of the present story.) Three more equations complete the promised variety. 1 + P*P* + P <= P* (14) P* <= (P+Q)* (15) (P\P)* <= P\P (16) (induction, equationally) [1] Equation (14) says that P* is a reflexive transitive element greater or equal to P. Equation (15) merely asserts the monotonicity of *. Equation (16) is the equational expression of induction. It is equivalent to P(P\P)* <= P (16') That is, the repeated action of P\P preserves P. The interest in P\P is first of all that it preserves P, i.e. P(P\P) <= P as an immediate consequence (by (RR)) of P\P <= P\P; and second that it is the weakest (greatest) preserver of P, since if PQ <= P then Q <= P\P (by (RR)). This makes (16') the instance of induction in which the preserver of P happens to be P\P. But since P\P is the _weakest_ preserver of P, we can now obtain the general (nonequational) induction principle, namely from PQ <= P infer PQ* <= P, from this specific equationally expressible instance of it, viz. PQ <= P Q <= P\P by (RR) Q* <= (P\P)* by (15) (monotonicity of *) PQ* <= P(P\P)* by (9) (additivity of P. implies its monotonicity) <= P by (16') That is, the induction principle (IND) holds in the variety axiomatized by (1)-(16). More than this however, the unary operation * is uniquely determined by (14)-(16) by virtue of P* being the least (hence unique) reflexive transitive element of the semiring greater or equal to P. To see this, consider any reflexive transitive X. By transitivity XX <= X so X <= X\X, whence X* <= (X\X)* <= X\X. Hence XX* <= X. Concatenating X* on the right of each side of 1 <= X yields X* <= XX* <= X. Now suppose P <= X. Then P* <= X* <= X, making P* the least reflexive transitive element >= P. The residuals are of course uniquely determined by (10)-(13). So any semiring can be expanded with residuation and star so as to satisfy (10)-(16) in at most one way. That is, those seven equations not only single out those semirings admitting such an expansion but serve to fully define pre- and post-implication as well as reflexive transitive closure, entirely in terms of the given semiring. Given the well-known difficulties of defining the natural numbers using Peano's mathematical induction, or by any other first order means, it is a pleasant change to see an ostensibly intractable operation such as P* pinned down exactly in this way, and even more pleasant that it is all done purely equationally. 4. Back to the question We may now reword the original question in the light of the foregoing. To what variety can one similarly associate suitable operations fully defined equationally so as to include an equationally expressed principal of coinduction? -- Vaughan Pratt [1] @Article( NT77, Author="Ng, K.C. and Tarski, A.", Title="Relation algebras with transitive closure, {A}bstract 742-02-09", Journal="Notices Amer. Math. Soc.", Volume=24, Pages="A29-A30", Year=1977) [2] @InProceedings( Pr79c, Author="Pratt, V.R.", Title="Models of program logics", BookTitle="20th Symposium on foundations of Computer Science", Address="San Juan", Month=Oct, Year=1979) [3] @InProceedings( Pr90b, Author="Pratt, V.R.", Title="Action Logic and Pure Induction", BookTitle="Logics in AI: European Workshop JELIA '90", Series=LNCS, Volume=478, Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120", Address="Amsterdam, NL", Month=Sep, Year=1990)
Hi all, although I cannot say much on coinduction itself, I would like to mention one possible point of view on "universal coalgebra" commented on by Dusko at the end of his message:
PS i have a great appreciation for jan rutten's work on coinduction, but it seems to me that the title of *universal coalgebra* is a bit exaggerated. universal algebra does not dualize. by design, it is meant to be model theory of algebraic theories. what would be the "coalgebraic theories", leading to coalgebras as their models? what would their functorial semantics look like? (implicitly, these questions are already in manes' book.)
and then, moving from coalgebraic theories to comonads, like from algebraic theories to monads, should presumably yield an HSP-like characterization for the categories of (comonad) coalgebras. but coalgebras for a comonad over a topos usually form just another topos.
i may be missing something essential here, but then i do stand to be corrected.
I would say that, although there is no straightforward dualization, there might be a "hidden" one. In my opinion, comonads can sometimes play the role of "strengtheners" or "enrichers" for monads, so that while monads can be viewed as a "substrate for structure", comonads are "substrate for semantics". Rather than trying to give sense to this vague phrase, let me give three illustrations. -1- S. Kobayashi, Monad as modality. Theoret. Comput. Sci. 175 (1997), no. 1, 29--74. The starting point in that paper is the monad semantics by Moggi. It seems that for computer-scientific purposes strength of the monad is too restrictive a requirement, and the author modifies the semantics by assuming strength of the monad *only*with* respect*to*a*comonad*. This means that the monad and comonad distribute in such a way that the monad descends to a strong monad on the category of coalgebras over the comonad. Under the Curry-Howard correspondence this yields an interesting intuitionistic version of the modal system S4. A realizability interpretation is also given. -2- Freyd, Yetter, Lawvere, Kock, Reyes and others have studied "atoms", or infinitesimal objects - objects I in a cartesian closed category with the property that the exponentiation functor I->(_) has a right adjoint. This induces a monad, which cannot be strong in a nontrivial way, just as in the previous example. There is a "largest possible" subcategory over which it is strong, namely the category of I-discrete objects, i.e. those objects X for which the adjunction unit from X to I->X is iso. In good cases the inclusion of this subcategory is comonadic. As Bill pointed out, one might view Cantor's idea of set theory as a case of this: the universe of sets is the largest - necessarily "discrete" - part of "analysis" over which the latter can be "enriched" (well, this is awfully inaccurate, sorry -- consider it as a metaphor). -3- In differential homotopical algebra, there was developed a notion of torsor (principal homogeneous object) which works in a non-cartesian monoidal category. This notion requires not just a (right) action of a monoid M on an object P, but also a "cartesianizer" in form of a left coaction of a comonoid C on P which commutes with the action, and is principal in an appropriate sense. It turns out that the monoid and the comonoid enter in an entirely symmetric way. In the monoidal category of differential graded modules over a commutative ring, principal C-M-objects are classified by s.c. twisting cochains from C to M. Moreover in that category, for a monoid M there is a universal choice of P and C given by the Eilenberg-Mac Lane bar construction, and for a comonoid C there is a universal choice of P and M, given by the Adams' cobar construction. I would be grateful for a reference to a version of these for general monads/comonads. Regards, Mamuka
but wouldn't it be nice to keep the standard definition of induction, which says that the equations
f(0) = c f(n+1) = g(f(n))
determine a unique f, given c and g? this is the definition that most first year
I have always considered the statement regarding existence of a unique
function f to be the principle of recursion.
the recursion schema, as defined by godel in 1930, is a bit stronger: g is allowed to depend on n, not only on f(n).
The principle of induction is, in my mind, the weaker principle that says that if a property holds of 0 and is closed under successor, then it holds of N.
in a topos, this principle is equivalent with the above schema. and the schema itself, of course, just means that [0,s] : 1+N --> N is initial: any algebra [c,g] : 1+X --> X induces a unique homomorphism f : N-->X. using the exponents, we do recursion. as i said last time, induction and recursion have been in heavy use for so long, that they really don't leave much space for redefining, even for the sake of symmetry with coinduction and corecursion. -- dusko
participants (4)
-
Dusko Pavlovic -
jesse＠andrew.cmu.edu -
Mamuka Jibladze -
Vaughan Pratt