Thun/docs/Correcet_Programming.ipynb

Cerrect

Corroct

Correct Programming

Symbolic Logic in the Laws of Form ○ Python Expressions to Represent Forms ○ Reify Forms in an Environment ○ Building Circuits ○ Simplifying Expressions ○ SAT Solver ○ A Model of Computation

Introduction

In 1969 George Spencer-Brown (GSB) published "Laws of Form" which presented a logical system based on a single action, a distinction, that is both an operation and a value. This notebook describes a Python implementation that mimics the Laws of Form notation and uses it to develop a model of computer circuits.

The Laws of Form

See The Markable Mark.

Arithmetic

(()) =
()() = ()

Calculus

A((B)) = AB
A() = ()
A(AB) = A(B)

I call these three laws the Bricken Basis after William Bricken who figured out that the third law is complete with the other two. GSB had the first two laws and "Each Way" as the basis. (TODO: Find and include the references for all this.)

(If anything here is unclear read The Markable Mark. George Burnett-Stuart has done a fantastic job there explaining the Laws of Form.)

Python Sets and Strings as Laws of Form Calculus Expressions

We can use data structures made solely out of Python frozenset and string objects to represent the forms of the Laws of Form notation. I'm going to use the terms "expression" and "form" interchangably in this document.

In [1]:

class Form(frozenset):

    def __str__(self):
        # Because frozenset is immutable, and the contents are all string or frozenset,
        # we can cache the string repr of a form.
        try:
            return self._str
        except AttributeError:
            self._str = '(%s)' % ' '.join(sorted(map(str, self)))
        return self._str

    __repr__ = __str__
    

def F(*terms):
    '''Create a Form from terms.'''
    return Form([
        term if isinstance(term, (basestring, Form)) else F(*term)
        for term in terms
    ])

Define a few variable names.

In [2]:

a, b, c = 'abc'

Some examples of forms.

In [3]:

A = F(a, b, c)
A

Out [3]:

(a b c)

In [4]:

B = F(a, (b, (c,)))
B

Out [4]:

(((c) b) a)

Forms like a b c must be enclosed in a pair of nested containers like so (( a b c )), this lets us treat them as a single (Python) object without inverting the logical value of the form.

In [5]:

C = F((a, b, c))
C

Out [5]:

((a b c))

Duplicate terms in a form are automatically removed by frozenset.

In [6]:

F(a, (b,), a, (b,))

Out [6]:

((b) a)

Order is irrelevant, again due to frozenset.

In [7]:

F(b, a, c) == F(a, b, c)

Out [7]:

True

It's prefectly okay to create forms out of other forms (not just strings.)

In [8]:

F(A, (B, (C,)), a)

Out [8]:

(((((a b c))) (((c) b) a)) (a b c) a)

Mark and Void.

In [9]:

Mark = F()
Mark

Out [9]:

()

There is no way to represent Void directly in a programming language so we have to use the simplest Void-valued form instead.

In [10]:

Void = F(Mark)
Void

Out [10]:

(())

Environments

We can use a Python dict as a context or environment that supplies values (Mark or Void) for the names in a form.

In [11]:

env = dict(a=Mark, b=Mark, c=Mark)

The reify(form, environment) Function

Given forms with string variable names in them we want to be able to substitute values from an environment. If these values are Mark or Void the result will be a pure arithmentic form.

In [12]:

def reify(form, environment):
    if isinstance(form, basestring):
        return environment.get(form, form)
    return Form(reify(inner, environment) for inner in form)

In [13]:

for form in (A, B, C):
    print form, u'⟶', reify(form, env)

(a b c) ⟶ (())
(((c) b) a) ⟶ (((()) ()) ())
((a b c)) ⟶ ((()))

The void(form) Function

Once the forms have been rendered to pure arithmetic we can use the void() function to find the value of each expression.

In [14]:

def void(form):
    return any(not void(i) for i in form)

The void() function returns a Boolean value (Python True or False), for convenience let's write a function that returns the Mark or Void value of a form.

