Proving Termination of Context-Sensitive Rewriting by Transformation

Author

Salvador Lucas

Abstract

Context-sensitive rewriting (CSR) is a restriction of rewriting which forbids reductions on selected arguments of functions. With CSR we can achieve a terminating behavior with non-terminating Term Rewriting Systems, by pruning (all) infinite rewrite sequences. Proving termination of CSR has been recently recognized as an interesting problem with several applications in the fields of term rewriting and programming languages. Several methods have been developed for proving termination of CSR. In particular, a number of transformations which permit to treat this problem as a standard termination problem have been described. The main goal of this paper is to contribute to a better comprehension and practical use of transformations for proving termination of CSR.

Keywords

Program analysis, term rewriting, termination.