FOM: organizing; Boolean rings; signature

[Till Mossakowski]

Vaughan Pratt wrote:
>My proposal to Steve for achieving basis independence was simply not
>to permit signatures to exist in isolation from theories.  With this
>approach it becomes possible to have signatures some operations of
>which are e.g. composites of others.  This is possible because such
>relationships can be encoded in the associated theory.  The point that
>Steve had drawn my attention to is that in the absence of any theory
>at all, the situation when considering a signature in isolation, all
>symbols must be independent (unless one introduces some other structure
>on signatures to encode such composition relationships, but this is
>pointless when the theory itself can do this job).
>
>When Steve challenged me as to whether this anti-isolation principle
>for signatures had been worked out I said that I hadn't wanted to say so
>because he wouldn't like it, but that this exactly described both Lawvere
>algebraic theories and monads, both of which characterize varieties,
>neither in a way that has a notion of signature independent of theory.
>
>Naturally Steve views Lawvere theories, monads, and all other "categorical
>dys-foundations" as "incredibly complex."  This should come as no suprise
>to anyone who's read Steve's correspondence with Colin McLarty.  Steve is
>convinced category theory will join communism in hell.

Lawvere theories and monads are indeed more complex than standard
signatures. Rather than replacing standard signatures, they
should accompany them. Cf. the "signed theories" (i.e. Lawvere theories
with some signature included) by Goguen and Burstall.*

Till Mossakowski

*J. A. Goguen and R. M. Burstall,
Some Fundamentals Algebraic Tools for the Semantics of Computation.
Part 2: Signed and Abstract Theories, Theoretical Computer Science 31,
263--295, 1984