diff --git a/docs/0._This_Implementation_of_Joy_in_Python.html b/docs/0._This_Implementation_of_Joy_in_Python.html index 0a4a6eb..67706aa 100644 --- a/docs/0._This_Implementation_of_Joy_in_Python.html +++ b/docs/0._This_Implementation_of_Joy_in_Python.html @@ -1,9 +1,14 @@ -0._This_Implementation_of_Joy_in_Python + +0._This_Implementation_of_Joy_in_Python + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-
- -
-
-
-
-

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)?

- -
-
-
-
-
-
In [54]:
-
-
-
class PervadeTest0(unittest.TestCase):
-
-    def testPervade0(self):
-        a = 'a'
-        f = F(a, (a,))
-        self.assertEqual(Void, simplify(f))
-
-    def testPervade1(self):
-        a = 'a'
-        f = F(((a,),), (a,))
-        self.assertEqual(Void, simplify(f))
-        
-    def testPervade2(self):
-        a = 'a'
-        b = 'b'
-        f = F(a, (b, (a,)))
-        e = F(a)
-        self.assertEqual(e, simplify(f))
-
-
-def simplify(form, exclude=None):
-
-    # 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.)
-
-    if exclude is None:
-        exclude = set()
-
-    new_stuff = form - exclude 
-    exclude = exclude | new_stuff
-
-    result = []
-    for inner in simplify_gen(new_stuff, exclude):
-        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
-
-
-def simplify_gen(form, exclude):
-    
-    for inner in form:
-        
-        inner = simplify(inner, exclude)
-        # 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', 'PervadeTest0'], exit=False)
-
- -
-
-
- -
-
- - -
- -
- - -
-
...
-----------------------------------------------------------------------
-Ran 3 tests in 0.004s
-
-OK
-
-
-
- -
-
- -
-
-
-
-
-

TODO set up Hypothesis to generate test cases...

- -
-
-
-
-
-
In [55]:
-
-
-
# Run ALL the tests!
-
-if __name__ == '__main__':
-    unittest.main(argv=['ignored'], exit=False)
-
- -
-
-
- -
-
- - -
- -
- - -
-
.................
-----------------------------------------------------------------------
-Ran 17 tests in 0.022s
-
-OK
-
-
-
- -
-
- -
-
-
-
-
-

Using "Each-Way" to Simplify Forms

GSB called this "Each-Way":

- -
a = ((a b) (a (b)))
- -
-
-
-
-
-
In [56]:
-
-
-
truth_table(F((a, b), (a, (b,))))
-
- -
-
-
- -
-
- - -
- -
- - -
-
(((b) a) (a b))
- a  b | Value
-------+------
-      | 
-   () | 
-()    | ()
-() () | ()
-
-
-
- -
-
- -
-
-
-
-
-

The form says, "if b then a else a". I'll come back to the interpretation of "Each-Way" as an if-then-else statement later.

-

The thing to note here is that the value for a can be a whole expression which appears twice in the new form: once next to b and once next to (b).

-

In the first case we can remove any occurances of b from the a next to it

- -
b (...(b c (d ...)))
-b (...(  c (d ...)))
-
-
-

and in the second case we can change any occurances of b to the Mark.

- -
(b)(...(b     c (d ...)))
-(b)((b)(b     c (d ...)))
-(b)(...(b (b) c (d ...)))
-(b)(...(b ( ) c (d ...)))
-(b)(...(  ( )          ))
-(b)(...                 )
-
-
-

We can send (b) into the form until it reaches and b, at which point b(b) becomes () and sweeps out any siblings rendering its containing form Void.

-

For the first case we can use simplify() and pass in b as a member of the exclude set.

- -
-
-
-
-
-
In [57]:
-
-
-
A = F(a, (b, (c,)))
-A
-
- -
-
-
- -
-
- - -
- -
Out[57]:
- - - - -
-
(((c) b) a)
-
- -
- -
-
- -
-
-
-
In [58]:
-
-
-
simplify(A, {b})
-
- -
-
-
- -
-
- - -
- -
Out[58]:
- - - - -
-
(a c)
-
- -
- -
-
- -
-
-
-
-
-

with_mark

In the second case (b)...b... = (b)...()... we can modify the simplify() function to accept a name that it should treat as Mark-valued.

- -
-
-
-
-
-
In [59]:
-
-
-
class MarkitTest0(unittest.TestCase):
-
-    def testMarkit0(self):
-        a, b, c = 'abc'
-        f = F(a, (b, (c,)))
-        e = F(a)
-        self.assertEqual(e, simplify(f, with_mark=b))
-
-
-def simplify(form, exclude=None, with_mark=None):
-
-    # 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.)
-
-    if exclude is None:
-        exclude = set()
-
-    new_stuff = form - exclude 
-    exclude = exclude | new_stuff
-
-    result = []
-    for inner in simplify_gen(new_stuff, exclude, with_mark):
-        if inner == Mark or inner == with_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
-
-
-def simplify_gen(form, exclude, with_mark):
-    
-    for inner in form:
-        
-        inner = simplify(inner, exclude, with_mark)
-        # 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 or inner == with_mark:
-            yield Mark
-            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:
-                if inner_inner_inner == with_mark:
-                    yield Mark
-                    assert False  # The simplify() function will not keep iterating after this.
-                    return  # Never reached, could delete this line.
-                yield inner_inner_inner
-            continue
-
-        #else:  # inner_inner = foo ; inner = (foo)
-        
-        yield inner
-
-
-if __name__ == '__main__':
-    unittest.main(argv=['ignored', 'MarkitTest0'], exit=False)
-
- -
-
-
- -
-
- - -
- -
- - -
-
.
-----------------------------------------------------------------------
-Ran 1 test in 0.001s
-
-OK
-
-
-
- -
-
- -
-
-
-
In [60]:
-
-
-
simplify(A, with_mark=b)
-
- -
-
-
- -
-
- - -
- -
Out[60]:
- - - - -
-
(a)
-
- -
- -
-
- -
-
-
-
-
-

Now we can create a new form that is equivalent to A.

- -
-
-
-
-
-
In [61]:
-
-
-
def each_way(form, name):
-    return simplify(F(
-        ( name  , form),
-        ((name,), simplify(form, with_mark=name)),
-    ))
-
-Ab = each_way(A, b)
-
-print A, '=', Ab
-
- -
-
-
- -
-
- - -
- -
- - -
-
(((c) b) a) = (((a c) b) ((a) (b)))
-
-
-
- -
-
- -
-
-
-
-
-

In this particular case the original form A was so simple that the new version Ab is actually a bit larger. With a large expression to start with the form after simplification would (usually) be smaller.

- -
-
-
-
-
-
-
-

Simplifying the Full-Bit Adder

Recall our original expressions for the sum and carry bits of a full-bit adder circuit, derived from the truth tables:

- -
-
-
-
-
-
In [62]:
-
-
-
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 [63]:
-
-
-
Sum
-
- -
-
-
- -
-
- - -
- -
Out[63]:
- - - - -
-
((((a) (b) (c)) ((a) b c) ((b) a c) ((c) a b)))
-
- -
- -
-
- -
-
-
-
In [64]:
-
-
-
Carry
-
- -
-
-
- -
-
- - -
- -
Out[64]:
- - - - -
-
((((a) (b) (c)) ((a) (b) c) ((a) (c) b) ((b) (c) a)))
-
- -
- -
-
- -
-
-
-
-
-

And the expressions derived from the definitions on Wikipedia:

- -
-
-
-
-
-
In [65]:
-
-
-
Sum, Carry = full_bit_adder(a, b, c)
-
- -
-
-
- -
-
-
-
In [66]:
-
-
-
Sum
-
- -
-
-
- -
-
- - -
- -
Out[66]:
- - - - -
-
((((((((a) b) ((b) a)))) c) (((((a) b) ((b) a))) (c))))
-
- -
- -
-
- -
-
-
-
In [67]:
-
-
-
Carry
-
- -
-
-
- -
-
- - -
- -
Out[67]:
- - - - -
-
((((((((a) b) ((b) a)))) (c)) ((a) (b))))
-
- -
- -
-
- -
-
-
-
-
-

We can use the each_way() function to look for simpler equivalent forms by, for example, iterating though the names and trying it with each. Try the following cells with both versions of the Sum and Carry above.

- -
-
-
-
-
-
In [68]:
-
-
-
print Sum
-for name in (a, b, c, a, b, c):
-    Sum = each_way(Sum, name)
-    print Sum
-
- -
-
-
- -
-
- - -
- -
- - -
-
((((((((a) b) ((b) a)))) c) (((((a) b) ((b) a))) (c))))
-((((b) (c)) (a) (b c)) (((b) c) ((c) b) a))
-(((((a) (c)) (a c)) b) ((((a) c) ((c) a)) (b)))
-(((((a) (b)) (a b)) c) ((((a) b) ((b) a)) (c)))
-(((((b) (c)) (b c)) a) ((((b) c) ((c) b)) (a)))
-(((((a) (c)) (a c)) b) ((((a) c) ((c) a)) (b)))
-(((((a) (b)) (a b)) c) ((((a) b) ((b) a)) (c)))
-
-
-
- -
-
- -
-
-
-
In [69]:
-
-
-
print Carry
-for name in (a, b, c, a, b, c):
-    Carry = each_way(Carry, name)
-    print Carry
-
- -
-
-
- -
-
- - -
- -
- - -
-
((((((((a) b) ((b) a)))) (c)) ((a) (b))))
-((((b) (c)) a) ((a) b c))
-(((((a) c) (a)) b) ((b) a c))
-(((((b) a) (b)) c) ((c) a b))
-(((((c) b) (c)) a) ((a) b c))
-(((((a) c) (a)) b) ((b) a c))
-(((((b) a) (b)) c) ((c) a b))
-
-
-
- -
-
- -
-
-
-
-
-

Let's redefine the full_bit_adder() function with the smallest version of each above.

- -
-
-
-
-
-
In [70]:
-
-
-
def full_bit_adder(a, b, c):
-    '''From the truth table.'''
-    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,)) ),),
-    )
-# Sizes: [63, 327, 1383, 5607, 22503, 90087, 360423, 1441767, 1441773]
-
- -
-
-
- -
-
-
-
In [71]:
-
-
-
def full_bit_adder(a, b, c):
-    '''Simplest forms from above.'''
-    return (
-        F( (((b,), (c,)), (a,), (b, c)), (((b,), c), ((c,), b), a) ),
-        F( (((a,), (c,)), b), ((b,), a, c) ),
-    )
-# Sizes: [57, 177, 417, 897, 1857, 3777, 7617, 15297, 7653]
-
- -
-
-
- -
-
-
-
In [72]:
-
-
-
def full_bit_adder(a, b, c):
-    '''Based on the definitions from Wikipedia.'''
-    return (
-        xor(xor(a, b), c),  # ((((((((a) b) ((b) a)))) c) (((((a) b) ((b) a))) (c))))
-        or_(and_(a, b), and_(c, xor(a, b))),  # ((((((((a) b) ((b) a)))) (c)) ((a) (b))))
-    )
-# Sizes: [67, 159, 251, 343, 435, 527, 619, 711, 371]
-
- -
-
-
- -
-
-
-
In [73]:
-
-
-
def full_bit_adder(a, b, c):
-    '''Based on the definitions from Wikipedia.'''
-    return (
-        simplify(xor(xor(a, b), c)),
-        simplify(or_(and_(a, b), and_(c, xor(a, b)))),
-    )
-# Sizes: [59, 135, 211, 287, 363, 439, 515, 591, 311]
-
- -
-
-
- -
-
-
-
-
-

In this case, the version from the definitions does much better than the other two.

- -
-
-
-
-
-
In [74]:
-
-
-
Sum, Carry = full_bit_adder(a, b, c)
-
-truth_table(Sum)
-print
-truth_table(Carry)
-print
-
-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)
-
-print map(len, map(str, (sum0, sum1, sum2, sum3, sum4, sum5, sum6, sum7, cout)))
-
- -
-
-
- -
-
- - -
- -
- - -
-
((((((a) b) ((b) a)) c) (((a) b) ((b) a) (c))))
- a  b  c | Value
----------+------
-         | 
-      () | ()
-   ()    | ()
-   () () | 
-()       | ()
-()    () | 
-() ()    | 
-() () () | ()
-
-((((((a) b) ((b) a)) (c)) ((a) (b))))
- a  b  c | Value
----------+------
-         | 
-      () | 
-   ()    | 
-   () () | ()
-()       | 
-()    () | ()
-() ()    | ()
-() () () | ()
-
-[59, 135, 211, 287, 363, 439, 515, 591, 311]
-
-
-
- -
-
- -
-
-
-
-
-

Davis–Putnam–Logemann–Loveland (DPLL) algorithm SAT Solver

This is something of an Interlude, we aren't going to use it below, but it's too cool to omit mention.

-

We can use the simplify() function to create a more efficient SAT solver along the lines of the DPLL algorithm.

-

It works by selecting a name from the form, and simplifying the form with that name first as Void then as Mark, then recursing with the new form and the next name. If the resulting simplified form becomes the Mark then our choices (of assigning Void or Mark to the names selected so far) constitute a "solution" to the original form. That is, if we reify() the form with the environment returned by the dpll() function the result will be Mark-valued.

- -
-
-
-
-
-
In [75]:
-
-
-
def dpll(E, partial=None, unit=True):
-    if partial is None:
-        partial = {}
-    else:
-        partial = partial.copy() # so we can backtrack later..
-
-    if isinstance(E, basestring):
-        partial[E] = Mark
-        return partial
-
-    if unit:
-        E = assign_unit_clauses(E, partial)
-
-    if not E:
-        return partial
-
-    if Mark in E:
-        return
-
-    v = next_symbol_of(E)
-
-    partial[v] = Void
-
-    res = dpll(simplify(E, {v}), partial, unit)
-    if res is not None: 
-        return res
-
-    partial[v] = Mark
-
-    return dpll(simplify(E, with_mark=v), partial, unit)
-
-
-def assign_unit_clauses(E, partial):
-    '''
-    Find and assign values to an "unit clauses" in the form, simplifying as you go.
-    A unit clause is a bare name or a negated name: a or (a), for these clauses we
-    can set them to Void or Mark, respectively, to contibute to making their containing
-    Form the Mark.
-    '''
-    on, off, E = find_units(E)
-    while on or off:
-        while on:
-            if on & off: return Void
-            term = first_of(on)
-            partial[term] = Mark
-            ON, OFF, E = find_units(simplify(E, with_mark=term))
-            on |= ON
-            on.remove(term)
-            off |= OFF
-        while off:
-            if on & off: return Void
-            term = first_of(off)
-            partial[term] = Void
-            ON, OFF, E = find_units(simplify(E, {term}))
-            off |= OFF
-            off.remove(term)
-            on |= ON
-    return E
-
-
-def next_symbol_of(E):
-    if isinstance(E, basestring):
-        return E
-    for it in E:
-        return next_symbol_of(it)
-    raise Exception("no more symbols")
-
-
-def find_units(E):
-    '''
-    Return two sets and a possibly-reduced E.  The literals in the first
-    set must be Void and those in the second must be set Mark to have the
-    entire expression become Void.
-    '''
-    on, off, poly = set(), set(), set()
-    for clause in E:
-        if isinstance(clause, basestring):
-            off.add(clause)
-            continue
-        if len(clause) != 1:
-            poly.add(clause)
-            continue
-        (n,) = clause # Unwrap one layer of containment.
-        if isinstance(n, basestring):
-            on.add(n)
-        else:
-            poly.add(clause)
-    return on, off, Form(poly)
-
-
-# Return any item from a form.
-first_of = lambda form: next(iter(form))
-
- -
-
-
- -
-
-
-
In [76]:
-
-
-
A = F(a, (b, (c,)))
-truth_table(A)
-solution = dpll(A)
-arith = reify(A, solution)
-print
-print 'A solution:', solution
-print
-print 'Reifies to', arith, u'⟶', value_of(arith)
-
- -
-
-
- -
-
- - -
- -
- - -
-
(((c) b) a)
- a  b  c | Value
----------+------
-         | ()
-      () | 
-   ()    | ()
-   () () | ()
-()       | 
-()    () | 
-() ()    | 
-() () () | 
-
-A solution: {'a': (()), 'c': (()), 'b': (())}
-
-Reifies to ((((())) (())) (())) ⟶ ()
-
-
-
- -
-
- -
-
-
-
-
-

dpll_iter()

We can write a generator version of the function that keeps looking for solutions after the first.

- -
-
-
-
-
-
In [77]:
-
-
-
def dpll_iter(E, partial=None, unit=True):
-    if partial is None:
-        partial = {}
-    else:
-        partial = partial.copy() # so we can backtrack later..
-
-    if isinstance(E, basestring):
-        partial[E] = Mark
-        yield partial
-        return
-
-    if unit:
-        E = assign_unit_clauses(E, partial)
-
-    if not E:
-        yield partial
-        return
-
-    if Mark in E:
-        return
-
-    v = next_symbol_of(E)
-
-    partial[v] = Void
-
-    for res in dpll_iter(simplify(E, {v}), partial, unit):
-        yield res
-
-    partial[v] = Mark
-
-    for res in dpll_iter(simplify(E, with_mark=v), partial, unit):
-        yield res
-
- -
-
-
- -
-
-
-
In [78]:
-
-
-
for solution in dpll_iter(A):
-    print (solution)
-
- -
-
-
- -
-
- - -
- -
- - -
-
{'a': (()), 'c': (()), 'b': (())}
-{'a': (()), 'b': ()}
-
-
-
- -
-
- -
-
-
-
In [79]:
-
-
-
Sum, Carry = full_bit_adder(a, b, c)
-
- -
-
-
- -
-
-
-
In [80]:
-
-
-
for solution in dpll_iter(Sum, unit=False):
-    r = reify(Sum, solution)
-    print (solution), r, '=', simplify(r)
-
- -
-
-
- -
-
- - -
- -
- - -
-
{'a': (()), 'c': (), 'b': (())} (((((((())) (()))) ()) ((((())) (())) (())))) = ()
-{'a': (()), 'c': (()), 'b': ()} (((((((())) ()) ((()))) (())) ((((())) ()) ((()))))) = ()
-{'a': (), 'c': (()), 'b': (())} (((((((())) ()) ((()))) (())) ((((())) ()) ((()))))) = ()
-{'a': (), 'c': (), 'b': ()} ((((((()) ())) ()) (((()) ()) (())))) = ()
-
-
-
- -
-
- -
-
-
-
In [81]:
-
-
-
for solution in dpll_iter(Carry, unit=False):
-    r = reify(Carry, solution)
-    print (solution), r, '=', simplify(r)
-
- -
-
-
- -
-
- - -
- -
- - -
-
{'a': (()), 'c': (), 'b': ()} (((((((())) ()) ((()))) (())) (((())) (())))) = ()
-{'a': (), 'c': (), 'b': (())} (((((((())) ()) ((()))) (())) (((())) (())))) = ()
-{'a': (), 'b': ()} ((((((()) ())) (c)) ((())))) = ()
-
-
-
- -
-
- -
-
-
-
-
-

