Higher-Order Termination with Logical Constraints

Computer programs are generally hard to get right; even the most experienced programmers might nevertheless make mistakes. Program analysis addresses various aspects of program behavior, and helps improve the reliability of programs. This thesis concerns termination analysis; not only is termination itself critical to the correctness of certain programs, but it also can be a prerequisite for determining other properties, such as program equivalence.

Instead of focusing on programs written in a particular programming language, this thesis studies term rewriting systems (TRSs), which can represent a broad range of programs. Traditional TRSs lack support for primitive data types or higher-order functions; while extensions of TRSs that incorporate one of these features have been proposed, the combination of both in a TRS has remained unexplored. This thesis defines logically constrained simply-typed TRSs (LCSTRSs) — a higher-order formalism which accommodates primitive data types by means of logical constraints — and analyzes their termination.

The non-modularity of termination poses a major challenge: in general, we cannot conclude that a multipart system as a whole is terminating from the termination of all its parts, and it is not always possible to analyze the entire system in one go. To meet this challenge, this thesis extends the dependency pair (DP) method to LCSTRSs so that a termination problem becomes a DP problem, which in turn may be simplified, dissected, and eventually discharged. This way the initial problem can be solved incrementally.

This thesis also explores another dimension of modularity in termination analysis — the analysis of a module in a program without prior knowledge of how exactly the functions it defines may be used in a different part of the program. Universal computability — a new concept that has its roots in higher-order term rewriting — is proposed to deal with that scenario, and it is shown that the DP method can adapt to this concept.

To further bridge the gap between TRSs and real-world programs, this thesis additionally considers call-by-value rewriting on LCSTRSs. Call-by-value rewriting better reflects the execution of programs written in, say, OCaml and most imperative languages, and it allows for more refined analysis to study termination in this setting.