In [15]:

def value_of(form, m=Mark, v=Void):
    return (m, v)[void(form)]

Now we can use the void() function (by way of value_of()) to calculate the base value of each expression structure.

In [16]:

for form in (A, B, C):
    arith = reify(form, env)
    print form, u'⟶', arith, u'⟶', value_of(arith)

(a b c) ⟶ (()) ⟶ (())
(((c) b) a) ⟶ (((()) ()) ()) ⟶ (())
((a b c)) ⟶ ((())) ⟶ ()

All Possible Environments

For n variables there are 2^n possible assignments of the two values of Mark and Void. If we generate environments that each contain one of the possible assignments of names to the base value we can evaluate an expression containing those names and compute its value.

In [17]:

from itertools import product, izip


BASE = Void, Mark


def environments_of_variables(*variables):
    universe = [BASE] * len(variables)
    for values in product(*universe):
        yield dict(izip(variables, values))


envs = list(environments_of_variables(*'abc'))


envs

Out [17]:

[{'a': (()), 'b': (()), 'c': (())},
 {'a': (()), 'b': (()), 'c': ()},
 {'a': (()), 'b': (), 'c': (())},
 {'a': (()), 'b': (), 'c': ()},
 {'a': (), 'b': (()), 'c': (())},
 {'a': (), 'b': (()), 'c': ()},
 {'a': (), 'b': (), 'c': (())},
 {'a': (), 'b': (), 'c': ()}]

This is a bit hard to read, so let's define a helper function to convert an environment to a string format.

In [18]:

def format_env(env, m='()', v='  '):
    return ' '.join((v, m)[not env[k]] for k in sorted(env))

# Note that Mark is an empty frozenset so in a Boolean context in Python it is False,
# likewise Void is a set with one member, so Python considers it True in a Boolean context.
# The `not` in the expression is just to force such a Boolean context, and we compensate
# by putting `v` in the zero-is-False position in the indexed tuple.

Now we can print out the environments in a table. Notice that it looks just like a list of the eight three-bit binary numbers.

In [19]:

print 'i  a  b  c  i in Binary'
for i, env in enumerate(envs):
    print i, format_env(env, v='--'), '%3s' % (bin(i)[2:],)

i  a  b  c  i in Binary
0 -- -- --   0
1 -- -- ()   1
2 -- () --  10
3 -- () ()  11
4 () -- -- 100
5 () -- () 101
6 () () -- 110
7 () () () 111

Reify the Forms with Each Meaning

Let's pick one of the expressions and iterate through the environments showing the result of reifying that expression in that environment.

In [20]:

print B
print '-----------'
for i, env in enumerate(envs):
    e = reify(B, env)
    print i, format_env(env, v='--'), u'⟶', e, u'⟶', value_of(e, m='()', v='')

(((c) b) a)
-----------
0 -- -- -- ⟶ ((((())) (())) (())) ⟶ ()
1 -- -- () ⟶ (((())) (())) ⟶ 
2 -- () -- ⟶ ((((())) ()) (())) ⟶ ()
3 -- () () ⟶ (((()) ()) (())) ⟶ ()
4 () -- -- ⟶ ((((())) (())) ()) ⟶ 
5 () -- () ⟶ (((())) ()) ⟶ 
6 () () -- ⟶ ((((())) ()) ()) ⟶ 
7 () () () ⟶ (((()) ()) ()) ⟶ 

Truth Table

Let's render the above as a Truth Table.

In [21]:

def truth_table_3(expression):
    print expression
    print ' a  b  c | Value'
    print '---------+------'
    for E in envs:
        e = reify(expression, E)
        print format_env(E), '|', value_of(e, m='()', v='')

In [22]:

truth_table_3(B)

(((c) b) a)
 a  b  c | Value
---------+------
         | ()
      () | 
   ()    | ()
   () () | ()
()       | 
()    () | 
() ()    | 
() () () | 

