WG211/M10Danvy

On Leftmost Outermost Disjunctive Normalization by Olivier Danvy (joint work with Jacob Johannsen and Ian Zerny)

This work continues the material presented at the 20th anniversary of
PEPM in January 2011. It illustrates semantics-based program
manipulation by inter-deriving reduction-based and reduction-free
normalization functions for Boolean formulas.
The PEPM presentation concerned negational normal forms,
and this continuation turns to disjunctive normal forms.
The challenge is to distribute conjunctions over disjunctions
in a context-free manner.
Once this challenge is met, we are back to business as usual:
an inter-derivation of a small-step, reduction-based normalizer
and of a big-step, reduction-free normalizer that is compositional
and operates in one pass. This normalizer provides a new application
of delimited continuations.