Syntactic Definitions of Undefined: On Defining the Undefined

In the A-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 undefinednessshould satisfy, and explore some of their consequences. The axioms lead to a concept analogous to the BShm trees of the A-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. AMS Subject Classification: 68Q42 CR Subject Classification: FI.1, F4.1, F4.2 Keywords 8,= Phrases: Orthogonal term rewriting systems, B5hm Trees, undefined terms, lambda calculus, solvabili...

• Type: Conference
• Year: 1994
• Where: TACS
• Authors: Zena M. Ariola, Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, Fer-Jan de Vries
• Keywords: Orthogonal Term, Rewrite System, Software Engineering, TACS 1994, Various Equivalent Characterisations