| Meaningless Terms in Rewriting (1996) | |||||||||||||||
Abstract | |||||||||||||||
| We present an axiomatic approach to the 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, confluence modulo equality 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 The concept of a meaningless term in a rewrite system originates with the lambda calculus [Bar84, Bar92]. There exist terms in the lambda calculus which, Email addresses: jrk@sys.uea.ac.uk, oostrom@cs.vu.nl, and ferjan@etl.go.jp. Richard Kennaway was s... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||