CNF reduction in ML
Exercise 1: Reduction to CNF - a first exercise in ML
Issued 12 January 2005
Introduction
In this assignment you will gain some
familiarity with the programming language ML and implement a
non-trivial CNF reduction.
ML
The ML recommended for this
course is Dave Matthews'
PolyML, which is freely
available for download for a number of platforms. The PolyML site also
includes useful documentation.
PolyML is installed on DICE machines and is invoked with the shell command "poly".
Alternatives include "Moscow ML" and
"Standard ML of New Jersey", which implement the same language (for
our purposes at least), and can be tracked down using Google.
Hints
- Use emacs with two buffers: one editing a file with your code; one with a shell running poly.
- Use the extension .sml (Standard ML) or .ml for your ML code files - emacs should load sml-mode automatically.
- To interrupt PolyML at any time, type ^C, then at the prompt, f (for fail) or q (to quit PolyML).
- To include code previously saved in a file with name filename.sml, or filename.ml ((or indeed, just filename) type use "filename"; to the PolyML prompt.
- There are several ML tutorials available on the web. The closest to home is
Stephen Gilmore's
ML Tutorial
Refer to to the contents page. You will probably find it helpful to refer to the first four sections on "Simple Applicative Programming", the first two on "Higher-order programming", the section on "Defining Datatypes", and the section on "Lists".
Tasks
-
The example file CNF conversion in ML provides a partial implementation of the naive CNF conversion (Sebastiani p.24). Read and understand the code. Look at the warnings generated when you compile (ie "use") this file. Test this on a number of example formulae, and complete any missing cases.
-
Implement the labelling CNF conversion (Sebastiani p.25).
You will probably find the following code snippet useful.
val gensym =
let val count = ref 0 in
fn () => (count := !count +1; "X"^(Int.toString (!count)))
end
(Repeated evaluations of gensym() generate a sequence of strings "X1", "X2", etc. which can be used as names of new variables.)
- (Optional) Implement the improved labelling CNF conversion (Sebastiani p. 27)
Author: Michael Fourman
Revision 1.5 by
MichaelFourman
2006/01/12 09:16:07