This article continues the series of articles that have appeared here related to program synthesis. It attempts to a) provide an example scenario where the applicability of program synthesis techniques may not be readily apparent, and b) showcase how the capabilities of Lisp (in particular, S-expressions and homoiconicity) make it a natural fit for code generation and hence, program synthesis. While the individual techniques and concepts used in the solution are well known, I hope that the way they have been put together can serve to kindle readers’ interest in program synthesis and language abstractions in Lisp that support it.

The Problem

The problem we’ll take up is a textbook problem that figures in introductory electronics/CS courses (not to mention technical interviews): the derivation of the different logic gates using only NAND or NOR, the universal gates. In mathematical logic, the underlying principle is known as expressive completeness. Stating the problem more formally, our goal is to synthesize an expression conveyed by this grammar whose meaning matches that of the logic gate G we are interested in:

exp ::= nand(exp, exp) | A | B
A ::= 0 | 1
B ::= 0 | 1

Here, A and B are the two input wires of the gate G.

Searching for the Solution

A reasonable solution is to employ the program synthesis technique of enumerative search: systematically generate expressions matching the grammar, and stop when you find one that is functionally equivalent to G. The question is how to generate expressions effectively. Automated and semi-automated techniques for doing so are their own area of research, e.g., to support property-based random testers like QuickCheck. Our approach is to visualize the search for valid expressions as a tree using the atoms nand, A, and B, and to traverse the tree to generate valid expressions.

This tree is of infinite depth, since there is no limit to expression construction, as indicated by the recursive nature of the grammar. However, we know that all the derived gates can be obtained with a handful of nested calls to nand, so this is not a cause for worry.

The next step is to figure out how to convert a path of the form nand A nand A B into a computable expression. A couple of facts show us the way:

1. nand is always an operator, and it takes two arguments
2. A and B are always operands (taking the values 0 or 1)

Therefore, the only logical way to interpret the above path is, in function form, nand(A, nand(A,B)).

“Wait a minute”, I hear someone from the backbenches say. “How can we be sure that we always get syntactically correct expressions?” Good question. Careful analysis of the tree will show that, at whatever point you stop the traversal, one of two things will always be true:

1. You will have formed a syntactically correct, computable expression, or
2. You will have an incomplete expression that can be made complete by further traversal (you may have to walk an infinite number of edges, though)

Lisp and Code Generation

The above tree that captures the structure of valid expressions in our grammar can be readily represented in Lisp’s ‘native’ data structure, the list (or, more accurately, the S-expression). Moreover, if we look at nand as a function, the tree can also be interpreted as an abstract syntax tree.

Which brings us to the key reason for using Lisp as the implementation language for this problem: its property of homoiconicity, a.k.a. ‘Code is data’ – the fact that the data, namely the tree of valid expressions, can equivalently be looked at as a function expression embodying the nand call(s). Actually, ‘data is code’ is more appropriate, but we’ll bow to tradition here.

Once we have generated a candidate expression, evaluating the expression in Lisp is simply a matter of calling Lisp’s in-built eval operator, passing the expression as an argument. Here’s where the power of Lisp shines through: while it is possible to map the expression to a suitable data structure in any Turing-complete language, and do a reflection/reification operation on this data structure in a manner of speaking, such overheads are neatly avoided in Lisp. At the risk of repeating myself, code is already data.

It’s Implementation Time

Let’s start off with the basic functions we’ll need (this might be a good time to mention that we will be using Common Lisp).

(defun nand (x y)
  (if (and (equal x 1) (equal y 1)) 0 1))

This is a straightforward definition of NAND: if both arguments are 1, return 0, otherwise return 1.

