| Meaningless Terms in Rewriting (1996) | |||||||||||||||
Abstract | |||||||||||||||
| We present an axiomatic approach to concept of meaninglessness in finite and transfinite term rewriting and lambda calculus. We justify our axioms in several ways. They can be intuitively justified from the viewpoint of rewriting as computation. 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 and models of rewrite systems. Finally, we show that they can be easily verified for many existing notions of meaninglessness, and easily refuted for some notions that are known not to be good characterisations 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 Email addresses: jrk@sys.uea.ac.uk, oostrom@cs.vu.nl, and ferjan@etl.go.jp. Richard... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||