Notice that the reified form still has c in it but that doesn't prevent the simplify() function from reducing the form to the Mark. This should be the case for all solutions generated by the dpll_iter() function.

- -
-
-
-
-
-
In [82]:
-
-
-
for solution in dpll_iter(cout):
-    print simplify(reify(cout, solution)),
-
- -
-
-
- -
-
- - -
- -
- - -
-
() () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () (((a5) a5)) (((a5) a5)) () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () (((a5) a5)) (((a5) a5)) () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () (((a5) a5)) (((a5) a5)) () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () () (((a5) a5)) (((a5) a5)) () ()
-
-
-
- -
-
- -
-
-
-
-
-

Interesting! Some solutions do not simplify() completely in one go. The form (((a5) a5)) is Mark-valued:

- -
(((a5) a5))
-(((  ) a5))
-(((  )   ))
-(         )
-()
- -
-
-
-
-
-
In [83]:
-
-
-
E = F(((a,), a))
-print E
-print simplify(E)
-
- -
-
-
- -
-
- - -
- -
- - -
-
(((a) a))
-()
-
-
-
- -
-
- -
-
-
-
-
-

Something to keep in mind.

- -
-
-
-
-
-
-
-

Now back to Circuits

Using the Adder Circuits to Add

In order to keep things tractable I'm going to use just four bits rather than eight.

- -
-
-
-
-
-
In [84]:
-
-
-
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)
-
- -
-
-
- -
-
-
-
-
-

Put the circuit expressions into a handy dictionary, and we are ready to add some numbers.

- -
-
-
-
-
-
In [85]:
-
-
-
CIRCUITS = {
-    'sum0': sum0,
-    'sum1': sum1,
-    'sum2': sum2,
-    'sum3': sum3,
-    'cout': cout,
-}
-
- -
-
-
- -
-
-
-
-
-

A bunch of crufty junk to print out a nice truth table with the columns arranged to make it (relatively) easy to see the addition.

- -
-
-
-
-
-
In [86]:
-
-
-
def stringy_env(env):
-    return {
-        k: value_of(e, v='--', m='()')
-        for k, e in env.items()
-    }
-
-INPUTs = ('Cin', 'a3', 'a2', 'a1', 'a0', 'b3', 'b2', 'b1', 'b0')
-OUTPUTs = ('cout', 'sum3', 'sum2', 'sum1', 'sum0')
-
-format_string = '%(' + ')s %('.join(INPUTs) + ')s | %(' + ')s %('.join(OUTPUTs) + ')s'
-
-
-print 'Ci|a3 a2 a1 a0|b3 b2 b1 b0 | Co s3 s2 s1 s0'
-results = {}
-for env in environments_of_variables(*INPUTs):
-
-    for name, expression in CIRCUITS.items():
-        results[name] = value_of(reify(expression, env))
-
-    env.update(results)
-    print format_string % stringy_env(env)
-
- -
-
-
- -
-
- - -
- -
- - -
-
Ci|a3 a2 a1 a0|b3 b2 b1 b0 | Co s3 s2 s1 s0
--- -- -- -- -- -- -- -- -- | -- -- -- -- --
--- -- -- -- -- -- -- -- () | -- -- -- -- ()
--- -- -- -- -- -- -- () -- | -- -- -- () --
--- -- -- -- -- -- -- () () | -- -- -- () ()
--- -- -- -- -- -- () -- -- | -- -- () -- --
--- -- -- -- -- -- () -- () | -- -- () -- ()
--- -- -- -- -- -- () () -- | -- -- () () --
--- -- -- -- -- -- () () () | -- -- () () ()
--- -- -- -- -- () -- -- -- | -- () -- -- --
--- -- -- -- -- () -- -- () | -- () -- -- ()
--- -- -- -- -- () -- () -- | -- () -- () --
--- -- -- -- -- () -- () () | -- () -- () ()
--- -- -- -- -- () () -- -- | -- () () -- --
--- -- -- -- -- () () -- () | -- () () -- ()
--- -- -- -- -- () () () -- | -- () () () --
--- -- -- -- -- () () () () | -- () () () ()
--- -- -- -- () -- -- -- -- | -- -- -- -- ()
--- -- -- -- () -- -- -- () | -- -- -- () --
--- -- -- -- () -- -- () -- | -- -- -- () ()
--- -- -- -- () -- -- () () | -- -- () -- --
--- -- -- -- () -- () -- -- | -- -- () -- ()
--- -- -- -- () -- () -- () | -- -- () () --
--- -- -- -- () -- () () -- | -- -- () () ()
--- -- -- -- () -- () () () | -- () -- -- --
--- -- -- -- () () -- -- -- | -- () -- -- ()
--- -- -- -- () () -- -- () | -- () -- () --
--- -- -- -- () () -- () -- | -- () -- () ()
--- -- -- -- () () -- () () | -- () () -- --
--- -- -- -- () () () -- -- | -- () () -- ()
--- -- -- -- () () () -- () | -- () () () --
--- -- -- -- () () () () -- | -- () () () ()
--- -- -- -- () () () () () | () -- -- -- --
--- -- -- () -- -- -- -- -- | -- -- -- () --
--- -- -- () -- -- -- -- () | -- -- -- () ()
--- -- -- () -- -- -- () -- | -- -- () -- --
--- -- -- () -- -- -- () () | -- -- () -- ()
--- -- -- () -- -- () -- -- | -- -- () () --
--- -- -- () -- -- () -- () | -- -- () () ()
--- -- -- () -- -- () () -- | -- () -- -- --
--- -- -- () -- -- () () () | -- () -- -- ()
--- -- -- () -- () -- -- -- | -- () -- () --
--- -- -- () -- () -- -- () | -- () -- () ()
--- -- -- () -- () -- () -- | -- () () -- --
--- -- -- () -- () -- () () | -- () () -- ()
--- -- -- () -- () () -- -- | -- () () () --
--- -- -- () -- () () -- () | -- () () () ()
--- -- -- () -- () () () -- | () -- -- -- --
--- -- -- () -- () () () () | () -- -- -- ()
--- -- -- () () -- -- -- -- | -- -- -- () ()
--- -- -- () () -- -- -- () | -- -- () -- --
--- -- -- () () -- -- () -- | -- -- () -- ()
--- -- -- () () -- -- () () | -- -- () () --
--- -- -- () () -- () -- -- | -- -- () () ()
--- -- -- () () -- () -- () | -- () -- -- --
--- -- -- () () -- () () -- | -- () -- -- ()
--- -- -- () () -- () () () | -- () -- () --
--- -- -- () () () -- -- -- | -- () -- () ()
--- -- -- () () () -- -- () | -- () () -- --
--- -- -- () () () -- () -- | -- () () -- ()
--- -- -- () () () -- () () | -- () () () --
--- -- -- () () () () -- -- | -- () () () ()
--- -- -- () () () () -- () | () -- -- -- --
--- -- -- () () () () () -- | () -- -- -- ()
--- -- -- () () () () () () | () -- -- () --
--- -- () -- -- -- -- -- -- | -- -- () -- --
--- -- () -- -- -- -- -- () | -- -- () -- ()
--- -- () -- -- -- -- () -- | -- -- () () --
--- -- () -- -- -- -- () () | -- -- () () ()
--- -- () -- -- -- () -- -- | -- () -- -- --
--- -- () -- -- -- () -- () | -- () -- -- ()
--- -- () -- -- -- () () -- | -- () -- () --
--- -- () -- -- -- () () () | -- () -- () ()
--- -- () -- -- () -- -- -- | -- () () -- --
--- -- () -- -- () -- -- () | -- () () -- ()
--- -- () -- -- () -- () -- | -- () () () --
--- -- () -- -- () -- () () | -- () () () ()
--- -- () -- -- () () -- -- | () -- -- -- --
--- -- () -- -- () () -- () | () -- -- -- ()
--- -- () -- -- () () () -- | () -- -- () --
--- -- () -- -- () () () () | () -- -- () ()
--- -- () -- () -- -- -- -- | -- -- () -- ()
--- -- () -- () -- -- -- () | -- -- () () --
--- -- () -- () -- -- () -- | -- -- () () ()
--- -- () -- () -- -- () () | -- () -- -- --
--- -- () -- () -- () -- -- | -- () -- -- ()
--- -- () -- () -- () -- () | -- () -- () --
--- -- () -- () -- () () -- | -- () -- () ()
--- -- () -- () -- () () () | -- () () -- --
--- -- () -- () () -- -- -- | -- () () -- ()
--- -- () -- () () -- -- () | -- () () () --
--- -- () -- () () -- () -- | -- () () () ()
--- -- () -- () () -- () () | () -- -- -- --
--- -- () -- () () () -- -- | () -- -- -- ()
--- -- () -- () () () -- () | () -- -- () --
--- -- () -- () () () () -- | () -- -- () ()
--- -- () -- () () () () () | () -- () -- --
--- -- () () -- -- -- -- -- | -- -- () () --
--- -- () () -- -- -- -- () | -- -- () () ()
--- -- () () -- -- -- () -- | -- () -- -- --
--- -- () () -- -- -- () () | -- () -- -- ()
--- -- () () -- -- () -- -- | -- () -- () --
--- -- () () -- -- () -- () | -- () -- () ()
--- -- () () -- -- () () -- | -- () () -- --
--- -- () () -- -- () () () | -- () () -- ()
--- -- () () -- () -- -- -- | -- () () () --
--- -- () () -- () -- -- () | -- () () () ()
--- -- () () -- () -- () -- | () -- -- -- --
--- -- () () -- () -- () () | () -- -- -- ()
--- -- () () -- () () -- -- | () -- -- () --
--- -- () () -- () () -- () | () -- -- () ()
--- -- () () -- () () () -- | () -- () -- --
--- -- () () -- () () () () | () -- () -- ()
--- -- () () () -- -- -- -- | -- -- () () ()
--- -- () () () -- -- -- () | -- () -- -- --
--- -- () () () -- -- () -- | -- () -- -- ()
--- -- () () () -- -- () () | -- () -- () --
--- -- () () () -- () -- -- | -- () -- () ()
--- -- () () () -- () -- () | -- () () -- --
--- -- () () () -- () () -- | -- () () -- ()
--- -- () () () -- () () () | -- () () () --
--- -- () () () () -- -- -- | -- () () () ()
--- -- () () () () -- -- () | () -- -- -- --
--- -- () () () () -- () -- | () -- -- -- ()
--- -- () () () () -- () () | () -- -- () --
--- -- () () () () () -- -- | () -- -- () ()
--- -- () () () () () -- () | () -- () -- --
--- -- () () () () () () -- | () -- () -- ()
--- -- () () () () () () () | () -- () () --
--- () -- -- -- -- -- -- -- | -- () -- -- --
--- () -- -- -- -- -- -- () | -- () -- -- ()
--- () -- -- -- -- -- () -- | -- () -- () --
--- () -- -- -- -- -- () () | -- () -- () ()
--- () -- -- -- -- () -- -- | -- () () -- --
--- () -- -- -- -- () -- () | -- () () -- ()
--- () -- -- -- -- () () -- | -- () () () --
--- () -- -- -- -- () () () | -- () () () ()
--- () -- -- -- () -- -- -- | () -- -- -- --
--- () -- -- -- () -- -- () | () -- -- -- ()
--- () -- -- -- () -- () -- | () -- -- () --
--- () -- -- -- () -- () () | () -- -- () ()
--- () -- -- -- () () -- -- | () -- () -- --
--- () -- -- -- () () -- () | () -- () -- ()
--- () -- -- -- () () () -- | () -- () () --
--- () -- -- -- () () () () | () -- () () ()
--- () -- -- () -- -- -- -- | -- () -- -- ()
--- () -- -- () -- -- -- () | -- () -- () --
--- () -- -- () -- -- () -- | -- () -- () ()
--- () -- -- () -- -- () () | -- () () -- --
--- () -- -- () -- () -- -- | -- () () -- ()
--- () -- -- () -- () -- () | -- () () () --
--- () -- -- () -- () () -- | -- () () () ()
--- () -- -- () -- () () () | () -- -- -- --
--- () -- -- () () -- -- -- | () -- -- -- ()
--- () -- -- () () -- -- () | () -- -- () --
--- () -- -- () () -- () -- | () -- -- () ()
--- () -- -- () () -- () () | () -- () -- --
--- () -- -- () () () -- -- | () -- () -- ()
--- () -- -- () () () -- () | () -- () () --
--- () -- -- () () () () -- | () -- () () ()
--- () -- -- () () () () () | () () -- -- --
--- () -- () -- -- -- -- -- | -- () -- () --
--- () -- () -- -- -- -- () | -- () -- () ()
--- () -- () -- -- -- () -- | -- () () -- --
--- () -- () -- -- -- () () | -- () () -- ()
--- () -- () -- -- () -- -- | -- () () () --
--- () -- () -- -- () -- () | -- () () () ()
--- () -- () -- -- () () -- | () -- -- -- --
--- () -- () -- -- () () () | () -- -- -- ()
--- () -- () -- () -- -- -- | () -- -- () --
--- () -- () -- () -- -- () | () -- -- () ()
--- () -- () -- () -- () -- | () -- () -- --
--- () -- () -- () -- () () | () -- () -- ()
--- () -- () -- () () -- -- | () -- () () --
--- () -- () -- () () -- () | () -- () () ()
--- () -- () -- () () () -- | () () -- -- --
--- () -- () -- () () () () | () () -- -- ()
--- () -- () () -- -- -- -- | -- () -- () ()
--- () -- () () -- -- -- () | -- () () -- --
--- () -- () () -- -- () -- | -- () () -- ()
--- () -- () () -- -- () () | -- () () () --
--- () -- () () -- () -- -- | -- () () () ()
--- () -- () () -- () -- () | () -- -- -- --
--- () -- () () -- () () -- | () -- -- -- ()
--- () -- () () -- () () () | () -- -- () --
--- () -- () () () -- -- -- | () -- -- () ()
--- () -- () () () -- -- () | () -- () -- --
--- () -- () () () -- () -- | () -- () -- ()
--- () -- () () () -- () () | () -- () () --
--- () -- () () () () -- -- | () -- () () ()
--- () -- () () () () -- () | () () -- -- --
--- () -- () () () () () -- | () () -- -- ()
--- () -- () () () () () () | () () -- () --
--- () () -- -- -- -- -- -- | -- () () -- --
--- () () -- -- -- -- -- () | -- () () -- ()
--- () () -- -- -- -- () -- | -- () () () --
--- () () -- -- -- -- () () | -- () () () ()
--- () () -- -- -- () -- -- | () -- -- -- --
--- () () -- -- -- () -- () | () -- -- -- ()
--- () () -- -- -- () () -- | () -- -- () --
--- () () -- -- -- () () () | () -- -- () ()
--- () () -- -- () -- -- -- | () -- () -- --
--- () () -- -- () -- -- () | () -- () -- ()
--- () () -- -- () -- () -- | () -- () () --
--- () () -- -- () -- () () | () -- () () ()
--- () () -- -- () () -- -- | () () -- -- --
--- () () -- -- () () -- () | () () -- -- ()
--- () () -- -- () () () -- | () () -- () --
--- () () -- -- () () () () | () () -- () ()
--- () () -- () -- -- -- -- | -- () () -- ()
--- () () -- () -- -- -- () | -- () () () --
--- () () -- () -- -- () -- | -- () () () ()
--- () () -- () -- -- () () | () -- -- -- --
--- () () -- () -- () -- -- | () -- -- -- ()
--- () () -- () -- () -- () | () -- -- () --
--- () () -- () -- () () -- | () -- -- () ()
--- () () -- () -- () () () | () -- () -- --
--- () () -- () () -- -- -- | () -- () -- ()
--- () () -- () () -- -- () | () -- () () --
--- () () -- () () -- () -- | () -- () () ()
--- () () -- () () -- () () | () () -- -- --
--- () () -- () () () -- -- | () () -- -- ()
--- () () -- () () () -- () | () () -- () --
--- () () -- () () () () -- | () () -- () ()
--- () () -- () () () () () | () () () -- --
--- () () () -- -- -- -- -- | -- () () () --
--- () () () -- -- -- -- () | -- () () () ()
--- () () () -- -- -- () -- | () -- -- -- --
--- () () () -- -- -- () () | () -- -- -- ()
--- () () () -- -- () -- -- | () -- -- () --
--- () () () -- -- () -- () | () -- -- () ()
--- () () () -- -- () () -- | () -- () -- --
--- () () () -- -- () () () | () -- () -- ()
--- () () () -- () -- -- -- | () -- () () --
--- () () () -- () -- -- () | () -- () () ()
--- () () () -- () -- () -- | () () -- -- --
--- () () () -- () -- () () | () () -- -- ()
--- () () () -- () () -- -- | () () -- () --
--- () () () -- () () -- () | () () -- () ()
--- () () () -- () () () -- | () () () -- --
--- () () () -- () () () () | () () () -- ()
--- () () () () -- -- -- -- | -- () () () ()
--- () () () () -- -- -- () | () -- -- -- --
--- () () () () -- -- () -- | () -- -- -- ()
--- () () () () -- -- () () | () -- -- () --
--- () () () () -- () -- -- | () -- -- () ()
--- () () () () -- () -- () | () -- () -- --
--- () () () () -- () () -- | () -- () -- ()
--- () () () () -- () () () | () -- () () --
--- () () () () () -- -- -- | () -- () () ()
--- () () () () () -- -- () | () () -- -- --
--- () () () () () -- () -- | () () -- -- ()
--- () () () () () -- () () | () () -- () --
--- () () () () () () -- -- | () () -- () ()
--- () () () () () () -- () | () () () -- --
--- () () () () () () () -- | () () () -- ()
--- () () () () () () () () | () () () () --
-() -- -- -- -- -- -- -- -- | -- -- -- -- ()
-() -- -- -- -- -- -- -- () | -- -- -- () --
-() -- -- -- -- -- -- () -- | -- -- -- () ()
-() -- -- -- -- -- -- () () | -- -- () -- --
-() -- -- -- -- -- () -- -- | -- -- () -- ()
-() -- -- -- -- -- () -- () | -- -- () () --
-() -- -- -- -- -- () () -- | -- -- () () ()
-() -- -- -- -- -- () () () | -- () -- -- --
-() -- -- -- -- () -- -- -- | -- () -- -- ()
-() -- -- -- -- () -- -- () | -- () -- () --
-() -- -- -- -- () -- () -- | -- () -- () ()
-() -- -- -- -- () -- () () | -- () () -- --
-() -- -- -- -- () () -- -- | -- () () -- ()
-() -- -- -- -- () () -- () | -- () () () --
-() -- -- -- -- () () () -- | -- () () () ()
-() -- -- -- -- () () () () | () -- -- -- --
-() -- -- -- () -- -- -- -- | -- -- -- () --
-() -- -- -- () -- -- -- () | -- -- -- () ()
-() -- -- -- () -- -- () -- | -- -- () -- --
-() -- -- -- () -- -- () () | -- -- () -- ()
-() -- -- -- () -- () -- -- | -- -- () () --
-() -- -- -- () -- () -- () | -- -- () () ()
-() -- -- -- () -- () () -- | -- () -- -- --
-() -- -- -- () -- () () () | -- () -- -- ()
-() -- -- -- () () -- -- -- | -- () -- () --
-() -- -- -- () () -- -- () | -- () -- () ()
-() -- -- -- () () -- () -- | -- () () -- --
-() -- -- -- () () -- () () | -- () () -- ()
-() -- -- -- () () () -- -- | -- () () () --
-() -- -- -- () () () -- () | -- () () () ()
-() -- -- -- () () () () -- | () -- -- -- --
-() -- -- -- () () () () () | () -- -- -- ()
-() -- -- () -- -- -- -- -- | -- -- -- () ()
-() -- -- () -- -- -- -- () | -- -- () -- --
-() -- -- () -- -- -- () -- | -- -- () -- ()
-() -- -- () -- -- -- () () | -- -- () () --
-() -- -- () -- -- () -- -- | -- -- () () ()
-() -- -- () -- -- () -- () | -- () -- -- --
-() -- -- () -- -- () () -- | -- () -- -- ()
-() -- -- () -- -- () () () | -- () -- () --
-() -- -- () -- () -- -- -- | -- () -- () ()
-() -- -- () -- () -- -- () | -- () () -- --
-() -- -- () -- () -- () -- | -- () () -- ()
-() -- -- () -- () -- () () | -- () () () --
-() -- -- () -- () () -- -- | -- () () () ()
-() -- -- () -- () () -- () | () -- -- -- --
-() -- -- () -- () () () -- | () -- -- -- ()
-() -- -- () -- () () () () | () -- -- () --
-() -- -- () () -- -- -- -- | -- -- () -- --
-() -- -- () () -- -- -- () | -- -- () -- ()
-() -- -- () () -- -- () -- | -- -- () () --
-() -- -- () () -- -- () () | -- -- () () ()
-() -- -- () () -- () -- -- | -- () -- -- --
-() -- -- () () -- () -- () | -- () -- -- ()
-() -- -- () () -- () () -- | -- () -- () --
-() -- -- () () -- () () () | -- () -- () ()
-() -- -- () () () -- -- -- | -- () () -- --
-() -- -- () () () -- -- () | -- () () -- ()
-() -- -- () () () -- () -- | -- () () () --
-() -- -- () () () -- () () | -- () () () ()
-() -- -- () () () () -- -- | () -- -- -- --
-() -- -- () () () () -- () | () -- -- -- ()
-() -- -- () () () () () -- | () -- -- () --
-() -- -- () () () () () () | () -- -- () ()
-() -- () -- -- -- -- -- -- | -- -- () -- ()
-() -- () -- -- -- -- -- () | -- -- () () --
-() -- () -- -- -- -- () -- | -- -- () () ()
-() -- () -- -- -- -- () () | -- () -- -- --
-() -- () -- -- -- () -- -- | -- () -- -- ()
-() -- () -- -- -- () -- () | -- () -- () --
-() -- () -- -- -- () () -- | -- () -- () ()
-() -- () -- -- -- () () () | -- () () -- --
-() -- () -- -- () -- -- -- | -- () () -- ()
-() -- () -- -- () -- -- () | -- () () () --
-() -- () -- -- () -- () -- | -- () () () ()
-() -- () -- -- () -- () () | () -- -- -- --
-() -- () -- -- () () -- -- | () -- -- -- ()
-() -- () -- -- () () -- () | () -- -- () --
-() -- () -- -- () () () -- | () -- -- () ()
-() -- () -- -- () () () () | () -- () -- --
-() -- () -- () -- -- -- -- | -- -- () () --
-() -- () -- () -- -- -- () | -- -- () () ()
-() -- () -- () -- -- () -- | -- () -- -- --
-() -- () -- () -- -- () () | -- () -- -- ()
-() -- () -- () -- () -- -- | -- () -- () --
-() -- () -- () -- () -- () | -- () -- () ()
-() -- () -- () -- () () -- | -- () () -- --
-() -- () -- () -- () () () | -- () () -- ()
-() -- () -- () () -- -- -- | -- () () () --
-() -- () -- () () -- -- () | -- () () () ()
-() -- () -- () () -- () -- | () -- -- -- --
-() -- () -- () () -- () () | () -- -- -- ()
-() -- () -- () () () -- -- | () -- -- () --
-() -- () -- () () () -- () | () -- -- () ()
-() -- () -- () () () () -- | () -- () -- --
-() -- () -- () () () () () | () -- () -- ()
-() -- () () -- -- -- -- -- | -- -- () () ()
-() -- () () -- -- -- -- () | -- () -- -- --
-() -- () () -- -- -- () -- | -- () -- -- ()
-() -- () () -- -- -- () () | -- () -- () --
-() -- () () -- -- () -- -- | -- () -- () ()
-() -- () () -- -- () -- () | -- () () -- --
-() -- () () -- -- () () -- | -- () () -- ()
-() -- () () -- -- () () () | -- () () () --
-() -- () () -- () -- -- -- | -- () () () ()
-() -- () () -- () -- -- () | () -- -- -- --
-() -- () () -- () -- () -- | () -- -- -- ()
-() -- () () -- () -- () () | () -- -- () --
-() -- () () -- () () -- -- | () -- -- () ()
-() -- () () -- () () -- () | () -- () -- --
-() -- () () -- () () () -- | () -- () -- ()
-() -- () () -- () () () () | () -- () () --
-() -- () () () -- -- -- -- | -- () -- -- --
-() -- () () () -- -- -- () | -- () -- -- ()
-() -- () () () -- -- () -- | -- () -- () --
-() -- () () () -- -- () () | -- () -- () ()
-() -- () () () -- () -- -- | -- () () -- --
-() -- () () () -- () -- () | -- () () -- ()
-() -- () () () -- () () -- | -- () () () --
-() -- () () () -- () () () | -- () () () ()
-() -- () () () () -- -- -- | () -- -- -- --
-() -- () () () () -- -- () | () -- -- -- ()
-() -- () () () () -- () -- | () -- -- () --
-() -- () () () () -- () () | () -- -- () ()
-() -- () () () () () -- -- | () -- () -- --
-() -- () () () () () -- () | () -- () -- ()
-() -- () () () () () () -- | () -- () () --
-() -- () () () () () () () | () -- () () ()
-() () -- -- -- -- -- -- -- | -- () -- -- ()
-() () -- -- -- -- -- -- () | -- () -- () --
-() () -- -- -- -- -- () -- | -- () -- () ()
-() () -- -- -- -- -- () () | -- () () -- --
-() () -- -- -- -- () -- -- | -- () () -- ()
-() () -- -- -- -- () -- () | -- () () () --
-() () -- -- -- -- () () -- | -- () () () ()
-() () -- -- -- -- () () () | () -- -- -- --
-() () -- -- -- () -- -- -- | () -- -- -- ()
-() () -- -- -- () -- -- () | () -- -- () --
-() () -- -- -- () -- () -- | () -- -- () ()
-() () -- -- -- () -- () () | () -- () -- --
-() () -- -- -- () () -- -- | () -- () -- ()
-() () -- -- -- () () -- () | () -- () () --
-() () -- -- -- () () () -- | () -- () () ()
-() () -- -- -- () () () () | () () -- -- --
-() () -- -- () -- -- -- -- | -- () -- () --
-() () -- -- () -- -- -- () | -- () -- () ()
-() () -- -- () -- -- () -- | -- () () -- --
-() () -- -- () -- -- () () | -- () () -- ()
-() () -- -- () -- () -- -- | -- () () () --
-() () -- -- () -- () -- () | -- () () () ()
-() () -- -- () -- () () -- | () -- -- -- --
-() () -- -- () -- () () () | () -- -- -- ()
-() () -- -- () () -- -- -- | () -- -- () --
-() () -- -- () () -- -- () | () -- -- () ()
-() () -- -- () () -- () -- | () -- () -- --
-() () -- -- () () -- () () | () -- () -- ()
-() () -- -- () () () -- -- | () -- () () --
-() () -- -- () () () -- () | () -- () () ()
-() () -- -- () () () () -- | () () -- -- --
-() () -- -- () () () () () | () () -- -- ()
-() () -- () -- -- -- -- -- | -- () -- () ()
-() () -- () -- -- -- -- () | -- () () -- --
-() () -- () -- -- -- () -- | -- () () -- ()
-() () -- () -- -- -- () () | -- () () () --
-() () -- () -- -- () -- -- | -- () () () ()
-() () -- () -- -- () -- () | () -- -- -- --
-() () -- () -- -- () () -- | () -- -- -- ()
-() () -- () -- -- () () () | () -- -- () --
-() () -- () -- () -- -- -- | () -- -- () ()
-() () -- () -- () -- -- () | () -- () -- --
-() () -- () -- () -- () -- | () -- () -- ()
-() () -- () -- () -- () () | () -- () () --
-() () -- () -- () () -- -- | () -- () () ()
-() () -- () -- () () -- () | () () -- -- --
-() () -- () -- () () () -- | () () -- -- ()
-() () -- () -- () () () () | () () -- () --
-() () -- () () -- -- -- -- | -- () () -- --
-() () -- () () -- -- -- () | -- () () -- ()
-() () -- () () -- -- () -- | -- () () () --
-() () -- () () -- -- () () | -- () () () ()
-() () -- () () -- () -- -- | () -- -- -- --
-() () -- () () -- () -- () | () -- -- -- ()
-() () -- () () -- () () -- | () -- -- () --
-() () -- () () -- () () () | () -- -- () ()
-() () -- () () () -- -- -- | () -- () -- --
-() () -- () () () -- -- () | () -- () -- ()
-() () -- () () () -- () -- | () -- () () --
-() () -- () () () -- () () | () -- () () ()
-() () -- () () () () -- -- | () () -- -- --
-() () -- () () () () -- () | () () -- -- ()
-() () -- () () () () () -- | () () -- () --
-() () -- () () () () () () | () () -- () ()
-() () () -- -- -- -- -- -- | -- () () -- ()
-() () () -- -- -- -- -- () | -- () () () --
-() () () -- -- -- -- () -- | -- () () () ()
-() () () -- -- -- -- () () | () -- -- -- --
-() () () -- -- -- () -- -- | () -- -- -- ()
-() () () -- -- -- () -- () | () -- -- () --
-() () () -- -- -- () () -- | () -- -- () ()
-() () () -- -- -- () () () | () -- () -- --
-() () () -- -- () -- -- -- | () -- () -- ()
-() () () -- -- () -- -- () | () -- () () --
-() () () -- -- () -- () -- | () -- () () ()
-() () () -- -- () -- () () | () () -- -- --
-() () () -- -- () () -- -- | () () -- -- ()
-() () () -- -- () () -- () | () () -- () --
-() () () -- -- () () () -- | () () -- () ()
-() () () -- -- () () () () | () () () -- --
-() () () -- () -- -- -- -- | -- () () () --
-() () () -- () -- -- -- () | -- () () () ()
-() () () -- () -- -- () -- | () -- -- -- --
-() () () -- () -- -- () () | () -- -- -- ()
-() () () -- () -- () -- -- | () -- -- () --
-() () () -- () -- () -- () | () -- -- () ()
-() () () -- () -- () () -- | () -- () -- --
-() () () -- () -- () () () | () -- () -- ()
-() () () -- () () -- -- -- | () -- () () --
-() () () -- () () -- -- () | () -- () () ()
-() () () -- () () -- () -- | () () -- -- --
-() () () -- () () -- () () | () () -- -- ()
-() () () -- () () () -- -- | () () -- () --
-() () () -- () () () -- () | () () -- () ()
-() () () -- () () () () -- | () () () -- --
-() () () -- () () () () () | () () () -- ()
-() () () () -- -- -- -- -- | -- () () () ()
-() () () () -- -- -- -- () | () -- -- -- --
-() () () () -- -- -- () -- | () -- -- -- ()
-() () () () -- -- -- () () | () -- -- () --
-() () () () -- -- () -- -- | () -- -- () ()
-() () () () -- -- () -- () | () -- () -- --
-() () () () -- -- () () -- | () -- () -- ()
-() () () () -- -- () () () | () -- () () --
-() () () () -- () -- -- -- | () -- () () ()
-() () () () -- () -- -- () | () () -- -- --
-() () () () -- () -- () -- | () () -- -- ()
-() () () () -- () -- () () | () () -- () --
-() () () () -- () () -- -- | () () -- () ()
-() () () () -- () () -- () | () () () -- --
-() () () () -- () () () -- | () () () -- ()
-() () () () -- () () () () | () () () () --
-() () () () () -- -- -- -- | () -- -- -- --
-() () () () () -- -- -- () | () -- -- -- ()
-() () () () () -- -- () -- | () -- -- () --
-() () () () () -- -- () () | () -- -- () ()
-() () () () () -- () -- -- | () -- () -- --
-() () () () () -- () -- () | () -- () -- ()
-() () () () () -- () () -- | () -- () () --
-() () () () () -- () () () | () -- () () ()
-() () () () () () -- -- -- | () () -- -- --
-() () () () () () -- -- () | () () -- -- ()
-() () () () () () -- () -- | () () -- () --
-() () () () () () -- () () | () () -- () ()
-() () () () () () () -- -- | () () () -- --
-() () () () () () () -- () | () () () -- ()
-() () () () () () () () -- | () () () () --
-() () () () () () () () () | () () () () ()
-
-
-
- -
-
- -
-
-
-
-
-

