FOM: organizing; Boolean rings; signature

[Vaughan Pratt]

From: Till Mossakowski <till at Informatik.Uni-Bremen.DE>
>Sometimes, this abstractness [of Lawvere theories] is desirable, because
>almost all interesting properties can be formulated at the abstract
>level, and the concrete level of signatures makes distinctions that are
>not relevant.  But often you still need traditional algebraic signatures.
>Namely, if you want to give some *presentation*, do proofs with that
>presentation, or want to do an implementation.

That need is met with a finite basis.  It is not necessary to divorce
signature from theory in order to define "finite basis" and use the
notion for the purpose of presentation.  In fact doing so can hamper
efficiency in representation, as I will explain at the end.

The question under debate is whether "signature" should be understood
as a self-contained notion or in partnership with an equational theory.
The traditional understanding is the former, and it had not occurred to
me to question this before this debate.

What I came to realize while discussing the matter offline with Steve
Simpson is that with the theory-independent notion of signature there
can be no canonical signature other than in the Reuben Hersh sense of
mathematics as a social activity: everyone agrees to settle on some
arbitrarily chosen signature and take that as the definition of Boolean
algebra.  This leaves all other signatures competing for that honor out
in the cold, which I for one find disturbing.

>For example, in circuit theory, you can choose different sets of basic
>circuits, corresponding to different signatures, but all being
>functionally complete wrt. Boolean algebra, i.e. inducing the
>same Lawvere theory.

Circuit engineers do not divorce AND and OR gates from their semantics
the way the notion of signature does.

In some areas of hardware design binary operations are presented not
as uninterpreted symbols but as nybbles (4-bit quantities) explicitly
representing their truth table.  This is done for example in the 74181
Arithmetic-Logic Unit, and also in the PDP-10/20 instruction set.
This presentation is the binary case of the representation of Boolean
operations as finitary operations on {0,1}, a slick way of describing
the Lawvere theory of Boolean algebras that I have mentioned in a couple
of previous messages.

In some situations one wants the ternary case, e.g. with monochrome
framebuffers where one wants the new pixel of the destination to be an
arbitrary Boolean combination of three pixels: source, old destination,
and mask.  Early Sun framebuffers, and also Pixrect, Sun's object-oriented
framebuffer driver which I implemented in 1983, provided this capability,
with ternary operations being represented with 8 bits.

But of course human programmers can't reasonably be expected to work
with such an extremely abstract representation, finding expressions
like (DST&~SRC)&MSK more readable.  Fortunately algebra comes to the
rescue here.  By defining

#define DST	0xaa
#define SRC	0xcc
#define MSK	0xf0

one has in effect represented the generators of the free Boolean algebra
on three generators, whose 256 elements denote the 256 Boolean operations.
The C expression (SRC&MSK)^DST then evaluates to 0x6a, the 8-bit
representation of the Boolean operation which ands the source and mask
pixels and then XOR's (^ is XOR in C) the result with the destination.
These three C #define's can be understood as the link between the
traditional term-based view of Boolean operations, natural for humans,
and the more abstract view of them natural for computers.

The fact that such an abstract presentation is preferred over the
traditional term-based approach in some areas of hardware and software
demonstrates that the term-based approach is not essential for effective
presentations.

In fact abstractness helps, permitting more efficient presentations.
You only need 4 bits to represent all sixteen binary Boolean operations,
and 8 for the ternary ones, the information-theoretic minimum.  With the
less abstract approach of building up formulas from the "canonical"
Boolean signature AND/OR/NOT, the existence of multiple representations
of binary operations like IMP (as either NOT A OR B, or NOT(A AND NOT
B), etc.) and EQV guarantees that the information-theoretically minimal
presentation cannot be achieved with the traditional signature-based
presentation of Boolean operations.

Bottom line: When optimizing the representation of Boolean terms, it
helps to keep the theory in mind.  These optimizations are not available
for terms considered in isolation from their associated theory.

Vaughan Pratt