Vaughan Pratt wrote:
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?
In the same way an induction principle is expressible by means of a least fixed point, one could expect coinductive principles to be expressible by means of greatest fixed points. The following example will clarify what I have in mind. Let G,H two graphs, then we can construct the graph G*H, where (G*H)_0 = G_0 x H_0 and (G*H)_1 = (G_1 x H_0) + (G_0 x H_1) . Every transition of G*H is labeled: it is either a left transition or a right transition. We obtain in this way two modal operators on the subsets of G_0 x H_0, call them <l> and <r>. A bisimulation is a subset B of G_0 x H_0 such that B <= [r]<l>B and B <= [l]<r> , where the [] are the duals of <>. If G = H, then saying that G has no proper quotient amounts to saying that the greatest bisimulation is equal to the diagonal D. Therefore a principle of coinduction can be expressed as follows: \nu_z.([r]<l>z \wedge [l]<r>z) = D where \nu_z.f(z) is the greatest fixed point of f(z). The example can be generalized. The following question arises: is the greatest postfixed point definable equationally? The answer is yes, at least in several cases, as it is the least prefixed point. Consider a theory which contains the signature <0,+,.,\>. <0,+> satisfy the semilattice axioms and, with respect to induced order, a.x is left adjoint to a\x, for a fixed a. Let f(z) be any term of the theory, then the following holds: g(x) is the parameterized least prefixed point of f(z).x if and only if the equations f(g(x)).x = g(x) g(x) <= g(x+y) g(f(x)\x) <= x hold. It is an easy exercise to check this is true, using the fact that f(x).(f(x)\x) <= x . If . has a right unit 1, then g(1) is the least prefixed point of f(z). Similar results hold for the greatest postfixed point if we can find an operation . with a parameterized right adjoint. Algebraic models of the propositional $\mu$-calculus form a variety, as the models of PDL do, and hopefully coinductive principles can be expressed. One could also define something like a $\mu$-linear logic, its models would form a variety. Best regards, Luigi -- Luigi Santocanale, BRICS Department of Computer Science Telephone: +45 8942 3288 University of Aarhus Telefax: +45 8942 3255 Ny Munkegade, building 540 http://www.brics.dk/~luigis/ DK - 8000 Ã rhus C, Denmark. mailto:luigis@brics.dk