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