Version 26 of NAND

Updated 2008-10-21 12:42:01 by dkf

Richard Suchenwirth 2002-12-04 - "NAND is not AND." By popular demand, here's some codelets to demonstrate how all Boolean operations can be expressed in terms of the single NAND operator, which returns true if not both his two inputs are true (NOR would have done equally well). We have Boolean operators in expr, so here goes:}

 proc nand {A B} {expr {!($A && $B)}}

# The only unary operator NOT can be written in terms of nand:

 proc not {A} {nand $A $A}

# .. and everything else can be built from them too:

 proc and {A B} {not [nand $A $B]}

 proc or {A B} {nand [not $A] [not $B]}

 proc nor {A B} {not [or $A $B]}

 proc eq {A B} {or [and $A $B] [nor $A $B]}

 proc ne {A B} {nor [and $A $B] [nor $A $B]}

if 0 {Here's some testing tools - to see whether an implementation is correct, look at its truth table, here done as the four results for A,B combinations 0,0 0,1 1,0 1,1 - side note how easily procs can be passed in:}

 proc truthtable f {
    set res {}
    foreach A {0 1} {
        foreach B {0 1} {
            lappend res [$f $A $B]
        }
    }
    set res
 }
 # Test:
 catch {console show}
 puts "nand: [truthtable nand]"

if 0 {

 % truthtable and
 0 0 0 1
 % truthtable nand
 1 1 1 0
 % truthtable or
 0 1 1 1
 % truthtable nor
 1 0 0 0
 % truthtable eq
 1 0 0 1

To see how efficient the implementation is (in terms of NAND units used), try this, which relies on the fact that Boolean functions contain no lowercase letters apart from the operator names:}

 proc nandcount f {
    regsub -all {[^a-z]} [info body $f] " " list
    set nums [string map {nand 1 not 1 and 2 nor 4 or 3 eq 6} $list]
    expr [join $nums +]
 }

A very different idea, having nothing to do with NAND as elementary function, but I like it because it "implements" Boolean functions very intuitively, by just giving their truth table for look-up at runtime:

 proc booleanFunction {truthtable a b} {lindex $truthtable [expr {!!$a+!!$a+!!$b}]}
 interp alias {} and  {} booleanFunction {0 0 0 1}
 interp alias {} or   {} booleanFunction {0 1 1 1}
 interp alias {} nand {} booleanFunction {1 1 1 0}

!! is a cute little Booleanizer (thanks KPV on Toggling a Boolean variable!)


TV Always good to have a page on the thing that can be proven to be a basic building block of pretty much the whole universe of computers! For digital designers with some historical perspective (and sense), NANDs are pieces of electronics that have in minimal form 3 pins each, and are represented by 'iron' symbols, where the output has an extra circle, which indicates it is not an AND but a NAND (with inverted output). Inverters are more fun, because one cannot construct something inverting with gates that do not invert. Otherwise, mathematically one can construct ANY logical function from ANY logical building blocks that has two inputs and inverts and does something like an and or or function.

From Texas Instruments datasheet: http://82.171.148.176/Wiki/nand7400.jpg

For a course proof on how any logical function can be constructed, also from NANDs, see Boolean Logic


Laws of Form shows a model of Boolean arithmetics with two operators, one of them being the empty string "", however...


Not only can NAND be used to construct all truth functions, it can also be taken as the sole logical connective in an axiomatization of the propositional calculus. [Mendelson, ISBN 0-534-06624-0], following [J.G. Nicod: A reduction in the number of primitive propositions in logic, Proc. Camb. Phil. Soc. 19 (1917), 32–41] and denoting NAND by |, give the interference rule

  A, A|(B|C) ⊢ C

(cf. modus ponens, which would be A, A⇒B ⊢ B in the same notation) and the axiom schema

  (A|(B|C))|((D|(D|D))|((E|B)|((A|E)|(A|E))))

as being sufficient for deriving any tautology.

As an example of this, the easiest instance of that axiom schema is the one where all occurrencies of formula variables (A–E) are set to the same logical variable x:

  (x|(x|x))|((x|(x|x))|((x|x)|((x|x)|(x|x))))

The easy way to compute that is to use string map:

    string map {A x B x C x D x E x} (A|(B|C))|((D|(D|D))|((E|B)|((A|E)|(A|E))))

In order to derive something from that formula of all x's, it is necessary to find another instance of the axiom schema which matches it well enough for the interference rule to apply. Since that all x's formula is the shortest of all axioms, it'll have to be the A in the interference rule. The axiom used as A|(B|C) must furthermore have exactly the all x's formula as the left operand of the outermost |, which forces values for variables A, B, and C in the schema; the possible axioms are thus by

    string map {A (x|(x|x)) B (x|(x|x)) C ((x|x)|((x|x)|(x|x)))}  (A|(B|C))|((D|(D|D))|((E|B)|((A|E)|(A|E))))

computed to be on the form

  ((x|(x|x))|((x|(x|x))|((x|x)|((x|x)|(x|x)))))|((D|(D|D))|((E|(x|(x|x)))|(((x|(x|x))|E)|((x|(x|x))|E))))

and the part there corresponding to C of the interference rule is

  (E|(x|(x|x)))|(((x|(x|x))|E)|((x|(x|x))|E))

so any formula on that form is thus a theorem of this propositional calculus, and thus a tautology.

As usual with compact axiomatizations of a known theory however, it takes quite some work to find a sequence of axiom combinations that produce the theorems that express the usual laws of logic…


See also: A little proving engineParsing Polish notation


A Little Bit O' History

Links Lately Added

Jon Awbrey : http://www.mywikibiz.com/Directory:Jon_Awbrey


TP 2008-10-20 - I recently found The Elements of Computing Systems: Building a Modern Computer from First Principles [L1 ] for those software guys & gals (like me) who want to learn more about digital logic, gates, etc. Designed as a mid-level college course, it starts with NAND and progresses from digital logic to building gates, higher level chips, finally culminating into a CPU. From there, the book goes into software from basic assembly language to building a VM, compiler, and OS, based on the CPU built earlier. Resources include book, Google Tech Talk video, software (HDL simulator, CPU emulator, VM, etc.), study plans. I just purchased the book, and hope to work through the problems.