A Model of Computation.

That was a bit steep, let's formalize it and make it a little easier to work with.

-

First let's have a register of named values:

- -
-
-
-
-
-
In [87]:
-
-
-
R = {name: Void for name in 'Cin a3 a2 a1 a0 b3 b2 b1 b0 Cout'.split()}
-
- -
-
-
- -
-
-
-
-
-

Let's have a program of named expressions that give new values when evaluated in terms of the current values in R (this is just the same CIRCUITS, but feeding back the results into the "b" bits):

- -
-
-
-
-
-
In [88]:
-
-
-
P = {
-    'b0': sum0,
-    'b1': sum1,
-    'b2': sum2,
-    'b3': sum3,
-    'Cout': cout,
-}
-
- -
-
-
- -
-
-
-
-
-

One cycle of the machine means to evaluate each named expression in the program with the current values in the register.

- -
-
-
-
-
-
In [89]:
-
-
-
make_reify_reducer = lambda env: lambda form: value_of(reify(form, env))
-
-
-def cycle(program, register):
-    rr = make_reify_reducer(register)
-    return {bit: rr(expression) for bit, expression in program.iteritems()}
-
- -
-
-
- -
-
-
-
-
-

With all the register values at "zero" (Void) nothing happens.

- -
-
-
-
-
-
In [90]:
-
-
-
R.update(cycle(P, R))
-R
-
- -
-
-
- -
-
- - -
- -
Out[90]:
- - - - -
-
{'Cin': (()),
- 'Cout': (()),
- 'a0': (()),
- 'a1': (()),
- 'a2': (()),
- 'a3': (()),
- 'b0': (()),
- 'b1': (()),
- 'b2': (()),
- 'b3': (())}
-
- -
- -
-
- -
-
-
-
-
-

Let's make a nice display function to inspect our little adder computer.

- -
-
-
-
-
-
In [91]:
-
-
-
def show_as_int(*names):
-    '''
-    Return a function that converts a sequence of
-    named bits (as Void/Mark values) into a integer.
-    '''
-    def inner(register):
-        i, n = 0, 1
-        for name in names:
-            if not register[name]:
-                i += n
-            n <<= 1
-        return i
-    return inner
-
- -
-
-
- -
-
-
-
In [92]:
-
-
-
a_register = show_as_int('a0', 'a1', 'a2', 'a3')
-b_register = show_as_int('b0', 'b1', 'b2', 'b3')
-
-
-def show_computer_state(R):
-    print 'a: %-3i b: %-3i Cin: %-3i Cout: %-3i' % (
-        a_register(R),
-        b_register(R),
-        int(not R['Cin']),
-        int(not R['Cout']),
-    )
-
- -
-
-
- -
-
-
-
In [93]:
-
-
-
show_computer_state(R)
-
- -
-
-
- -
-
- - -
- -
- - -
-
a: 0   b: 0   Cin: 0   Cout: 0  
-
-
-
- -
-
- -
-
-
-
-
-

Let's set one bit to true (Mark-valued in the chosen convention. We could have Void be true but we would have to form the circuit expressions differently.)

- -
-
-
-
-
-
In [94]:
-
-
-
R['a0'] = Mark
-
- -
-
-
- -
-
-
-
-
-

Now let's count to twenty.

