| Meaningless Terms in Rewriting (1996) | |||||||||||||||
Abstract | |||||||||||||||
| . We present an axiomatic approach to meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in two ways. First, they are shown to imply important properties of meaninglessness: genericity of the class of meaningless terms, the consistency of equating all meaningless terms, and the construction of Bohm trees. Second we show that they can be easily verified for existing notions of meaninglessness. 1 Introduction Many notions have appeared in the literature of what it means for a term in a rewrite system to be "meaningless". In this paper we present axioms that a set of terms in a rewrite system should satisfy to be considered as a reasonable notion of meaninglessness. The axioms can be easily verified for many existing notions of meaninglessness, and are sufficient to prove several important properties of such notions, which in the past have been proved separately for each one. We consider term rewrite systems and lambda calculus, in both f... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||