NAND

Richard Suchenwirth 2002-12-04: NAND means "not AND". By popular demand, here are 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: Image TV Wiki nand7400.jpg

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…

Reference

Jon Awbrey: various links to topics related to logic

Glossary

Ampheck: refers to either one of the NAND or NNOR operators

logical graph: one of the systems of graphical syntax developed by Charles Sanders Peirce

minimal negation operator

zeroth order logic

NAND

Reference

Glossary

See Also