- -
-
-
-
-
-
In [95]:
-
-
-
for _ in range(20):
-    show_computer_state(R)
-    R.update(cycle(P, R))
-
- -
-
-
- -
-
- - -
- -
- - -
-
a: 1   b: 0   Cin: 0   Cout: 0  
-a: 1   b: 1   Cin: 0   Cout: 0  
-a: 1   b: 2   Cin: 0   Cout: 0  
-a: 1   b: 3   Cin: 0   Cout: 0  
-a: 1   b: 4   Cin: 0   Cout: 0  
-a: 1   b: 5   Cin: 0   Cout: 0  
-a: 1   b: 6   Cin: 0   Cout: 0  
-a: 1   b: 7   Cin: 0   Cout: 0  
-a: 1   b: 8   Cin: 0   Cout: 0  
-a: 1   b: 9   Cin: 0   Cout: 0  
-a: 1   b: 10  Cin: 0   Cout: 0  
-a: 1   b: 11  Cin: 0   Cout: 0  
-a: 1   b: 12  Cin: 0   Cout: 0  
-a: 1   b: 13  Cin: 0   Cout: 0  
-a: 1   b: 14  Cin: 0   Cout: 0  
-a: 1   b: 15  Cin: 0   Cout: 0  
-a: 1   b: 0   Cin: 0   Cout: 1  
-a: 1   b: 1   Cin: 0   Cout: 0  
-a: 1   b: 2   Cin: 0   Cout: 0  
-a: 1   b: 3   Cin: 0   Cout: 0  
-
-
-
- -
-
- -
-
-
-
-
-

You can see that at the sixteenth step the "Cout" carry bit is true and the count cycles back to zero.

- -
-
-
-
-
-
In [96]:
-
-
-
# Reset the register.
-R = {name: Void for name in 'Cin a3 a2 a1 a0 b3 b2 b1 b0 Cout'.split()}
-
-# Count by three.
-R['a0'] = R['a1'] = Mark
-
-# Print out twenty cycles.
-for _ in range(20):
-    show_computer_state(R)
-    R.update(cycle(P, R))
-
- -
-
-
- -
-
- - -
- -
- - -
-
a: 3   b: 0   Cin: 0   Cout: 0  
-a: 3   b: 3   Cin: 0   Cout: 0  
-a: 3   b: 6   Cin: 0   Cout: 0  
-a: 3   b: 9   Cin: 0   Cout: 0  
-a: 3   b: 12  Cin: 0   Cout: 0  
-a: 3   b: 15  Cin: 0   Cout: 0  
-a: 3   b: 2   Cin: 0   Cout: 1  
-a: 3   b: 5   Cin: 0   Cout: 0  
-a: 3   b: 8   Cin: 0   Cout: 0  
-a: 3   b: 11  Cin: 0   Cout: 0  
-a: 3   b: 14  Cin: 0   Cout: 0  
-a: 3   b: 1   Cin: 0   Cout: 1  
-a: 3   b: 4   Cin: 0   Cout: 0  
-a: 3   b: 7   Cin: 0   Cout: 0  
-a: 3   b: 10  Cin: 0   Cout: 0  
-a: 3   b: 13  Cin: 0   Cout: 0  
-a: 3   b: 0   Cin: 0   Cout: 1  
-a: 3   b: 3   Cin: 0   Cout: 0  
-a: 3   b: 6   Cin: 0   Cout: 0  
-a: 3   b: 9   Cin: 0   Cout: 0  
-
-
-
- -
-
- -
-
-
-
-
-

You can see that the "b" bits are indeed counting by threes: 0, 3, 6, 9, 12, 15 & carry, 2, 5, 8, 11, 14 & carry, 1, 4, 7, 10, 13 & carry, 0, 3, 6, 9, ...

-

This is my basic model for computation: A register, a program, and a cycle function. Note that reducing the form on each cycle isn't necessary, we can run the cycles and just reify() without reducing and we get new circuits that define bits in terms of the register values N cycles in the past.

- -
-
-
-
-
-
-
-

Simple One-Dimensional Cellular Automaton

-
-
-
-
-
-
In [97]:
-
-
-
# Universe
-U = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz'
-
-
-# Register.
-R = {name: Void for name in U}
-
-
-# A program to XOR each bit with its neighbor, wrapping at the edge.
-P = {
-    name: xor(name, U[(U.index(name) + 1) % len(U)])
-    for name in U
-}
-
-
-def show(reg):
-    '''Simple visualization of the register.'''
-    print ''.join('.0'[not reg[name]] for name in U)
-
-
-# Set one "bit" in the register.
-R[U[-1]] = Mark
-
-
-# Run through some cycles.
-for _ in range(100):
-    show(R)
-    R.update(cycle(P, R))
-
- -
-
-
- -
-
- - -
- -
- - -
-
...................................................0
-..................................................00
-.................................................0.0
-................................................0000
-...............................................0...0
-..............................................00..00
-.............................................0.0.0.0
-............................................00000000
-...........................................0.......0
-..........................................00......00
-.........................................0.0.....0.0
-........................................0000....0000
-.......................................0...0...0...0
-......................................00..00..00..00
-.....................................0.0.0.0.0.0.0.0
-....................................0000000000000000
-...................................0...............0
-..................................00..............00
-.................................0.0.............0.0
-................................0000............0000
-...............................0...0...........0...0
-..............................00..00..........00..00
-.............................0.0.0.0.........0.0.0.0
-............................00000000........00000000
-...........................0.......0.......0.......0
-..........................00......00......00......00
-.........................0.0.....0.0.....0.0.....0.0
-........................0000....0000....0000....0000
-.......................0...0...0...0...0...0...0...0
-......................00..00..00..00..00..00..00..00
-.....................0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0
-....................00000000000000000000000000000000
-...................0...............................0
-..................00..............................00
-.................0.0.............................0.0
-................0000............................0000
-...............0...0...........................0...0
-..............00..00..........................00..00
-.............0.0.0.0.........................0.0.0.0
-............00000000........................00000000
-...........0.......0.......................0.......0
-..........00......00......................00......00
-.........0.0.....0.0.....................0.0.....0.0
-........0000....0000....................0000....0000
-.......0...0...0...0...................0...0...0...0
-......00..00..00..00..................00..00..00..00
-.....0.0.0.0.0.0.0.0.................0.0.0.0.0.0.0.0
-....0000000000000000................0000000000000000
-...0...............0...............0...............0
-..00..............00..............00..............00
-.0.0.............0.0.............0.0.............0.0
-0000............0000............0000............0000
-...0...........0...0...........0...0...........0....
-..00..........00..00..........00..00..........00....
-.0.0.........0.0.0.0.........0.0.0.0.........0.0....
-0000........00000000........00000000........0000....
-...0.......0.......0.......0.......0.......0...0...0
-..00......00......00......00......00......00..00..00
-.0.0.....0.0.....0.0.....0.0.....0.0.....0.0.0.0.0.0
-0000....0000....0000....0000....0000....000000000000
-...0...0...0...0...0...0...0...0...0...0............
-..00..00..00..00..00..00..00..00..00..00............
-.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0............
-0000000000000000000000000000000000000000............
-.......................................0...........0
-......................................00..........00
-.....................................0.0.........0.0
-....................................0000........0000
-...................................0...0.......0...0
-..................................00..00......00..00
-.................................0.0.0.0.....0.0.0.0
-................................00000000....00000000
-...............................0.......0...0.......0
-..............................00......00..00......00
-.............................0.0.....0.0.0.0.....0.0
-............................0000....00000000....0000
-...........................0...0...0.......0...0...0
-..........................00..00..00......00..00..00
-.........................0.0.0.0.0.0.....0.0.0.0.0.0
-........................000000000000....000000000000
-.......................0...........0...0...........0
-......................00..........00..00..........00
-.....................0.0.........0.0.0.0.........0.0
-....................0000........00000000........0000
-...................0...0.......0.......0.......0...0
-..................00..00......00......00......00..00
-.................0.0.0.0.....0.0.....0.0.....0.0.0.0
-................00000000....0000....0000....00000000
-...............0.......0...0...0...0...0...0.......0
-..............00......00..00..00..00..00..00......00
-.............0.0.....0.0.0.0.0.0.0.0.0.0.0.0.....0.0
-............0000....000000000000000000000000....0000
-...........0...0...0.......................0...0...0
-..........00..00..00......................00..00..00
-.........0.0.0.0.0.0.....................0.0.0.0.0.0
-........000000000000....................000000000000
-.......0...........0...................0...........0
-......00..........00..................00..........00
-.....0.0.........0.0.................0.0.........0.0
-....0000........0000................0000........0000
-
-
-
- -
-
- -
-
-
-
-
-

A More Efficient Implementation

Before building larger "computers" I want to switch to a more efficient implementation based on a register as a set of names that are currently Mark-valued, and a set_solve() function that evaluates a form in terms of such a set, and assuming all other names are Void-valued.

- -
-
-
-
-
-
In [98]:
-
-
-
def set_solve(form, marks):
-    '''
-    Given a form and a set of names that are Marks assume all other names
-    in the form are Void and reduce to basic value (Mark or Void.)
-    '''
-    return (
-        (Void, Mark)[form in marks]
-        if isinstance(form, basestring)
-        else _set_solve(form, marks)
-    )
-
-
-def _set_solve(form, marks):
-    for inner in form:
-        if isinstance(inner, basestring):
-            if inner in marks: 
-                return Void
-            continue
-        if not _set_solve(inner, marks): # Mark
-            return Void
-    return Mark
-
- -
-
-
- -
-
-
-
In [99]:
-
-
-
A = F(a, (b, (c,)))
-print A
-print set_solve(A, {a})
-print set_solve(A, {b})
-print set_solve(A, {c})
-
- -
-
-
- -
-
- - -
- -
- - -
-
(((c) b) a)
-(())
-()
-(())
-
-
-
- -
-
- -
-
-
-
-
-

To calculate the new R first collect all the names in R that are not mentioned in P (and so cannot be -set to Void by it) then add the names evaluated by solving P's expressions with the marks in R.

- -
-
-
-
-
-
In [100]:
-
-
-
def set_cycle(R, P):
-    return R.difference(P).union(
-        signal
-        for signal, expression in P.iteritems()
-        if not set_solve(expression, R)
-        )
-
- -
-
-
- -
-
-
-
In [101]:
-
-
-
# Universe
-U = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz'
-
-
-# Register.
-R = {U[-1]}
-
-
-# A program to XOR each bit with its neighbor, wrapping at the edge.
-P = {
-    name: xor(name, U[(U.index(name) + 1) % len(U)])
-    for name in U
-}
-
-
-def show(reg):
-    '''Simple visualization of the register.'''
-    print ''.join('.0'[name in reg] for name in U)
-
-
-# Run through some cycles.
-for _ in range(100):
-    show(R)
-    R = set_cycle(R, P)
-
- -
-
-
- -
-
- - -
- -
- - -
-
...................................................0
-..................................................00
-.................................................0.0
-................................................0000
-...............................................0...0
-..............................................00..00
-.............................................0.0.0.0
-............................................00000000
-...........................................0.......0
-..........................................00......00
-.........................................0.0.....0.0
-........................................0000....0000
-.......................................0...0...0...0
-......................................00..00..00..00
-.....................................0.0.0.0.0.0.0.0
-....................................0000000000000000
-...................................0...............0
-..................................00..............00
-.................................0.0.............0.0
-................................0000............0000
-...............................0...0...........0...0
-..............................00..00..........00..00
-.............................0.0.0.0.........0.0.0.0
-............................00000000........00000000
-...........................0.......0.......0.......0
-..........................00......00......00......00
-.........................0.0.....0.0.....0.0.....0.0
-........................0000....0000....0000....0000
-.......................0...0...0...0...0...0...0...0
-......................00..00..00..00..00..00..00..00
-.....................0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0
-....................00000000000000000000000000000000
-...................0...............................0
-..................00..............................00
-.................0.0.............................0.0
-................0000............................0000
-...............0...0...........................0...0
-..............00..00..........................00..00
-.............0.0.0.0.........................0.0.0.0
-............00000000........................00000000
-...........0.......0.......................0.......0
-..........00......00......................00......00
-.........0.0.....0.0.....................0.0.....0.0
-........0000....0000....................0000....0000
-.......0...0...0...0...................0...0...0...0
-......00..00..00..00..................00..00..00..00
-.....0.0.0.0.0.0.0.0.................0.0.0.0.0.0.0.0
-....0000000000000000................0000000000000000
-...0...............0...............0...............0
-..00..............00..............00..............00
-.0.0.............0.0.............0.0.............0.0
-0000............0000............0000............0000
-...0...........0...0...........0...0...........0....
-..00..........00..00..........00..00..........00....
-.0.0.........0.0.0.0.........0.0.0.0.........0.0....
-0000........00000000........00000000........0000....
-...0.......0.......0.......0.......0.......0...0...0
-..00......00......00......00......00......00..00..00
-.0.0.....0.0.....0.0.....0.0.....0.0.....0.0.0.0.0.0
-0000....0000....0000....0000....0000....000000000000
-...0...0...0...0...0...0...0...0...0...0............
-..00..00..00..00..00..00..00..00..00..00............
-.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0.0............
-0000000000000000000000000000000000000000............
-.......................................0...........0
-......................................00..........00
-.....................................0.0.........0.0
-....................................0000........0000
-...................................0...0.......0...0
-..................................00..00......00..00
-.................................0.0.0.0.....0.0.0.0
-................................00000000....00000000
-...............................0.......0...0.......0
-..............................00......00..00......00
-.............................0.0.....0.0.0.0.....0.0
-............................0000....00000000....0000
-...........................0...0...0.......0...0...0
-..........................00..00..00......00..00..00
-.........................0.0.0.0.0.0.....0.0.0.0.0.0
-........................000000000000....000000000000
-.......................0...........0...0...........0
-......................00..........00..00..........00
-.....................0.0.........0.0.0.0.........0.0
-....................0000........00000000........0000
-...................0...0.......0.......0.......0...0
-..................00..00......00......00......00..00
-.................0.0.0.0.....0.0.....0.0.....0.0.0.0
-................00000000....0000....0000....00000000
-...............0.......0...0...0...0...0...0.......0
-..............00......00..00..00..00..00..00......00
-.............0.0.....0.0.0.0.0.0.0.0.0.0.0.0.....0.0
-............0000....000000000000000000000000....0000
-...........0...0...0.......................0...0...0
-..........00..00..00......................00..00..00
-.........0.0.0.0.0.0.....................0.0.0.0.0.0
-........000000000000....................000000000000
-.......0...........0...................0...........0
-......00..........00..................00..........00
-.....0.0.........0.0.................0.0.........0.0
-....0000........0000................0000........0000
-
-
-
- -
-
- -
-
-
-
In [102]:
-
-
-
def set_show_as_int(*names):
-    def inner(register):
-        i, n = 0, 1
-        for name in names:
-            if name in register:
-                i += n
-            n <<= 1
-        return i
-    return inner
-
- -
-
-
- -
-
-
-
-
-

Each-Way as If... Then...

-
-
-
-
-
-
In [103]:
-
-
-
def ifte(predicate, true, false):
-    return F(
-        ((predicate,), true),
-        ( predicate  , false),
-    )
-
-
-E = ifte(a, b, c)
-
-
-truth_table(E)
-
- -
-
-
- -
-
- - -
- -
- - -
-
(((a) b) (a c))
- a  b  c | Value
----------+------
-         | 
-      () | ()
-   ()    | 
-   () () | ()
-()       | 
-()    () | 
-() ()    | ()
-() () () | ()
-
-
-
- -
-
- -
-
-
-
-
-

If a is Mark-valued the value of the whole form is that of b, but if a is Void-valued the value of the whole form is that of c.

- -
w/ a = ()
-
-((( a) b) ( a c))
-(((()) b) (() c))
-((     b) (()  ))
-((     b)       )
-       b
-
-w/ a =
-
-(((a) b) (a c))
-((( ) b) (  c))
-((( )  ) (  c))
-(        (  c))
-            c
- -
-
-
-
-
-
-
-

Flip-Flops for Memory

-
-
-
-
-
-
In [104]:
-
-
-
def flip_flop(q, reset, set_):
-    return F(reset, (q, set_))
-
-q, r, s = 'qrs'
-E = flip_flop(q, r, s)
-truth_table(E)
-
- -
-
-
- -
-
- - -
- -
- - -
-
((q s) r)
- q  r  s | Value
----------+------
-         | 
-      () | ()
-   ()    | 
-   () () | 
-()       | ()
-()    () | ()
-() ()    | 
-() () () | 
-
-
-
- -
-
- -
-
-
-
-
-

This is a form that can be used in a circuit to "remember" a value.

- -
w/ r = ()
-
-((q s)  r)
-((q s) ())
-(      ())
-
-w/ s = (), r = ___
-
-((q  s) r)
-((q ())  )
-((  ())  )
-(        )
-
-w/ s = ___, r = ___
-
-((q s) r)
-((q  )  )
-  q
-
-
-

If both are Void then the form is just q, if r is Mark then the form is Void, otherwise if s is Mark the form becomes Mark. This is called a "flip-flop" circuit, and it comprises a simple machine to remember one bit.

-

Consider a simple computer:

- -
-
-
-
-
-
In [105]:
-
-
-
U = q, r, s = 'qrs'
-
-P = {
-    q: flip_flop(q, r, s),
-    r: Void,
-    s: Void,
-}
-
-R = set()  # Initially all signals are off, Void-valued.
-
- -
-
-
- -
-
-
-
In [106]:
-
-
-
bools_of = lambda universe: lambda register: (name in register for name in universe)
-
-
-def simple_show(universe):
-    B = bools_of(universe)
-    def _shower(register):
-        print ''.join('.0'[b] for b in B(register))
-    return _shower
-
- -
-
-
- -
-
-
-
In [107]:
-
-
-
show = simple_show(U)
-show(R)
-
- -
-
-
- -
-
- - -
- -
- - -
-
...
-
-
-
- -
-
- -
-
-
-
In [108]:
-
-
-
def SET(R):
-    R |= {s}
-    show(R)
-    return set_cycle(R, P)
-
-
-def RESET(R):
-    R |= {r}
-    show(R)
-    return set_cycle(R, P)
-
- -
-
-
- -
-
-
-
In [109]:
-
-
-
print U
-show(R) ; R = set_cycle(R, P)
-show(R) ; R = set_cycle(R, P)
-show(R) ; R = set_cycle(R, P)
-
-R = SET(R)
-
-show(R) ; R = set_cycle(R, P)
-show(R) ; R = set_cycle(R, P)
-
-R = SET(R)
-
-show(R) ; R = set_cycle(R, P)
-show(R) ; R = set_cycle(R, P)
-
-R = RESET(R)
-
-show(R) ; R = set_cycle(R, P)
-show(R) ; R = set_cycle(R, P)
-
-R = RESET(R)
-
-show(R) ; R = set_cycle(R, P)
-show(R) ; R = set_cycle(R, P)
-
- -
-
-
- -
-
- - -
- -
- - -
-
qrs
-...
-...
-...
-..0
-0..
-0..
-0.0
-0..
-0..
-00.
-...
-...
-.0.
-...
-...
-
-
-
- -
-
- -
-
-
-
-
-

