\documentstyle{article}
\title{Termination of Higher-order Rewrite Systems}
\author{Jaco van de Pol\\Eindhoven University of Technology}
\date{}
\begin{document}
\maketitle
\thispagestyle{empty}

{\bf Higher-order rewrite systems} (HRS) extend usual term
rewriting systems (TRS) with bound variables. In a HRS, the objects
are simply-typed lambda terms, containing typed function symbols. These
function symbols are defined by providing rewrite rules.

We have only one binding operator, $\lambda$.  Other bindings can be
mimiced, using higher-order function symbols, e.g.~$\forall: ({\tt
term}\rightarrow {\tt prop})\rightarrow {\tt prop}$.  Moreover, we use
$\beta$-reduction as a mechanism to perform (possibly nested)
substitutions. To match a given term with the rules, $\beta$-expansion
is required sometimes. The $\beta$-steps are not seen as separate
steps, but are performed ``under water''. Technically, the rewrite
relation is defined {\em modulo} $\beta$-equality.

\medskip
{\bf Termination} (or strong normalization) of higher-order
rewrite systems is the property that every rewrite sequence eventually
terminates.

Termination of a TRS can be shown by giving a monotone
algebra. A monotone algebra is an interpretation of the function symbols
as monotone functions over some well-founded partial order, such that
each rewrite rule denotes a descending pair. The existence of a monotone
algebra guarantees termination of a rewrite system.

This approach is extended by interpreting an HRS in the model of
functionals of finite type, based on a well-founded partial order. This
ordering is pointwise lifted to functionals.  Note that $\beta$-equal
terms denote the same functional.  If a model can be found where the
constants denote strict functionals, and the rules denote pairs of the
lifted order, then termination is again guaranteed.

\medskip
{\bf Applications} of HRSs can be found in proof theory: proof systems 
in natural deduction style can be modeled as HRSs,
by mapping proofs to lambda terms, and normalization steps
to rewrite steps.

Using the method sketched above, termination can be proved of
the usual conversion rules on natural deduction rules, including
proper reductions and permutative conversions. Also termination
of G\"odel's~T can be proved by this method.

\medskip
{\bf Acknowledgment.}
The talk is based on my thesis, written at Utrecht University.
There are connections with the work of Gandy, Klop, Nipkow, de~Vrijer,
Zantema.  Moreover, part of the research is joint work with
H.~Schwichtenberg.  

\end{document}