The NAND Programming Language

Version: 0.2

The NAND programming language was designed to accompany the upcoming book "Introduction to Theoretical Computer Science". This is an appendix to this book, which is also available online as a Jupyter notebook in the boazbk/nandnotebooks on Github. You can also try the live binder version.

The NAND programming language is part of a family of languages:

  • NAND: The NAND programming language is equivalent in expressive power to Boolean circuits. Specifically NAND programs are straightline programs with the NAND operation, which are equivalent to Boolean circuits with NAND gates.

  • NAND++: The NAND++ programming language is equivalent in expressive power to Turing Machines. NAND++ programs are obtained by adding loops and unbounded arrays to NAND programs. Specifically, NAND++ programs can be thought of as capturing oblivious single tape Turing Machines, that are polynomially equivalent to all other standard variants of Turing Machines and Turing-equivalent models of computation.

  • NAND<<: The NAND<< programing language is a formalization of RAM Machines. NAND<< programs are obtained by adding integer-valued variables and arrays, and the standard "C type" operations on them, as well as indirect indexing of arrays via integer variables. NAND<< programs are equivalent up to polylogarithmic terms to standard models of RAM machines, and up to polynomial terms with NAND++ and all other standard Turing-equivalent models.

  • QNAND: QNAND is only used in a single chapter of the book, and is meant to capture Quantum Boolean Circuits and so can be used to define the class BQP of polyonmial time quantum computaiton.

Syntax of NAND programs

This notebook/appendix is concerned with the first and simplest of these languages: the NAND Programming Language, which appears in Chapter 3: "Defining Computation".

A NAND program consists of a sequence of lines, each of the following form:

foo = NAND(bar,blah)

where foo, bar and blah are variable identifiers.

We have two special types of variables: input variables have the form X[ $i$ ] where $i$ is a natural number, and output variables have the form Y[$j$ ] where $j$ is a natural number. When a NAND program is executed on input $x \in \{0,1\}^n$, the variable X[$i$ ] is assigned the value $x_i$ for all $i\in [n]$. The output of the program is the list of $m$ values Y[0]$\ldots$ Y[$m-1$ ], where $m-1$ is the largest index for which the variable Y[$m-1$ ] is assigned a value in the program.

Here is an example of a NAND program:

In [1]:
xor = r'''
u = NAND(X[0],X[1]) 
v = NAND(X[0],u)
w = NAND(X[1],u)  
Y[0] = NAND(v,w)

To evaluate this program on inputs $x_0,x_1 \in \{0,1\}$, we can use a simple Python function that would keep track of the values assigned to variables.

In [2]:
def NAND(x,y):
    """Compute the NAND of two 0/1 valued variables."""
    return 1 - x*y
In [3]:
import re

def EVAL(prog,x):
    """Evaluate NAND program prog on input x."""
    (n,m) = numinout(prog) # utility function to get num of inputs/outputs
    vartable = {} # dictionary for variables
    for i in range(n): vartable[f'X[{i}]']=x[i] # assign x[i] to variable "X[i]"
    for line in filter(None,prog.split('\n')): # split into lines, throw out empty ones
        # split to components of a line:
        foo,bar,blah, = filter(None,re.split('\s*=\s*NAND\s*\(\s*|\s*\,\s*|\s*\)\s*|\s+',line)) 
        vartable[foo] =  NAND(vartable[bar],vartable[blah])
    return [vartable[f'Y[{j}]'] for j in range(m)]
In [4]:
# The code in this and other notebooks should not be considered as an example of good coding practice.
# I am not a coder by any means. 
# Also, whenever faced with a choice, I picked simplicity of code or brevity over robustness.
# It is quite possible that running these functions with malformed inputs would trigger the Zombie apocalypse.
In [5]:
# utility function
def numinout(prog):
    '''Compute the number of inputs and outputs of a NAND program, given as a string of source code.'''
    n = max([int(s[2:-1]) for s in re.findall(r'X\[\d+\]',prog)])+1
    m = max([int(s[2:-1]) for s in re.findall(r'Y\[\d+\]',prog)])+1
    return n,m

(2, 1)
In [6]:

Specification of NAND Programming language

We now describe a NAND program a little more formally. Every line in a NAND program has the form

$id1$ = NAND( $id2$ , $id3$ )

where $id1$,$id2$,$id3$ are variable identifier. A variable identifier is any sequence of letters, digits, and underscore and square bracket characters _,[,].

Variables whose identifiers have the form X[ $i$ ] where $i$ is a sequence of digits are called input variables.

Variables whose identifiers have the form Y[ $j$ ] where $j$ is a sequence of digits are called output variables.

All variables in NAND are Boolean: the can only get the values $0$ and $1$. If a variable is accessed before it is assigned a value then we assume the value defaults to zero (however such accesses are not legal in standard NAND programs, see below).

Execution of a NAND program

The number of inputs of a NAND program $P$ is one plus the largest number $i$ such that a variable of the form X[ $i$ ] appears in $P$. The number of outputs of $P$ is one plus the largest number $j$ such that a variable of the form Y[ $j$ ] appears in $P$.

If $P$ is a program with $n$ inputs and $m$ outputs, then the _execution of $P$ on input $x\in \{0,1\}^n$ is defined as follows:

  1. We assign to the variable X[ $i$ ] the value $x_i$ for all $i\in [n]$.

  2. We execute line by line the program, where for each line of the form $id1$ = NAND( $id2$ , $id3$ ) we assign to the variable identified by $id1$ the NAND of the values of the variables identified by $id2$ and $id3$.

  3. We output the $m$ values assigned to the variables Y[ $0$ ] $,\ldots,$ Y[ $m-1$ ]

Standard or "well formed" NAND programs

We define the following as the "standard form" of a NAND program:

  • While a priori variables can be any sequence of letters, digits, underscores and brackets, we will assume our identifiers have one of the following two forms:

    • A sequence of lower case letters, numbers, and underscores, that contain no upper case letters or brackets. For example foo, bar_blah , hello_world , boaz1234.

    • An identifier starting with a single capital letter, optionally followed by lower case letters, numbers, and underscores, and ending in [ $i$ ] where $i$ is a sequence of digits with no leading zeroes. For example X[17] or Foo[22] or Bar_blah[103].

  • We will assume no variable is used before it is assigned a value. The output variables are never read from (i.e., never on the lefthand side of an assignment) and the input variables are never written to (i.e., never on the righthand side of an assignment).

  • All output variables are written to, and all input variables are read from. That is, if a variable of the form X[ $i$ ] appears in the program then X[ $i'$ ] should also appear for all $0 \leq i' < i$. If a variable of the form Y[ $j$ ] appears in the program, then Y[ $j'$ ] should also appear for all $0 \leq j' < j$.

By default, every NAND program is assumed to be in standard form. Note that it is very easy to transform a NAND program into standard form, with a small cost in the number of lines. Specifically, we can ensure standard form by doing the following:

  1. Modify variable names to fit out convention.
  2. Add two lines to define a zero variable that is identically zero, and then use that in place of variables that haven't been assigned a value.
  3. Add at most $n+m$ lines to touch all input and output variables.

For simplicity, we will often describe our results only for standard form NAND programs (for example the function EVAL above would throw an Exception if a variable is accessed before it's assigned a value), but they are of course easy to extend to general NAND programs through the transformation above.

NAND interpreter via Python

While we could easily write a "NAND interpreter" in any programming language, by design a NAND program uses valid Python code. So we can also write NAND programs as python functions:

In [7]:
def XOR(a,b):
    t1 = NAND(a,b)
    t2 = NAND(a,t1)
    t3 = NAND(b,t1)
    return NAND(t2,t3)


We can translate such a function into standard NAND code using a simple trick. The idea is that we evaluate the program "symbolically" giving it as inputs the pair of strings X[0] and X[1] instead of integers.

In [112]:
except Exception as e:
can't multiply sequence by non-int of type 'str'

Of course we get a type error since NAND expects integers. When we need to do is to "override" the NAND function to take a pair of strings bar, blah instead of integers as input and generate the line of code foo = NAND(bar,blah) instead of computing the NAND function.

For example, the following almost works (except the output variable is not of the right form Y[ $j$ ])

In [9]:
count = 0

# Redfine NAND to take strings as input rather than integers
def NAND(bar,blah): 
    global count
    foo = f"Temp[{count}]"
    count +=1
    print(f"{foo} = NAND({bar},{blah}))")
    return foo

Temp[0] = NAND(X[0],X[1]))
Temp[1] = NAND(X[0],Temp[0]))
Temp[2] = NAND(X[1],Temp[0]))
Temp[3] = NAND(Temp[1],Temp[2]))

Let us fix the definition of NAND back to its right form, and then give a more robust version of a program that maps a Python function that implements a NAND program into the code/

In [10]:
def NAND(a,b): return 1-a*b
In [11]:
def nandcode(f):
    Extract the NAND code of a given function f.
    Works by temporarily modifying NAND to take strings instead of integers,
    and generate on imput bar,blah a temporary variable identifier foo and the line
    'foo = NAND(bar,blah)'
    n = numarguments(f)
    counter = 0 # to ensure unique temporary variables.
    code = ''
    def tempNAND(bar,blah):
        nonlocal code, counter 
        foo = f'Temp[{counter}]'
        counter += 1
        code += f'{foo} = NAND({bar},{blah})\n'
        return foo
    outputs = runwith(lambda : f(*[f'X[{i}]' for i in range(n)]),"NAND",tempNAND) 
    # execute f on the strings "X[0]", "X[1]", ... with NAND reassigned to tempNAND
    if type(outputs)==str: outputs = [outputs] # make single output into singleton list
    for j in range(len(outputs)):
        code = code.replace(outputs[j],f'Y[{j}]')
    return code
In [12]:
# Some utility functions 
# (can ignore on first read, uses some Python trickery that's not so important for us)

from inspect import signature
def numarguments(f):
    """Number of arguments a Python function takes."""
    return len(signature(f).parameters)

def runwith(f,*args):
    """Evaluate function f binding name to func"""
    g = globals()
    old = {}
    new = {}
    for i in range(0,len(args),2):
        old[args[i]] = g[args[i]]
        new[args[i]] = args[i+1]
        # a little bit of an ugly hack 
        # if you know a nicer way, please let me know
        for name in new: g[name] = new[name]
        res = f()
        for name in old: g[name] = old[name]
    return res
In [13]:
Temp[0] = NAND(X[0],X[1])
Temp[1] = NAND(X[0],Temp[0])
Temp[2] = NAND(X[1],Temp[0])
Y[0] = NAND(Temp[1],Temp[2])

In [14]:

Syntactic sugar

NAND is pretty bare bones, and writing NAND code directly gets real old real fast. However, we can use "syntactic sugar" to make it a little less tedious. For example we can use function definitions to avoid copying again and again repetitive code.

We will use the Python-like syntax of def func(...): to define functions and so we can write the XOR on 4 bits function as follows:

In [15]:
def XOR4(a,b,c,d):
    return XOR(XOR(a,b),XOR(c,d))


To verify that this is indeed merely "syntactic sugar" and this can be translated to pure NAND we can use our nandcode function:

In [16]:
Temp[0] = NAND(X[0],X[1])
Temp[1] = NAND(X[0],Temp[0])
Temp[2] = NAND(X[1],Temp[0])
Temp[3] = NAND(Temp[1],Temp[2])
Temp[4] = NAND(X[2],X[3])
Temp[5] = NAND(X[2],Temp[4])
Temp[6] = NAND(X[3],Temp[4])
Temp[7] = NAND(Temp[5],Temp[6])
Temp[8] = NAND(Temp[3],Temp[7])
Temp[9] = NAND(Temp[3],Temp[8])
Temp[10] = NAND(Temp[7],Temp[8])
Y[0] = NAND(Temp[9],Temp[10])

Once we have this, we can also define other functions such as AND, OR, NOT, and also the IF function that on input cond, a and b returns a if cond equals 1 and b otherwise.

In [17]:
def NOT(a):
    return NAND(a,a)

def AND(a,b):
    return NOT(NAND(a,b))

def OR(a,b):
    return NAND(NOT(a),NOT(b))

def IF(cond,first,sec):
    temp1 = AND(cond,first) # zero if cond=0, otherwise first
    temp2 = AND(NOT(cond),sec) # zero if cond=1, otherwise second
    return OR(temp1,temp2)

def one(a):
    return NAND(a,NOT(a))

def zero(a):
    return NOT(one(a))

def COPY(a):
    return NOT(NOT(a))


We can use more python-inspired syntactic sugar:

In [18]:
def increment(X): # increment integer given in binary representation
    n = len(X)
    Y = ["*"]*(n+1) # will be overwritten anyway
    carry = one(X[0])
    for i in range(n):
        Y[i] = XOR(X[i],carry)
        carry = AND(X[i],carry)
    Y[n] = COPY(carry)
    return Y

def inc5(a,b,c,d,e):
    return increment([a,b,c,d,e])
In [19]:
[0, 0, 1, 0, 0, 0]
In [20]:
Temp[0] = NAND(X[0],X[0])
Temp[1] = NAND(X[0],Temp[0])
Temp[2] = NAND(X[0],Temp[1])
Temp[3] = NAND(X[0],Temp[2])
Temp[4] = NAND(Temp[1],Temp[2])
Y[0] = NAND(Temp[3],Temp[4])
Temp[6] = NAND(X[0],Temp[1])
Temp[7] = NAND(Temp[6],Temp[6])
Temp[8] = NAND(X[1],Temp[7])
Temp[9] = NAND(X[1],Temp[8])
Temp[10] = NAND(Temp[7],Temp[8])
Y[1] = NAND(Temp[9],Temp[10])
Temp[12] = NAND(X[1],Temp[7])
Temp[13] = NAND(Temp[12],Temp[12])
Temp[14] = NAND(X[2],Temp[13])
Temp[15] = NAND(X[2],Temp[14])
Temp[16] = NAND(Temp[13],Temp[14])
Y[2] = NAND(Temp[15],Temp[16])
Temp[18] = NAND(X[2],Temp[13])
Temp[19] = NAND(Temp[18],Temp[18])
Temp[20] = NAND(X[3],Temp[19])
Temp[21] = NAND(X[3],Temp[20])
Temp[22] = NAND(Temp[19],Temp[20])
Y[3] = NAND(Temp[21],Temp[22])
Temp[24] = NAND(X[3],Temp[19])
Temp[25] = NAND(Temp[24],Temp[24])
Temp[26] = NAND(X[4],Temp[25])
Temp[27] = NAND(X[4],Temp[26])
Temp[28] = NAND(Temp[25],Temp[26])
Y[4] = NAND(Temp[27],Temp[28])
Temp[30] = NAND(X[4],Temp[25])
Temp[31] = NAND(Temp[30],Temp[30])
Temp[32] = NAND(Temp[31],Temp[31])
Y[5] = NAND(Temp[32],Temp[32])

In [21]:
[0, 1, 1, 0, 0, 0]

We can create functions such as inc5 for every n via a little Python trickery:

In [22]:
def restrict(f,n):
    """Create function that restricts the function f to exactly n inputs"""
    args = ", ".join(f'arg{i}' for i in range(n))
    code =  rf'''
