dnf と cnf（nnsolve その2）

選言標準形，連言標準形は代数で言えば，それぞれ展開，因数分解に当たる基本的なものであり，前者は所謂（排他的とは限らない）場合分けなので，方程式系の解の構成には欠かせません．

その実装は簡単で，例えば，A ∧ (B ∨ C) を (A ∧ B) ∨ (A ∧ C) に可能な限り置き換えれば良いだけです．

が，．．．それは連言，選言が 2 項オペレーターの場合の話．%and，%or は nary なので，そのままではパターンにマッチしません．

というわけで，作ったのが以下の dnf と cnf です．

infix(Or,60,40)$
infix(And,60,40)$

/* n項 %and,%or を2項 And,Or の合成に */
orand2orand(f):=block([g],g:f,
if atom(g) then return(g),
if op(g)="%or" then g:xreduce("Or",args(g)),
if op(g)="%and" then g:xreduce("And",args(g)),g)$

/* 分配 */
matchdeclare([aa,bb,cc],true)$
defrule(ru05r, (aa) Or ((bb) And (cc)), ((aa) Or (bb)) And ((aa) Or (cc)))$
defrule(ru08r, ((bb) And (cc)) Or (aa), ((aa) Or (bb)) And ((aa) Or (cc)))$
defrule(ru05a, (aa) And ((bb) Or (cc)), ((aa) And (bb)) Or ((aa) And (cc)))$
defrule(ru08a, ((bb) Or (cc)) And (aa), ((aa) And (bb)) Or ((aa) And (cc)))$

/* subst の並列でも可 */
defrule(ru00r, (aa) Or (bb), (aa) %or (bb))$
defrule(ru00a, (aa) And (bb), (aa) %and (bb))$

cnf(f):=applyb2(applyb2(scanmap(orand2orand,f),ru05r,ru08r),ru00r,ru00a)$
dnf(f):=applyb2(applyb2(scanmap(orand2orand,f),ru05a,ru08a),ru00r,ru00a)$

実行例

Maxima 5.36.1 http://maxima.sourceforge.net
using Lisp CMU Common Lisp 20d (20D Unicode)
Distributed under the GNU Public License. See the file COPYING.
Dedicated to the memory of William Schelter.
The function bug_report() provides bug reporting information.
(%i1) (x=0)%or((x-1=0)%and(y=0)%and(z=0));
(%o1)         (x = 0) %or ((x - 1 = 0) %and (y = 0) %and (z = 0))
(%i2) cnf(%);
(%o2) ((x - 1 = 0) %or (x = 0)) %and ((x = 0) %or (y = 0))
                                                     %and ((x = 0) %or (z = 0))
(%i3) dnf(%);
(%o3) (x = 0) %or ((x - 1 = 0) %and (x = 0))
 %or ((x - 1 = 0) %and (x = 0) %and (y = 0))
 %or ((x - 1 = 0) %and (x = 0) %and (z = 0))
 %or ((x - 1 = 0) %and (y = 0) %and (z = 0)) %or ((x = 0) %and (y = 0))
 %or ((x = 0) %and (y = 0) %and (z = 0)) %or ((x = 0) %and (z = 0))
(%i4) cnf(%);
(%o4) ((x - 1 = 0) %or (x = 0)) %and ((x - 1 = 0) %or (x = 0) %or (y = 0))
 %and ((x - 1 = 0) %or (x = 0) %or (y = 0) %or (z = 0))
 %and ((x - 1 = 0) %or (x = 0) %or (z = 0)) %and ((x = 0) %or (y = 0))
 %and ((x = 0) %or (y = 0) %or (z = 0)) %and ((x = 0) %or (z = 0))
(%i5) dnf(%);
(%o5) (x = 0) %or ((x - 1 = 0) %and (x = 0))
 %or ((x - 1 = 0) %and (x = 0) %and (y = 0))
 %or ((x - 1 = 0) %and (x = 0) %and (y = 0) %and (z = 0))
 %or ((x - 1 = 0) %and (x = 0) %and (z = 0))
 %or ((x - 1 = 0) %and (y = 0) %and (z = 0)) %or ((x = 0) %and (y = 0))
 %or ((x = 0) %and (y = 0) %and (z = 0)) %or ((x = 0) %and (z = 0))
(%i6) cnf(%);
(%o6) ((x - 1 = 0) %or (x = 0)) %and ((x - 1 = 0) %or (x = 0) %or (y = 0))
 %and ((x - 1 = 0) %or (x = 0) %or (y = 0) %or (z = 0))
 %and ((x - 1 = 0) %or (x = 0) %or (z = 0)) %and ((x = 0) %or (y = 0))
 %and ((x = 0) %or (y = 0) %or (z = 0)) %and ((x = 0) %or (z = 0))
(%i7) nns(qe([],%));
(%o7)         (x = 0) %or ((x - 1 = 0) %and (y = 0) %and (z = 0))