Higher-Order Rewriting with Dependent Types



Higher-order, typed logic programming languages such as lambda-Prolog and Twelf have emerged in this last decade as the solution to many of the shortcomings of first-order languages like Prolog. A strongly-typed system allows early detection of many common programming mistakes, and it accounts for smaller and faster runtime environments. Lambda abstraction provides proper representation to the concept of bound variable, ubiquitous in mathematics. Because of these features, these languages have found in the last few years applications in several interesting areas, such as security protocols for mobile code. Unfortunately, use of these tools also evidenced a few problems in these languages, mostly due to the inadequate representation of equality that they offer.

Early development of Prolog faced similar problems, which were ultimately tackled through two different approaches. Both of these founded their roots in the theory of Term Rewriting Systems, but evolved along quite different paths. Constraint Logic Programming extended Prolog by integrating decision procedures for specific theories to the inference engine.  Rewriting Logic offered a new approach to logic programming, where term rewriting, rather than proof search, was used as model of computation.

We believe that the development of higher-order languages, in order to address their current inadequacies, should evolve along similar paths. For this reason, we study in this dissertation a theory of Higher-order Term Rewriting for the LF calculus, on which Twelf is based.

The results presented here can be divided in two parts. In the first part,we analyze an extension to LF where types can also be converted modulo an equational theory. As the LF calculus is very sensitive to changes in the type conversion relation used, all the confluence properties of  beta-reduction and (restricted) eta-expansion, and existence of normal forms have to re-examined. We show that our extension is conservative, and all the usual properties continue to hold, albeit in a weaker form.

In the second part, we proceed in defining a notion of rewriting. Since in a dependently typed calculus terms are allowed to appear inside types, a naive definition, extending the one given by Nipkow for simply typed calculi, is inapplicable, as it may lead to situations where rewriting invalidates the typed of an expression. Hence, we turn our attention to the study of special preorders, called dependence relations, that allow us to extract type information that is implicit in a LF signature, and use it to restrict rewriting to well-behaved instances.

Dependence relations turn out also to be useful when studying confluence of rewriting, which, as usual, can be reduced to checking some special rewriting configurations known as {\it critical pairs}. Together with a general Critical Pair Criterion, we present a specialized version, where fewer critical pairs need to be checked thanks to the type information conveyed by these preorders.

A few examples conclude the presentation, demonstrating some of the potential of the concepts introduced. We present applications to Milner's Action and Process Calculi, Category Theory, and Proof Theory.

Final draft: DVI, PostScript, PDF