Termination of Lazy Rewriting Revisited

Lazy rewriting is a proper restriction of term rewriting that dynamically restricts the reduction of certain arguments of functions in order to obtain termination. In contrast to context-sensitive rewriting reductions at such argument positions are not completely forbidden but delayed. Based on the observation that the only existing (non-trivial) approach to prove termination of such lazy rewrite systems is flawed, we develop a modified approach for transforming lazy rewrite systems into context-sensitive ones that is sound and complete with respect to termination.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Felix Schernhammer, Bernhard Gramlich
• Keywords: Context-sensitive Rewriting Reductions, ENTCS 2008, Lazy Rewrite Systems, Proper Restriction