Methods for proving termination of rewriting-based programming languages
by transformation
Author
Francisco Durán, Salvador Lucas, and José Meseguer
Abstract
Despite the remarkable development of the theory of termination of rewriting,
its application to high-level (rewriting-based) programming languages is far
from being optimal. This is due to the need for features such as conditional
equations and rules, types and subtypes, (possibly programmable) strategies
for controlling the execution, matching modulo axioms, and so on, that are
used in many programs and tend to place such programs outside the scope of
current termination tools. The operational meaning of such features is often
formalized in a proof theoretic manner by means of an inference system rather
than just by a rewriting relation. The corresponding termination notions can
also differ from the standard ones. During the last years we have introduced
and implemented different notions and transformation techniques which have
been proved useful for proving and disproving termination of such programs
by using existing tools for proving termination of (variants of) rewriting.
In this paper we provide an overview of our main achievements in this field.
Keywords
Program analysis and verification, Rewriting Logic, Term Rewriting, Termination, Tools