You can see that q is stable unless s or r set or reset it.

- -
-
-
-
-
-
-
-

Using Flip-Flops and If...Then...Else... to make RAM

We can use the system we have developed so far to build addressable RAM.

- -
-
-
-
-
-
In [110]:
-
-
-
# Width in bits of the DATA registers.
-WIDTH = 2
-
-# Width in bits of the ADDR registers.
-LENGTH = 3  # Actual length 2**LENGTH
-
- -
-
-
- -
-
-
-
In [111]:
-
-
-
P = {}
-
- -
-
-
- -
-
-
-
-
-

We'll assume a single WRITE bit that sets a RAM location determined by the ADDR sub-register to the contents of the DATA sub-register.

- -
-
-
-
-
-
In [112]:
-
-
-
WRITE = 'WRITE'
-
- -
-
-
- -
-
-
-
In [113]:
-
-
-
# Address register.
-ADDR = ['addr_%i' % i for i in range(LENGTH)]
-ADDR
-
- -
-
-
- -
-
- - -
- -
Out[113]:
- - - - -
-
['addr_0', 'addr_1', 'addr_2']
-
- -
- -
-
- -
-
-
-
In [114]:
-
-
-
# Data register.
-DATA = ['a%i' % i for i in range(WIDTH)]
-DATA
-
- -
-
-
- -
-
- - -
- -
Out[114]:
- - - - -
-
['a0', 'a1']
-
- -
- -
-
- -
-
-
-
-
-

We can recognize which RAM location we want to address by using the expressions for each row from above to create a predicate for each location that depends on the ADDR bits.

- -
-
-
-
-
-
In [115]:
-
-
-
def make_ram(program, addrs, data, width, write):
-    RAM = []
-    for addr, env in enumerate(environments_of_variables(*addrs)):
-
-        addr_predicate = F((name,) if env[name] else name for name in env)
-
-        predicate = and_(write, addr_predicate)
-
-        for bit in range(width):
-            ram = 'RAM_%i_%i' % (addr, bit)
-            RAM.append(ram)
-            program[ram] = simplify(ifte(predicate, data[bit], ram))
-
-    return RAM
-
- -
-
-
- -
-
-
-
In [116]:
-
-
-
RAM = make_ram(P, ADDR, DATA, WIDTH, WRITE)
-RAM
-
- -
-
-
- -
-
- - -
- -
Out[116]:
- - - - -
-
['RAM_0_0',
- 'RAM_0_1',
- 'RAM_1_0',
- 'RAM_1_1',
- 'RAM_2_0',
- 'RAM_2_1',
- 'RAM_3_0',
- 'RAM_3_1',
- 'RAM_4_0',
- 'RAM_4_1',
- 'RAM_5_0',
- 'RAM_5_1',
- 'RAM_6_0',
- 'RAM_6_1',
- 'RAM_7_0',
- 'RAM_7_1']
-
- -
- -
-
- -
-
-
-
In [117]:
-
-
-
P
-
- -
-
-
- -
-
- - -
- -
Out[117]:
- - - - -
-
{'RAM_0_0': (((((addr_0) (addr_1) (addr_2)) (WRITE)) RAM_0_0) (((addr_0) (addr_1) (addr_2)) (WRITE) a0)),
- 'RAM_0_1': (((((addr_0) (addr_1) (addr_2)) (WRITE)) RAM_0_1) (((addr_0) (addr_1) (addr_2)) (WRITE) a1)),
- 'RAM_1_0': (((((addr_0) (addr_1) addr_2) (WRITE)) RAM_1_0) (((addr_0) (addr_1) addr_2) (WRITE) a0)),
- 'RAM_1_1': (((((addr_0) (addr_1) addr_2) (WRITE)) RAM_1_1) (((addr_0) (addr_1) addr_2) (WRITE) a1)),
- 'RAM_2_0': (((((addr_0) (addr_2) addr_1) (WRITE)) RAM_2_0) (((addr_0) (addr_2) addr_1) (WRITE) a0)),
- 'RAM_2_1': (((((addr_0) (addr_2) addr_1) (WRITE)) RAM_2_1) (((addr_0) (addr_2) addr_1) (WRITE) a1)),
- 'RAM_3_0': (((((addr_0) addr_1 addr_2) (WRITE)) RAM_3_0) (((addr_0) addr_1 addr_2) (WRITE) a0)),
- 'RAM_3_1': (((((addr_0) addr_1 addr_2) (WRITE)) RAM_3_1) (((addr_0) addr_1 addr_2) (WRITE) a1)),
- 'RAM_4_0': (((((addr_1) (addr_2) addr_0) (WRITE)) RAM_4_0) (((addr_1) (addr_2) addr_0) (WRITE) a0)),
- 'RAM_4_1': (((((addr_1) (addr_2) addr_0) (WRITE)) RAM_4_1) (((addr_1) (addr_2) addr_0) (WRITE) a1)),
- 'RAM_5_0': (((((addr_1) addr_0 addr_2) (WRITE)) RAM_5_0) (((addr_1) addr_0 addr_2) (WRITE) a0)),
- 'RAM_5_1': (((((addr_1) addr_0 addr_2) (WRITE)) RAM_5_1) (((addr_1) addr_0 addr_2) (WRITE) a1)),
- 'RAM_6_0': (((((addr_2) addr_0 addr_1) (WRITE)) RAM_6_0) (((addr_2) addr_0 addr_1) (WRITE) a0)),
- 'RAM_6_1': (((((addr_2) addr_0 addr_1) (WRITE)) RAM_6_1) (((addr_2) addr_0 addr_1) (WRITE) a1)),
- 'RAM_7_0': ((((WRITE) (addr_0 addr_1 addr_2)) RAM_7_0) ((WRITE) (addr_0 addr_1 addr_2) a0)),
- 'RAM_7_1': ((((WRITE) (addr_0 addr_1 addr_2)) RAM_7_1) ((WRITE) (addr_0 addr_1 addr_2) a1))}
-
- -
- -
-
- -
-
-
-
In [118]:
-
-
-
E = P['RAM_0_0']
-E
-
- -
-
-
- -
-
- - -
- -
Out[118]:
- - - - -
-
(((((addr_0) (addr_1) (addr_2)) (WRITE)) RAM_0_0) (((addr_0) (addr_1) (addr_2)) (WRITE) a0))
-
- -
- -
-
- -
-
-
-
-
-

Note that if the WRITE bit is unset then each RAM bit is just set to itself.

- -
-
-
-
-
-
In [119]:
-
-
-
simplify(E, exclude={'WRITE'})
-
- -
-
-
- -
-
- - -
- -
Out[119]:
- - - - -
-
'RAM_0_0'
-
- -
- -
-
- -
-
-
-
-
-

But if the WRITE bit is set then each RAM location still depends on the -per-location-predicate.

- -
-
-
-
-
-
In [120]:
-
-
-
simplify(E, with_mark='WRITE')
-
- -
-
-
- -
-
- - -
- -
Out[120]:
- - - - -
-
((((addr_0) (addr_1) (addr_2)) a0) ((addr_0) (addr_1) (addr_2) RAM_0_0))
-
- -
- -
-
- -
-
-
-
In [121]:
-
-
-
def make_accumulator(program, addrs, data, width, read, alts):
-
-    addr_predicates = [
-        F((name,) if env[name] else name for name in env)
-        for env in environments_of_variables(*addrs)
-    ]
-
-    for bit in range(width):
-        a = data[bit]
-        alt = alts[bit]
-        foo = Void
-        for addr, predicate in enumerate(addr_predicates):
-            ram = 'RAM_%i_%i' % (addr, bit)
-            foo = (ifte(predicate, ram, foo))
-        program[a] = ifte(read, foo, alt)
-
- -
-
-
- -
-
-
-
In [122]:
-
-
-
p = {}
-make_accumulator(p, ADDR, DATA, WIDTH, 'READ', DATA)
-p
-
- -
-
-
- -
-
- - -
- -
Out[122]:
- - - - -
-
{'a0': ((((((((((((((((((((((addr_0) (addr_1) (addr_2)))) RAM_0_0) ((((addr_0) (addr_1) (addr_2))) (()))) (((addr_0) (addr_1) addr_2))) (((((addr_0) (addr_1) addr_2))) RAM_1_0)) (((addr_0) (addr_2) addr_1))) (((((addr_0) (addr_2) addr_1))) RAM_2_0)) (((addr_0) addr_1 addr_2))) (((((addr_0) addr_1 addr_2))) RAM_3_0)) (((addr_1) (addr_2) addr_0))) (((((addr_1) (addr_2) addr_0))) RAM_4_0)) (((addr_1) addr_0 addr_2))) (((((addr_1) addr_0 addr_2))) RAM_5_0)) (((addr_2) addr_0 addr_1))) (((((addr_2) addr_0 addr_1))) RAM_6_0)) ((addr_0 addr_1 addr_2))) ((((addr_0 addr_1 addr_2))) RAM_7_0)) (READ)) (READ a0)),
- 'a1': ((((((((((((((((((((((addr_0) (addr_1) (addr_2)))) RAM_0_1) ((((addr_0) (addr_1) (addr_2))) (()))) (((addr_0) (addr_1) addr_2))) (((((addr_0) (addr_1) addr_2))) RAM_1_1)) (((addr_0) (addr_2) addr_1))) (((((addr_0) (addr_2) addr_1))) RAM_2_1)) (((addr_0) addr_1 addr_2))) (((((addr_0) addr_1 addr_2))) RAM_3_1)) (((addr_1) (addr_2) addr_0))) (((((addr_1) (addr_2) addr_0))) RAM_4_1)) (((addr_1) addr_0 addr_2))) (((((addr_1) addr_0 addr_2))) RAM_5_1)) (((addr_2) addr_0 addr_1))) (((((addr_2) addr_0 addr_1))) RAM_6_1)) ((addr_0 addr_1 addr_2))) ((((addr_0 addr_1 addr_2))) RAM_7_1)) (READ)) (READ a1))}
-
- -
- -
-
- -
-
-
-
In [123]:
-
-
-
E = p[DATA[0]]
-E
-
- -
-
-
- -
-
- - -
- -
Out[123]:
- - - - -
-
((((((((((((((((((((((addr_0) (addr_1) (addr_2)))) RAM_0_0) ((((addr_0) (addr_1) (addr_2))) (()))) (((addr_0) (addr_1) addr_2))) (((((addr_0) (addr_1) addr_2))) RAM_1_0)) (((addr_0) (addr_2) addr_1))) (((((addr_0) (addr_2) addr_1))) RAM_2_0)) (((addr_0) addr_1 addr_2))) (((((addr_0) addr_1 addr_2))) RAM_3_0)) (((addr_1) (addr_2) addr_0))) (((((addr_1) (addr_2) addr_0))) RAM_4_0)) (((addr_1) addr_0 addr_2))) (((((addr_1) addr_0 addr_2))) RAM_5_0)) (((addr_2) addr_0 addr_1))) (((((addr_2) addr_0 addr_1))) RAM_6_0)) ((addr_0 addr_1 addr_2))) ((((addr_0 addr_1 addr_2))) RAM_7_0)) (READ)) (READ a0))
-
- -
- -
-
- -
-
-
-
In [124]:
-
-
-
simplify(E, with_mark='READ')
-
- -
-
-
- -
-
- - -
- -
Out[124]:
- - - - -
-
((((((((((((((((((addr_0) (addr_1) (addr_2)) RAM_0_0) ((addr_0) (addr_1) (addr_2))) (addr_0) (addr_1) addr_2) (((addr_0) (addr_1) addr_2) RAM_1_0)) (addr_0) (addr_2) addr_1) (((addr_0) (addr_2) addr_1) RAM_2_0)) (addr_0) addr_1 addr_2) (((addr_0) addr_1 addr_2) RAM_3_0)) (addr_1) (addr_2) addr_0) (((addr_1) (addr_2) addr_0) RAM_4_0)) (addr_1) addr_0 addr_2) (((addr_1) addr_0 addr_2) RAM_5_0)) (addr_2) addr_0 addr_1) (((addr_2) addr_0 addr_1) RAM_6_0)) addr_0 addr_1 addr_2) ((addr_0 addr_1 addr_2) RAM_7_0))
-
- -
- -
-
- -
-
-
-
In [125]:
-
-
-
simplify(E, {'READ'})
-
- -
-
-
- -
-
- - -
- -
Out[125]:
- - - - -
-
'a0'
-
- -
- -
-
- -
-
-
-
In [126]:
-
-
-
each_way(E, 'a0')
-
- -
-
-
- -
-
- - -
- -
Out[126]:
- - - - -
-
((((((((((((((((((((((addr_0) (addr_1) (addr_2)) RAM_0_0) ((addr_0) (addr_1) (addr_2))) (addr_0) (addr_1) addr_2) (((addr_0) (addr_1) addr_2) RAM_1_0)) (addr_0) (addr_2) addr_1) (((addr_0) (addr_2) addr_1) RAM_2_0)) (addr_0) addr_1 addr_2) (((addr_0) addr_1 addr_2) RAM_3_0)) (addr_1) (addr_2) addr_0) (((addr_1) (addr_2) addr_0) RAM_4_0)) (addr_1) addr_0 addr_2) (((addr_1) addr_0 addr_2) RAM_5_0)) (addr_2) addr_0 addr_1) (((addr_2) addr_0 addr_1) RAM_6_0)) addr_0 addr_1 addr_2) ((addr_0 addr_1 addr_2) RAM_7_0)) (READ)) (READ)) a0) ((((addr_0 addr_1 addr_2) RAM_7_0) (RAM_6_0 addr_0 addr_1 addr_2)) (READ) (a0)))
-
- -
- -
-
- -
-
-
-
In [127]:
-
-
-
each_way(E, 'WRITE')
-
- -
-
-
- -
-
- - -
- -
Out[127]:
- - - - -
-
((((((((((((((((((((((addr_0) (addr_1) (addr_2)) RAM_0_0) ((addr_0) (addr_1) (addr_2))) (addr_0) (addr_1) addr_2) (((addr_0) (addr_1) addr_2) RAM_1_0)) (addr_0) (addr_2) addr_1) (((addr_0) (addr_2) addr_1) RAM_2_0)) (addr_0) addr_1 addr_2) (((addr_0) addr_1 addr_2) RAM_3_0)) (addr_1) (addr_2) addr_0) (((addr_1) (addr_2) addr_0) RAM_4_0)) (addr_1) addr_0 addr_2) (((addr_1) addr_0 addr_2) RAM_5_0)) (addr_2) addr_0 addr_1) (((addr_2) addr_0 addr_1) RAM_6_0)) addr_0 addr_1 addr_2) ((addr_0 addr_1 addr_2) RAM_7_0)) (READ)) (READ a0)) WRITE) ((((((addr_0 addr_1 addr_2) RAM_7_0) (RAM_6_0 addr_0 addr_1 addr_2)) (READ)) (READ a0)) (WRITE)))
-
- -
- -
-
- -
-
-
-
In [128]:
-
-
-
each_way(E, 'addr_0')
-
- -
-
-
- -
-
- - -
- -
Out[128]:
- - - - -
-
((((((((((((((addr_1) (addr_2)) RAM_4_0) ((addr_1) (addr_2) RAM_3_0)) (addr_1) addr_2) (((addr_1) addr_2) RAM_5_0)) (addr_2) addr_1) (((addr_2) addr_1) RAM_6_0)) addr_1 addr_2) ((addr_1 addr_2) RAM_7_0)) (READ)) (READ a0)) addr_0) ((((READ) RAM_7_0) (READ a0)) (addr_0)))
-
- -
- -
-
- -
-
-
-
In [129]:
-
-
-
each_way(E, 'a0')
-
- -
-
-
- -
-
- - -
- -
Out[129]:
- - - - -
-
((((((((((((((((((((((addr_0) (addr_1) (addr_2)) RAM_0_0) ((addr_0) (addr_1) (addr_2))) (addr_0) (addr_1) addr_2) (((addr_0) (addr_1) addr_2) RAM_1_0)) (addr_0) (addr_2) addr_1) (((addr_0) (addr_2) addr_1) RAM_2_0)) (addr_0) addr_1 addr_2) (((addr_0) addr_1 addr_2) RAM_3_0)) (addr_1) (addr_2) addr_0) (((addr_1) (addr_2) addr_0) RAM_4_0)) (addr_1) addr_0 addr_2) (((addr_1) addr_0 addr_2) RAM_5_0)) (addr_2) addr_0 addr_1) (((addr_2) addr_0 addr_1) RAM_6_0)) addr_0 addr_1 addr_2) ((addr_0 addr_1 addr_2) RAM_7_0)) (READ)) (READ)) a0) ((((addr_0 addr_1 addr_2) RAM_7_0) (RAM_6_0 addr_0 addr_1 addr_2)) (READ) (a0)))
-
- -
- -
-
- -
-
-
-
In [130]:
-
-
-
simplify(each_way(E, 'WRITE'), with_mark='WRITE')
-
- -
-
-
- -
-
- - -
- -
Out[130]:
- - - - -
-
(((((addr_0 addr_1 addr_2) RAM_7_0) (RAM_6_0 addr_0 addr_1 addr_2)) (READ)) (READ a0))
-
- -
- -
-
- -
-
-
-
-
-

, Sorting Networks for routing, more basic functions.

-

Eventually: Orchestration with Joy.

- -
-
-
-
-
-
-
-

FIN for now.

-
-
-
-
-
-
-
-

Appendix: Demonstration of A(AB) = A(B)

