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 rst-order languages like Prolog. A stronglytyped 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 o er. Early development of Prolog faced similar problems, which were ultimately tackled through two di erent approaches. Both of these founded their roots in the theory of Term Rewriting Systems, but evolved along quite di erent paths. Constraint Logic Programming extended Prolog by integrating decision procedures for speci c theories to the inference engine. Rewriting Logic o ered 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 rst 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 con uence properties of -reduction and (restricted) -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 de ning a notion of rewriting. Since in a dependently typed calculus terms are allowed to appear inside types, a naive de nition, extending the one given by Nipkow for simply typed calculi, is inapplicable, as it may lead to situations where rewriting invalidates the type 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 con uence of rewriting, which, as usual, can be reduced to checking some special rewriting con gurations known as 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.