Inverse Semigroups, Categories & Laws of Form 2

154 views
Skip to first unread message

Mark Hopkins

unread,
Jul 17, 1996, 3:00:00 AM7/17/96
to

>From ha...@umnstat.stat.umn.edu (Michael Hardy):
> Has anyone written a _readable_ account of the mathematics in
>that book? (I imagine it would be much shorter than Spencer-Brown's
>book.)

Since you asked, I will start the promised followup article with a short
summary of Spencer-Brown's Laws of Form.

Three systems are defined in the book. The first serves, essentially,
as a proof theory for the trivial boolean algebra { 0, 1 } and is given by
the set of reduction rules:

n: ()() -> () o: (()) -> 1

where 1 denotes the empty space. Terms in the underlying language are
(as mentioned in the previous article) built out of sequences of properly
nested brackets. In the Laws of Form book, you'll see nested circles used
instead, or an upside down L used to bracket terms (called the "cross" as
in 'crossing a boundary'). The notation I use above is essentially an
ASCII rendering of this and is (almost) equivalent.

The second serves as a proof theory for boolean algebras in general. Terms
this time can be constructed out of brackets and symbols (the variables),
again, as long as the brackets properly nest. The following reductions are
explicitly postulated:

p: ((p)p) -> 1 t: ((pr)(qr)) -> ((p)(q)) r

The underlying language, being two-dimensional, also has the commutativity
rule in it implicitly: c: ab -> ba.

This system is complete with respect to the Boolean algebra under the
interpretation:

1 <--> true ab <--> a and b (a) <--> not a

(Spencer Brown gives the dual interpretation with 1 = false, ab = a or b).

In a more conventional notation an equational axiomitization can be
written based on the reduction rules above:

