Meaningless terms in rewriting


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 Böhm trees. Second we show that they can be easily verified for existing notions of meaninglessness.