プログラミングのない世界 (2)#

自動的にプログラムを作成する (論理合成、定理証明)#

剰余 divmod と等価な論理演算

import itertools
for i,j in itertools.product([0,1], repeat=2):
    print("{:d}+{:d}={:02b}".format(i,j,i+j))
0+0=00
0+1=01
1+0=01
1+1=10
for i,j in itertools.product([0,1], repeat=2):
    print("{:d}+{:d}={:02b} ".format(i,j,i+j), end="")
    print("({:d},{:d})".format(*divmod(i+j,2)))
0+0=00 (0,0)
0+1=01 (0,1)
1+0=01 (0,1)
1+1=10 (1,0)

Boolean Function#

前回、繰り上がりについて not(a^b)&(a|b) などとコーディングしてしまったが、簡約化すると a&b

def binary_add(a, b):
    if not (a >=0 and b >= 0 and a < 2 and b < 2):
        raise ValueError
    # YOUR CODE HERE
    #return [(a+b)//2, (a+b)%2]
    #return list(divmod(a+b, 2))
    return [(not(a^b))&(a|b), a^b]
from sympy.abc import x,y,z
from sympy.logic import simplify_logic
simplify_logic(~(x^y)&(x|y))
\[\displaystyle x \wedge y\]
for i,j in itertools.product([0,1], repeat=2):
    print("{:d}+{:d}={:02b} ".format(i,j,i+j), end="")
    print("({:d},{:d})".format(i&j, i^j))
0+0=00 (0,0)
0+1=01 (0,1)
1+0=01 (0,1)
1+1=10 (1,0)

すなわち、divmod(i+j,2)(i&j, i^j) は「相等 (equal)」

論理演算関数 (Boolean Function) では、出力が決まれば論理演算を決定できる

list(itertools.product([0,1],repeat=2))
[(0, 0), (0, 1), (1, 0), (1, 1)]
from sympy.abc import x,y,z
from sympy.logic import simplify_logic
from sympy.logic.boolalg import ANFform, to_cnf, to_dnf
ANFform([x,y], [0,0,0,0])
\[\displaystyle \text{False}\]
ANFform([x,y], [1,1,1,1])
\[\displaystyle \text{True}\]
ANFform([x,y], [0,0,0,1])
\[\displaystyle x \wedge y\]
ANFform([x,y], [0,1,1,0])
\[\displaystyle x \veebar y\]
ANFform([x,y], [0,1,1,1])
\[\displaystyle x \veebar y \veebar \left(x \wedge y\right)\]
simplify_logic(x^y^(x&y), form='cnf')
\[\displaystyle x \vee y\]
simplify_logic(x^y^(x&y), form='dnf')
\[\displaystyle x \vee y\]

まとめ)

import operator
for op in [operator.and_, operator.or_, operator.xor]:
    print([op(i,j) for i,j in itertools.product([0,1],repeat=2)])
[0, 0, 0, 1]
[0, 1, 1, 1]
[0, 1, 1, 0]
for op in [operator.and_, operator.or_, operator.xor]:
    print(ANFform([x,y], [op(i,j) for i,j in itertools.product([0,1],repeat=2)]))
x & y
x ^ y ^ (x & y)
x ^ y

一桁の二進数の加算と等価な論理演算#

for i,j in itertools.product([0,1], repeat=2):
    print("{:d}+{:d}={:02b} ".format(i,j,i+j), end="")
    print("({:d},{:d})".format(*divmod(i+j,2)))
0+0=00 (0,0)
0+1=01 (0,1)
1+0=01 (0,1)
1+1=10 (1,0)
list(zip(*[divmod(i+j,2) for i,j in itertools.product([0,1], repeat=2)]))
[(0, 0, 0, 1), (0, 1, 1, 0)]
for qr in zip(*[divmod(i+j,2) for i,j in itertools.product([0,1], repeat=2)]):
    print(ANFform([x,y], qr))
x & y
x ^ y

xor (^) を用いずに CNF や DNF で表現すると

for qr in zip(*[divmod(i+j,2) for i,j in itertools.product([0,1], repeat=2)]):
    print(to_cnf(ANFform([x,y], qr), simplify=True))
x & y
(x | y) & (~x | ~y)
for qr in zip(*[divmod(i+j,2) for i,j in itertools.product([0,1], repeat=2)]):
    print(to_dnf(ANFform([x,y], qr), simplify=True))
x & y
(x & ~y) | (y & ~x)

繰り上がりを考慮した一桁の二進数の加算#

import itertools
for i,j,k in itertools.product([0,1], repeat=3):
    print("{:d}+{:d}+{:d}={:02b} ".format(i,j,k,i+j+k), end="")
    print("({:d},{:d})".format(*divmod(i+j+k,2)))
0+0+0=00 (0,0)
0+0+1=01 (0,1)
0+1+0=01 (0,1)
0+1+1=10 (1,0)
1+0+0=01 (0,1)
1+0+1=10 (1,0)
1+1+0=10 (1,0)
1+1+1=11 (1,1)
list(zip(*[divmod(i+j+k,2) for i,j,k in itertools.product([0,1], repeat=3)]))
[(0, 0, 0, 1, 0, 1, 1, 1), (0, 1, 1, 0, 1, 0, 0, 1)]
for qr in zip(*[divmod(i+j+k,2) for i,j,k in itertools.product([0,1], repeat=3)]):
    print(ANFform([x,y,z], qr))
(x & y) ^ (x & z) ^ (y & z)
x ^ y ^ z

xor (^) を用いずにCNFやDNFで表現すると煩雑な表現になる (xor演算がが重用される理由) :

for qr in zip(*[divmod(i+j+k,2) for i,j,k in itertools.product([0,1], repeat=3)]):
    print(to_cnf(ANFform([x,y,z], qr), simplify=True))
(x | y) & (x | z) & (y | z)
(x | y | z) & (x | ~y | ~z) & (y | ~x | ~z) & (z | ~x | ~y)
for qr in zip(*[divmod(i+j+k,2) for i,j,k in itertools.product([0,1], repeat=3)]):
    print(to_dnf(ANFform([x,y,z], qr), simplify=True))
(x & y) | (x & z) | (y & z)
(x & y & z) | (x & ~y & ~z) | (y & ~x & ~z) | (z & ~x & ~y)