Hi.
I'm currently writing a compiler in C, which among other things includes
normalizing an expression to do certain translations.
Since I just couldn't figure that part out in C I went to prototype the
algorithm in Lisp yesterday.
Still for some reason my brain keeps thinking in circles and I can'
reach a solution.
I have some code which takes an expression like:
(and (or (var a) (var b)) (var c))
and should translate it into something like
(or (and (var a) (var c)) (and (var b) (var c)))
(I'll add code for handling NOT later).
(defun norm-and (ex)
(cons 'or (mapcar #'(lambda (l) (cons 'and (car l)))
(norm-and-list (cdr ex)))))
(defun norm-and-list (ls)
(if (null (cdr ls)) (list ls)
(let ((ands (norm-and-list (cdr ls)))
(ex (car ls)))
(cond ((eq 'or (car ex))
;; cons the "or" exprs on every list
(mapcar #'(lambda (ex)
(mapcar #'(lambda (ls)
(cons ex ls))
ands))
(cdr ex)))
;; "and" simple exprs
(t (mapcar #'(lambda (l) (cons ex l)) ands))))))
This code works fine sometimes:
(norm-and '(and (or (var c) (var d)) (var a) (var b)))
=> (OR (AND (VAR C) (VAR A) (VAR B)) (AND (VAR D) (VAR A) (VAR B))),
but fails on other lists:
(norm-and '(and (var a) (var b) (or (var c) (var d))))
=> (OR (AND VAR A))
I'd be really thankful for any hints, or just _what_ is wrong, as I
can't figure it out right now.
Regards, Ulrich
P.S. The above probably is very bad Lisp, since I haven't used it for
years (and only some Scheme back then).
On Thu, 24 Jun 2004, Ulrich Hobelmann wrote:
> Hi.
> I'm currently writing a compiler in C, which among other things includes
> normalizing an expression to do certain translations.
> Since I just couldn't figure that part out in C I went to prototype the
> algorithm in Lisp yesterday.
> Still for some reason my brain keeps thinking in circles and I can'
> reach a solution.
>
So you want to convert from conjunctive normal form to disjunctive normal
form. If you think of it inductively on the list, then there is an
algorithm that goes something like this:
Base case: no conjuncts --> (or (and))
Case (and a ...) -->
Hypothesis: (cnf->dnf ...) returns valid DNF
The inductive step then is to combine a with the result of above,
and produce valid DNF.
(defun preprocess (form)
"Convert to our CNF representation: a list of lists where the top-level
list represents a conjunction and each inner list represents a disjunction."
(mapcar #'(lambda (subform)
(cond ((and (consp subform)
(eql 'or (first subform)))
(rest subform))
(t (list subform))))
(rest form)))
(defun %cnf->dnf (cnf)
(if (null cnf)
;; Base Case
'(()) ; (or (and))
;; else
(let ((disjuncts (first cnf))
(dnf (%cnf->dnf (rest cnf))))
;; dnf here is the result DNF from the CNF
;; following the current disjuncts.
;; we need to merge the current disjuncts into
;; the rest of the DNF in order to complete
;; the inductive step
(loop for a in disjuncts appending
(loop for b in dnf collecting
(cons a b))))))
(defun postprocess (dnf)
"Convert from our DNF representation: a list of lists where the top-level
list represents a disjunction and each inner list represents a conjunction."
(cons 'or (mapcar #'(lambda (c)
(if (and (not (null c))
(null (rest c)))
c
(cons 'and c)))
dnf)))
(defun cnf->dnf (form &optional (output nil))
"Conjuctive Normal Form -> Disjunctive Normal Form"
(let ((*print-circle* nil)
(result (postprocess (%cnf->dnf (preprocess form)))))
(if output
(format output "~S" result)
result)))
CL-USER> (cnf->dnf '(nil) t)
(or (and))
CL-USER> (cnf->dnf '(and (or (var a) (var b)) (var c)) t)
(or (and (var a) (var c)) (and (var b) (var c)))
CL-USER> (cnf->dnf '(and (or (var c) (var d)) (var a) (var b)) t)
(or (and (var c) (var a) (var b)) (and (var d) (var a) (var b)))
CL-USER> (cnf->dnf '(and (var a) (var b) (or (var c) (var d))) t)
(or (and (var a) (var b) (var c)) (and (var a) (var b) (var d)))
Matthew Danish wrote:
> So you want to convert from conjunctive normal form to disjunctive normal
> form. If you think of it inductively on the list, then there is an
> algorithm that goes something like this:
Unfortunately, no. Originally I have a parse tree, part of which is
(binary) expressions. I convert these binary expressions into
conjunctive or disjunctive lists, i.e. (and (and (var a) (var b)) (var
c)) becomes (and (var a) (var b) (var c)).
What I still have is arbitrarily nested "and"s "or"s and "not"s. My
goal is the DNF of these expressions.
My idea was to bring all "or"s in "and"s to the toplevel first by
transforming stuff like (and a (or b c)) to (or (and a b) (and a c)).
Then I would invert expressions inside a not (rather easy) and bring
those to the top level too (should be no more than a recursive transform
call on (invert stuff)).
Right now my head is too dizzy, but I'll take a look at your code later.
Anyway, thanks a lot.
Ulrich