def _temp({args}):
    return f([{args}])
    l = dict(locals())
    return l["_temp"]
In [23]:
inc7 = restrict(increment,7)

[0, 0, 0, 1, 0, 0, 1, 0]
In [24]:
Temp[0] = NAND(X[0],X[0])
Temp[1] = NAND(X[0],Temp[0])
Temp[2] = NAND(X[0],Temp[1])
Temp[3] = NAND(X[0],Temp[2])
Temp[4] = NAND(Temp[1],Temp[2])
Y[0] = NAND(Temp[3],Temp[4])
Temp[6] = NAND(X[0],Temp[1])
Temp[7] = NAND(Temp[6],Temp[6])
Temp[8] = NAND(X[1],Temp[7])
Temp[9] = NAND(X[1],Temp[8])
Temp[10] = NAND(Temp[7],Temp[8])
Y[1] = NAND(Temp[9],Temp[10])
Temp[12] = NAND(X[1],Temp[7])
Temp[13] = NAND(Temp[12],Temp[12])
Temp[14] = NAND(X[2],Temp[13])
Temp[15] = NAND(X[2],Temp[14])
Temp[16] = NAND(Temp[13],Temp[14])
Y[2] = NAND(Temp[15],Temp[16])
Temp[18] = NAND(X[2],Temp[13])
Temp[19] = NAND(Temp[18],Temp[18])
Temp[20] = NAND(X[3],Temp[19])
Temp[21] = NAND(X[3],Temp[20])
Temp[22] = NAND(Temp[19],Temp[20])
Y[3] = NAND(Temp[21],Temp[22])
Temp[24] = NAND(X[3],Temp[19])
Temp[25] = NAND(Temp[24],Temp[24])
Temp[26] = NAND(X[4],Temp[25])
Temp[27] = NAND(X[4],Temp[26])
Temp[28] = NAND(Temp[25],Temp[26])
Y[4] = NAND(Temp[27],Temp[28])
Temp[30] = NAND(X[4],Temp[25])
Temp[31] = NAND(Temp[30],Temp[30])
Temp[32] = NAND(X[5],Temp[31])
Temp[33] = NAND(X[5],Temp[32])
Temp[34] = NAND(Temp[31],Temp[32])
Y[5] = NAND(Temp[33],Temp[34])
Temp[36] = NAND(X[5],Temp[31])
Temp[37] = NAND(Temp[36],Temp[36])
Temp[38] = NAND(X[6],Temp[37])
Temp[39] = NAND(X[6],Temp[38])
Temp[40] = NAND(Temp[37],Temp[38])
Y[6] = NAND(Temp[39],Temp[40])
Temp[42] = NAND(X[6],Temp[37])
Temp[43] = NAND(Temp[42],Temp[42])
Temp[44] = NAND(Temp[43],Temp[43])
Y[7] = NAND(Temp[44],Temp[44])

NAND Programs and circuits

NAND programs are equivalent to the model of Boolean circuits. We can present the graph corresponding to a NAND function using ideas similar to those we used to print the code. Below we have some python code to draw circuits; as usual you can skip over it in a first reading.

In [25]:
%matplotlib inline
%config InlineBackend.figure_format = 'svg'
In [26]:
# Below we have two different implementations, that use two different libraries to draw circuits
# Schemdraw has nicer gates, but doesn't do automatic layout of graphs
# Graphviz has automatic layout but I couldn't figure out a way to get the gates to look as nice
# Hopefully eventually I'll find the optimal way - help is welcome!
In [27]:
# Use schemdraw to visualize circuits
import SchemDraw as schem
import SchemDraw.elements as e
import SchemDraw.logic as l