This makes it clear that each expression in Laws of Form calculus is describing a digital Boolean circuit. The names are its inputs and its Void/Mark value is its output. Each boundary is a multi-input NOR gate, known as the Peirce arrow or Quine dagger (See Sheffer stroke and NOR gate.) Instead of two Boolean values there is only one value and non-existance.

Let's build Circuits

In order to work with expressions as digital circuits, let's define some helper functions that will create logic circuits out of simpler forms. The names of the functions below reflect the choice of Mark as Boolean True but this is just a convention.

In [23]:

nor = lambda *bits: F(*bits)
or_ = lambda *bits: F(bits)
and_ = lambda *bits: Form(F(bit) for bit in bits)
nand = lambda *bits: nor(and_(*bits))
nxor = eqiv = lambda a, b: F((a, (b,)), ((a,), b))
xor = lambda a, b: F(nxor(a, b))

# To build logical expressions with Void as Boolean True use these functions.
anti_nor = nand
anti_or = and_
anti_and = or_
anti_nand = nor
anti_eqiv = xor
anti_xor = eqiv

Some examples:

In [24]:

a, b, c = 'abc'


some_expressions = (
    nor(a, b, c),
    or_(a, b, c),
    and_(a, b, c),
    nand(a, b, c),
    xor(a, b),
    eqiv(a, b),
    xor(a, xor(b, c)),
)


for expression in some_expressions:
    print expression

(a b c)
((a b c))
((a) (b) (c))
(((a) (b) (c)))
((((a) b) ((b) a)))
(((a) b) ((b) a))
((((((((b) c) ((c) b)))) a) (((((b) c) ((c) b))) (a))))

And let's rewrite the truth_table_3() function to make it work for any number of variables.

In [25]:

def yield_variables_of(expression):
    '''Yield all string members of an expression.'''
    if isinstance(expression, basestring):
        yield expression
    else:
        for inner in expression:
            for leaf in yield_variables_of(inner):
                yield leaf


def collect_names(expression):
    '''Return a set of the variables mentioned in an expression.'''
    return set(yield_variables_of(expression))


def truth_table(expression):
    '''Print a truth table for an expression.'''
    names = sorted(collect_names(expression))
    header = ' ' + '  '.join(names)
    n = 1 + len(header)
    header += ' | Value'
    print expression
    print header
    print '-' * n + '+------'
    for env in environments_of_variables(*names):
        e = reify(expression, env)
        print format_env(env), '|', ['()', ''][void(e)]

We can use this truth_table() function to examine the expressions we created above.

In [26]:

truth_table(nor(a, b, c))

(a b c)
 a  b  c | Value
---------+------
         | ()
      () | 
   ()    | 
   () () | 
()       | 
()    () | 
() ()    | 
() () () | 

In [27]:

truth_table(or_(a, b, c))

((a b c))
 a  b  c | Value
---------+------
         | 
      () | ()
   ()    | ()
   () () | ()
()       | ()
()    () | ()
() ()    | ()
() () () | ()

In [28]:

truth_table(and_(a, b, c))

((a) (b) (c))
 a  b  c | Value
---------+------
         | 
      () | 
   ()    | 
   () () | 
()       | 
()    () | 
() ()    | 
() () () | ()

In [29]:

truth_table(xor(a, b))

((((a) b) ((b) a)))
 a  b | Value
------+------
      | 
   () | ()
()    | ()
() () | 

In [30]:

truth_table(eqiv(a, b))

(((a) b) ((b) a))
 a  b | Value
------+------
      | ()
   () | 
()    | 
() () | ()

In [31]:

truth_table(xor(a, xor(b, c)))

((((((((b) c) ((c) b)))) a) (((((b) c) ((c) b))) (a))))
 a  b  c | Value
---------+------
         | 
      () | ()
   ()    | ()
   () () | 
()       | ()
()    () | 
() ()    | 
() () () | ()

In [32]:

E1 = and_(
    or_(and_(a, b), and_(b, c), and_(c, a)),  # Any two variables...
    nand(a, b, c)  # ...but not all three.
)
truth_table(E1)