(ab)c = a(bc), a1 = a, ab = ba, (a'a)' = 1
((ac)'(bc)')' = (a'b')'c

This yields an equational algebra equivalent to a Boolean Algebra.

The third system is not formally axiomatized -- and cannot be. Terms
in this language are allowed to be infinite, such that their underlying
parse trees are rational. A rational tree is a (possibly infinite) tree
which consists of a finite number of distinct subtrees (up to isomorphism).
Note: this portion of the book (along with the rest of it) was written
nearly a decade before anyone was considering such infinite structures in
the Computer Science literature.

A rational tree can be compactly represented by a finite graph. Therefore
a graphical notation is developed in the last part of the book.

The rational terms are restricted to those whose underlying structure can
be represented by a finite system of structural equations:

qi = (v1 v2 ... v_{ni}), i = 1, ..., m
v's in Q union X
q's in Q union Y
Example:
q = ((((....)))) is denoted by a single structural equation
q = (q)
or equivalently by a pair of structural equations
q = (r), r = (q).

Each node in the graph therefore corresponds to an equation of the form
q = (v v ... v), and thus represents a NAND gate (or NOR gate).

Since there is no finite axiomitization, a purely semantic approach is
adopted in which terms are interpreted as boolean functions of time (i.e.
waveforms). No consistent formal account is given in the book, but it
is easy to provide one, e.g.:

For each q in Q with equation q = (v1 v2 ... v_{ni}):
q(0) = 1
q(t+1) = ( v1(t) v2(t) ... v_{ni}(t) )
For each y in Y with similar equation:
y(t) = ( v1(t) v2(t) ... v_{ni}(t) )

This specifies a pair of transition functions delta: X x Q -> Q and
action: X x Q -> Y, and a constant Q_0 in Q.

In other words, we have a formalization of boolean Finite State machines,
i.e., digital circuits.

Though there is no finite equational axiom system which completely
captures the algebra of Boolean finite state machines, there should be a
finite implicational axiom system analogous to that for the algebra of
finite state automata. An example of the latter is given below:

a(bc) = (ab)c, a1 = a = 1a, a0d = 0, a(b+c)d = abd+acd
a+(b+c) = (a+b)+c, a+0 = a, a+b = b+a, a+a = a
a* = 1 + a a*
if a + bx + xc + x = x then b* a c* + x = x

where finite state automata are represented by regular expressions. The
algebra R(X), freely generated from X, is one and the same as the algebra of
regular expressions over X, and the algebra R(X, Y) generated from X union Y
subject to the relations (xy = yx, x in X, y in Y) is the algebra of
rational transductions (which characterise finite state machines).
A similar algebraic formulation for *boolean* finite state machines
should be possible.

And now on the the second and third examples of "Transformation Categories"
Suprisingly, as it turns out (something I didn't fully realise until now),
these are NOT Transformation Categories and (thus) cannot be extended to
inverse semigroups. The one property that fails is that the objects will
only form a partial ordering, but not a lower semilattice. The reason
for this is that two terms will not generally have a single most general
unifier, but rather a finite number of maximal unifiers. This is
characteristic of the Spencer-Brown notation where the underlying language
has non-trivial algebraic properties built into it. For example, the
two terms
((A)(B)) C ((D)D) E

will have the following as maximal unifiers:

(1) (((B))(B))E with A -> (B), C -> E, D -> (B)
(2) ((A)(A))E with B -> (A), C -> E, D -> (A)
(3) ((A)(B))((D)D) with C -> ((D)D), E -> ((A)(B))

(if we allow for the commutativity rule, see below).

With these provisos, the following examples are presented.

EXAMPLE 2: LOF 2. In this system, the underlying language consists of all
sequences from the set X union { "(", ")" } (where we're assuming
that neither "(" nor ")" is in X), such that brackets are properly
nested.
Let LOF(X) denote this language. Corresponding to any map f: X -> LOF(X),
there is an extension f: LOF(X) -> LOF(X) uniquely defined by the following:

[ab]f = [a]f [b]f [1]f = 1 [(a)]f = ([a]f)
[x]f = f(x)

Such maps will be called substitutions. A preordering on LOF(X) may be
given based on this. We write:

T <= U if [U]f = T for some substitution f

In the following, we'll refer to this as a partial ordering by identifying
a term T with its equivalence class [T] = { U: T <= U and U <= T }. Each
element x in X is maximal in this ordering, with [x] = [x'] for all x, x'
in X. Equivalent terms, in general, are those which differ by a change of
variables.

The morphisms of LOF 2 are those generated by the following rules:

(1) For all non-zero terms A, B and C:
r[A]: ((A)A) -> A
t[A,B,C]: ((AC)(BC)) -> ((A)(B))C
c[A,B]: AB -> BA
(2) 1[A]: A -> A, for each object A
(3) If f: A -> B, g: B -> C then fg: A -> C (again note the convention
whereby we denote compositions in reverse order).
(4) If f: A -> B then f': B -> A
(5) If f: A -> B then ~f: (A) -> (B)
(6) If f: A -> B and g: C -> D then f x g: AC -> BD

subject to the following identities (the same as for LOF 1):

If f: A -> B then 1[A] f = f = f 1[B], f f' = 1[A], f' f = 1[B]
(fg)h = f(gh)
(f x g)(h x k) = fh x gk, ~(fg) = ~f ~g, 1[A] x 1[B] = 1[AB]
(f x g)' = f' x g', (~f)' = ~(f'), ~1[A] = 1[(A)]

from which we can also derive the identities:

f'' = f, (fg)' = g' f', 1[A]' = 1[A].

A partial ordering generated by the following is then imposed on the
morphisms:
g[A1,...,An] <= g[B1,...,Bn] if A1 <= B1, ..., An <= Bn

where g[T1,...,Tn] is any morphism built up from the ones listed above
depending on terms T1, ..., Tn. For example:

If A <= B, C <= D, E <= F
then 1[A] x c[C, E] <= 1[B] x c[D, F]

EXAMPLE 3: LOF 3. This is defined in the same way, except that item (1)
is replaced by the following:
(1) For all non-zero terms A and B:
c[A,B]: AB -> BA
m[A,B]: (AB)(B) -> (B)
n[A]: AA -> A
o[A]: ((A)) -> A
p[A]: (A)A -> ()

Both of these systems may be shown to satisfy all of the defining
properties of a Transformation Category, except for the absence of a lower
semilattice structure. In general, two terms T and U will have more than
one maximal unifier. Nevertheless, we can still write down a partial
product wherever unique unifiers exist:

EXAMPLE: n[A] p[B] >= f[C]: (C)C(C)C -> (), which is obtained by
unifying A with (B)B via the substitutions: s: A |-> (C)C and
t: B |-> C. Thus:

[n[A]]s = n[(C)C]: (C)C(C)C -> (C)C
[p[B]]t = p[C]: (C)C -> ()
and
[n[A]]s [p[B]]t: (C)C(C)C -> ()

f[C] is maximal, therefore we can write f[C] = n[A] p[B].

(This particular derivation, by the way, follows very closely the explanation
given in Spencer-Brown on how the axioms of the system are to be applied).

In the following, we will make a simplifying assumption which will
remove the need for the commutativity rule. Let B(X) denote the family
of formal sums over X. Each element of B(X) can be represented as a
map f: X -> { 0, 1, 2, ... } such that { x in X: f(x) > 0 } = supp(f) is
finite, with:
f <--> f(x1) x1 + f(x2) x2 + ... + f(xn) xn
where supp(f) = { x1, x2, ..., xn }

We define f+g as the function which maps x to f(x) + g(x), and 0 as the
zero function. This, for example:

(2x + 3y) + (4x + z) = (2+4)x + 3y + z = 6x + 3y + z

as one would expect.
Define J(X) as follows:

J_0(X) = B(X)
J_{n+1}(X) = B(X union J_n(X))
J(X) = union n>=0: J_n(X).

The let J(X) is the least solution to the set equation

J = B(X union J).

J(X) is a partial realisation of LOF 2 and LOF 3 with the following
correspondences:

x <--> 1x, for each x in X
(A) <--> 1A, for each A in J(X)
A B <--> A + B, for A, B in J(X)
1 <--> 0

With this convention, we can identify c[A, B] = 1[AB], since AB = BA.
This establishes a closer connection to Spencer-Brown's original treatment
which freely uses the identity AB = BA in virtue of the two-dimensionality
of its notation.

Also, with the ordering structure imposed on morphisms, there is not
much loss of generality in writing down morphisms with the parameters
left unspecified. There will be a degree of non-determinism in the sense
that a given combination will be resolveable in more than one way in
general. For instance, we can define s = r x 1. This can only be
resolved in one way:
r[A]: ((A)A) -> 1 1[B]: B -> B
therefore
s[A,B] = r[A] x 1[B]: ((A)A) B -> B

But if we define u = t s, then we can resolve u in several distinct ways:

t[A,B,C]: ((AC)(BC)) -> ((A)(B))C
s[D,E]: ((D)D) E -> E

u1[B,E]: (((B)E)(BE)) -> E with A=D=(B), C=E
u2[A,E]: ((AE)((A)E)) -> E with B=D=(A), C=E
u3[A,B,D]: ((A((D)D))(B((D)D))) -> ((A)(B))
with C = ((D)D), E = ((A)(B))

For reference below, let u[B,E] = u1[B,E] = t[(B),B,E] s[(B),E]. Then

u[B,E]: (((B)E) (BE)) -> E

THEOREM 1: LOF 3 is deriveable from LOF 2.
Proof:
The following derivation for o[A] can be established in LOF 2. Define
s[A, B] = r[A] x 1[B] and u[A, B] = s[(A), B] t[(A), A, B] as above. Then

s[A, B]: B -> ((A)A) B
u[A, B]: B -> (((A)B) (AB))

We can resolve v = u ~s' in several ways, which will allow us to define
the morphisms of LOF 3 in terms of those of LOF 2:

u[A, B]: B -> (((A)B) (AB))
~s[C, D]': (((C)C) D) -> (D)

The terms
(((A)B) (AB)) and (((C)C) D)

unify in several distinct ways:

(1) (((B)B) (BB)) with A = C = B, and D = (BB)
(2) (((A)((A))) (A((A)))) with C = (A), B = ((A)), D = (A((A)))
(3) ((((C))C) ((C)C)) with A = (C), B = C, D = (((C))C)
(4) (((C)(C)) (C(C))) with A = C, B = (C), D = ((C)(C))

thus yielding the following resolutions for v:

v1[B]: B -> ((BB)) v1[B] = u[B,B] ~s[B,(BB)]'
v2[A]: ((A)) -> ((A((A)))) v2[A] = u[A,((A))] ~s[(A), (A((A)))]'
v3[C]: C -> ((((C))C)) v3[C] = u[(C),C] ~s[C, (((C))C)]'
v4[C]: (C) -> (((C)(C))) v4[C] = u[C,(C)] ~s[C, ((C)(C))]'

Thus, we may define:

o[A] = v2[A] v3[A]': ((A)) -> A
and n[A] = o[AA]' v1[A]': AA -> A

From this, we easily obtain a definition for p:

p[A] = o[(A)A]' ~r[A]: (A)A -> ()
and
l[A] = (p[A] x 1[A])' (1[(A)] x n[A]) p[A]: ()A -> ()
Thus
m1[A,B] = t[A,1,B] (~p[(A)] o[1] x 1[B]): ((AB)(B)) -> B
and
m[A, B] = o[(AB)(B)]' ~m1[A, B]: (AB)(B) -> (B)

gives us our desired definition for m.

DEFINITION: Define Q(X) as the term language generated by the following:
1 is in Q(X), X is a subset of Q(X)
If a and b are in Q(X), then so are a' and ab.
Let BOOL be the axioms for a boolean lattice, and ORTHO the
axioms for an ortho lattice. We may conveniently thoose the
following systems:
ORTHO: a1 = a, ab = ba, (ab)c = a(bc), aa = a
a a' = 0, a'' = a, if a b = a then b'a' = b'
BOOL: All the ORTHO axioms, plus: a(b v c) = ab v ac
where
0 = 1', b v c = (b'c')'

Without loss of generality, we can replace the axiom (ab = a -> b'a' = b')
by the equational axiom ((ab)' b' = b'), thus yielding a purely equational
axiomitization of both BOOL and ORTHO.

THEOREM 2: Completeness
Define T: LOF(X) -> Q(X) by the following:
T[1] = 1, T[x] = x for all x in X
T[ab] = T[a] T[b], T[(a)] = T[a]'
Then
(a) T is a one-one correspondence between LOF(X) and Q(X).
(b) f: A -> B in LOF 3 <==> ORTHO |= T[A] = T[B]
(c) f: A -> B in LOF 2 <==> BOOL |= T[A] = T[B]

All the proofs are elementary, since I purposely designed the axiom systems
for BOOL and ORTHO to match those of LOF 2 and LOF 3. For LOF 2, we only
need to establish the additional property

f: T^{-1}[a(b v c)] -> T^{-1}[ab v ac]
i.e.,
f: a((b)(c)) -> ((ab)(ac))

which is realised by f = t[b,c,a]'.

COROLLARY: The following provides an equivalent axiomitization for BOOL:
LOF Axioms: a(bc) = (ab)c, a1 = a, ab = ba,
Axiom R: (a'a)' = 1,
Axiom T: ((ac)'(bc)')' = (a'b')'c

Another form of completeness is proven in Spencer-Brown, as specified by
the following theorem:

THEOREM 3: System LOF 2 is Equationally Complete with respect to LOF 1.

This can be broken down into two parts:

LEMMA 1: The morphisms n: ()() -> () and o: (()) -> 1 are defineable in LOF 2
Proof:
Tane n = n[()] and o = o[1].

LEMMA 2: If e(v) and f(v) are terms involving a variable v, with morphisms:
A0: e(()) -> f(())
A1: e(1) -> f(1)
then there is a morphism
A[v]: e(v) -> f(v)

To prove LEMMA 2, we'd need to use some kind of normal form property, e.g.

LEMMA 3: For any term e(v), there is a morphism
<e>[v]: e(v) -> ((v) e0) (v e1)
such that e0 and e1 contain no occurrences of variable v.
Proof outline:
This consists of defining the following morphisms:
c1: v -> ((v) 1) (v ())
c2: A -> ((v) (A)) (v (A)), where A has no occurrences of v
c3: ( ((v)A) (vB) ) -> ((v)(A)) (v(B))
c4: ((v)A) (vB) ((v)C) (vD) -> ((v)((A)(C))) (v ((B)(D)))

and using them as needed to build up a normal form for a term e(v).

Proof outline of LEMMA 2:
Assuming we have a normal form morphism:

<e>[v]: e(v) -> ((v) e0) (v e1)
then
<e>[1]: e(1) -> (() e0) (e1)
<e>[()]: e(()) -> ((()) e0) (() e1)

Therefore
e_1 = <e>[1] ( ~l[e0] x 1[(e1)] ): e(1) -> (e1)
e_0 = <e>[()] ( ~(o[1] x 1[e0]) x (~l[e1] o[1])): e(0) -> (e0)

with f_1: f(1) -> (f1) and f_0: f(()) -> (f0) defined similarly. We can
then build up the following definitions:

a_0 = o[e0]' ~(e_0' A_0 f_0) o[f0]: e0 -> f0
a_1 = o[e1]' ~(e_1' A_1 f_1) p[f1]: e1 -> f1
and
<e>[v] ( ~(1[(v)] x a_0) x ~(1[v] x a_1) ) <f>[v]': e(v) -> f(v)

CONJECTURE: There exists an extension of the axioms for LOF 3 (LOF 2)
such that:
(a) A canonical form morphism <T>: T -> NF(T) be
defineable
(b) f: T -> U <==> NF(T) = NF(U)
(c) f: T -> U => f = <T> <U>'

We proved this property for LOF 1. To extend the result to LOF 2 and LOF 3
would involve formalising an algorithm for deriving normal forms, probably
along the lines illustrated in LEMMA 3.


Reply all
Reply to author
Forward
0 new messages