OCaml Pattern Matching Negation normal form : deep pattern matching

Example

Pattern matching allows to deconstruct complex values and it is by no way limited to the “outer most” level of the representation of a value. To illustrate this, we implement the function transforming a boolean expression into a boolean expression where all negations are only on atoms, the so called negation normal form and a predicate recognising expressions in this form:

We define the type of boolean expressions whose atoms are identified by strings as

type expr =
| Atom of string
| Not of expr
| And of expr * expr
| Or of expr * expr

Let us first define a predicate recognising expressions in negation normal form:

let rec is_nnf = function
| (Atom(_) | Not(Atom(_))) -> true
| Not(_) -> false
| (And(expr1, expr2) | Or(expr1, expr2)) -> is_nnf expr1 && is_nnf expr2

As you see, it is possible to match against nested patterns like Not(Atom(_)). Now we implement a function mapping a boolean expression to an equivalent boolean expression in negation normal form:

let rec nnf = function
| (Atom(_) | Not(Atom(_))) as expr -> expr
| Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
| Not(Or(expr1, expr2)) -> And(nnf(Not(expr1)),nnf(Not(expr2)))
| And(expr1, expr2) -> And(nnf expr1, nnf expr2)
| Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
| Not(Not(expr)) -> nnf expr

This second function makes even more uses of nested patterns. We finally can test our code in the toplevel on the negation of an implication:

# let impl a b =
Or(Not(a), b);;
  val impl : expr -> expr -> expr = <fun>
# let expr = Not(impl (Atom "A") (Atom "B"));;
val expr : expr = Not (Or (Not (Atom "A"), Atom "B"))
# nnf expr;;
- : expr = And (Atom "A", Not (Atom "B"))
# is_nnf (nnf expr);;
- : bool = true

The OCaml type system is able to verify the exhaustivity of a pattern matching. For instance, if we omit the Not(Or(expr1, expr2)) case in the nnf function, the compiler issues a warning:

# let rec non_exhaustive_nnf = function
| (Atom(_) | Not(Atom(_))) as expr -> expr
| Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
| And(expr1, expr2) -> And(nnf expr1, nnf expr2)
| Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
| Not(Not(expr)) -> nnf expr;;
          Characters 14-254:
  ..............function
  | (Atom(_) | Not(Atom(_))) as expr -> expr
  | Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
  | And(expr1, expr2) -> And(nnf expr1, nnf expr2)
  | Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
  | Not(Not(expr)) -> nnf expr..
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Not (Or (_, _))
val non_exhaustive_nnf : expr -> expr = <fun>

(This warning can be treated as an error with the -w @8 option when invoking the compiler or the interpreter.)

This feature provides an increased level of safety and correctness in programs that are accepted by the compiler. It has however other uses and can for instance be used in explorative programming. It is is very fun to write a conversion to a normal form, starting with crude versions of the function that handle the easy cases and using examples of non-matched cases provided by the compiler to refine the treatment.