154 views

Skip to first unread message

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

Search

Clear search

Close search

Google apps

Main menu