((((((a) (b)) ((a) (c)) ((b) (c))))) ((((a) (b) (c)))))
 a  b  c | Value
---------+------
         | 
      () | 
   ()    | 
   () () | ()
()       | 
()    () | ()
() ()    | ()
() () () | 

This is a brute-force SAT solver that doesn't even bother to stop once it's found a solution.

Expressions from Truth Tables

Sometimes we will have a function for which we know the behavior (truth table) but not an expression and we want the expression. For example, imagine that we didn't just create the expression for this table:

 a  b  c | Value
---------+------
         | 
      () | 
   ()    | 
   () () | ()
()       | 
()    () | ()
() ()    | ()
() () () | 

Each Row can be Represented as an Expression

To write an expression for this table, first we should understand that each row can be represented as an expression.

         ⟶ ( a   b   c )
      () ⟶ ( a   b  (c))
   ()    ⟶ ( a  (b)  c )
   () () ⟶ ( a  (b) (c))
()       ⟶ ((a)  b   c )
()    () ⟶ ((a)  b  (c))
() ()    ⟶ ((a) (b)  c )
() () () ⟶ ((a) (b) (c))

Each of the above expressions will be true (Mark-valued) for only one possible combination of the three input variables. For example, let's look at the sixth expression above:

In [33]:

e6 = F((a,), b, (c,))
truth_table(e6)

((a) (c) b)
 a  b  c | Value
---------+------
         | 
      () | 
   ()    | 
   () () | 
()       | 
()    () | ()
() ()    | 
() () () | 

To make an expression that is Mark-valued for just certain rows of the table, pick those rows' expressions,

   () () | ( a  (b) (c))
()    () | ((a)  b  (c))
() ()    | ((a) (b)  c )

And write them down as terms in an OR expression:

E = (a(b)(c)) ((a)b(c)) ((a)(b)c)

In conventional notation this is called Disjunctive normal form:

E = (¬a ∧ b ∧ c) ∨ (a ∧ ¬b ∧ c) ∨ (a ∧ b ∧ ¬c)

Here it is in action:

In [34]:

e4 = ( a,   (b,),  (c,))
e6 = ((a,),  b,    (c,))
e7 = ((a,), (b,),   c  )

E2 = or_(e4, e6, e7)

truth_table(E2)

((((a) (b) c) ((a) (c) b) ((b) (c) a)))
 a  b  c | Value
---------+------
         | 
      () | 
   ()    | 
   () () | ()
()       | 
()    () | ()
() ()    | ()
() () () | 

Equivalence

Note that the expression E2 above is equivalent to the ealier expression E1 that has the same truth table, in other words:

((((((a) (b)) ((b) (c)) ((c) (a))))) ((((a) (b) (c)))))

equals

(((a (b) (c)) ((a) b (c)) ((a) (b) c)))

We can demonstrate this equivalence by evaluating the expression formed by eqiv() from these two.

For every environment (from the set of possible values for the variables) if both expressions have the same value when evaluated then the eqiv() of those expressions will be Mark-valued (true in our chosen context.)

In [35]:

truth_table(eqiv(E1, E2))

(((((((((a) (b)) ((a) (c)) ((b) (c))))) ((((a) (b) (c)))))) ((((a) (b) c) ((a) (c) b) ((b) (c) a)))) (((((((a) (b)) ((a) (c)) ((b) (c))))) ((((a) (b) (c))))) (((((a) (b) c) ((a) (c) b) ((b) (c) a))))))
 a  b  c | Value
---------+------
         | ()
      () | ()
   ()    | ()
   () () | ()
()       | ()
()    () | ()
() ()    | ()
() () () | ()

The truth table above shows that the equivalence expression is true (Mark-valued by our current convention) for all possible assignments of Mark/Void to the three variables a, b, and c. This indicates that the expression is a tautology.

Half-Bit Adder

If you have two binary digits ("bits") and you are interested in the (binary) sum of these digits you will need two circuits, one for the "ones place" and one for the "twos place" or "carry bit".

Consider:

