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.

Böhm Trees, Lambda calculus, Orthogonal term rewriting systems, Solvability, Undefined terms
International Conference on Theoretical Aspects of Computer Science
Centrum Wiskunde & Informatica, Amsterdam, 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).