The rule A(AB) = A(B) is the powerhouse of LoF.

-

w/ A = ()

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

w/ A =

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

Be aware of the recursive nature of this rule:

- -
A(...(...(A B)))
-A(.A.(...(A B)))
-A(.A.(.A.(A B)))
-A(.A.(.A.(  B)))
-A(.A.(...(  B)))
-A(...(...(  B)))
-
-
-

There is this too:

- -
(A)(...(...(... A B)))
-(A)((A)(...(... A B)))
-(A)((A)((A)(... A B)))
-(A)((A)((A)((A) A B)))
-(A)((A)((A)(( ) A B)))
-(A)((A)(...(( )    )))
-(A)(...(...         ))
-
-
-

Summarized:

- -
(A)(...(...(...  A )))
-(A)(...(...(... () )))
-(A)(...(...         ))
- -
-
-
-
-
-
-
-

Appendix: Reduce String Expressions by Substitution

Given a string form of an arithmetic expression (in other words a string that consists of only balanced pairs of parentheses) we can reduce it to its Mark/Void value by substitution to a fixed-point.

- -
-
-
-
-
-
In [131]:
-
-
-
# Translate the LoF Arithmetic rules to string substitution rules.
-reduce_string = lambda s: (
-    s
-    .replace('()()', '()')
-    .replace('(())', '')
-)
-
- -
-
-
- -
-
-
-
In [132]:
-
-
-
def to_fixed_point(initial_value, F, limit=10000):
-    '''Do value = F(value) until value == F(value).'''
-    
-    next_value = F(initial_value)
-    
-    while next_value != initial_value:
-        
-        if not limit:  # A safety mechanism.  Bail out after N iterations.
-            raise RuntimeError('Reached limit of allowed iterations without finding fixed point.')
-        limit -= 1
-        
-        initial_value = next_value
-        next_value = F(initial_value)
-    
-    return initial_value
-
- -
-
-
- -
-
-
-
In [133]:
-
-
-
from operator import add
-
-
-def dyck_language(left, right=0, t='', A='(', B=')', op=add):
-    '''Yield balanced pairs of A and B.'''
-    if not (left or right):
-        yield t
-        return
-
-    if left > 0:
-        for i in dyck_language(left - 1, right + 1, op(t, A), A, B, op):
-            yield i
-
-    if right > 0:
-        for i in dyck_language(left, right - 1, op(t, B), A, B, op):
-            yield i
-
- -
-
-
- -
-
-
-
In [134]:
-
-
-
for s in dyck_language(5):
-    print s, u'⟶', to_fixed_point(s, reduce_string)
-
- -
-
-
- -
-
- - -
- -
- - -
-
((((())))) ⟶ ()
-(((()()))) ⟶ 
-(((())())) ⟶ ()
-(((()))()) ⟶ 
-(((())))() ⟶ ()
-((()(()))) ⟶ ()
-((()()())) ⟶ ()
-((()())()) ⟶ 
-((()()))() ⟶ ()
-((())(())) ⟶ ()
-((())()()) ⟶ 
-((())())() ⟶ ()
-((()))(()) ⟶ ()
-((()))()() ⟶ ()
-(()((()))) ⟶ 
-(()(()())) ⟶ 
-(()(())()) ⟶ 
-(()(()))() ⟶ ()
-(()()(())) ⟶ 
-(()()()()) ⟶ 
-(()()())() ⟶ ()
-(()())(()) ⟶ 
-(()())()() ⟶ ()
-(())((())) ⟶ ()
-(())(()()) ⟶ 
-(())(())() ⟶ ()
-(())()(()) ⟶ ()
-(())()()() ⟶ ()
-()(((()))) ⟶ ()
-()((()())) ⟶ ()
-()((())()) ⟶ ()
-()((()))() ⟶ ()
-()(()(())) ⟶ ()
-()(()()()) ⟶ ()
-()(()())() ⟶ ()
-()(())(()) ⟶ ()
-()(())()() ⟶ ()
-()()((())) ⟶ ()
-()()(()()) ⟶ ()
-()()(())() ⟶ ()
-()()()(()) ⟶ ()
-()()()()() ⟶ ()
-
-
-
- -
-
- -
-
-
-
-
-

Appendix: void() and mark()

The void() and mark() functions can be defined recursively in terms of each other. Note that void() uses any() while mark() uses all(). These functions implement a depth-first search. If we used versions of any() and all() that evaluated their arguments in parallel void() could return after the True result while mark() depends on all terms's results so its runtime will be bound by term with the greatest runtime.

- -
-
-
-
-
-
In [135]:
-
-
-
def void(form):
-    return any(mark(i) for i in form)
-
-def mark(form):
-    return all(void(i) for i in form)
-
-for form in BASE:
-    for func in (void, mark):
-        print form, 'is', func.__name__, '?', func(form)
-
- -
-
-
- -
-
- - -
- -
- - -
-
(()) is void ? True
-(()) is mark ? False
-() is void ? False
-() is mark ? True
-
-
-
- -
-
- -
-
-
-
-
-

Appendix: Duals

The Void and the Mark are not Boolean true and false. Rather they correspond to non-existance and existance. When translating a traditional logical statement into Laws of Form the first thing we must do is choose which mapping we would like to use: true = Mark or true = Void. The notation works the same way once the translation is made, so the only real criteria for choosing is which gives the smaller form.

-

If you examine the truth tables for the basic forms above in light of this, you can see that each defines two logical functions depending on whether you treat Void as true and Mark as false, or Void as false and Mark as true.

-

For example, the juxtaposition of two terms next to each other a b corresponds to OR if Mark is true, and to AND if Void is true. Likewise, the form ((a)(b)) is AND if Mark is true and OR if Void is true.

-

Consider:

- -
(A ∧ ¬B) ∨ (C ∧ D)
-
-
-

(This reads "(A and not B) or (C and D)" in case you have a hard time remembering what the symbols mean like I do.)

-

If we choose Mark to be true then the form is:

- -
((A) B) ((C)(D))
-
-
-

If we choose Void to be true then the form is:

- -
((A (B)) (C D))
-
-
-

As I said above, the notation works the same way either way, so once the translation is made you can forget about the Boolean true/false and just work with the Laws of Form rules. Logic is containers.

-

De Morgan Duals

Consider also the De Morgan dual of the original statement:

- -
¬((¬A ∨ B) ∧ (¬C ∨ ¬D))
-
-
-

If we choose Mark to be true then the form is:

- -
(( ((A) B) ((C)(D)) ))
-
-
-

The outer pair of containers can be deleted leaving the same form as above:

- -
((A) B) ((C)(D))
-
-
-

Likewise, if we choose Void to be true then the form is:

- -
((((A)) (B)) (((C)) ((D))))
-
-
-

Again, A((B)) => AB reduces this form to the same one above:

- -
((A (B)) (C D))
-
-
-

In the Laws of Form there are no De Morgan Dual statements. If you translate a logic statement and its dual into Laws of Form notation they both reduce to the same form.

-

To me this is a clear indication that the Laws of Form are superior to the traditional notation involving ¬ ∨ ∧, etc. LoF replaces all the symbols with just names and boundaries. The Laws of Form are not dualistic, they work directly in terms of existance and non-existance. Duality only comes in when you interpret the forms as Boolean statements and have to pick a mapping.

- -
-
-
-
-
-
-
-

Misc. Junk

-
-
-
-
-
-
In [136]:
-
-
-
from collections import Counter
-
-histo = Counter(yield_variables_of(cout))
-histo
-
- -
-
-
- -
-
- - -
- -
Out[136]:
- - - - -
-
Counter({'Cin': 1,
-         'a0': 3,
-         'a1': 3,
-         'a2': 3,
-         'a3': 3,
-         'b0': 3,
-         'b1': 3,
-         'b2': 3,
-         'b3': 3})
-
- -
- -
-
- -
-
-
-
In [137]:
-
-
-
#import pprint as pp
-
-
-#E = cout
-#for var, count in histo.most_common():
-#    print 'stan', var, count
-#    E = to_fixed_point(simplify(standardize(E, var)), simplify)
-#    print len(str(E))
-#    pp.pprint(dict(Counter(yield_variables_of(E))))
-#    print '------'
-
- -
-
-
- -
-
-
-
-
-

Rather than manually calling standard_form() let's define a function that reduces a form to a (hopefully) smaller equivalent form by going through all the variables in the form and using standard_form() with each. Along with clean and unwrap we can drive an expression to a fixed point.

- -
-
-
-
-
-
In [138]:
-
-
-
def STAN(form):
-    for var, _ in Counter(yield_variables_of(form)).most_common():
-        form = to_fixed_point(simplify(standardize(form, var)), simplify)
-    return form
-
- -
-
-
- -
-
-
-
In [139]:
-
-
-
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)
-
-map(len, map(str, (sum0, sum1, sum2, sum3, cout)))
-
- -
-
-
- -
-
- - -
- -
Out[139]:
- - - - -
-
[59, 135, 211, 287, 159]
-
- -
- -
-
- -
-
-
-
In [140]:
-
-
-
sum0, cout = full_bit_adder('a0', 'b0', 'Cin')
-sum0 = to_fixed_point(sum0, STAN)
-cout = to_fixed_point(cout, STAN)
-
-sum1, cout = full_bit_adder('a1', 'b1', cout)
-sum1 = to_fixed_point(sum1, STAN)
-cout = to_fixed_point(cout, STAN)
-
-sum2, cout = full_bit_adder('a2', 'b2', cout)
-sum2 = to_fixed_point(sum2, STAN)
-cout = to_fixed_point(cout, STAN)
-
-sum3, cout = full_bit_adder('a3', 'b3', cout)
-sum3 = to_fixed_point(sum3, STAN)
-cout = to_fixed_point(cout, STAN)
-
-
-map(len, map(str, (sum0, sum1, sum2, sum3, cout)))
-
- -
-
-
- -
-
- - -
- -
- - -
-
----------------------------------------------------------------------------
-NameError                                 Traceback (most recent call last)
-<ipython-input-140-34665b9e1d61> in <module>()
-      1 sum0, cout = full_bit_adder('a0', 'b0', 'Cin')
-----> 2 sum0 = to_fixed_point(sum0, STAN)
-      3 cout = to_fixed_point(cout, STAN)
-      4 
-      5 sum1, cout = full_bit_adder('a1', 'b1', cout)
-
-<ipython-input-132-bf263ba512a2> in to_fixed_point(initial_value, F, limit)
-      2     '''Do value = F(value) until value == F(value).'''
-      3 
-----> 4     next_value = F(initial_value)
-      5 
-      6     while next_value != initial_value:
-
-<ipython-input-138-99179e550c4a> in STAN(form)
-      1 def STAN(form):
-      2     for var, _ in Counter(yield_variables_of(form)).most_common():
-----> 3         form = to_fixed_point(simplify(standardize(form, var)), simplify)
-      4     return form
-
-NameError: global name 'standardize' is not defined
-
-
- -
-
- -
-
-
-
-
-

It would be useful and fun to write a simple search algorithm that tried different ways to reduce a form to see if it could find particulaly compact versions.

-

Let's generate the expressions for the next two output bits, and the carry bit.

- -
-
-
-
-
-
-
-

The sum3 bit expression is pretty big.

- -
-
-
-
-
-
In [ ]:
-
-
-
sum3
-
- -
-
-
- -
-
-
-
-
-

But it's only about 1/9th of size of the previous version (which was 9261.)

- -
-
-
-
-
-
In [ ]:
-
-
-
len(str(sum3))
-
- -
-
-
- -
-
-
-
-
-

Let's simplify the first one manually just for fun:

- -
(((((())) (())) ((()))))
-  ((    )     ) (    )
-                (    )
-
-
-

Sure enough, it reduces to Mark after just a few applications of the rule (()) = __ (the underscores indicates the absence of any value, aka Void.) We could also just delete variables that are Void in the original expression:

- -
((((a)b)(c)))
-  (( ) )( )
-        ( )
- -
-
-
-
-
-
In [ ]:
-
-
-
C = F((a, b))
-for form in (A, B, C):
-    arth = reify(form, env)
-    print form, u'⟶', arth, u'⟶', value_of(arth)
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
print A
-Aa = simplify(A, {a})
-print a, Aa
-Aab = simplify(Aa, {b})
-print a, b, Aab
-Aabc = simplify(Aab, {c})
-print a, b, c, Aabc
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
print a, Aa
-Aab = simplify(Aa, with_mark=b)
-print a, F(b), Aab
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
print a, Aa
-Aac = simplify(Aa, with_mark=c)
-print a, F(c), Aac
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
print a, Aa
-Aac = simplify(Aa, {c})
-print a, c, Aac
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
from collections import Counter
-
-histo = Counter(yield_variables_of(sum7))
-histo
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
len(str(sum7))
-
- -
-
-
- -
-
-
-
-
-

Immediately we can just call simplify() until it stops shinking the expression.

- -
-
-
-
-
-
In [ ]:
-
-
-
s7 = simplify(sum7)
-len(str(s7))
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
s7 = simplify(s7)
-len(str(s7))
-
- -
-
-
- -
-
-
-
-
-

Once was enough (we should consider adding a call to simplify() in the full_bit_adder() function.)

-

Let's try using each_way() with the most common names in the form.

- -
-
-
-
-
-
In [ ]:
-
-
-
s7 = simplify(each_way(s7, 'a0'))
-len(str(s7))
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
s7 = simplify(s7)
-len(str(s7))
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
Counter(yield_variables_of(s7))
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
s7 = sum7
-
-#for name, count in histo.most_common():
-#    s7 = simplify(each_way(s7, name))
-#    print len(str(s7))
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
def super_simple(form):
-    return to_fixed_point(form, simplify)
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
len(str(sum7))
-s7 = super_simple(sum7)
-len(str(s7))
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
s7 = sum7
-
-#for name, count in histo.most_common():
-#    s7 = super_simple(each_way(s7, name))
-#    print len(str(s7))
-
- -
-
-
- -
-
-
-
In [ ]:
-
-
-
print ' '.join(name[:2] for name in sorted(R))
-for _ in range(20):
-    print format_env(R), '=', b_register(R)
-    R.update(cycle(P, R))
-
- -
-
-
- -
-
-
- - - - - - diff --git a/docs/sphinx_docs/_build/html/notebooks/Derivatives_of_Regular_Expressions.html b/docs/sphinx_docs/_build/html/notebooks/Derivatives_of_Regular_Expressions.html index f269260..345f954 100644 --- a/docs/sphinx_docs/_build/html/notebooks/Derivatives_of_Regular_Expressions.html +++ b/docs/sphinx_docs/_build/html/notebooks/Derivatives_of_Regular_Expressions.html @@ -1,19 +1,18 @@ - + - + - - + ∂RE — Thun 0.2.0 documentation - - - - - + + + + + + @@ -29,6 +28,8 @@
+ +
@@ -95,14 +96,14 @@ R∘λ = λ∘R = R

Implementation

-
from functools import partial as curry
-from itertools import product
+
from functools import partial as curry
+from itertools import product
 

 

 

 
ϕ and λ

 
The empty set and the set of just the empty string.

-
phi = frozenset()   # ϕ
+
phi = frozenset()   # ϕ
 y = frozenset({''}) # λ
 

 

@@ -114,7 +115,7 @@ illustrate the algorithm and because you can represent any other
 alphabet with two symbols (if you had to.)

 
I chose the names O and l (uppercase “o” and lowercase “L”) to
 look like 0 and 1 (zero and one) respectively.

-
syms = O, l = frozenset({'0'}), frozenset({'1'})
+
syms = O, l = frozenset({'0'}), frozenset({'1'})
 

 

 

@@ -132,7 +133,7 @@ expression is one of:

 

 

 
Where R and S stand for regular expressions.

-
AND, CONS, KSTAR, NOT, OR = 'and cons * not or'.split()  # Tags are just strings.
+
AND, CONS, KSTAR, NOT, OR = 'and cons * not or'.split()  # Tags are just strings.
 

 

 
Because they are formed of frozenset, tuple and str objects
@@ -140,7 +141,7 @@ only, these datastructures are immutable.

 

 

 
String Representation of RE Datastructures

-
def stringy(re):
+
def stringy(re):
     '''
     Return a nice string repr for a regular expression datastructure.
     '''
@@ -179,10 +180,10 @@ only, these datastructures are immutable.

 
I = (0|1)*
 

 

-
I = (KSTAR, (OR, O, l))
+
I = (KSTAR, (OR, O, l))
 

 

-
print stringy(I)
+
print stringy(I)
 

 

 
.
@@ -197,13 +198,13 @@ only, these datastructures are immutable.

 

 

 
Note that it contains one of everything.

-
a = (CONS, I, (CONS, l, (CONS, l, (CONS, l, I))))
+
a = (CONS, I, (CONS, l, (CONS, l, (CONS, l, I))))
 b = (CONS, I, (CONS, O, l))
 c = (CONS, l, (KSTAR, l))
 it = (AND, a, (NOT, (OR, b, c)))
 

 