a b | c s
----+----
0 0 | 0 0
0 1 | 0 1
1 0 | 0 1
1 1 | 1 0

Treating each output column ('c' for carry, 's' for sum) as a single expression, it's easy to see that the carry bit is just AND and the sum bit is just XOR of the two input bits.

In [36]:

a, b = 'ab'


half_bit_adder = {
    'Sum': xor(a, b),
    'Carry': and_(a, b),
}


for name, expr in half_bit_adder.items():
    print name
    truth_table(expr)
    print

Carry
((a) (b))
 a  b | Value
------+------
      | 
   () | 
()    | 
() () | ()

Sum
((((a) b) ((b) a)))
 a  b | Value
------+------
      | 
   () | ()
()    | ()
() () | 

Full-bit Adder

In order to add two multi-bit binary numbers we need adder circuits that are designed to work with three input bits: the two bits to add together and a carry bit from the previous addition:

 a  b Cin   Sum Cout
 0  0  0  |  0  0
 0  0  1  |  1  0
 0  1  0  |  1  0
 0  1  1  |  0  1
 1  0  0  |  1  0
 1  0  1  |  0  1
 1  1  0  |  0  1
 1  1  1  |  1  1

Looking back at our table of three-variable expressions:

         ⟶ ( a   b   c )
      () ⟶ ( a   b  (c))
   ()    ⟶ ( a  (b)  c )
   () () ⟶ ( a  (b) (c))
()       ⟶ ((a)  b   c )
()    () ⟶ ((a)  b  (c))
() ()    ⟶ ((a) (b)  c )
() () () ⟶ ((a) (b) (c))

We can easily determine expressions for sum and carry:

Sum = (a b (c)) (a (b) c) ((a) b c) ((a) (b) (c))

Cout = (a (b) (c)) ((a) b (c)) ((a) (b) c) ((a) (b) (c))

In [37]:

Sum = F(( (a, b, (c,)), (a, (b,), c), ((a,), b, c), ((a,), (b,), (c,)) ),)
Carry = F(( (a, (b,), (c,)), ((a,), b, (c,)), ((a,), (b,),  c), ((a,), (b,), (c,)) ),)

In [38]:

print 'Sum'
truth_table(Sum)
print
print 'Carry'
truth_table(Carry)

Sum
((((a) (b) (c)) ((a) b c) ((b) a c) ((c) a b)))
 a  b  c | Value
---------+------
         | 
      () | ()
   ()    | ()
   () () | 
()       | ()
()    () | 
() ()    | 
() () () | ()

Carry
((((a) (b) (c)) ((a) (b) c) ((a) (c) b) ((b) (c) a)))
 a  b  c | Value
---------+------
         | 
      () | 
   ()    | 
   () () | ()
()       | 
()    () | ()
() ()    | ()
() () () | ()

Let's make a full_bit_adder() function that can define new expressions in terms of variables (or expressions) passed into it.

In [39]:

def full_bit_adder(a, b, c):
    return (
        F(( (a, b, (c,)), (a, (b,), c), ((a,), b, c), ((a,), (b,), (c,)) ),),
        F(( (a, (b,), (c,)), ((a,), b, (c,)), ((a,), (b,),  c), ((a,), (b,), (c,)) ),),
    )

Now we can chain it to make a set of circuits that define together an eight-bit adder circuit with carry.

In [40]:

sum0, cout = full_bit_adder('a0', 'b0', 'Cin')
sum1, cout = full_bit_adder('a1', 'b1', cout)
sum2, cout = full_bit_adder('a2', 'b2', cout)
sum3, cout = full_bit_adder('a3', 'b3', cout)
sum4, cout = full_bit_adder('a4', 'b4', cout)
sum5, cout = full_bit_adder('a5', 'b5', cout)
sum6, cout = full_bit_adder('a6', 'b6', cout)
sum7, cout = full_bit_adder('a7', 'b7', cout)

Unfortunately, the sizes of the resulting expression explode:

In [41]:

