Meaningless terms in rewriting

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 Böhm 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.