FOM: organizing; Boolean rings; signature
Vaughan Pratt
pratt at cs.Stanford.EDU
Fri Mar 20 14:39:32 EST 1998
From: Till Mossakowski <till at Informatik.Uni-Bremen.DE>
>Lawvere theories and monads are indeed more complex than standard signatures.
Certainly anyone who's worked with standard signatures long enough finds
them not at all complex ("what else could you possibly use instead?").
But those who've worked with Lawvere theories for a comparable length of
time are likely to disagree with you, even if they've spent the same
amount of time with signatures.
Merely saying that something is a category seems automatically to make
it seem a more complex notion, regardless of whether it actually is
complex or not.
So let me fling categories out the window and describe Lawvere theories
in ordinary set theoretic language.
A Lawvere theory T consists of terms and equations, both defined on
an arbitrary graph G (strictly speaking a multigraph, one that permits
multiple edges between two vertices, in the manner of e.g. automata).
The terms of T are defined to be the paths in G. The equations take
the form of an arbitrary congruence on those paths with respect to path
concatenation.
That's *all* a Lawvere theory is. There is nothing else. The notion
is delightfully simple.
All this is just as for the ordinary signature-based approach, except
that (i) we have defined terms as paths in a graph instead of as
expressions. and (ii) in place of the usual definition of "signature" as
"family of arities" and the explanation of how terms are built up from
signatures, we instead simply rely on the reader's intuition about how
paths in a graph work. (They form a partial monoid under concatenation,
but it would never occur to a non-logician computer scientist to define
"path in a graph" that formally, the notion is too obvious.)
In an earlier message on Lawvere theories I gave three examples of this
nonalgebraic kind, namely simplicial sets, cubical sets and locomotives
("rolling stock").
An *algebraic* Lawvere theory is more complicated, as befits algebra.
It has the additional constraints that (i) the vertices of the graph
are the natural numbers, and (ii) for each vertex n there is a family
<p_1,p_2,...,p_n> of n edges from vertex n to vertex 1, called the
*projections* of n. The projections collectively have the properties
that (a) for any vertex m and family <q_1,q_2,...,q_n> of n edges from
vertex m to vertex 1, there is at least one edge e from m to n such that
the path ep_i from m to 1 is congruent to q_i, and (b) all edges e from
m to n satisfying (a) are congruent.
In the same earlier message, I gave three examples of algebraic Lawvere
theories, namely empty signature, Boolean algebras, and commutative
rings with unit.
Speaking as someone comfortable with graph theory, I don't find the
concept of a congruence (with respect to path concatenation) on the paths
of a graph to be terribly complicated. However I am starting to form
the impression from this discussion that what is pretty simple to some
people is complicated to other people, and even "incredibly complicated"
to some.
Paradoxically this is correlated with their ability to draw important
distinctions that I can't. :)
Vaughan Pratt
More information about the FOM
mailing list