map(len, map(str, (sum0, sum1, sum2, sum3, sum4, sum5, sum6, sum7, cout)))

Out [41]:

[63, 327, 1383, 5607, 22503, 90087, 360423, 1441767, 1441773]

Using the definitions for Sum and Carry

We could also use the definitions from the Wikipedia article:

S = A ⊕ B ⊕ C
Cout = (A ⋅ B) + (Cin ⋅ (A ⊕ B))

In [42]:

def full_bit_adder(a, b, c):
    return (
        xor(xor(a, b), c),
        or_(and_(a, b), and_(c, xor(a, b))),
    )

In [43]:

sum0, cout = full_bit_adder('a0', 'b0', 'Cin')

In [44]:

print 'Sum'
truth_table(sum0)
print
print 'Carry'
truth_table(cout) 

Sum
((((((((a0) b0) ((b0) a0)))) Cin) (((((a0) b0) ((b0) a0))) (Cin))))
 Cin  a0  b0 | Value
-------------+------
         | 
      () | ()
   ()    | ()
   () () | 
()       | ()
()    () | 
() ()    | 
() () () | ()

Carry
((((((((a0) b0) ((b0) a0)))) (Cin)) ((a0) (b0))))
 Cin  a0  b0 | Value
-------------+------
         | 
      () | 
   ()    | 
   () () | ()
()       | 
()    () | ()
() ()    | ()
() () () | ()

In [45]:

sum1, cout = full_bit_adder('a1', 'b1', cout)
sum2, cout = full_bit_adder('a2', 'b2', cout)
sum3, cout = full_bit_adder('a3', 'b3', cout)
sum4, cout = full_bit_adder('a4', 'b4', cout)
sum5, cout = full_bit_adder('a5', 'b5', cout)
sum6, cout = full_bit_adder('a6', 'b6', cout)
sum7, cout = full_bit_adder('a7', 'b7', cout)

The sizes of these expression are much more tractable:

In [46]:

map(len, map(str, (sum0, sum1, sum2, sum3, sum4, sum5, sum6, sum7, cout)))

Out [46]:

[67, 159, 251, 343, 435, 527, 619, 711, 371]

Simplifying Expressions

The Form Python datastructure is based on frozenset so duplicate terms are automatically removed and order of terms is irrelevant just as we would prefer. But we want to be able to automatically simplify forms beyond just that. Ideally, we would like a function that applies the rules of the calculus automatically:

A((B)) = AB
A() = ()
A(AB) = A(B)

I'm going to specify the behaviour of the desired function in a unittest.

In [47]:

import unittest

Three Easy Cases

Let's deal with three easy cases first: string, the Mark, and the Void. The simplify() function should just return them unchanged.

In [48]:

class UnwrapTest0(unittest.TestCase):

    def testMark(self):
        self.assertEqual(Mark, simplify(Mark))
  
    def testVoid(self):
        self.assertEqual(Void, simplify(Void))

    def testLeaf(self):
        self.assertEqual('a', simplify('a'))


def simplify(form):
    # Three easy cases, for strings, Mark, or Void, just return it.
    if isinstance(form, basestring) or form in BASE:
        return form


if __name__ == '__main__':
    unittest.main(argv=['ignored', 'UnwrapTest0'], exit=False)

...
----------------------------------------------------------------------
Ran 3 tests in 0.004s

OK

(a)

A single string in a form (a) should also be returned unchanged:

In [49]:

class UnwrapTest1(unittest.TestCase):

    def testNegatedLeaf(self):
        a = nor('a')
        self.assertEqual(a, simplify(a))


def simplify(form):

    # Three easy cases, for strings, Mark, or Void, just return it.
    if isinstance(form, basestring) or form in BASE:
        return form
    
    # We know it's a Form and it's not empty (else it would be the Mark and
    # returned above.)
    
    # Let's just recurse.
    return Form(simplify(inner) for inner in form)


if __name__ == '__main__':
    unittest.main(argv=['ignored', 'UnwrapTest1'], exit=False)

