Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting
Author
Beatriz Alarcón and Salvador Lucas
Abstract
Computational systems based on reducing expressions usually have a
predefined reduction strategy to break down the nondeterminism which
is inherent to reduction relations. The innermost strategy
corresponds to call by value or eager computation, that is,
the computational mechanism of several programming languages like
Maude, OBJ, etc. where the arguments of a function call are always
evaluated before calling the function. This strategy usually
fails to terminate when nonterminating computations are possible in
the programs and many eager programming languages also admit the
specification of a particular class of strategy
annotations to (try to) avoid them. Context-Sensitive Rewriting
provides an abstract model to describe and analyze the operational
behavior of such programs. This paper aims at contributing to the
development of appropriate techniques and tools for the verification
of program termination in the aforementioned programming
languages, so we focus on termination of innermost
(context-sensitive) rewriting. We adapt the notion of usable
argument introduced by Fernández to prove innermost termination by
proving termination of context-sensitive rewriting. Thanks to our
recent developments for proving termination of (innermost)
context-sensitive rewriting using dependency pairs, now we can also
relax monotonicity requirements for proving innermost termination of
(context-sensitive) rewriting. We have implemented these new
improvements in the termination tool MU-TERM and evaluated the
results with some benchmarks.
Keywords
Dependency pairs, innermost rewriting, context-sensitive rewriting
program analysis, termination.