Syntactic definitions of undefined: On defining the undefined

In the λ-calculus, there is a standard notion of what terms should be considered to be “undefined”: the unsolvable terms. There are various equivalent characterisations of this property of terms. We attempt to find a similar notion for orthogonal term rewrite systems. We find that in general the properties of terms analogous to the various characterisations of solvability differ.

We give two axioms that a notion of undefinedness should satisfy, and explore some of their consequences. The axioms lead to a concept analogous to the Böhm trees of the λ-calculus. Each term has a unique Böhm tree, and the set of such trees forms a domain which provides a denotational semantics for the rewrite system. We consider several particular notions of undefinedness satisfying the axioms, and compare them.

Authors and Affiliations

1. Computer and Information Science Department, University of Oregon, Eugene, Oregon

   Zena Ariola

2. School of Information Systems, University of East Anglia, NR4 7TJ, Norwich, UK

   Richard Kennaway & Ronan Sleep

3. CWI, P.O. Box 94079, 1090, GB Amsterdam, the Netherlands

   Jan Willem Klop & Fer-Jan de Vries

Reprints and permissions

© 1994 Springer-Verlag Berlin Heidelberg

Policies and ethics