(defun valid-exp (exp)
   (cond ((or (equal exp 'a) (equal exp 'b)) t)
         ((not (listp exp))                  nil)
         ((not (equal (length exp) 3))       nil)
         ((and (equal (car exp) 'nand)
               (valid-exp (cadr exp))
               (valid-exp (caddr exp)))      t)
         (t nil)))

The function valid-exp takes as argument lists like (nand a b), (nand (nand) a), and tells us whether we’re looking at valid (complete) expressions or at incomplete (work-in-progress) expressions.

The next function looks a bit complicated, but is conceptually simple:

(defun clone-and-plug-exp (skel-exp exp)
   (cond ((or (equal skel-exp nil)
              (equal skel-exp 'a)
              (equal skel-exp 'b)
              (equal skel-exp '(nand a b))
              (equal skel-exp '(nand b a)))  skel-exp)
         ((and (listp skel-exp)
               (< (length skel-exp) 3))     (concatenate 'list skel-exp (list exp)))
         (t   (if (valid-exp (cadr skel-exp))
                  (list (car skel-exp) cadr skel-exp) (clone-and-plug-exp (caddr skel-exp) exp))
                (list (car skel-exp) (clone-and-plug-exp (cadr skel-exp) exp) (caddr skel-exp)))))

Given an incomplete expression and a phrase, it plugs this phrase into the first available ‘hole’. An example will make things clear: given the expression (nand (nand)), and a, this function will produce (nand (nand a)). Note that this is still an incomplete expression: both the nand‘s are missing their second parameters, which will hopefully be supplied by future traversals down the tree.

This brings us to the meat of our program, the actual traversal/search:

(defun find-equivalent (fn)
   (let ((queue '((nand)))
         (iterations 0)
         (e))
     (loop do
       (setq e (car queue))
       (if (valid-exp e)
           (if (funcall fn e)
               (return-from find-equivalent e)
             (setq queue (cdr queue)))
         (setq queue (concatenate 'list (cdr queue)
                                  (mapcar (lambda (x) (clone-and-plug-exp e x)) '(a b (nand))))))
       (incf iterations)
       while (< iterations 1000)))
   'no-solutions)

This is a breadth-first search, as indicated by the use of a queue for the backtracking. (We’d use a stack if we wanted a depth-first search. Pop quiz: A DFS in this case is not A Good Thing ™ — why?). We limit our search to 1000 iterations, but since the search terminates much earlier, this is not a problem.

The code involving mapcar needs some explaining: it basically appends three items to the queue, items that are formed by plugging in a, b and (nand) to the element popped from the queue.

When a valid expression is produced, the checking function fn is called to see if we have found the gate G we are interested in. This is a convenient use of Lisp’s treatment of functions as first-class objects. The checking functions for OR and AND are given below:

(defun is-equiv-to-or (exp)
   (and (equal (evaluate exp 0 0) 0)
        (equal (evaluate exp 0 1) 1)
        (equal (evaluate exp 1 0) 1)
        (equal (evaluate exp 1 1) 1)))

(defun is-equiv-to-and (exp)
  (and (equal (evaluate exp 0 0) 0)
       (equal (evaluate exp 0 1) 0)
       (equal (evaluate exp 1 0) 0)
       (equal (evaluate exp 1 1) 1)))

We also prime our queue with the root node, namely (nand), which makes sense since we’re sure that the solution would definitely involve a nand() as the, for want of a better word, super-caller.

One more function that we’ll need is to do the actual evaluation of an expression:

(defun evaluate (exp a b)
  (eval (list 'let (list (list 'a a) (list 'b b)) exp)))

This function constructs a Lisp program and uses Lisp’s own evaluator to run it.

The Rubber Meets the Road

It’s time now to put our program to the test:

CL-USER> (find-equivalent #'is-equiv-to-or)
(NAND (NAND A A) (NAND B B))
CL-USER>
CL-USER> (find-equivalent #'is-equiv-to-and)
(NAND (NAND A B) (NAND A B))
CL-USER>

It’s a trivial matter to verify that these expressions do correspond to OR and AND respectively. Let’s throw the function a curveball – ask it to derive NAND itself:

CL-USER> (defun is-equiv-to-nand (exp)
          (and (equal (evaluate exp 0 0) 1)
               (equal (evaluate exp 0 1) 1)
               (equal (evaluate exp 1 0) 1)
               (equal (evaluate exp 1 1) 0)))
CL-USER> <output elided>
CL-USER> (find-equivalent #'is-equiv-to-nand)
(NAND A B)
Duh!
CL-USER>

(Easy there with the attitude, Computer).

Deriving the other gates is left as an exercise for the gentle reader.

This article has approached program synthesis indirectly, and has focussed more on first principles and on implementation aspects and choices. If you are looking for a more formal perspective, e.g., obtaining your desired program as an analytical or a formal solution (as opposed to an enumerative search, as illustrated in this article), James Bornholt’s recent article would be a good place to start. In fact, reimplementing the code here in Rosette might be a fun weekend project. Happy hacking!

Bio: Rajesh Jayaprakash is a researcher at Tata Consultancy Services. He is the author of pLisp, a friendly Lisp dialect and IDE for beginners.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.