.
----------------------------------------------------------------------
Ran 1 test in 0.001s

OK

Doubly-Wrapped Forms

So far, so good. But what about ((a))? This should be returned as just a. And ((a b)) should remain ((a b)) because we can't represent just a b as a single Python object, so we have to retain the outer pair of containers to hold them without inverting the Mark/Void value (if we just used one container.)

In [50]:

class UnwrapTest2(unittest.TestCase):

    def testUnwrapLeaf(self):
        '''((a)) = a'''
        a = or_('a')
        self.assertEqual('a', simplify(a))

    def testDoNotUnwrapTwoLeaves(self):
        '''((a b)) = ((a b))'''
        a = or_('a', 'b')
        self.assertEqual(a, simplify(a))


def simplify(form):

    # Three easy cases, for strings, Mark, or Void, just return it.
    if isinstance(form, basestring) or form in BASE:
        return form
    
    # We know it's a Form and it's not empty (else it would be the Mark and
    # returned above.)
    
    # Let's just recurse.
    result = Form(simplify(inner) for inner in form)
    
    # Check for ((a)) and return just a.
    # If there is more than one item in the inner container ((a b..))
    # then we must keep the outer containers.
    if len(result) == 1:
        inner, = result  # inner = (a)
        if isinstance(inner, Form) and len(inner) == 1:
            a, = inner
            return a

    return result


if __name__ == '__main__':
    unittest.main(argv=['ignored', 'UnwrapTest2'], exit=False)

..
----------------------------------------------------------------------
Ran 2 tests in 0.002s

OK

Does it work for (((a))) = (a) and ((((a)))) = a and so on?

In [51]:

class UnwrapTest3(unittest.TestCase):

    def testMultiUnwrapLeaf(self):
        A = 'a'
        B = nor(A)
        a = nor(B)
        self.assertEqual(A, simplify(a))
        a = nor(a)
        self.assertEqual(B, simplify(a))
        a = nor(a)
        self.assertEqual(A, simplify(a))
        a = nor(a)
        self.assertEqual(B, simplify(a))
        a = nor(a)
        self.assertEqual(A, simplify(a))
        a = nor(a)
        self.assertEqual(B, simplify(a))

    def testMultiDoNotUnwrapTwoLeaves(self):
        e = F('a', 'b')
        f = a = nor(e)
        self.assertEqual(f, simplify(a))
        a = nor(a)
        self.assertEqual(e, simplify(a))
        a = nor(a)
        self.assertEqual(f, simplify(a))
        a = nor(a)
        self.assertEqual(e, simplify(a))
        a = nor(a)
        self.assertEqual(f, simplify(a))
        a = nor(a)
        self.assertEqual(e, simplify(a))

# Technically, several of the tests above are redundant,
# I'm not willing to figure out the right point ot stop
# right now, so I just do extra tests.

if __name__ == '__main__':
    unittest.main(argv=['ignored', 'UnwrapTest3'], exit=False)

..
----------------------------------------------------------------------
Ran 2 tests in 0.003s

OK

Unwrapping Inner Forms

But now let's trick our function, it can't handle (a ((b c))) = (a b c) yet. This is going to require an auxiliary helper function that is similar to simplify() but that yields terms into an outer context.

In [52]:

class UnwrapTest4(unittest.TestCase):

    def testMultiUnwrapLeaf(self):
        a, b, c = 'abc'
        f = F(a,((b, c),))
        e = F(a, b, c)
        self.assertEqual(e, simplify(f))

    def testMulti_blah_Leaf(self):
        a, b, c = 'abc'
        f = F(a,(((b, c),),),)
        e = F(a, (b, c))
        self.assertEqual(e, simplify(f))

    def testMulti_blah_blah_Leaf(self):
        a, b, c, d = 'abcd'
        f = F(a,((((b, c),), d),))
        e = F(a, b, c, d)
        self.assertEqual(e, simplify(f))