-
print stringy(it)
+
print stringy(it)
 

 

 
(.111.) & ((.01 | 11*)')
@@ -213,7 +214,7 @@ only, these datastructures are immutable.

 

 
nully()

 
Let’s get that auxiliary predicate function δ out of the way.

-
def nully(R):
+
def nully(R):
     '''
     δ - Return λ if λ ⊆ R otherwise ϕ.
     '''
@@ -251,7 +252,7 @@ only, these datastructures are immutable.

 
This is the straightforward version with no “compaction”. It works fine,
 but does waaaay too much work because the expressions grow each
 derivation.

-
def D(symbol):
+
def D(symbol):
 
     def derv(R):
 
@@ -295,7 +296,7 @@ derivation.

 

 

 
Compaction Rules

-
def _compaction_rule(relation, one, zero, a, b):
+
def _compaction_rule(relation, one, zero, a, b):
     return (
         b if a == one else  # R*1 = 1*R = R
         a if b == one else
@@ -305,7 +306,7 @@ derivation.

 

 

 
An elegant symmetry.

-
# R ∧ I = I ∧ R = R
+
# R ∧ I = I ∧ R = R
 # R ∧ ϕ = ϕ ∧ R = ϕ
 _and = curry(_compaction_rule, AND, I, phi)
 
@@ -324,14 +325,14 @@ derivation.

 
We can save re-processing by remembering results we have already
 computed. RE datastructures are immutable and the derv() functions
 are pure so this is fine.

-
class Memo(object):
+
class Memo(object):
 
-    def __init__(self, f):
+    def __init__(self, f):
         self.f = f
         self.calls = self.hits = 0
         self.mem = {}
 
-    def __call__(self, key):
+    def __call__(self, key):
         self.calls += 1
         try:
             result = self.mem[key]
@@ -346,7 +347,7 @@ are pure so this is fine.

 
With “Compaction”

 
This version uses the rules above to perform compaction. It keeps the
 expressions from growing too large.

-
def D_compaction(symbol):
+
def D_compaction(symbol):
 
     @Memo
     def derv(R):
@@ -394,7 +395,7 @@ expressions from growing too large.

 

 
Let’s try it out…

 
(FIXME: redo.)

-
o, z = D_compaction('0'), D_compaction('1')
+
o, z = D_compaction('0'), D_compaction('1')
 REs = set()
 N = 5
 names = list(product(*(N * [(0, 1)])))
@@ -498,8 +499,8 @@ machine transition table.

 

 

 
Says, “Three or more 1’s and not ending in 01 nor composed of all 1’s.”

-

-omg.svg
omg.svg

+

+omg.svg
omg.svg

 

 
Start at a and follow the transition arrows according to their
 labels. Accepting states have a double outline. (Graphic generated with
@@ -552,18 +553,18 @@ a --1--> ∂1(a)
 
You can see the one-way nature of the g state and the hij “trap”
 in the way that the .111. on the left-hand side of the &
 disappears once it has been matched.

-
from collections import defaultdict
-from pprint import pprint
-from string import ascii_lowercase
+
from collections import defaultdict
+from pprint import pprint
+from string import ascii_lowercase
 

 

-
d0, d1 = D_compaction('0'), D_compaction('1')
+
d0, d1 = D_compaction('0'), D_compaction('1')
 

 

 

 

 
explore()

-
def explore(re):
+
def explore(re):
 
     # Don't have more than 26 states...
     names = defaultdict(iter(ascii_lowercase).next)
@@ -589,7 +590,7 @@ disappears once it has been matched.

     return table, accepting
 

 

-
table, accepting = explore(it)
+
table, accepting = explore(it)
 table
 

 

@@ -615,7 +616,7 @@ disappears once it has been matched.

  ('j', 1): 'h'}
 

 

-
accepting
+
accepting
 

 

 
{'h', 'i'}
@@ -626,7 +627,7 @@ disappears once it has been matched.

 
Generate Diagram

 
Once we have the FSM table and the set of accepting states we can
 generate the diagram above.

-
_template = '''\
+
_template = '''\
 digraph finite_state_machine {
   rankdir=LR;
   size="8,5"
@@ -650,7 +651,7 @@ generate the diagram above.

         )
 

 

-
print make_graph(table, accepting)
+
print make_graph(table, accepting)
 

 

 
digraph finite_state_machine {
@@ -696,7 +697,7 @@ hard-code the information in the table into a little patch of branches.

 
Trampoline Function

 
Python has no GOTO statement but we can fake it with a “trampoline”
 function.

-
def trampoline(input_, jump_from, accepting):
+
def trampoline(input_, jump_from, accepting):
     I = iter(input_)
     while True:
         try:
@@ -711,7 +712,7 @@ function.

 
Stream Functions

 
Little helpers to process the iterator of our data (a “stream” of “1”
 and “0” characters, not bits.)

-
getch = lambda I: int(next(I))
+
getch = lambda I: int(next(I))
 
 
 def _1(I):
@@ -732,7 +733,7 @@ and “0” characters, not bits.)

 code. (You have to imagine that these are GOTO statements in C or
 branches in assembly and that the state names are branch destination
 labels.)

-
a = lambda I: c if getch(I) else b
+
a = lambda I: c if getch(I) else b
 b = lambda I: _0(I) or d
 c = lambda I: e if getch(I) else b
 d = lambda I: f if getch(I) else b
@@ -747,11 +748,11 @@ labels.)

 
Note that the implementations of h and g are identical ergo
 h = g and we could eliminate one in the code but h is an
 accepting state and g isn’t.

-
def acceptable(input_):
+
def acceptable(input_):
     return trampoline(input_, a, {h, i})
 

 

-
for n in range(2**5):
+
for n in range(2**5):
     s = bin(n)[2:]
     print '%05s' % s, acceptable(s)
 

@@ -821,7 +822,7 @@ derivative-with-respect-to-N of some other state/RE:

 
b = d10(a)
 

 

-
‘’‘

+
‘’’

 
j = d1(d0(j))
 

 

@@ -842,46 +843,50 @@ derivative-with-respect-to-N of some other state/RE:

 
 
           

+          
         

       

       
       

       

@@ -921,7 +925,7 @@ derivative-with-respect-to-N of some other state/RE:

 
 

 Thun Documentation by Simon Forman is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Based on a work at https://osdn.net/projects/joypy/.
-      Created using Sphinx 1.7.3.
+      Created using Sphinx 3.0.2.
     

 
   
diff --git a/docs/sphinx_docs/_build/html/notebooks/Developing.html b/docs/sphinx_docs/_build/html/notebooks/Developing.html
index 0e2fe6b..d10eab4 100644
--- a/docs/sphinx_docs/_build/html/notebooks/Developing.html
+++ b/docs/sphinx_docs/_build/html/notebooks/Developing.html
@@ -1,19 +1,18 @@
 
-
+
 
-
+
   
-    
-    
+    
     Developing a Program in Joy — Thun 0.2.0 documentation
     
     
-    
-    
-    
-    
-    
+    
+    
+    
+    
+    
+    
     
     
     
@@ -30,6 +29,8 @@
     

       

         

+          
+
           

             
   

@@ -41,17 +42,17 @@
 
If we list all the natural numbers below 10 that are multiples of 3 or 5, we get 3, 5, 6 and 9. The sum of these multiples is 23.

 
Find the sum of all the multiples of 3 or 5 below 1000.

 

-
from notebook_preamble import J, V, define
+
from notebook_preamble import J, V, define
 

 

 

 
Sum a range filtered by a predicate

 
Let’s create a predicate that returns True if a number is a multiple
 of 3 or 5 and False otherwise.

-
define('P == [3 % not] dupdip 5 % not or')
+
define('P == [3 % not] dupdip 5 % not or')
 

 

-
V('80 P')
+
V('80 P')
 

 

 
             . 80 P
@@ -114,10 +115,10 @@ the counter to the running sum. This function will do that:

 
PE1.1 == + [+] dupdip
 

 

-
define('PE1.1 == + [+] dupdip')
+
define('PE1.1 == + [+] dupdip')
 

 

-
V('0 0 3 PE1.1')
+
V('0 0 3 PE1.1')
 

 

 
        . 0 0 3 PE1.1
@@ -132,7 +133,7 @@ the counter to the running sum. This function will do that:

     3 3 .
 

 

-
V('0 0 [3 2 1 3 1 2 3] [PE1.1] step')
+
V('0 0 [3 2 1 3 1 2 3] [PE1.1] step')
 

 

 
                            . 0 0 [3 2 1 3 1 2 3] [PE1.1] step
@@ -215,26 +216,26 @@ total to 60.

 

 

 
How many multiples to sum?

-
1000 / 15
+
1000 / 15
 

 

 
66
 

 

-
66 * 15
+
66 * 15
 

 

 
990
 

 

-
1000 - 990
+
1000 - 990
 

 

 
10
 

 

 
We only want the terms less than 1000.

-
999 - 990
+
999 - 990
 

 

 
9
@@ -242,10 +243,10 @@ total to 60.

 

 
That means we want to run the full list of numbers sixty-six times to
 get to 990 and then the first four numbers 3 2 1 3 to get to 999.

-
define('PE1 == 0 0 66 [[3 2 1 3 1 2 3] [PE1.1] step] times [3 2 1 3] [PE1.1] step pop')
+
define('PE1 == 0 0 66 [[3 2 1 3 1 2 3] [PE1.1] step] times [3 2 1 3] [PE1.1] step pop')
 

 

-
J('PE1')
+
J('PE1')
 

 

 
233168
@@ -265,16 +266,16 @@ integer terms from the list.

 0b 11 10 01 11 01 10 11 == 14811
 

 

-
0b11100111011011
+
0b11100111011011
 

 

 
14811
 

 

-
define('PE1.2 == [3 & PE1.1] dupdip 2 >>')
+
define('PE1.2 == [3 & PE1.1] dupdip 2 >>')
 

 

-
V('0 0 14811 PE1.2')
+
V('0 0 14811 PE1.2')
 

 

 
                      . 0 0 14811 PE1.2
@@ -297,7 +298,7 @@ integer terms from the list.

              3 3 3702 .
 

 

-
V('3 3 3702 PE1.2')
+
V('3 3 3702 PE1.2')
 

 

 
                     . 3 3 3702 PE1.2
@@ -320,7 +321,7 @@ integer terms from the list.

              8 5 925 .
 

 

-
V('0 0 14811 7 [PE1.2] times pop')
+
V('0 0 14811 7 [PE1.2] times pop')
 

 

 
                      . 0 0 14811 7 [PE1.2] times pop
@@ -457,10 +458,10 @@ integer terms from the list.

 

 

 
And so we have at last:

-
define('PE1 == 0 0 66 [14811 7 [PE1.2] times pop] times 14811 4 [PE1.2] times popop')
+
define('PE1 == 0 0 66 [14811 7 [PE1.2] times pop] times 14811 4 [PE1.2] times popop')
 

 

-
J('PE1')
+
J('PE1')
 

 

 
233168
@@ -475,14 +476,14 @@ integer terms from the list.

 n 14811 swap [PE1.2] times pop
 

 

-
define('PE1.3 == 14811 swap [PE1.2] times pop')
+
define('PE1.3 == 14811 swap [PE1.2] times pop')
 

 

 
Now we can simplify the definition above:

-
define('PE1 == 0 0 66 [7 PE1.3] times 4 PE1.3 pop')
+
define('PE1 == 0 0 66 [7 PE1.3] times 4 PE1.3 pop')
 

 

-
J('PE1')
+
J('PE1')
 

 

 
233168
@@ -505,10 +506,10 @@ I hope it’s clear.

 then four more. In the Generator Programs notebook we derive a
 generator that can be repeatedly driven by the x combinator to
 produce a stream of the seven numbers repeating over and over again.

-
define('PE1.terms == [0 swap [dup [pop 14811] [] branch [3 &] dupdip 2 >>] dip rest cons]')
+
define('PE1.terms == [0 swap [dup [pop 14811] [] branch [3 &] dupdip 2 >>] dip rest cons]')
 

 

-
J('PE1.terms 21 [x] times')
+
J('PE1.terms 21 [x] times')
 

 

 
3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 [0 swap [dup [pop 14811] [] branch [3 &] dupdip 2 >>] dip rest cons]
@@ -516,19 +517,19 @@ produce a stream of the seven numbers repeating over and over again.

 

 
We know from above that we need sixty-six times seven then four more
 terms to reach up to but not over one thousand.

-
J('7 66 * 4 +')
+
J('7 66 * 4 +')
 

 

 
466
 

 

-
J('PE1.terms 466 [x] times pop')
+
J('PE1.terms 466 [x] times pop')
 

 

 
3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3
 

 

-
J('[PE1.terms 466 [x] times pop] run sum')
+
J('[PE1.terms 466 [x] times pop] run sum')
 

 

 
999
@@ -537,7 +538,7 @@ terms to reach up to but not over one thousand.

 
Now we can use PE1.1 to accumulate the terms as we go, and then
 pop the generator and the counter from the stack when we’re done,
 leaving just the sum.

-
J('0 0 PE1.terms 466 [x [PE1.1] dip] times popop')
+
J('0 0 PE1.terms 466 [x [PE1.1] dip] times popop')
 

 

 
233168
@@ -548,7 +549,7 @@ leaving just the sum.

 
A little further analysis renders iteration unnecessary.

 
Consider finding the sum of the positive integers less than or equal to
 ten.

-
J('[10 9 8 7 6 5 4 3 2 1] sum')
+
J('[10 9 8 7 6 5 4 3 2 1] sum')
 

 

 
55
@@ -571,10 +572,10 @@ positive integers is:

 

 
(The formula also works for odd values of N, I’ll leave that to you if
 you want to work it out or you can take my word for it.)

-
define('F == dup ++ * 2 floordiv')
+
define('F == dup ++ * 2 floordiv')
 

 

-
V('10 F')
+
V('10 F')
 

 

 
      . 10 F
@@ -598,13 +599,13 @@ each, starting with:

 

 

 
If we reverse one of these two blocks and sum pairs…

-
J('[3 5 6 9 10 12 15] reverse [978 980 981 984 985 987 990] zip')
+
J('[3 5 6 9 10 12 15] reverse [978 980 981 984 985 987 990] zip')
 

 

 
[[978 15] [980 12] [981 10] [984 9] [985 6] [987 5] [990 3]]
 

 

-
J('[3 5 6 9 10 12 15] reverse [978 980 981 984 985 987 990] zip [sum] map')
+
J('[3 5 6 9 10 12 15] reverse [978 980 981 984 985 987 990] zip [sum] map')
 

 

 
[993 992 991 993 991 992 993]
@@ -612,7 +613,7 @@ each, starting with:

 

 
(Interesting that the sequence of seven numbers appears again in the
 rightmost digit of each term.)

-
J('[ 3 5 6 9 10 12 15] reverse [978 980 981 984 985 987 990] zip [sum] map sum')
+
J('[ 3 5 6 9 10 12 15] reverse [978 980 981 984 985 987 990] zip [sum] map sum')
 

 

 
6945
@@ -626,7 +627,7 @@ additional unpaired terms between 990 and 1000:

 

 
So we can give the “sum of all the multiples of 3 or 5 below 1000” like
 so:

-
J('6945 33 * [993 995 996 999] cons sum')
+
J('6945 33 * [993 995 996 999] cons sum')
 

 

 
233168
@@ -662,27 +663,50 @@ is just:

 
 
           

+          
         

       

       
       

       

@@ -723,7 +746,7 @@ is just:

 
 

 Thun Documentation by Simon Forman is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Based on a work at https://osdn.net/projects/joypy/.
-      Created using Sphinx 1.7.3.
+      Created using Sphinx 3.0.2.
     

 
   
diff --git a/docs/sphinx_docs/_build/html/notebooks/Generator_Programs.html b/docs/sphinx_docs/_build/html/notebooks/Generator_Programs.html
index ac0e819..220cd32 100644
--- a/docs/sphinx_docs/_build/html/notebooks/Generator_Programs.html
+++ b/docs/sphinx_docs/_build/html/notebooks/Generator_Programs.html
@@ -1,19 +1,18 @@
 
-
+
 
-
+
   
-    
-    
+    
     Using x to Generate Values — Thun 0.2.0 documentation
     
     
-    
-    
-    
-    
-    
+    
+    
+    
+    
+    
+    
     
     
     
@@ -30,12 +29,14 @@
     

       

         

+          
+
           

             
   

 
Using x to Generate Values

 
Cf. jp-reprod.html

-
from notebook_preamble import J, V, define
+
from notebook_preamble import J, V, define
 

 

 
Consider the x combinator:

@@ -75,7 +76,7 @@ function C

 

 
Let’s try it:

-
V('[0 swap [dup ++] dip rest cons] x')
+
V('[0 swap [dup ++] dip rest cons] x')
 

 

 
                                           . [0 swap [dup ++] dip rest cons] x
@@ -94,7 +95,7 @@ function C
 
After one application of x the quoted program contains 1 and
 0 is below it on the stack.

-
J('[0 swap [dup ++] dip rest cons] x x x x x pop')
+
J('[0 swap [dup ++] dip rest cons] x x x x x pop')
 

 

 
0 1 2 3 4
@@ -102,10 +103,10 @@ function C
 

 
direco

-
define('direco == dip rest cons')
+
define('direco == dip rest cons')
 

 

-
V('[0 swap [dup ++] direco] x')
+
V('[0 swap [dup ++] direco] x')
 

 

 
                                    . [0 swap [dup ++] direco] x
@@ -146,17 +147,17 @@ our quoted program:

 G == [direco] cons [swap] swoncat cons
 

 

-
define('G == [direco] cons [swap] swoncat cons')
+
define('G == [direco] cons [swap] swoncat cons')
 

 

 
Let’s try it out:

-
J('0 [dup ++] G')
+
J('0 [dup ++] G')
 

 

 
[0 swap [dup ++] direco]
 

 

-
J('0 [dup ++] G x x x pop')
+
J('0 [dup ++] G x x x pop')
 

 

 
0 1 2
@@ -164,7 +165,7 @@ our quoted program:

 

 

 
Powers of 2

-
J('1 [dup 1 <<] G x x x x x x x x x pop')
+
J('1 [dup 1 <<] G x x x x x x x x x pop')
 

 

 
1 2 4 8 16 32 64 128 256
@@ -175,7 +176,7 @@ our quoted program:

 
[x] times

 
If we have one of these quoted programs we can drive it using times
 with the x combinator.

-
J('23 [dup ++] G 5 [x] times')
+
J('23 [dup ++] G 5 [x] times')
 

 

 
23 24 25 26 27 [28 swap [dup ++] direco]
@@ -199,10 +200,10 @@ int:

 

 
And pick them off by masking with 3 (binary 11) and then shifting the
 int right two bits.

-
define('PE1.1 == dup [3 &] dip 2 >>')
+
define('PE1.1 == dup [3 &] dip 2 >>')
 

 

-
V('14811 PE1.1')
+
V('14811 PE1.1')
 

 

 
                  . 14811 PE1.1
@@ -219,7 +220,7 @@ int right two bits.

 

 

 
If we plug 14811 and [PE1.1] into our generator form…

-
J('14811 [PE1.1] G')
+
J('14811 [PE1.1] G')
 

 

 
[14811 swap [PE1.1] direco]
@@ -227,7 +228,7 @@ int right two bits.

 

 
…we get a generator that works for seven cycles before it reaches
 zero:

-
J('[14811 swap [PE1.1] direco] 7 [x] times')
+
J('[14811 swap [PE1.1] direco] 7 [x] times')
 

 

 
3 2 1 3 1 2 3 [0 swap [PE1.1] direco]
@@ -237,16 +238,16 @@ zero:

 
Reset at Zero

 
We need a function that checks if the int has reached zero and resets it
 if so.

-
define('PE1.1.check == dup [pop 14811] [] branch')
+
define('PE1.1.check == dup [pop 14811] [] branch')
 

 

-
J('14811 [PE1.1.check PE1.1] G')
+
J('14811 [PE1.1.check PE1.1] G')
 

 

 
[14811 swap [PE1.1.check PE1.1] direco]
 

 

-
J('[14811 swap [PE1.1.check PE1.1] direco] 21 [x] times')
+
J('[14811 swap [PE1.1.check PE1.1] direco] 21 [x] times')
 

 

 
3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 [0 swap [PE1.1.check PE1.1] direco]
@@ -262,20 +263,20 @@ say.)

 
In the PE1 problem we are asked to sum all the multiples of three and
 five less than 1000. It’s worked out that we need to use all seven
 numbers sixty-six times and then four more.