def disp(self):
schem.Drawing._ipython_display_ =  disp
In [28]:
# Schemdraw version
def sdnandcircuit(f):
    """Compute the graph representating a NAND circuit for a NAND program, given as a Python function."""
    n = numarguments(f)
    counter = 0 # to ensure unique temporary variables.
    G =   schem.Drawing(unit=.5,fontsize=8)
    curx,cury = 0,0
    def incr(jump = False):
        nonlocal curx, cury, n;
        UX = 2.5
        UY = 3.5
        if not jump and (cury>-UY*(n-1)):
            cury -= UY
            cury = 0
            curx = (curx // UX)*UX + UX
        if (curx): curx += abs(cury)*UX/(2*n*UY)
    nodes = {}
    def tempNAND(bar,blah):
        nonlocal G, counter, curx,cury
        var = f'Temp[{counter}]'
        counter += 1
        g = G.add(l.NAND2,xy=[curx,cury], d="right")#, label=var)
        nodes[var] = g
        i1 = nodes[bar]
        in1 = i1.out if "out" in dir(i1)   else i1.end 
        i2 = nodes[blah]
        in2 = i2.out if "out" in dir(i2)   else i2.end 
        return var
    for i in range(n):
        nodes[f'X[{i}]'] = G.add(e.DOT, xy = [curx,cury], lftlabel=f'X[{i}]') 
    outputs = runwith(lambda: f(*[f'X[{i}]' for i in range(n)]),'NAND',tempNAND)
    if type(outputs)==str: outputs = [outputs] # make single output into singleton list
    for j in range(len(outputs)):
        g= nodes[outputs[j]]
        o =G.add(e.DOT,xy=[curx,cury],rgtlabel=f'Y[{j}]')
    return G
In [29]:
#Use Graphviz to visualize circuits
import graphviz
from graphviz import Graph
from graphviz import Digraph
In [30]:
#Graphviz version
def gvnandcircuit(f):
    """Compute the graph representating a NAND circuit for a NAND program, given as a Python function."""
    n = numarguments(f)
    counter = 0 # to ensure unique temporary variables.
    G =  Digraph(graph_attr= {"rankdir":"LR"}) # schem.Drawing(unit=.5)
    def tempNAND(bar,blah):
        nonlocal G, counter 
        var = f'Temp[{counter}]'
        counter += 1
        return var
    for i in range(n):
        G.node(f'X[{i}]',label=f'X[{i}]', fontcolor='blue',shape='circle') 
    outputs = runwith(lambda: f(*[f'X[{i}]' for i in range(n)]),'NAND',tempNAND)
    if type(outputs)==str: outputs = [outputs] # make single output into singleton list
    for j in range(len(outputs)):
    return G
In [31]:
def nandcircuit(f,method="Graphviz"):
    return gvnandcircuit(f) if method=="Graphviz" else sdnandcircuit(f)

We can now use these functions to draw the circuit corresponding to a NAND function:

In [32]:
In [33]:
%3 X[0] X[0] Temp[0] ∧̅ X[0]->Temp[0] Temp[1] ∧̅ X[0]->Temp[1] X[1] X[1] X[1]->Temp[0] Temp[2] ∧̅ X[1]->Temp[2] Temp[0]->Temp[1] Temp[0]->Temp[2] Temp[3] Y[0] Temp[1]->Temp[3] Temp[2]->Temp[3]
In [34]:
%3 X[0] X[0] Temp[0] ∧̅ X[0]->Temp[0] X[0]->Temp[0] Temp[1] ∧̅ X[0]->Temp[1] Temp[2] ∧̅ X[0]->Temp[2] Temp[3] ∧̅ X[0]->Temp[3] Temp[6] ∧̅ X[0]->Temp[6] X[1] X[1] Temp[8] ∧̅ X[1]->Temp[8] Temp[9] ∧̅ X[1]->Temp[9] Temp[12] ∧̅ X[1]->Temp[12] X[2] X[2] Temp[14] ∧̅ X[2]->Temp[14] Temp[15] ∧̅ X[2]->Temp[15] Temp[18] ∧̅ X[2]->Temp[18] Temp[0]->Temp[1] Temp[1]->Temp[2] Temp[4] ∧̅ Temp[1]->Temp[4] Temp[1]->Temp[6] Temp[2]->Temp[3] Temp[2]->Temp[4] Temp[5] Y[0] Temp[3]->Temp[5] Temp[4]->Temp[5] Temp[7] ∧̅ Temp[6]->Temp[7] Temp[6]->Temp[7] Temp[7]->Temp[8] Temp[10] ∧̅ Temp[7]->Temp[10] Temp[7]->Temp[12] Temp[8]->Temp[9] Temp[8]->Temp[10] Temp[11] Y[1] Temp[9]->Temp[11] Temp[10]->Temp[11] Temp[13] ∧̅ Temp[12]->Temp[13] Temp[12]->Temp[13] Temp[13]->Temp[14] Temp[16] ∧̅ Temp[13]->Temp[16] Temp[13]->Temp[18] Temp[14]->Temp[15] Temp[14]->Temp[16] Temp[17] Y[2] Temp[15]->Temp[17] Temp[16]->Temp[17] Temp[19] ∧̅ Temp[18]->Temp[19] Temp[18]->Temp[19] Temp[20] ∧̅ Temp[19]->Temp[20] Temp[19]->Temp[20] Temp[21] Y[3] Temp[20]->Temp[21] Temp[20]->Temp[21]

Computing every function

It turns out that we can compute every function $f:\{0,1\}^n \rightarrow \{0,1\}$ by some NAND program.

The crucial element for that is the function LOOKUP that on input an index $i\in [n]$ (represented as a string of length $\log n$) and a table $T\in \{0,1\}^n$, outputs $t_i$.

In [35]:
def LOOKUP(T,i):
    l = len(i)
    if l==1:
        return IF(i[0],T[1],T[0])
    return IF(i[l-1],LOOKUP(T[2**(l-1):],i[:-1]),LOOKUP(T[:2**(l-1)],i[:-1]))

In [36]:
# A more efficient IF .. not strictly necessary
def IF(cond,a,b):
    notcond = NAND(cond,cond)
    temp = NAND(b,notcond)
    temp1 = NAND(a,cond)
    return NAND(temp,temp1)

# Let's check that it works
[f"{(a,b,c)}:{IF(a,b,c)}" for a in [0,1] for b in [0,1] for c in [0,1]]
['(0, 0, 0):0',
 '(0, 0, 1):1',
 '(0, 1, 0):0',
 '(0, 1, 1):1',
 '(1, 0, 0):0',
 '(1, 0, 1):0',
 '(1, 1, 0):1',
 '(1, 1, 1):1']

We can extract the NAND code of LOOKUP using the usual tricks.

In [37]:
# generalize restrict to handle functions that take more than one array
def restrict(f,*numinputs):
    """Create function that restricts the function f to exactly given input lengths n0,n1,..."""
    k = len(numinputs)
    args = []
    t = 0
    for i in range(k):
        if numinputs[i]: args = args + [", ".join(f'arg_{i}_{j}' for j in range(numinputs[i]))]
    sig = ", ".join(args)
    call = ", ".join(f"[{a}]" for a in args)
    code = rf'''
def _temp({sig}):
    return f({call})
    l = dict(locals())
    return l["_temp"]
In [38]:
def funclookup(l):
    return restrict(LOOKUP,2**l,l)
In [39]:
f = funclookup(3)
<function _temp(arg_0_0, arg_0_1, arg_0_2, arg_0_3, arg_0_4, arg_0_5, arg_0_6, arg_0_7, arg_1_0, arg_1_1, arg_1_2)>
In [40]:
In [44]:
Temp[0] = NAND(X[8],X[8])
Temp[1] = NAND(X[6],Temp[0])
Temp[2] = NAND(X[7],X[8])
Temp[3] = NAND(Temp[1],Temp[2])
Temp[4] = NAND(X[8],X[8])
Temp[5] = NAND(X[4],Temp[4])
Temp[6] = NAND(X[5],X[8])
Temp[7] = NAND(Temp[5],Temp[6])
Temp[8] = NAND(X[9],X[9])
Temp[9] = NAND(Temp[7],Temp[8])
Temp[10] = NAND(Temp[3],X[9])
Temp[11] = NAND(Temp[9],Temp[10])
Temp[12] = NAND(X[8],X[8])
Temp[13] = NAND(X[2],Temp[12])
Temp[14] = NAND(X[3],X[8])
Temp[15] = NAND(Temp[13],Temp[14])
Temp[16] = NAND(X[8],X[8])
Temp[17] = NAND(X[0],Temp[16])
Temp[18] = NAND(X[1],X[8])
Temp[19] = NAND(Temp[17],Temp[18])
Temp[20] = NAND(X[9],X[9])
Temp[21] = NAND(Temp[19],Temp[20])
Temp[22] = NAND(Temp[15],X[9])
Temp[23] = NAND(Temp[21],Temp[22])
Temp[24] = NAND(X[10],X[10])
Temp[25] = NAND(Temp[23],Temp[24])
Temp[26] = NAND(Temp[11],X[10])
Y[0] = NAND(Temp[25],Temp[26])

In [45]:
%3 X[0] X[0] Temp[17] ∧̅ X[0]->Temp[17] X[1] X[1] Temp[18] ∧̅ X[1]->Temp[18] X[2] X[2] Temp[13] ∧̅ X[2]->Temp[13] X[3] X[3] Temp[14] ∧̅ X[3]->Temp[14] X[4] X[4] Temp[5] ∧̅ X[4]->Temp[5] X[5] X[5] Temp[6] ∧̅ X[5]->Temp[6] X[6] X[6] Temp[1] ∧̅ X[6]->Temp[1] X[7] X[7] Temp[2] ∧̅ X[7]->Temp[2] X[8] X[8] Temp[0] ∧̅ X[8]->Temp[0] X[8]->Temp[0] X[8]->Temp[2] Temp[4] ∧̅ X[8]->Temp[4] X[8]->Temp[4] X[8]->Temp[6] Temp[12] ∧̅ X[8]->Temp[12] X[8]->Temp[12] X[8]->Temp[14] Temp[16] ∧̅ X[8]->Temp[16] X[8]->Temp[16] X[8]->Temp[18] X[9] X[9] Temp[8] ∧̅ X[9]->Temp[8] X[9]->Temp[8] Temp[10] ∧̅ X[9]->Temp[10] Temp[20] ∧̅ X[9]->Temp[20] X[9]->Temp[20] Temp[22] ∧̅ X[9]->Temp[22] X[10] X[10] Temp[24] ∧̅ X[10]->Temp[24] X[10]->Temp[24] Temp[26] ∧̅ X[10]->Temp[26] Temp[0]->Temp[1] Temp[3] ∧̅ Temp[1]->Temp[3] Temp[2]->Temp[3] Temp[3]->Temp[10] Temp[4]->Temp[5] Temp[7] ∧̅ Temp[5]->Temp[7] Temp[6]->Temp[7] Temp[9] ∧̅ Temp[7]->Temp[9] Temp[8]->Temp[9] Temp[11] ∧̅ Temp[9]->Temp[11] Temp[10]->Temp[11] Temp[11]->Temp[26] Temp[12]->Temp[13] Temp[15] ∧̅ Temp[13]->Temp[15] Temp[14]->Temp[15] Temp[15]->Temp[22] Temp[16]->Temp[17] Temp[19] ∧̅ Temp[17]->Temp[19] Temp[18]->Temp[19] Temp[21] ∧̅ Temp[19]->Temp[21] Temp[20]->Temp[21] Temp[23] ∧̅ Temp[21]->Temp[23] Temp[22]->Temp[23] Temp[25] ∧̅ Temp[23]->Temp[25] Temp[24]->Temp[25] Temp[27] Y[0] Temp[25]->Temp[27] Temp[26]->Temp[27]

We can also track by how much the number of lines grows: we see that it is about $4\cdot 2^\ell$:

In [42]:
[len(nandcode(funclookup(l)).split('\n'))/2**l for l in range(1,8,1)]
[2.5, 3.25, 3.625, 3.8125, 3.90625, 3.953125, 3.9765625]

Representing NAND programs as lists of triples

We can represent a NAND program in many ways including the string of its source code, as the graph corresponding to its circuit. One simple representation of a NAND program we will use is as the following:

We represent a NAND program of $t$ intermediate variables, $s$ lines, $n$ input variables, and $m$ input variables as a triple $(n,m,L)$ where $L$ is a list of $s$ triples of the form $(a,b,c)$ of numbers in $[n+t+m]$.

A triple $(a,b,c)$ corresponds to the line assigning to the variable corresponding $a$ the NAND of the variables corresponding to $b$ and $c$. We identify the first $n$ variables with the input and the last $m$ variables with the outputs.

We can again compute this representation using Python:

In [46]:
def nandrepresent(f):
    """Compute the list of triple representation for a NAND program, given by a Python function."""
    n = numarguments(f)
    counter = n # to ensure unique temporary variables.
    L = [] # list of tuples
    def tempNAND(bar,blah):
        nonlocal L, counter 
        var = counter
        counter += 1
        L += [(var,bar,blah)] 
        return var
    outputs = runwith(lambda: f(*range(n)), "NAND", tempNAND) 
    if type(outputs)==int: outputs = [outputs] # make single output into singleton list
    m = len(outputs)
    # make sure outputs are last m variables
    for j in range(m):
        def flip(a):
            nonlocal counter, outputs, j
            if a==outputs[j]:  return counter+j
            return a
        L = [(flip(a),flip(b),flip(c)) for (a,b,c) in L]
    return (n,m,compact(L))

# utlity function
def compact(L):
    """Compact list of triples to remove unused variables."""
    s = sorted(set.union(*[set(T) for T in L]))
    return [ (s.index(a),s.index(b),s.index(c)) for (a,b,c) in L]

(2, 1, [(2, 0, 1), (3, 0, 2), (4, 1, 2), (5, 3, 4)])

We can directly evaluate a NAND program based on its list of triples representation:

In [47]:
def EVALnand(prog,X):
    """Evaluate a NAND program from its list of triple representation."""
    n,m,L = prog
    vartable = X+[0]*(max(max(a,b,c) for (a,b,c) in L)-n+1)
    for (a,b,c) in L:
        vartable[a] = NAND(vartable[b],vartable[c])
    return [vartable[-m+j] for j in range(m)]
In [49]:
In [50]:

Pruning (optional)

We can do some simple transformations to reduce the size of our programs/circuits. For example, if two gates have exactly the same inputs then we can identify them with one another. We can also use the equality NOT(NOT(a))=a, as well as remove unused variables.

In [51]:
def prune(prog):
    """Prune representation of program as tuples, removing duplicate lines and unused variables."""
    n,m,L = prog
    L = list(L)
    def identify(L,e,f):
        # identify vertex e with vertex f
        def ident(k): 
            nonlocal e,f
            return f if k==e else k
        return [(ident(a),ident(b),ident(c)) for (a,b,c) in L]
    t = max([max(a,b,c) for (a,b,c) in L])+1

    while True:
        neighborhood = {}
        neighbors = {}
        found = False 
        for (a,b,c) in L:
            N = frozenset([b,c])
            if a>=t-m: continue # don't remove output variables
            if N in neighborhood: # there was prior duplicate line
                L = identify(L,a,neighborhood[N])
                found = True
            if b==c and b in neighbors and len(neighbors[b])==1: # line is NOT of NOT of prior line
                L = identify(L,a,next(iter(neighbors[b])))
                found = True
            neighborhood[N] = a
            neighbors[a] = N
        touched   = {a: False for a in range(t)} 
        for (a,b,c) in L: 
            touched[b] = True
            touched[c] = True

        for d in range(n,t-m,1): # remove non output and input variables that are not used
            if not touched[d]: 
                for (a,b,c) in L:
                    if a==d:
                        found =True
        if not found: break
    return (n,m,compact(L))        

Some examples

In [52]:
# Majority
def MAJ(a,b,c): return NAND(NAND(NAND(NAND(a,b),NAND(a,c)),NAND(NAND(a,b),NAND(a,c))),NAND(b,c))

# Integer addition of two n bit numbers
def ADD(A,B):
    n = len(A)
    Result = [0]*(n+1)
    Carry  = [0]*(n+1)
    Carry[0] = zero(A[0])
    for i in range(n):
        Result[i] = XOR(Carry[i],XOR(A[i],B[i]))
        Carry[i+1] = MAJ(Carry[i],A[i],B[i])
    Result[n] = Carry[n]
    return Result
In [53]:
f = restrict(ADD,2,2)
P = nandrepresent(f)
In [54]:
all([(f(a,b,c,d)==EVALnand(prune(P),[a,b,c,d])) for a in [0,1] for b in [0,1] for c in [0,1] for d in [0,1] ])

From representation to code or graph

We can use the list of triples representation as a starting point to obtain the NAND program as a list of lines of code, or as a circuit (i.e., directed acyclic graph).

In [65]:
# Graphviz version
def gvrep2circuit(P):
    """Return circuit (i.e., graph) corresponding to NAND program P given in list of tuples representation."""
    n,m,L = P
    G = Digraph(graph_attr= {"rankdir":"LR"})
    for i in range(n):
        G.node(f"v{i}",label=f'X[{i}]', fontcolor='blue',shape='square')
    t = n
    for (a,b,c) in L:
        G.node(f"v{a}",label='∧\u0305',shape='invhouse',orientation='90')  # shape='none' image='NAND_gate.png') 
        t = max(t,a,b,c)

    t += 1
    for j in range(m):
    return G
In [66]:

# Schemdraw version
def sdrep2circuit(P):
    """Return circuit (i.e., graph) corresponding to NAND program P given in list of tuples representation."""
    n,m,L = P
    G =   schem.Drawing(unit=.5,fontsize=8)
    curx,cury = 0,0
    def incr(jump = False):
        nonlocal curx, cury, n;
        UX = 2.5
        UY = 3.5
        if not jump and (cury>-UY*(n-1)):
            cury -= UY
            cury = 0
            curx = (curx // UX)*UX + UX
        if (curx): curx += abs(cury)*UX/(2*n*UY)
    nodes = {}
    for i in range(n):
        nodes[f'v{i}'] = G.add(e.DOT, xy = [curx,cury], lftlabel=f'X[{i}]') 
    t = n
    for (a,b,c) in L:
        var = f"v{a}"
        g = G.add(l.NAND2,xy=[curx,cury], d="right")#, label=var)
        nodes[var] = g
        i1 = nodes[f"v{b}"]
        in1 = i1.out if "out" in dir(i1)   else i1.end 
        i2 = nodes[f"v{c}"]
        in2 = i2.out if "out" in dir(i2)   else i2.end 
        t = max(t,a,b,c)

    t += 1
    for j in range(m):
        g= nodes[f"v{t-m+j}"]
        o =G.add(e.DOT,xy=[curx,cury],rgtlabel=f'Y[{j}]')
    return G
In [67]:
def rep2circuit(P,method="Graphviz"):
    return gvrep2circuit(P) if method=="Graphviz" else sdrep2circuit(P)
In [68]:
%3 v0 X[0] v4 ∧̅ v0->v4 v0->v4 v5 ∧̅ v0->v5 v7 ∧̅ v0->v7 v8 ∧̅ v0->v8 v14 ∧̅ v0->v14 v17 ∧̅ v0->v17 v21 ∧̅ v0->v21 v1 X[1] v23 ∧̅ v1->v23 v24 ∧̅ v1->v24 v30 ∧̅ v1->v30 v33 ∧̅ v1->v33 v37 ∧̅ v1->v37 v2 X[2] v2->v7 v9 ∧̅ v2->v9 v15 ∧̅ v2->v15 v18 ∧̅ v2->v18 v2->v21 v3 X[3] v3->v23 v25 ∧̅ v3->v25 v31 ∧̅ v3->v31 v34 ∧̅ v3->v34 v3->v37 v4->v5 v6 ∧̅ v5->v6 v5->v6 v11 ∧̅ v6->v11 v12 ∧̅ v6->v12 v6->v14 v6->v15 v6->v17 v6->v18 v7->v8 v7->v9 v10 ∧̅ v8->v10 v9->v10 v10->v11 v13 ∧̅ v10->v13 v11->v12 v11->v13 v38 Y[0] v12->v38 v13->v38 v16 ∧̅ v14->v16 v15->v16 v20 ∧̅ v16->v20 v19 ∧̅ v17->v19 v18->v19 v19->v20 v22 ∧̅ v20->v22 v21->v22 v27 ∧̅ v22->v27 v28 ∧̅ v22->v28 v22->v30 v22->v31 v22->v33 v22->v34 v23->v24 v23->v25 v26 ∧̅ v24->v26 v25->v26 v26->v27 v29 ∧̅ v26->v29 v27->v28 v27->v29 v39 Y[1] v28->v39 v29->v39 v32 ∧̅ v30->v32 v31->v32 v36 ∧̅ v32->v36 v35 ∧̅ v33->v35 v34->v35 v35->v36 v40 Y[2] v36->v40 v37->v40
In [69]:
In [70]:
%3 v0 X[0] v4 ∧̅ v0->v4 v0->v4 v5 ∧̅ v0->v5 v7 ∧̅ v0->v7 v8 ∧̅ v0->v8 v14 ∧̅ v0->v14 v1 X[1] v19 ∧̅ v1->v19 v20 ∧̅ v1->v20 v26 ∧̅ v1->v26 v2 X[2] v2->v7 v9 ∧̅ v2->v9 v15 ∧̅ v2->v15 v3 X[3] v3->v19 v21 ∧̅ v3->v21 v27 ∧̅ v3->v27 v4->v5 v6 ∧̅ v5->v6 v5->v6 v11 ∧̅ v6->v11 v12 ∧̅ v6->v12 v6->v14 v6->v15 v7->v8 v7->v9 v18 ∧̅ v7->v18 v10 ∧̅ v8->v10 v9->v10 v10->v11 v13 ∧̅ v10->v13 v11->v12 v11->v13 v30 Y[0] v12->v30 v13->v30 v16 ∧̅ v14->v16 v15->v16 v17 ∧̅ v16->v17 v16->v17 v17->v18 v23 ∧̅ v18->v23 v24 ∧̅ v18->v24 v18->v26 v18->v27 v19->v20 v19->v21 v32 Y[2] v19->v32 v22 ∧̅ v20->v22 v21->v22 v22->v23 v25 ∧̅ v22->v25 v23->v24 v23->v25 v31 Y[1] v24->v31 v25->v31 v28 ∧̅ v26->v28 v27->v28 v29 ∧̅ v28->v29 v28->v29 v29->v32
In [72]:
def rep2code(P):
    """Return NAND code corresponding to NAND program P, given in list of tuples representation"""
    n,m,L = P
    code = ""
    t = max([max(a,b,c) for (a,b,c) in L])+1
    def var(a):
        if a<n: return f"X[{a}]"
        if a>=t-m: return f"Y[{a-t+m}]"
        return f"Temp[{a-n}]"
    for (a,b,c) in L:
        code += f"\n{var(a)} = NAND({var(b)},{var(c)})"

    return code
In [74]:
Temp[0] = NAND(X[0],X[0])
Temp[1] = NAND(X[0],Temp[0])
Temp[2] = NAND(Temp[1],Temp[1])
Temp[3] = NAND(X[0],X[2])
Temp[4] = NAND(X[0],Temp[3])
Temp[5] = NAND(X[2],Temp[3])
Temp[6] = NAND(Temp[4],Temp[5])
Temp[7] = NAND(Temp[2],Temp[6])
Temp[8] = NAND(Temp[2],Temp[7])
Temp[9] = NAND(Temp[6],Temp[7])
Y[0] = NAND(Temp[8],Temp[9])
Temp[10] = NAND(Temp[2],X[0])
Temp[11] = NAND(Temp[2],X[2])
Temp[12] = NAND(Temp[10],Temp[11])
Temp[13] = NAND(Temp[2],X[0])
Temp[14] = NAND(Temp[2],X[2])
Temp[15] = NAND(Temp[13],Temp[14])
Temp[16] = NAND(Temp[12],Temp[15])
Temp[17] = NAND(X[0],X[2])
Temp[18] = NAND(Temp[16],Temp[17])
Temp[19] = NAND(X[1],X[3])
Temp[20] = NAND(X[1],Temp[19])
Temp[21] = NAND(X[3],Temp[19])
Temp[22] = NAND(Temp[20],Temp[21])
Temp[23] = NAND(Temp[18],Temp[22])
Temp[24] = NAND(Temp[18],Temp[23])
Temp[25] = NAND(Temp[22],Temp[23])
Y[1] = NAND(Temp[24],Temp[25])
Temp[26] = NAND(Temp[18],X[1])
Temp[27] = NAND(Temp[18],X[3])
Temp[28] = NAND(Temp[26],Temp[27])
Temp[29] = NAND(Temp[18],X[1])
Temp[30] = NAND(Temp[18],X[3])
Temp[31] = NAND(Temp[29],Temp[30])
Temp[32] = NAND(Temp[28],Temp[31])
Temp[33] = NAND(X[1],X[3])
Y[2] = NAND(Temp[32],Temp[33])
In [75]:
Temp[0] = NAND(X[0],X[0])
Temp[1] = NAND(X[0],Temp[0])
Temp[2] = NAND(Temp[1],Temp[1])
Temp[3] = NAND(X[0],X[2])
Temp[4] = NAND(X[0],Temp[3])
Temp[5] = NAND(X[2],Temp[3])
Temp[6] = NAND(Temp[4],Temp[5])
Temp[7] = NAND(Temp[2],Temp[6])
Temp[8] = NAND(Temp[2],Temp[7])
Temp[9] = NAND(Temp[6],Temp[7])
Y[0] = NAND(Temp[8],Temp[9])
Temp[10] = NAND(Temp[2],X[0])
Temp[11] = NAND(Temp[2],X[2])
Temp[12] = NAND(Temp[10],Temp[11])
Temp[13] = NAND(Temp[12],Temp[12])
Temp[14] = NAND(Temp[13],Temp[3])
Temp[15] = NAND(X[1],X[3])
Temp[16] = NAND(X[1],Temp[15])
Temp[17] = NAND(X[3],Temp[15])
Temp[18] = NAND(Temp[16],Temp[17])
Temp[19] = NAND(Temp[14],Temp[18])
Temp[20] = NAND(Temp[14],Temp[19])
Temp[21] = NAND(Temp[18],Temp[19])
Y[1] = NAND(Temp[20],Temp[21])
Temp[22] = NAND(Temp[14],X[1])
Temp[23] = NAND(Temp[14],X[3])
Temp[24] = NAND(Temp[22],Temp[23])
Temp[25] = NAND(Temp[24],Temp[24])
Y[2] = NAND(Temp[25],Temp[15])

We can now redefine the nandcircuit and nandcode functions to work as follows:

  1. First obtain the list of triples representation
  2. Then prune it
  3. Then transform it to either code or circuit appropriately
In [76]:
def nandcode(f):
    return rep2code(prune(nandrepresent(f)))

def nandcircuit(f, method="Graphviz"):
    return rep2circuit(prune(nandrepresent(f)),method)
In [77]:
%3 v0 X[0] v7 ∧̅ v0->v7 v0->v7 v8 ∧̅ v0->v8 v9 ∧̅ v0->v9 v10 ∧̅ v0->v10 v1 X[1] v13 ∧̅ v1->v13 v14 ∧̅ v1->v14 v2 X[2] v17 ∧̅ v2->v17 v18 ∧̅ v2->v18 v3 X[3] v21 ∧̅ v3->v21 v22 ∧̅ v3->v22 v4 X[4] v25 ∧̅ v4->v25 v26 ∧̅ v4->v26 v5 X[5] v29 ∧̅ v5->v29 v30 ∧̅ v5->v30 v6 X[6] v33 ∧̅ v6->v33 v34 ∧̅ v6->v34 v7->v8 v8->v9 v11 ∧̅ v8->v11 v9->v10 v9->v11 v12 ∧̅ v9->v12 v9->v12 v36 Y[0] v10->v36 v11->v36 v12->v13 v15 ∧̅ v12->v15 v13->v14 v13->v15 v16 ∧̅ v13->v16 v13->v16 v37 Y[1] v14->v37 v15->v37 v16->v17 v19 ∧̅ v16->v19 v17->v18 v17->v19 v20 ∧̅ v17->v20 v17->v20 v38 Y[2] v18->v38 v19->v38 v20->v21 v23 ∧̅ v20->v23 v21->v22 v21->v23 v24 ∧̅ v21->v24 v21->v24 v39 Y[3] v22->v39 v23->v39 v24->v25 v27 ∧̅ v24->v27 v25->v26 v25->v27 v28 ∧̅ v25->v28 v25->v28 v40 Y[4] v26->v40 v27->v40 v28->v29 v31 ∧̅ v28->v31 v29->v30 v29->v31 v32 ∧̅ v29->v32 v29->v32 v41 Y[5] v30->v41 v31->v41 v32->v33 v35 ∧̅ v32->v35 v33->v34 v33->v35 v43 Y[7] v33->v43 v33->v43 v42 Y[6] v34->v42 v35->v42

Universal circuit evaluation or NAND interpreter in NAND

We can construct a NAND program $P$ that given the representation of a NAND program $Q$ and an input $x$, outputs $Q(x)$. We can obviously compute such a function since every finite function is computable by a NAND program, but it turns out we can do so in a program that is polynomial in the size of $P$ (even quasiliinear but we won't show that here).

We start with a reimplementation of NANDEVAL in Python:

In [78]:
def GET(V,i): return V[i]

def UPDATE(V,i,b):
    return V

def NANDEVAL(n,m,L,X):
    # Evaluate a NAND program from its list of triple representation.
    s = len(L) # number of lines
    t = max(max(a,b,c) for (a,b,c) in L)+1 # maximum index in L + 1

    Vartable = [0] * t # we'll simply use an array to store data


    # load input values to Vartable:
    for i in range(n): Vartable = UPDATE(Vartable,i,X[i])

    # Run the program
    for (i,j,k) in L:
        a = GET(Vartable,j)
        b = GET(Vartable,k)
        c = NAND(a,b)
        Vartable = UPDATE(Vartable,i,c)

    # Return outputs Vartable[t-m], Vartable[t-m+1],....,Vartable[t-1]
    return [GET(Vartable,t-m+j) for j in range(m)]
In [79]:
L = ((2, 0, 1), (3, 0, 2), (4, 1, 2), (5, 3, 4))
print(NANDEVAL(2,1,L,(0,1))) # XOR(0,1)

print(NANDEVAL(2,1,L,(1,1))) # XOR(1,1)

Now transform this to work with the representation of L as a binary string, namely as a sequence of $3s$ numbers in $[t]$, each represented as a string of length $\ell = \lceil \log 3s \rceil$.

In [80]:
from math import ceil, floor, log2
def triplelist2string(L):
    """Transform list of triples into its representation as a binary string"""
    s = len(L)
    ell = ceil(log2(3*s))
    B = [0]*(3*s*ell)
    FlatL = [a for T in L for a in T]
    for i in range(3*s):
        for j in range(ell):
            B[ell*i + j] = floor(FlatL[i]/ 2**j) % 2
    return B

Evaluating a NAND program given its string representation

We can now present NANDEVALBIN which will be a Python function that evaluates a NAND program given the representation of the program as a binary string. (We assume the parameters $n,m,s,t$ are given: we could have assumed they are part of the string representation, but this only makes things messier.)

In [81]:
def NANDEVALBIN(n,m,s,t,B,X):
    """Evaluate nand program given its description as a binary array"""

    ell = ceil(log2(3*s))
    Vartable = [0] * (2**ell) # we'll simply use an array to store data
    # load input values to Vartable:
    for i in range(n): Vartable[i] = X[i] 

    # Run the program
    for c in range(s):
        i = [B[c*3*ell+d] for d in range(ell)]
        j = [B[c*3*ell+ell+d] for d in range(ell)]
        k = [B[c*3*ell+2*ell+d] for d in range(ell)]
        a = GETB(Vartable,j)
        b = GETB(Vartable,k)
        c = NAND(a,b)
        Vartable = UPDATEB(Vartable,i,c)

    # Return outputs Vartable[t-m], Vartable[t-m+1],....,Vartable[t-1]
    return [Vartable[t-m+j] for j in range(m)]

We'll need some utility functions to deal with the binary representation (you can ignore these at a first read)

In [82]:
# utility functions
def nandconst(b,x):
    """Transform 0 or 1 to NAND zero or one functions"""
    if b: return one(x)
    return zero(x)

def i2s(i,ell=0):
    """Transform integer to binary representation of length ell"""
    if not ell: ell = ceil(log2(i))
    return [floor(i/2**j) %2  for j in range(ell)]

def GETB(V,i):
    return LOOKUP(V,i)

def EQUALB(j,i):
    flag = zero(i[0]) # if flag is one then i is different from j
    for t in range(len(j)):
        if type(j[t])==int:
            temp = NOT(i[t]) if j[t] else COPY(i[t])
            temp = OR(AND(j[t],NOT(i[t])),AND(NOT(j[t]),i[t]))
        flag = OR(temp,flag)
    return NOT(flag)

def UPDATEB(V,i,b):
    ell = ceil(log2(len(V)))
    UV = [0]*len(V)
    for j in range(len(V)):
        a = EQUALB(i2s(j,ell),i)
        UV[j] = IF(a,b,V[j])
    return UV

Now let's test this out on the XOR function

In [83]:
n,m,L = nandrepresent(XOR)
s = len(L)
t = max(max(T) for T in L)+1
XORstring = triplelist2string(L)
In [84]:
In [85]:

We can also try this on the XOR of 4 bits

In [86]:
def XOR4(a,b,c,d): return XOR(XOR(a,b),XOR(c,d))
n,m,L = nandrepresent(XOR4)
s = len(L)
t = max(max(T) for T in L)+1
XOR4string = triplelist2string(L)
In [87]:
In [88]:

From Python to NAND

We now transform the Python program NANDEVALBIN into a NAND program. In fact, it turns out that all our python code can be thought of as "syntacic sugar" and hence we can do this transformation automatically.

Specifically, for every numbers $n,m,s,t$ we will construct a NAND program $P$ on $3s\ell+n$ inputs (for $\ell = \lceil \log_2(3s) \rceil$ that on input a string $B\in \{0,1\}^{3s\ell}$ and $x\in \{0,1\}^n$ outputs $P(x)$ where $P$ is the program represented by $B$.

To do so, we simply first restrict NANDEVALBIN to the parameters $n,m,s,t$ and then run our usual "unsweetener" to extract the NAND code from it

In [89]:
def nandevalfunc(n,m,s,t):
    """Given n,m,s,t, return a function f that on input B,X returns the evaluation of the program encoded by B on X"""
    ell = ceil(log2(3*s))
    return restrict(lambda B,X: NANDEVALBIN(n,m,s,t,B,X),3*s*ell,n)

For example, let us set $n,m,s,t$ to be the parameters as in the XOR function

In [90]:
n,m,L = nandrepresent(XOR)
s = len(L)
t = max(max(T) for T in L)+1
XORstring = triplelist2string(L)
In [91]:
f = nandevalfunc(n,m,s,t)
In [92]:
In [93]:

f above is still a Python function, but we now transform it into a NAND function

In [94]:
nand_eval_in_nand = nandrepresent(f)

And test it out

In [95]:

It is important to note that nand_eval_in_nand is not specific to the XOR function: it will evaluate any NAND program of the given parameters $n,m,s,t$. Some "hardwiring" of parameters is inherently needed since NAND programs only take a fixed number of inputs.

We could have also generated a NAND program that computes $t$ from the other parameters. We just avoided it because it's a little more cumbersome.

Let's see that this doesn't work out just for XOR

In [96]:
n,m,L = nandrepresent(restrict(increment,1))
In [97]:
s = len(L)
t = max(max(T) for T in L)+1
(10, 11)
In [98]:
f = nandevalfunc(n,m,s,t)
In [99]:
inc_string = triplelist2string(nandrepresent(restrict(increment,1))[2])
In [100]:
[0, 1]
In [101]:
nand_eval_in_nand = nandrepresent(f)
In [102]:
[0, 1]
In [104]:
[0, 1]

If you are curious, here is the code and circuit representation of the NAND eval function for certain parameters:

In [111]:
show_code_and_circ = False # Change to "True" to run the (long) computation
In [109]:
# (pruning took too long, so skipped it for now)
if show_code_and_circ:
    code = rep2code(nand_eval_in_nand)
    # since it's so long, let's just print the first and last 10 lines:
    lines = code.split("\n")
Temp[0] = NAND(X[5],X[5])
Temp[1] = NAND(X[0],Temp[0])
Temp[2] = NAND(X[0],X[5])
Temp[3] = NAND(Temp[1],Temp[2])
Temp[4] = NAND(X[5],X[5])
Temp[5] = NAND(X[0],Temp[4])
Temp[6] = NAND(X[0],X[5])
Temp[7] = NAND(Temp[5],Temp[6])
Temp[8] = NAND(X[6],X[6])
Temp[12238] = NAND(Temp[12236],Temp[12237])
Temp[12239] = NAND(X[139],X[139])
Temp[12240] = NAND(Temp[12239],Temp[12239])
Temp[12241] = NAND(Temp[12238],Temp[12238])
Temp[12242] = NAND(Temp[12240],Temp[12241])
Temp[12243] = NAND(Temp[12242],Temp[12242])
Temp[12244] = NAND(Temp[12243],Temp[12243])
Temp[12245] = NAND(Temp[11024],Temp[12244])
Temp[12246] = NAND(Temp[11273],Temp[12243])
Temp[12247] = NAND(Temp[12245],Temp[12246])
In [108]:
rep2circuit(nand_eval_in_nand) if show_code_and_circ else ""
%3 v0 X[0] v152 ∧̅ v0->v152 v153 ∧̅ v0->v153 v156 ∧̅ v0->v156 v157 ∧̅ v0->v157 v164 ∧̅ v0->v164 v165 ∧̅ v0->v165 v168 ∧̅ v0->v168 v169 ∧̅ v0->v169 v180 ∧̅ v0->v180 v181 ∧̅ v0->v181 v184 ∧̅ v0->v184 v185 ∧̅ v0->v185 v192 ∧̅ v0->v192 v193 ∧̅ v0->v193 v196 ∧̅ v0->v196 v197 ∧̅ v0->v197 v212 ∧̅ v0->v212 v213 ∧̅ v0->v213 v216 ∧̅ v0->v216 v217 ∧̅ v0->v217 v224 ∧̅ v0->v224 v225 ∧̅ v0->v225 v228 ∧̅ v0->v228 v229 ∧̅ v0->v229 v240 ∧̅ v0->v240 v241 ∧̅ v0->v241 v244 ∧̅ v0->v244 v245 ∧̅ v0->v245 v252 ∧̅ v0->v252 v253 ∧̅ v0->v253 v257 ∧̅ v0->v257 v276 ∧̅ v0->v276 v277 ∧̅ v0->v277 v280 ∧̅ v0->v280 v281 ∧̅ v0->v281 v288 ∧̅ v0->v288 v289 ∧̅ v0->v289 v292 ∧̅ v0->v292 v293 ∧̅ v0->v293 v304 ∧̅ v0->v304 v305 ∧̅ v0->v305 v308 ∧̅ v0->v308 v309 ∧̅ v0->v309 v316 ∧̅ v0->v316 v317 ∧̅ v0->v317 v320 ∧̅ v0->v320 v321 ∧̅ v0->v321 v336 ∧̅ v0->v336 v337 ∧̅ v0->v337 v340 ∧̅ v0->v340 v341 ∧̅ v0->v341 v348 ∧̅ v0->v348 v349 ∧̅ v0->v349 v352 ∧̅ v0->v352 v353 ∧̅ v0->v353 v364 ∧̅ v0->v364 v365 ∧̅ v0->v365 v368 ∧̅ v0->v368 v369 ∧̅ v0->v369 v376 ∧̅ v0->v376 v377 ∧̅ v0->v377 v381 ∧̅ v0->v381 v400 ∧̅ v0->v400 v0->v400 v401 ∧̅ v0->v401 v403 ∧̅ v0->v403 v0->v403 v433 ∧̅ v0->v433 v0->v433 v434 ∧̅ v0->v434 v436 ∧̅ v0->v436 v0->v436 v462 ∧̅ v0->v462 v465 ∧̅ v0->v465 v0->v465 v466 ∧̅ v0->v466 v468 ∧̅ v0->v468 v0->v468 v494 ∧̅ v0->v494 v497 ∧̅ v0->v497 v0->v497 v498 ∧̅ v0->v498 v500 ∧̅ v0->v500 v0->v500 v525 ∧̅ v0->v525 v528 ∧̅ v0->v528 v0->v528 v529 ∧̅ v0->v529 v531 ∧̅ v0->v531 v0->v531 v557 ∧̅ v0->v557 v560 ∧̅ v0->v560 v0->v560 v561 ∧̅ v0->v561 v563 ∧̅ v0->v563 v0->v563 v588 ∧̅ v0->v588 v591 ∧̅ v0->v591 v0->v591 v592 ∧̅ v0->v592 v594 ∧̅ v0->v594 v0->v594 v619 ∧̅ v0->v619 v622 ∧̅ v0->v622 v0->v622 v623 ∧̅ v0->v623 v625 ∧̅ v0->v625 v0->v625 v649 ∧̅ v0->v649 v652 ∧̅ v0->v652 v0->v652 v653 ∧̅ v0->v653 v655 ∧̅ v0->v655 v0->v655 v681 ∧̅ v0->v681 v684 ∧̅ v0->v684 v0->v684 v685 ∧̅ v0->v685 v687 ∧̅ v0->v687 v0->v687 v712 ∧̅ v0->v712 v715 ∧̅ v0->v715 v0->v715 v716 ∧̅ v0->v716 v718 ∧̅ v0->v718 v0->v718 v743 ∧̅ v0->v743 v746 ∧̅ v0->v746 v0->v746 v747 ∧̅ v0->v747 v749 ∧̅ v0->v749 v0->v749 v773 ∧̅ v0->v773 v776 ∧̅ v0->v776 v0->v776 v777 ∧̅ v0->v777 v779 ∧̅ v0->v779 v0->v779 v804 ∧̅ v0->v804 v807 ∧̅ v0->v807 v0->v807 v808 ∧̅ v0->v808 v810 ∧̅ v0->v810 v0->v810 v834 ∧̅ v0->v834 v837 ∧̅ v0->v837 v0->v837 v838 ∧̅ v0->v838 v840 ∧̅ v0->v840 v0->v840 v864 ∧̅ v0->v864 v867 ∧̅ v0->v867 v0->v867 v868 ∧̅ v0->v868 v870 ∧̅ v0->v870 v0->v870 v893 ∧̅ v0->v893 v896 ∧̅ v0->v896 v0->v896 v897 ∧̅ v0->v897 v899 ∧̅ v0->v899 v0->v899 v925 ∧̅ v0->v925 v928 ∧̅ v0->v928 v0->v928 v929 ∧̅ v0->v929 v931 ∧̅ v0->v931 v0->v931 v956 ∧̅ v0->v956 v959 ∧̅ v0->v959 v0->v959 v960 ∧̅ v0->v960 v962 ∧̅ v0->v962 v0->v962 v987 ∧̅ v0->v987 v990 ∧̅ v0->v990 v0->v990 v991 ∧̅ v0->v991 v993 ∧̅ v0->v993 v0->v993 v1017 ∧̅ v0->v1017 v1020 ∧̅ v0->v1020 v0->v1020 v1021 ∧̅ v0->v1021 v1023 ∧̅ v0->v1023 v0->v1023 v1048 ∧̅ v0->v1048 v1051 ∧̅ v0->v1051 v0->v1051 v1052 ∧̅ v0->v1052 v1054 ∧̅ v0->v1054 v0->v1054 v1078 ∧̅ v0->v1078 v1081 ∧̅ v0->v1081 v0->v1081 v1082 ∧̅ v0->v1082 v1084 ∧̅ v0->v1084 v0->v1084 v1108 ∧̅ v0->v1108 v1111 ∧̅ v0->v1111 v0->v1111 v1112 ∧̅ v0->v1112 v1114 ∧̅ v0->v1114 v0->v1114 v1137 ∧̅ v0->v1137 v1140 ∧̅ v0->v1140 v0->v1140 v1141 ∧̅ v0->v1141 v1143 ∧̅ v0->v1143 v0->v1143 v1168 ∧̅ v0->v1168 v1171 ∧̅ v0->v1171 v0->v1171 v1172 ∧̅ v0->v1172 v1174 ∧̅ v0->v1174 v0->v1174 v1198 ∧̅ v0->v1198 v1201 ∧̅ v0->v1201 v0->v1201 v1202 ∧̅ v0->v1202 v1204 ∧̅ v0->v1204 v0->v1204 v1228 ∧̅ v0->v1228 v1231 ∧̅ v0->v1231 v0->v1231 v1232 ∧̅ v0->v1232 v1234 ∧̅ v0->v1234 v0->v1234 v1257 ∧̅ v0->v1257 v1260 ∧̅ v0->v1260 v0->v1260 v1261 ∧̅ v0->v1261 v1263 ∧̅ v0->v1263 v0->v1263 v1287 ∧̅ v0->v1287 v1290 ∧̅ v0->v1290 v0->v1290 v1291 ∧̅ v0->v1291 v1293 ∧̅ v0->v1293 v0->v1293 v1316 ∧̅ v0->v1316 v1319 ∧̅ v0->v1319 v0->v1319 v1320 ∧̅ v0->v1320 v1322 ∧̅ v0->v1322 v0->v1322 v1345 ∧̅ v0->v1345 v1348 ∧̅ v0->v1348 v0->v1348 v1349 ∧̅ v0->v1349 v1351 ∧̅ v0->v1351 v0->v1351 v1373 ∧̅ v0->v1373 v1 X[1] v408 ∧̅ v1->v408 v1->v408 v440 ∧̅ v1->v440 v1->v440 v473 ∧̅ v1->v473 v1->v473 v504 ∧̅ v1->v504 v1->v504 v536 ∧̅ v1->v536 v1->v536 v567 ∧̅ v1->v567 v1->v567 v599 ∧̅ v1->v599 v1->v599 v629 ∧̅ v1->v629 v1->v629 v660 ∧̅ v1->v660 v1->v660 v691 ∧̅ v1->v691 v1->v691 v723 ∧̅ v1->v723 v1->v723 v753 ∧̅ v1->v753 v1->v753 v784 ∧̅ v1->v784 v1->v784 v814 ∧̅ v1->v814 v1->v814 v845 ∧̅ v1->v845 v1->v845 v874 ∧̅ v1->v874 v1->v874 v904 ∧̅ v1->v904 v1->v904 v935 ∧̅ v1->v935 v1->v935 v967 ∧̅ v1->v967 v1->v967 v997 ∧̅ v1->v997 v1->v997 v1028 ∧̅ v1->v1028 v1->v1028 v1058 ∧̅ v1->v1058 v1->v1058 v1089 ∧̅ v1->v1089 v1->v1089 v1118 ∧̅ v1->v1118 v1->v1118 v1148 ∧̅ v1->v1148 v1->v1148 v1178 ∧̅ v1->v1178 v1->v1178 v1209 ∧̅ v1->v1209 v1->v1209 v1238 ∧̅ v1->v1238 v1->v1238 v1268 ∧̅ v1->v1268 v1->v1268 v1297 ∧̅ v1->v1297 v1->v1297 v1327 ∧̅ v1->v1327 v1->v1327 v1355 ∧̅ v1->v1355 v1->v1355 v2 X[2] v413 ∧̅ v2->v413 v2->v413 v445 ∧̅ v2->v445 v2->v445 v477 ∧̅ v2->v477 v2->v477 v508 ∧̅ v2->v508 v2->v508 v541 ∧̅ v2->v541 v2->v541 v572 ∧̅ v2->v572 v2->v572 v603 ∧̅ v2->v603 v2->v603 v633 ∧̅ v2->v633 v2->v633 v665 ∧̅ v2->v665 v2->v665 v696 ∧̅ v2->v696 v2->v696 v727 ∧̅ v2->v727 v2->v727 v757 ∧̅ v2->v757 v2->v757 v789 ∧̅ v2->v789 v2->v789 v819 ∧̅ v2->v819 v2->v819 v849 ∧̅ v2->v849 v2->v849 v878 ∧̅ v2->v878 v2->v878 v909 ∧̅ v2->v909 v2->v909 v940 ∧̅ v2->v940 v2->v940 v971 ∧̅ v2->v971 v2->v971 v1001 ∧̅ v2->v1001 v2->v1001 v1033 ∧̅ v2->v1033 v2->v1033 v1063 ∧̅ v2->v1063 v2->v1063 v1093 ∧̅ v2->v1093 v2->v1093 v1122 ∧̅ v2->v1122 v2->v1122 v1153 ∧̅ v2->v1153 v2->v1153 v1183 ∧̅ v2->v1183 v2->v1183 v1213 ∧̅ v2->v1213 v2->v1213 v1242 ∧̅ v2->v1242 v2->v1242 v1273 ∧̅ v2->v1273 v2->v1273 v1302 ∧̅ v2->v1302 v2->v1302 v1331 ∧̅ v2->v1331 v2->v1331 v1359 ∧̅ v2->v1359 v2->v1359 v3 X[3] v418 ∧̅ v3->v418 v3->v418 v450 ∧̅ v3->v450 v3->v450 v482 ∧̅ v3->v482 v3->v482 v513 ∧̅ v3->v513 v3->v513 v545 ∧̅ v3->v545 v3->v545 v576 ∧̅ v3->v576 v3->v576 v607 ∧̅ v3->v607 v3->v607 v637 ∧̅ v3->v637 v3->v637 v670 ∧̅ v3->v670 v3->v670 v701 ∧̅ v3->v701 v3->v701 v732 ∧̅ v3->v732 v3->v732 v762 ∧̅ v3->v762 v3->v762 v793 ∧̅ v3->v793 v3->v793 v823 ∧̅ v3->v823 v3->v823 v853 ∧̅ v3->v853 v3->v853 v882 ∧̅ v3->v882 v3->v882 v914 ∧̅ v3->v914 v3->v914 v945 ∧̅ v3->v945 v3->v945 v976 ∧̅ v3->v976 v3->v976 v1006 ∧̅ v3->v1006 v3->v1006 v1037 ∧̅ v3->v1037 v3->v1037 v1067 ∧̅ v3->v1067 v3->v1067 v1097 ∧̅ v3->v1097 v3->v1097 v1126 ∧̅ v3->v1126 v3->v1126 v1158 ∧̅ v3->v1158 v3->v1158 v1188 ∧̅ v3->v1188 v3->v1188 v1218 ∧̅ v3->v1218 v3->v1218 v1247 ∧̅ v3->v1247 v3->v1247 v1277 ∧̅ v3->v1277 v3->v1277 v1306 ∧̅ v3->v1306 v3->v1306 v1335 ∧̅ v3->v1335 v3->v1335 v1363 ∧̅ v3->v1363 v3->v1363 v4 X[4] v423 ∧̅ v4->v423 v4->v423 v455 ∧̅ v4->v455 v4->v455 v487 ∧̅ v4->v487 v4->v487 v518 ∧̅ v4->v518 v4->v518 v550 ∧̅ v4->v550 v4->v550 v581 ∧̅ v4->v581 v4->v581 v612 ∧̅ v4->v612 v4->v612 v642 ∧̅ v4->v642 v4->v642 v674 ∧̅ v4->v674 v4->v674 v705 ∧̅ v4->v705 v4->v705 v736 ∧̅ v4->v736 v4->v736 v766 ∧̅ v4->v766 v4->v766 v797 ∧̅ v4->v797 v4->v797 v827 ∧̅ v4->v827 v4->v827 v857 ∧̅ v4->v857 v4->v857 v886 ∧̅ v4->v886 v4->v886 v919 ∧̅ v4->v919 v4->v919 v950 ∧̅ v4->v950 v4->v950 v981 ∧̅ v4->v981 v4->v981 v1011 ∧̅ v4->v1011 v4->v1011 v1042 ∧̅ v4->v1042 v4->v1042 v1072 ∧̅ v4->v1072 v4->v1072 v1102 ∧̅ v4->v1102 v4->v1102 v1131 ∧̅ v4->v1131 v4->v1131 v1162 ∧̅ v4->v1162 v4->v1162 v1192 ∧̅ v4->v1192 v4->v1192 v1222 ∧̅ v4->v1222 v4->v1222 v1251 ∧̅ v4->v1251 v4->v1251 v1281 ∧̅ v4->v1281 v4->v1281 v1310 ∧̅ v4->v1310 v4->v1310 v1339 ∧̅ v4->v1339 v4->v1339 v1367 ∧̅ v4->v1367 v4->v1367 v5 X[5] v151 ∧̅ v5->v151 v5->v151 v5->v153 v155 ∧̅ v5->v155 v5->v155 v5->v157 v163 ∧̅ v5->v163 v5->v163 v5->v165 v167 ∧̅ v5->v167 v5->v167 v5->v169 v179 ∧̅ v5->v179 v5->v179 v5->v181 v183 ∧̅ v5->v183 v5->v183 v5->v185 v191 ∧̅ v5->v191 v5->v191 v5->v193 v195 ∧̅ v5->v195 v5->v195 v5->v197 v211 ∧̅ v5->v211 v5->v211 v5->v213 v215 ∧̅ v5->v215 v5->v215 v5->v217 v223 ∧̅ v5->v223 v5->v223 v5->v225 v227 ∧̅ v5->v227 v5->v227 v5->v229 v239 ∧̅ v5->v239 v5->v239 v5->v241 v243 ∧̅ v5->v243 v5->v243 v5->v245 v251 ∧̅ v5->v251 v5->v251 v5->v253 v255 ∧̅ v5->v255 v5->v255 v5->v257 v6 X[6] v159 ∧̅ v6->v159 v6->v159 v161 ∧̅ v6->v161 v171 ∧̅ v6->v171 v6->v171 v173 ∧̅ v6->v173 v187 ∧̅ v6->v187 v6->v187 v189 ∧̅ v6->v189 v199 ∧̅ v6->v199 v6->v199 v201 ∧̅ v6->v201 v219 ∧̅ v6->v219 v6->v219 v221 ∧̅ v6->v221 v231 ∧̅ v6->v231 v6->v231 v233 ∧̅ v6->v233 v247 ∧̅ v6->v247 v6->v247 v249 ∧̅ v6->v249 v259 ∧̅ v6->v259 v6->v259 v261 ∧̅ v6->v261 v7 X[7] v175 ∧̅ v7->v175 v7->v175 v177 ∧̅ v7->v177 v203 ∧̅ v7->v203 v7->v203 v205 ∧̅ v7->v205 v235 ∧̅ v7->v235 v7->v235 v237 ∧̅ v7->v237 v263 ∧̅ v7->v263 v7->v263 v265 ∧̅ v7->v265 v8 X[8] v207 ∧̅ v8->v207 v8->v207 v209 ∧̅ v8->v209 v267 ∧̅ v8->v267 v8->v267 v269 ∧̅ v8->v269 v9 X[9] v271 ∧̅ v9->v271 v9->v271 v273 ∧̅ v9->v273 v10 X[10] v275 ∧̅ v10->v275 v10->v275 v10->v277 v279 ∧̅ v10->v279 v10->v279 v10->v281 v287 ∧̅ v10->v287 v10->v287 v10->v289 v291 ∧̅ v10->v291 v10->v291 v10->v293 v303 ∧̅ v10->v303 v10->v303 v10->v305 v307 ∧̅ v10->v307 v10->v307 v10->v309 v315 ∧̅ v10->v315 v10->v315 v10->v317 v319 ∧̅ v10->v319 v10->v319 v10->v321 v335 ∧̅ v10->v335 v10->v335 v10->v337 v339 ∧̅ v10->v339 v10->v339 v10->v341 v347 ∧̅ v10->v347 v10->v347 v10->v349 v351 ∧̅ v10->v351 v10->v351 v10->v353 v363 ∧̅ v10->v363 v10->v363 v10->v365 v367 ∧̅ v10->v367 v10->v367 v10->v369 v375 ∧̅ v10->v375 v10->v375 v10->v377 v379 ∧̅ v10->v379 v10->v379 v10->v381 v11 X[11] v283 ∧̅ v11->v283 v11->v283 v285 ∧̅ v11->v285 v295 ∧̅ v11->v295 v11->v295 v297 ∧̅ v11->v297 v311 ∧̅ v11->v311 v11->v311 v313 ∧̅ v11->v313 v323 ∧̅ v11->v323 v11->v323 v325 ∧̅ v11->v325 v343 ∧̅ v11->v343 v11->v343 v345 ∧̅ v11->v345 v355 ∧̅ v11->v355 v11->v355 v357 ∧̅ v11->v357 v371 ∧̅ v11->v371 v11->v371 v373 ∧̅ v11->v373 v383 ∧̅ v11->v383 v11->v383 v385 ∧̅ v11->v385 v12 X[12] v299 ∧̅ v12->v299 v12->v299 v301 ∧̅ v12->v301 v327 ∧̅ v12->v327 v12->v327 v329 ∧̅ v12->v329 v359 ∧̅ v12->v359 v12->v359 v361 ∧̅ v12->v361 v387 ∧̅ v12->v387 v12->v387 v389 ∧̅ v12->v389 v13 X[13] v331 ∧̅ v13->v331 v13->v331 v333 ∧̅ v13->v333 v391 ∧̅ v13->v391 v13->v391 v393 ∧̅ v13->v393 v14 X[14] v395 ∧̅ v14->v395 v14->v395 v397 ∧̅ v14->v397 v15 X[15] v1625 ∧̅ v15->v1625 v15->v1625 v1626 ∧̅ v15->v1626 v1628 ∧̅ v15->v1628 v15->v1628 v1658 ∧̅ v15->v1658 v15->v1658 v1659 ∧̅ v15->v1659 v1661 ∧̅ v15->v1661 v15->v1661 v1690 ∧̅ v15->v1690 v15->v1690 v1691 ∧̅ v15->v1691 v1693 ∧̅ v15->v1693 v15->v1693 v1722 ∧̅ v15->v1722 v15->v1722 v1723 ∧̅ v15->v1723 v1725 ∧̅ v15->v1725 v15->v1725 v1753 ∧̅ v15->v1753 v15->v1753 v1754 ∧̅ v15->v1754 v1756 ∧̅ v15->v1756 v15->v1756 v1785 ∧̅ v15->v1785 v15->v1785 v1786 ∧̅ v15->v1786 v1788 ∧̅ v15->v1788 v15->v1788 v1816 ∧̅ v15->v1816 v15->v1816 v1817 ∧̅ v15->v1817 v1819 ∧̅ v15->v1819 v15->v1819 v1847 ∧̅ v15->v1847 v15->v1847 v1848 ∧̅ v15->v1848 v1850 ∧̅ v15->v1850 v15->v1850 v1877 ∧̅ v15->v1877 v15->v1877 v1878 ∧̅ v15->v1878 v1880 ∧̅ v15->v1880 v15->v1880 v1909 ∧̅ v15->v1909 v15->v1909 v1910 ∧̅ v15->v1910 v1912 ∧̅ v15->v1912 v15->v1912 v1940 ∧̅ v15->v1940 v15->v1940 v1941 ∧̅ v15->v1941 v1943 ∧̅ v15->v1943 v15->v1943 v1971 ∧̅ v15->v1971 v15->v1971 v1972 ∧̅ v15->v1972 v1974 ∧̅ v15->v1974 v15->v1974 v2001 ∧̅ v15->v2001 v15->v2001 v2002 ∧̅ v15->v2002 v2004 ∧̅ v15->v2004 v15->v2004 v2032 ∧̅ v15->v2032 v15->v2032 v2033 ∧̅ v15->v2033 v2035 ∧̅ v15->v2035 v15->v2035 v2062 ∧̅ v15->v2062 v15->v2062 v2063 ∧̅ v15->v2063 v2065 ∧̅ v15->v2065 v15->v2065 v2092 ∧̅ v15->v2092 v15->v2092 v2093 ∧̅ v15->v2093 v2095 ∧̅ v15->v2095 v15->v2095 v2121 ∧̅ v15->v2121 v15->v2121 v2122 ∧̅ v15->v2122 v2124 ∧̅ v15->v2124 v15->v2124 v2153 ∧̅ v15->v2153 v15->v2153 v2154 ∧̅ v15->v2154 v2156 ∧̅ v15->v2156 v15->v2156 v2184 ∧̅ v15->v2184 v15->v2184 v2185 ∧̅ v15->v2185 v2187 ∧̅ v15->v2187 v15->v2187 v2215 ∧̅ v15->v2215 v15->v2215 v2216 ∧̅ v15->v2216 v2218 ∧̅ v15->v2218 v15->v2218 v2245 ∧̅ v15->v2245 v15->v2245 v2246 ∧̅ v15->v2246 v2248 ∧̅ v15->v2248 v15->v2248 v2276 ∧̅ v15->v2276 v15->v2276 v2277 ∧̅ v15->v2277 v2279 ∧̅ v15->v2279 v15->v2279 v2306 ∧̅ v15->v2306 v15->v2306 v2307 ∧̅ v15->v2307 v2309 ∧̅ v15->v2309 v15->v2309 v2336 ∧̅ v15->v2336 v15->v2336 v2337 ∧̅ v15->v2337 v2339 ∧̅ v15->v2339 v15->v2339 v2365 ∧̅ v15->v2365 v15->v2365 v2366 ∧̅ v15->v2366 v2368 ∧̅ v15->v2368 v15->v2368 v2396 ∧̅ v15->v2396 v15->v2396 v2397 ∧̅ v15->v2397 v2399 ∧̅ v15->v2399 v15->v2399 v2426 ∧̅ v15->v2426 v15->v2426 v2427 ∧̅ v15->v2427 v2429 ∧̅ v15->v2429 v15->v2429 v2456 ∧̅ v15->v2456 v15->v2456 v2457 ∧̅ v15->v2457 v2459 ∧̅ v15->v2459 v15->v2459 v2485 ∧̅ v15->v2485 v15->v2485 v2486 ∧̅ v15->v2486 v2488 ∧̅ v15->v2488 v15->v2488 v2515 ∧̅ v15->v2515 v15->v2515 v2516 ∧̅ v15->v2516 v2518 ∧̅ v15->v2518 v15->v2518 v2544 ∧̅ v15->v2544 v15->v2544 v2545 ∧̅ v15->v2545 v2547 ∧̅ v15->v2547 v15->v2547 v2573 ∧̅ v15->v2573 v15->v2573 v2574 ∧̅ v15->v2574 v2576 ∧̅ v15->v2576 v15->v2576 v16 X[16] v1633 ∧̅ v16->v1633 v16->v1633 v1665 ∧̅ v16->v1665 v16->v1665 v1698 ∧̅ v16->v1698 v16->v1698 v1729 ∧̅ v16->v1729 v16->v1729 v1761 ∧̅ v16->v1761 v16->v1761 v1792 ∧̅ v16->v1792 v16->v1792 v1824 ∧̅ v16->v1824 v16->v1824 v1854 ∧̅ v16->v1854 v16->v1854 v1885 ∧̅ v16->v1885 v16->v1885 v1916 ∧̅ v16->v1916 v16->v1916 v1948 ∧̅ v16->v1948 v16->v1948 v1978 ∧̅ v16->v1978 v16->v1978 v2009 ∧̅ v16->v2009 v16->v2009 v2039 ∧̅ v16->v2039 v16->v2039 v2070 ∧̅ v16->v2070 v16->v2070 v2099 ∧̅ v16->v2099 v16->v2099 v2129 ∧̅ v16->v2129 v16->v2129 v2160 ∧̅ v16->v2160 v16->v2160 v2192 ∧̅ v16->v2192 v16->v2192 v2222 ∧̅ v16->v2222 v16->v2222 v2253 ∧̅ v16->v2253 v16->v2253 v2283 ∧̅ v16->v2283 v16->v2283 v2314 ∧̅ v16->v2314 v16->v2314 v2343 ∧̅ v16->v2343 v16->v2343 v2373 ∧̅ v16->v2373 v16->v2373 v2403 ∧̅ v16->v2403 v16->v2403 v2434 ∧̅ v16->v2434 v16->v2434 v2463 ∧̅ v16->v2463 v16->v2463 v2493 ∧̅ v16->v2493 v16->v2493 v2522 ∧̅ v16->v2522 v16->v2522 v2552 ∧̅ v16->v2552 v16->v2552 v2580 ∧̅ v16->v2580 v16->v2580 v17 X[17] v1638 ∧̅ v17->v1638 v17->v1638 v1670 ∧̅ v17->v1670 v17->v1670 v1702 ∧̅ v17->v1702 v17->v1702 v1733 ∧̅ v17->v1733 v17->v1733 v1766 ∧̅ v17->v1766 v17->v1766 v1797 ∧̅ v17->v1797 v17->v1797 v1828 ∧̅ v17->v1828 v17->v1828 v1858 ∧̅ v17->v1858 v17->v1858 v1890 ∧̅ v17->v1890 v17->v1890 v1921 ∧̅ v17->v1921 v17->v1921 v1952 ∧̅ v17->v1952 v17->v1952 v1982 ∧̅ v17->v1982 v17->v1982 v2014 ∧̅ v17->v2014 v17->v2014 v2044 ∧̅ v17->v2044 v17->v2044 v2074 ∧̅ v17->v2074 v17->v2074 v2103 ∧̅ v17->v2103