Fundamentals of context-sensitive rewriting
Recently we have introduced a novel class of rewrite relations we call
context-sensitive rewriting that proves useful to mechanize a particular class
of inference systems. In this paper, we give a more accurate characterization of
some properties of context-sensitive rewriting. We also show that several
reduction strategies used in lambda calculus namely weak reduction and lazy
(call by name) reduction, can be viewed as an instance of context-sensitive
term rewriting systems, regularity, functional programming.