-
J('7 66 * 4 +')
+
J('7 66 * 4 +')
 

 

 
466
 

 

 
If we drive our generator 466 times and sum the stack we get 999.

-
J('[14811 swap [PE1.1.check PE1.1] direco] 466 [x] times')
+
J('[14811 swap [PE1.1.check PE1.1] direco] 466 [x] times')
 

 

 
3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 1 2 3 3 2 1 3 [57 swap [PE1.1.check PE1.1] direco]
 

 

-
J('[14811 swap [PE1.1.check PE1.1] direco] 466 [x] times pop enstacken sum')
+
J('[14811 swap [PE1.1.check PE1.1] direco] 466 [x] times pop enstacken sum')
 

 

 
999
@@ -285,11 +286,11 @@ numbers sixty-six times and then four more.

 

 

 
Project Euler Problem One

-
define('PE1.2 == + dup [+] dip')
+
define('PE1.2 == + dup [+] dip')
 

 

 
Now we can add PE1.2 to the quoted program given to G.

-
J('0 0 0 [PE1.1.check PE1.1] G 466 [x [PE1.2] dip] times popop')
+
J('0 0 0 [PE1.1.check PE1.1] G 466 [x [PE1.2] dip] times popop')
 

 

 
233168
@@ -351,13 +352,13 @@ numbers sixty-six times and then four more.

 fib_gen == [1 1 F]
 

 

-
define('fib == + [popdd over] cons infra uncons')
+
define('fib == + [popdd over] cons infra uncons')
 

 

-
define('fib_gen == [1 1 fib]')
+
define('fib_gen == [1 1 fib]')
 

 

-
J('fib_gen 10 [x] times')
+
J('fib_gen 10 [x] times')
 

 

 
1 2 3 5 8 13 21 34 55 89 [144 89 fib]
@@ -367,26 +368,27 @@ numbers sixty-six times and then four more.

 

 
Project Euler Problem Two

 

-
By considering the terms in the Fibonacci sequence whose values do
-not exceed four million, find the sum of the even-valued terms.

+
By considering the terms in the Fibonacci sequence whose values do
+not exceed four million, find the sum of the even-valued terms.

+

 
Now that we have a generator for the Fibonacci sequence, we need a
 function that adds a term in the sequence to a sum if it is even, and
 pops it otherwise.

-
define('PE2.1 == dup 2 % [+] [pop] branch')
+
define('PE2.1 == dup 2 % [+] [pop] branch')
 

 

 
And a predicate function that detects when the terms in the series
 “exceed four million”.

-
define('>4M == 4000000 >')
+
define('>4M == 4000000 >')
 

 

 
Now it’s straightforward to define PE2 as a recursive function that
 generates terms in the Fibonacci sequence until they exceed four million
 and sums the even ones.

-
define('PE2 == 0 fib_gen x [pop >4M] [popop] [[PE2.1] dip x] primrec')
+
define('PE2 == 0 fib_gen x [pop >4M] [popop] [[PE2.1] dip x] primrec')
 

 

-
J('PE2')
+
J('PE2')
 

 

 
4613732
@@ -417,23 +419,23 @@ and sums the even ones.

 

 

 
Every third term is even.

-
J('[1 0 fib] x x x')  # To start the sequence with 1 1 2 3 instead of 1 2 3.
+
J('[1 0 fib] x x x')  # To start the sequence with 1 1 2 3 instead of 1 2 3.
 

 

 
1 1 2 [3 2 fib]
 

 

 
Drive the generator three times and popop the two odd terms.

-
J('[1 0 fib] x x x [popop] dipd')
+
J('[1 0 fib] x x x [popop] dipd')
 

 

 
2 [3 2 fib]
 

 

-
define('PE2.2 == x x x [popop] dipd')
+
define('PE2.2 == x x x [popop] dipd')
 

 

-
J('[1 0 fib] 10 [PE2.2] times')
+
J('[1 0 fib] 10 [PE2.2] times')
 

 

 
2 8 34 144 610 2584 10946 46368 196418 832040 [1346269 832040 fib]
@@ -441,7 +443,7 @@ and sums the even ones.

 

 
Replace x with our new driver function PE2.2 and start our
 fib generator at 1 0.

-
J('0 [1 0 fib] PE2.2 [pop >4M] [popop] [[PE2.1] dip PE2.2] primrec')
+
J('0 [1 0 fib] PE2.2 [pop >4M] [popop] [[PE2.1] dip PE2.2] primrec')
 

 

 
4613732
@@ -456,10 +458,10 @@ modifications to the default 
 

 
An Interesting Variation

-
define('codireco == cons dip rest cons')
+
define('codireco == cons dip rest cons')
 

 

-
V('[0 [dup ++] codireco] x')
+
V('[0 [dup ++] codireco] x')
 

 

 
                                 . [0 [dup ++] codireco] x
@@ -478,10 +480,10 @@ modifications to the default 0 [1 [dup ++] codireco] .
 

 

-
define('G == [codireco] cons cons')
+
define('G == [codireco] cons cons')
 

 

-
J('230 [dup ++] G 5 [x] times pop')
+
J('230 [dup ++] G 5 [x] times pop')
 

 

 
230 231 232 233 234
@@ -492,35 +494,50 @@ modifications to the default 
+          
         

       

       
       

@@ -561,7 +577,7 @@ modifications to the default 
 

 Thun Documentation by Simon Forman is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Based on a work at https://osdn.net/projects/joypy/.
-      Created using Sphinx 1.7.3.
+      Created using Sphinx 3.0.2.
     

 
   
diff --git a/docs/sphinx_docs/_build/html/notebooks/Intro.html b/docs/sphinx_docs/_build/html/notebooks/Intro.html
index 129327f..253478a 100644
--- a/docs/sphinx_docs/_build/html/notebooks/Intro.html
+++ b/docs/sphinx_docs/_build/html/notebooks/Intro.html
@@ -1,19 +1,18 @@
 
-
+
 
-
+
   
-    
-    
+    
     Thun: Joy in Python — Thun 0.2.0 documentation
     
     
-    
-    
-    
-    
-    
+    
+    
+    
+    
+    
+    
     
     
     
@@ -30,6 +29,8 @@
     

       

         

+          
+
           

             
   

@@ -38,10 +39,10 @@
 model and method of Joy. Python seems like a great implementation
 language for Joy for several reasons.

 
    
-
  • We can lean on the Python immutable types for our basic semantics and types: ints, floats, strings, and tuples, which enforces functional purity.
    • 
-
  • We get garbage collection for free.
    • 
-
  • Compilation via Cython.
    • 
-
  • Python is a “glue language” with loads of libraries which we can wrap in Joy functions.
    • 
+
  • We can lean on the Python immutable types for our basic semantics and types: ints, floats, strings, and tuples, which enforces functional purity.
    • 
+
  • We get garbage collection for free.
    • 
+
  • Compilation via Cython.
    • 
+
  • Python is a “glue language” with loads of libraries which we can wrap in Joy functions.
    • 
 

 

 
Read-Eval-Print Loop (REPL)

@@ -149,19 +150,19 @@ like that.

 

 

 
Examples

-
joy.parser.text_to_expression('1 2 3 4 5')  # A simple sequence.
+
joy.parser.text_to_expression('1 2 3 4 5')  # A simple sequence.
 

 

 
(1, (2, (3, (4, (5, ())))))
 

 

-
joy.parser.text_to_expression('[1 2 3] 4 5')  # Three items, the first is a list with three items
+
joy.parser.text_to_expression('[1 2 3] 4 5')  # Three items, the first is a list with three items
 

 

 
((1, (2, (3, ()))), (4, (5, ())))
 

 

-
joy.parser.text_to_expression('1 23 ["four" [-5.0] cons] 8888')  # A mixed bag. cons is
+
joy.parser.text_to_expression('1 23 ["four" [-5.0] cons] 8888')  # A mixed bag. cons is
                                                                  # a Symbol, no lookup at
                                                                  # parse-time.  Haiku docs.
 

@@ -169,13 +170,13 @@ like that.

 
(1, (23, (('four', ((-5.0, ()), (cons, ()))), (8888, ()))))
 

 

-
joy.parser.text_to_expression('[][][][][]')  # Five empty lists.
+
joy.parser.text_to_expression('[][][][][]')  # Five empty lists.
 

 

 
((), ((), ((), ((), ((), ())))))
 

 

-
joy.parser.text_to_expression('[[[[[]]]]]')  # Five nested lists.
+
joy.parser.text_to_expression('[[[[[]]]]]')  # Five nested lists.
 

 

 
((((((), ()), ()), ()), ()), ())
@@ -191,7 +192,7 @@ the Joy system. There are simple functions such as addition +, the library module supports aliases), and combinators which
 provide control-flow and higher-order operations.

 
Many of the functions are defined in Python, like dip:

-
print inspect.getsource(joy.library.dip)
+
print inspect.getsource(joy.library.dip)
 

 

 
def dip(stack, expression, dictionary):
@@ -204,11 +205,10 @@ provide control-flow and higher-order operations.

 When the interpreter executes a definition function that function just
 pushes its body expression onto the pending expression (the
 continuation) and returns control to the interpreter.

-
print joy.library.definitions
+
print joy.library.definitions
 

 

-
-second == rest first
+
second == rest first
 third == rest rest first
 product == 1 swap [*] step
 swons == swap cons
@@ -241,8 +241,7 @@ anamorphism == [pop []] swap [dip swons] genrec
 range == [0 <=] [1 - dup] anamorphism
 while == swap [nullary] cons dup dipd concat loop
 dudipd == dup dipd
-primrec == [i] genrec
-

+primrec == [i] genrec

 
Currently, there’s no function to add new definitions to the dictionary
 from “within” Joy code itself. Adding new definitions remains a
 meta-interpreter action. You have to do it yourself, in Python, and wash
@@ -291,37 +290,41 @@ developing structured processes.

 
 
           

+          
         

       

       
       

       

@@ -360,7 +362,7 @@ developing structured processes.

 
 

 Thun Documentation by Simon Forman is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Based on a work at https://osdn.net/projects/joypy/.
-      Created using Sphinx 1.7.3.
+      Created using Sphinx 3.0.2.
     

 
   
diff --git a/docs/sphinx_docs/_build/html/notebooks/Newton-Raphson.html b/docs/sphinx_docs/_build/html/notebooks/Newton-Raphson.html
index 441c57c..6c3d551 100644
--- a/docs/sphinx_docs/_build/html/notebooks/Newton-Raphson.html
+++ b/docs/sphinx_docs/_build/html/notebooks/Newton-Raphson.html
@@ -1,19 +1,18 @@
 
-
+
 
-
+
   
-    
-    
+    
     Newton’s method — Thun 0.2.0 documentation
     
     
-    
-    
-    
-    
-    
+    
+    
+    
+    
+    
+    
     
     
     
@@ -30,6 +29,8 @@
     

       

         

+          
+
           

             
   

@@ -38,7 +39,7 @@
 to write a function that can compute the square root of a number.

 
Cf. “Why Functional Programming Matters” by John
 Hughes

-
from notebook_preamble import J, V, define
+
from notebook_preamble import J, V, define
 

 

 

@@ -90,10 +91,10 @@ function we’re writing. If we let 1 be the initial approximation:

 1   [dup 23 over / + 2 /]                    make_generator
 

 

-
define('gsra == 1 swap [over / + 2 /] cons [dup] swoncat make_generator')
+
define('gsra == 1 swap [over / + 2 /] cons [dup] swoncat make_generator')
 

 

-
J('23 gsra')
+
J('23 gsra')
 

 

 
[1 [dup 23 over / + 2 /] codireco]
@@ -101,7 +102,7 @@ function we’re writing. If we let 1 be the initial approximation:

 

 
Let’s drive the generator a few time (with the x combinator) and
 square the approximation to see how well it works…

-
J('23 gsra 6 [x popd] times first sqr')
+
J('23 gsra 6 [x popd] times first sqr')
 

 

 
23.0000000001585
@@ -114,10 +115,11 @@ square the approximation to see how well it works…

 
From “Why Functional Programming Matters” by John
 Hughes:

 

-
The remainder of a square root finder is a function within, which
+
The remainder of a square root finder is a function within, which
 takes a tolerance and a list of approximations and looks down the
 list for two successive approximations that differ by no more than
-the given tolerance.

+the given tolerance.

+

 
(And note that by “list” he means a lazily-evaluated list.)

 
Using the output [a G] of the above generator for square root
 approximations, and further assuming that the first term a has been
@@ -142,7 +144,7 @@ generated already and epsilon ε is handy on the stack…

 (abs(a-b)<=ε)
 

 

-
define('_within_P == [first - abs] dip <=')
+
define('_within_P == [first - abs] dip <=')
 

 

 

@@ -154,7 +156,7 @@ generated already and epsilon ε is handy on the stack…

    b
 

 

-
define('_within_B == roll< popop first')
+
define('_within_B == roll< popop first')
 

 

 

@@ -164,9 +166,9 @@ generated already and epsilon ε is handy on the stack…

 

 

 
    
-
  1. Discard a.
    2. 
-
  2. Use x combinator to generate next term from G.
    3. 
-
  3. Run within with i (it is a primrec function.)
    4. 
+
  4. Discard a.
    5. 
+
  5. Use x combinator to generate next term from G.
    6. 
+
  6. Run within with i (it is a primrec function.)
    7. 
 

 
Pretty straightforward:

 
a [b G]        ε R0           [within] R1
@@ -179,7 +181,7 @@ generated already and epsilon ε is handy on the stack…

 b [c G] ε within
 

 

-
define('_within_R == [popd x] dip')
+
define('_within_R == [popd x] dip')
 

 

 

@@ -191,31 +193,31 @@ generated already and epsilon ε is handy on the stack…

 a [b G] ε ...
 

 

-
define('within == x 0.000000001 [_within_P] [_within_B] [_within_R] primrec')
+
define('within == x 0.000000001 [_within_P] [_within_B] [_within_R] primrec')
 define('sqrt == gsra within')
 

 

 
Try it out…

-
J('36 sqrt')
+
J('36 sqrt')
 

 

 
6.0
 

 

-
J('23 sqrt')
+
J('23 sqrt')
 

 

 
4.795831523312719
 

 

 
Check it.

-
4.795831523312719**2
+
4.795831523312719**2
 

 

 
22.999999999999996
 

 

-
from math import sqrt
+
from math import sqrt
 
 sqrt(23)
 

@@ -229,28 +231,50 @@ generated already and epsilon ε is handy on the stack…

 
 
           

+          
         

       

       
       

       

@@ -291,7 +314,7 @@ generated already and epsilon ε is handy on the stack…

 
 

 Thun Documentation by Simon Forman is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Based on a work at https://osdn.net/projects/joypy/.
-      Created using Sphinx 1.7.3.
+      Created using Sphinx 3.0.2.
     

 
   
diff --git a/docs/sphinx_docs/_build/html/notebooks/NoUpdates.html b/docs/sphinx_docs/_build/html/notebooks/NoUpdates.html
index 0d74e1c..f15ea6b 100644
--- a/docs/sphinx_docs/_build/html/notebooks/NoUpdates.html
+++ b/docs/sphinx_docs/_build/html/notebooks/NoUpdates.html
@@ -1,19 +1,18 @@
 
-
+
 
-
+
   
-    
-    
+    
     No Updates — Thun 0.2.0 documentation
     
     
-    
-    
-    
-    
-    
+    
+    
+    
+    
+    
+    
     
     
     
@@ -30,39 +29,82 @@
     

       

         

+          
+
           

             
   

 
No Updates

 
DRAFT

 
    
-
  1. Joy doesn’t need to change.
    2. 
+
  2. Joy doesn’t need to change.
    3. 
 

 

 
    
-
  1. The interpreter doesn’t need to change, viewer function can customize mainloop.  Or use a sub-interpreter (Joy in Joy.)  The base interpreter remains static.
    2. 
-
  2. Once a function has been named and defined never change that name.  It’s just not allowed.  If you need to change a function foo you have to call it foo_II or something.  Once a function (name mapped to behavior) is released to the public that’s it, it’s done.
    3. 
-
  3. The language evolves by adding new definitions and refactoring, always choosing new names for new functions.
    4. 
+
  4. The interpreter doesn’t need to change, viewer function can customize mainloop.  Or use a sub-interpreter (Joy in Joy.)  The base interpreter remains static.
    5. 
+
  5. Once a function has been named and defined never change that name.  It’s just not allowed.  If you need to change a function foo you have to call it foo_II or something.  Once a function (name mapped to behavior) is released to the public that’s it, it’s done.
    6. 
+
  6. The language evolves by adding new definitions and refactoring, always choosing new names for new functions.
    7. 
 

 

 
    
-
  1. Following Semantic Versioning there will never be a version 2.0.
    2. 
+
  2. Following Semantic Versioning there will never be a version 2.0.
    3. 
 

 

 
    
-
  1. Major version must be incremented if any backwards incompatible changes are introduced to the public API.
    2. 
-
  2. We never implement any backwards incompatible changes, so…
    3. 
-
  3. We could see e.g. Thun version 1.273.3!
    4. 
+
  4. Major version must be incremented if any backwards incompatible changes are introduced to the public API.
    5. 
+
  5. We never implement any backwards incompatible changes, so…
    6. 
+
  6. We could see e.g. Thun version 1.273.3!
    7. 
 

 

 

 
 
           

+