In the lambda-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 B5hm 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.

, , , ,
International Conference on Theoretical Aspects of Computer Science
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Ariola, Z.M, Kennaway, J.R, Klop, J.W, Sleep, M.R, & de Vries, F.-J. (1994). Syntactic definitions of undefined: On defining the undefined. In Lecture Notes in Computer Science (pp. 543–554).