Resumen de Termination of narrowing: automated proofs and modularity properties

José Iborra López

• In 1936, Alan Turing proved that the halting problem, that is, deciding whether a program terminates, is an undecidable problem over most practical programming languages. Even so, termination is so relevant that a vast number of techniques for proving the termination of (as many as possible) programs have been researched in the recent decades. Term rewriting systems provide an abstract theoretical framework ideally suited for the study of termination. In term rewriting systems, evaluation of a term corresponds to the left-to-right, non-deterministic application of rewriting rules.

  Narrowing is a generalization of term rewriting that provides a mechanism for automated reasoning. For instance, given a set of rules defining addition and multiplication with natural numbers, rewriting allows to perform evaluation of arithmetic expressions, whereas narrowing allows to solve equations with variables over arithmetic expressions. This thesis constitutes the first in-depth study of the termination properties of narrowing. The contributions are as follows.

  First, we identify classes of systems where narrowing behaves well, in the sense that it always terminates for any system belonging to these classes. Many methods of analysis, such as the semantics-based analysis of program properties by means of narrowing, benefit from this characterization.

  Second, we develop an automatic method to prove termination of narrowing for a particular system, based on the abstract framework of dependency pairs. For the first time, such an automatic method is not restricted to particular classes and hence is universally applicable.

  Third, we propose another automatic method to prove termination of narrowing from a particular term, also on top of the framework of dependency pairs. Termination from a particular term is relevant for many applications, including the termination analysis of programming languages. Our method generalizes the current state-of-the-art, enabling the study of termination of logic programs in terms of the termination of narrowing, something which was not possible previously.

  Fourth and last, the modularity properties of the termination of narrowing are considered in detail. That is, given two systems A and B where narrowing is terminating, determine whether it is still terminating in the union system. This notion of modularity has implications in many of the applications of narrowing. We develop the case of combining systems for equational unification.

  Furthermore, the automated approaches of the second and third contributions above have been implemented in Narradar, our tool for automatic proofs of termination of narrowing.