Putting Formulas in Normal Form

What would be a beautiful description for conversion to DNF?

The problem of converting a formula to DNF is easy to explain: Given a boolean formula, write it as a disjunction of conjunctions. For example, $(x \lor y) \land z$ may be rewritten, by distributivity, as $(x \land z) \lor (y \land z)$. The mechanism is also easy to describe: Push $\lnot$ down by de Morgan, then pull $\lor$ above $\land$ by distributivity.

How to turn this description into an algorithm?

I know a nice algorithm for the first half. Expressed in OCaml, it goes like this: We want a function with the type f1->f2, where

type f1 = [`Var of string | `Not of f1 | `And of f1 list | `Or of f1 list]
type f2 = [`Pos of string | `Neg of string | `And of f2 list | `Or of f2 list]

The trick is to keep around a parity.

let rec pnd (p : bool) : f1 -> f2 = function
  | `Var x -> if p then `Pos x else `Neg x
  | `Not f -> pnd (not p) f
  | `And fs ->
      let fs = List.map (pnd p) fs in
      if p then `And fs else `Or fs
  | `Or fs ->
      let fs = List.map (pnd p) fs in
      if p then `Or fs else `And fs

This algorithm I use when I do boolean manipulations on paper. So I like it. The code is nice, rather than beautiful, because it has some repetition.

What would be a similarly nice solution for the second half—applying distributivity? Expressed in OCaml, we want a function with the type f2->dnf, where

type dnf = [`Pos of string | `Neg of string] list list

Of course, I'm interested in solutions in any language.

Loops and Side-effects

TeX has a better looping construct.

I designed a small Java-like language for some experiments. I think it is a good idea to be able to say "this piece of code has no side-effects." (If you saw how I write C/++, you'd probably be surprised by what I just said.) There are various ways of isolating side-effects. My requirements were that (1) it must look much like Java and (2) there should be some way to contain side-effects. So I simply banned side-effects from expressions.

Then I proceeded to translate the following Java code.

while (i.hasNext()) {
  Object o = i.next();
  // bla
}

Method calls, however, possibly have side-effects so I could not use them in expressions. A method call is a statement in my toy language.

while (true) {
  boolean c = i.hasNext();
  if (!c) break;
  Object o = i.next();
  // bla
}

This loop reminded me of \loop ... \if ... \repeat in $\TeX$. The keywords loop and repeat, however, are rather un-Java-like-esque. So I decided to say do {...} while (...) {...}. This way, the normal do-loop and the while-loop are special cases obtained by omitting one of the bodies.

do boolean c = i.hasNext()
while (c) {
  Object o = i.next();
  // bla
}

Note that in Java (and C/++) one has the illusion that loops test their condition at the beginning (while) or at the end (do) but never in the middle. This is not true, because expressions may have side-effects.

If languages would have do-while-loops, then I'd probably break far less often.

I decided to write this post after seeing another post about how to write a similar kind of loop in OCaml.