def simplify(form):

    # Three easy cases, for strings, Mark, or Void, just return it.
    if isinstance(form, basestring) or form in BASE:
        return form

    # We know it's a Form and it's not empty (else it would be the Mark and
    # returned above.)
    
    result = []
    for inner in simplify_gen(form):  # Use the generator instead of recursing into simplify().
        result.append(inner)
    result = Form(result)
   
    # Check for ((a)) and return just a.
    # If there is more than one item in the inner container ((a b..))
    # then we must keep the outer containers.
    if len(result) == 1:
        inner, = result  # inner = (a)
        if isinstance(inner, Form):
            if len(inner) == 1:
                a, = inner
                return a
            else:
                # len(inner) cannot be 0, because that means form is Void
                # and would already have been returned.
                assert len(inner) > 1, repr(inner)
                
                # What to do here?
                # We cannot yield the items in inner into the containing context
                # because we don't have it (or even know if it exists.)
                # Therefore we need a different simplify() generator function that yields
                # the simplified contents of a form, and we have to call that instead
                # of recurring on simplify() above.
                pass
                

    return result


def simplify_gen(form):
    
    for inner in form:
        
        inner = simplify(inner)
        # Now inner is simplified, except for ((a b...)) which simplify() can't handle.

        # Three easy cases, strings, Mark, or Void.
        if isinstance(inner, basestring):
            yield inner
            continue

        if inner == Mark:
            yield inner
            assert False  # The simplify() function will not keep iterating after this.
            return  # Partial implementation of ()A = ().
        
        if inner == Void:
            continue  # Omit Void.  Implementation of (()) = .
    
        # We know it's a Form and it's not empty (else it would be the Mark and
        # yielded above.)
    
        # Check for ((...)) and return just ... .
        if len(inner) > 1:  # (foo bar)
            yield inner
            continue

        assert len(inner) == 1, repr(inner)  # Just in case...

        inner_inner, = inner
        if isinstance(inner_inner, Form):  # inner_inner = (...)
            for inner_inner_inner in inner_inner:
                yield inner_inner_inner
            continue

        #else:  # inner_inner = foo ; inner = (foo)
        
        yield inner

        
if __name__ == '__main__':
    unittest.main(argv=['ignored', 'UnwrapTest4'], exit=False)

...
----------------------------------------------------------------------
Ran 3 tests in 0.005s

OK

Marks

If the Mark occurs in a sub-form it should Occlude all sibling sub-forms, rendering its container form Void.

In [53]:

class MarkTest0(unittest.TestCase):

    def testMarkOccludes0(self):
        a, b, c = 'abc'
        f = F(a, (), b, c)
        self.assertEqual(Void, simplify(f))

    def testMarkOccludes1(self):
        a, b, c = 'abc'
        f = F(a, (b, c, ()))
        e = F(a)
        self.assertEqual(e, simplify(f))

    def testMarkOccludes2(self):
        a, b, c = 'abc'
        f = F(a, (b, ((), c)))
        e = F(a, (b,))
        self.assertEqual(e, simplify(f))


def simplify(form):

    # Three easy cases, for strings, Mark, or Void, just return it.
    if isinstance(form, basestring) or form in BASE:
        return form

    # We know it's a Form and it's not empty (else it would be the Mark and
    # returned above.)

    result = []
    for inner in simplify_gen(form):
        if inner == Mark:
            return Void  # Discard any other inner forms, form is Void.
        result.append(inner)
    result = Form(result)

    # Check for ((a)) and return just a.
    # If there is more than one item in the inner container ((a b..))
    # then we must keep the outer containers.
    if len(result) == 1:
        inner, = result  # inner = (a)
        if isinstance(inner, Form):
            if len(inner) == 1:
                a, = inner
                return a                

    return result


if __name__ == '__main__':
    unittest.main(argv=['ignored', 'MarkTest0'], exit=False)

...
----------------------------------------------------------------------
Ran 3 tests in 0.004s

OK

Pervade

So we have (()) = -- and ()A = () what about A(AB) = A(B)?

Warning:

Output truncated. This notebook contains too many cells to display efficiently.