CNF reduction in ML
Exercise 1: Reduction to CNF - a first exercise in ML
Issued 12 January 2005
In this assignment you will gain some
familiarity with the programming language ML and implement a
non-trivial CNF reduction.
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.
- 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
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".
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)))
(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
|Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail:
Please contact our webadmin with
any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright ©
The University of Edinburgh