1: \documentclass{llncs}
2:
3: \usepackage{times}
4: \usepackage{latexsym}
5: \usepackage{paralist}
6: \usepackage{citesort}
7: \usepackage{amssymb}
8:
9: \input{macros}
10:
11: \begin{document}
12:
13: \title{Higher-Order Termination:\\ From Kruskal to
14: Computability}
15:
16: \author{
17: Fr{\'e}d{\'e}ric Blanqui\inst{1}
18: \and
19: Jean-Pierre Jouannaud\inst{2}\thanks{Project
20: LogiCal, P{\^o}le Commun de Recherche en Informatique du Plateau de
21: Saclay, CNRS, {\'E}cole Polytechnique, INRIA, Universit{\'e} Paris-Sud.}
22: \and
23: Albert Rubio\inst{3}}
24:
25: \institute{
26: {INRIA \& LORIA, BP 101, 54602 Villiers-l{\'e}s-Nancy CEDEX, France}
27: \and
28: {LIX, {\'E}cole Polytechnique,
29: 91400 Palaiseau, France}
30: \and
31: {Technical University of Catalonia,
32: Pau Gargallo 5, 08028 Barcelona, Spain}
33: }
34:
35:
36: \maketitle
37:
38:
39:
40: \section{Introduction}
41: \label{s:introduction}
42:
43: Termination is a major question in both logic and computer science. In
44: logic, termination is at the heart of proof theory where it is usually
45: called strong normalization (of cut elimination). In computer science,
46: termination has always been an important issue for showing programs
47: correct. In the early days of logic, strong normalization was usually
48: shown by assigning ordinals to expressions in such a way that
49: eliminating a cut would yield an expression with a smaller ordinal. In
50: the early days of verification, computer scientists used similar
51: ideas, interpreting the arguments of a program call by a natural
52: number, such as their size. Showing the size of the arguments to
53: decrease for each recursive call gives a termination proof of the
54: program, which is however rather weak since it can only yield quite
55: small ordinals. In the sixties, Tait invented a new method for showing
56: cut elimination of natural deduction, based on a \emph{predicate} over
57: the set of terms, such that the membership of an expression to the
58: predicate implied the strong normalization property for that
59: expression. The predicate being defined by induction on types, or even
60: as a fixpoint, this method could yield much larger ordinals. Later
61: generalized by Girard under the name of \emph{reducibility} or
62: \emph{computability candidates}, it showed very effective in proving
63: the strong normalization property of typed lambda-calculi with
64: polymorphic types, dependent types, inductive types, and finally a
65: cumulative hierarchy of universes. On the programming side, research
66: on termination shifted from programming to executable specification
67: languages based on rewriting, and concentrated on automatable methods
68: based on the construction on well-founded orderings of the set of
69: terms. The milestone here is Dershowitz's \emph{recursive path
70: ordering} (RPO), in the late seventies, whose well-foundedness proof
71: is based on a powerful combinatorial argument, Kruskal's tree
72: theorem, which also yields rather large ordinals. While the
73: computability predicates must be defined for each particular case, and
74: their properties proved by hand, the recursive path ordering can be
75: effectively automated.
76:
77: These two methods are completely different. Computability arguments show
78: \emph{termination}, that is, infinite decreasing sequences of
79: expressions $e_0\succ e_1\succ\ldots e_n\succ e_{n+1}\ldots$ do not
80: exist. Kruskal's based arguments show \emph{well-orderedness}: for any
81: infinite sequence of expressions $\{e_i\}_i$, there is a pair $j<k$
82: such that $e_j\preceq e_k$. It is easy to see that well-orderedness
83: implies termination, but the converse is not true.
84:
85: In the late eighties, a new question arose: termination of a
86: simply-typed lambda-calculus language in which beta-reduction would be
87: supplemented with terminating first-order rewrite rules. Breazu-Tannen
88: and Gallier on the one hand~\cite{BTG90}, and
89: Okada~\cite{okada89issac} on the other hand, showed that termination
90: was satisfied by the combination
91: by using computability arguments. Indeed, when rewriting
92: operates at basic types and is generated by first-order rewrite
93: rules, beta-reduction and rewriting do not interfere. Their result,
94: proved for a polymorphic $\lambda$-calculus, was later generalized to
95: the calculus of constructions~\cite{barbanera90}. The situation becomes
96: radically different with higher-order rewriting generated by rules
97: operating on arrow-types, or involving lambda-bindings or higher-order
98: variables. Such an example is provided by G{\"o}del's system
99: $T$, in which higher-order primitive recursion for natural
100: numbers generated by Peano's constructors $0$ and $s$ is described by
101: the following two higher-order rules :
102: \begin{eqnarray*}
103: rec(0,U,V) &\ra& U\\
104: rec(s(X),U,V) &\ra& @(V,X,rec(X,U,V))
105: \end{eqnarray*}
106: where $rec$ is a function symbol of type $\Nat \ra
107: T \ra (\Nat\ra T \ra T)\ra T$, $U$ is a higher-order variable of type
108: $T$ and $V$ a higher-order variable of type $\Nat \ra T \ra T$, for all type $T$.
109: Jouannaud and Okada invented the so-called
110: general-schema~\cite{jouannaud91lics}, a powerful generalization of
111: G{\"o}del's higher-order primitive recursion of higher types. Following
112: the path initiated by Breazu-Tannen and Gallier on the one hand, and
113: Okada on the other hand, termination of calculi based on the general
114: schema was proved by using computability arguments as
115: well~\cite{jouannaud91lics,jouannaud97tcs,barbanera94lics}. The
116: general schema was then reformulated by Blanqui, Jouannaud and
117: Okada~\cite{blanqui99rta,blanqui02tcs} in order to incorporate
118: computability arguments directly in its definition, opening the way to
119: new generalizations. G{\"o}del's system $T$ can be generalized in two
120: ways, by introducing type constructors and dependent types, yielding
121: the Calculus of Constructions, and by introducing strictly positive
122: inductive types. Both together yield the Calculus of Inductive
123: Constructions~\cite{paulin93tlca}, the theory underlying the Coq
124: system~\cite{coq8.0}, in which rewrite rules like strong
125: elimination operate on types, raising new difficulties. Blanqui gave a
126: generalization of the general schema which includes the Calculus of
127: Inductive Constructions as a particular case under the name of
128: Calculus of Algebraic Constructions~\cite{blanqui05mscs,blanqui05fi}.
129:
130: The general schema, however, is too simple to analyze complex calculi
131: defined by higher-order rewrite rules such as encodings of logics. For
132: that purpose, Jouannaud and Rubio generalized the recursive path
133: ordering to the higher-order case, yielding the higher-order recursive
134: path ordering (HORPO)~\cite{jouannaud99lics}. The RPO
135: well-foundedness proof follows from Kruskal's tree theorem, but no
136: such theorem exists in presence of a binding construct, and it is not
137: at all clear that such a theorem may exist. What is remarkable is
138: that computability arguments fit with RPO's recursive structure. When
139: applied to RPO, these arguments result in a new, simple,
140: well-foundedness proof of RPO. One could even argue that this is the
141: \emph{first} well-foundedness proof of RPO, since Dershowitz showed
142: \emph{more}: well-orderedness.
143:
144: Combining the general schema and the HORPO is indeed easy because
145: their termination properties are both based on computability
146: arguments. The resulting relation, HORPO with closure, combines an
147: ordering relation with a membership predicate. In this paper, we
148: reformulate and improve a recent idea of Blanqui~\cite{blanqui06horpo}
149: by defining a new version of the HORPO with closure which integrates
150: smoothly the idea of the general schema into HORPO in the form of a
151: new ordering definition.
152:
153: So far, we have considered the kind of higher-order rewriting defined by
154: using first-order pattern matching as in the calculus of
155: constructions. These orderings need to contain $\beta$- and
156: $\eta$-reductions. Showing termination of higher-order rewrite rules
157: based on higher-order pattern matching, that is, rewriting modulo
158: $\beta$ and $\eta$ now used as equalities, turns out to require simple
159: modifications of HORPO~\cite{jouannaud06rta}. We will therefore concentrate here on
160: higher-order orderings containing $\beta$- and $\eta$-reductions.
161:
162: We introduce higher-order algebras in Section~\ref{s:preliminaries}.
163: In Section~\ref{s:computability}, we recall the computability argument
164: for this variation of the simply typed lambda calculus. Using a
165: computability argument again, we show in Section~\ref{s:rpo} that RPO
166: is well-founded. We introduce the general schema in
167: section~\ref{s:closure}, and the HORPO in Section~\ref{s:horpo} before
168: to combine both in Section~\ref{s:newhorpo}. We end up with related
169: work and open problems in the last two sections.
170:
171: \section{Higher-Order Algebras}
172: \label{s:preliminaries}
173:
174: The notion of a higher-order algebra given here is the monomorphic
175: version of the notion of polymorphic higher-order algebra defined
176: in~\cite{jouannaud06jacm}. Polymorphism has been ruled out for simplicity.
177:
178: \subsection{Types, Signatures and Terms}
179: \label{types}
180: Given a set $\Sort$ of \emph{sort symbols} of a fixed arity, denoted by
181: $s:*^n\Dra *$, the set $\Type$ of
182: \emph{types} is generated from these sets by the arrow
183: constructor:
184: \[
185: \begin{array}{c}
186: \Type := s(\Type^n) ~|~ (\Type \ra \Type) \\
187: \mbox{for } s: *^n\Dra *~\in\Sort
188: \end{array}
189: \]
190: Types headed by $\ra$ are \emph{arrow types} while the others
191: are \emph{basic types}. \emph{Type declarations} are expressions
192: of the form $\sigma_1 \times \cdots \times \sigma_n \ra \sigma$, where
193: $n$ is the \emph{arity} of the type declaration, and $\sigma_1,
194: \ldots,\sigma_n, \sigma$ are types. A type declaration is {\em
195: first-order} if it uses only sorts, otherwise \emph{higher-order}.
196:
197: We assume given a set of function symbols which are meant to be algebraic
198: operators. Each function symbol $f$ is equipped with a type
199: declaration $f\colon\sigma_1 \times\cdots \times \sigma_n \ra
200: \sigma$. We use $\F_n$ for the set of function symbols of arity $n$.
201: $\F$ is a \emph{first-order signature} if all its type
202: declarations are first-order, and a higher-order signature otherwise.
203:
204: The set of \emph{raw terms} is generated from
205: the signature ${\cal F}$ and a denumerable set $\X$ of
206: variables according to the grammar:
207: \[
208: \Term :=
209: \X \mid (\lambda \X . \Term) \mid @(\Term,\Term) \mid \F(\Term,\ldots,\Term).
210: \]
211: Terms generated by the first two grammar rules are called
212: \emph{algebraic}. Terms of the form $\lambda x.u$ are called
213: \emph{abstractions} while terms of the form $@(u,v)$ are called
214: \emph{applications}. The term $@(u,\vect{v})$ is called a (partial)
215: \emph{left-flattening} of $@(\dots @(@(u,v_1),v_2),\dots, v_n)$,
216: with
217: $u$ being possibly an application itself. Terms other than
218: abstractions are said to be \emph{neutral}. We denote by $\Var{t}$
219: ($\BVar{t}$) the set of free (bound) variables of $t$. We may assume
220: for convenience (and without further notice) that bound variables in a
221: term are all different, and are different from the free ones.
222:
223: Terms are identified with finite labeled trees by considering $\lambda
224: x .$, for each variable $x$, as a unary function symbol. {\em
225: Positions} are strings of positive integers, the empty string $\rootp$
226: denoting the root position. The {\it subterm} of $t$ at position $p$
227: is denoted by $t|_p$, and by $t[u]_p$ the result of replacing $t|_p$
228: at position $p$ in $t$ by $u$. We write $s\gtsubt u$ if $u$ is a
229: strict subterm of $s$. We use $t[~]_p$ for a term with a hole, called
230: a context. The notation $\vect{s}$ will be ambiguously used to denote
231: a list, a multiset, or a set of terms $s_1,\ldots,s_n$.
232:
233:
234: \subsection{Typing Rules}
235: \label{tr}
236: Typing rules restrict the set of terms by constraining them to follow
237: a precise discipline. Environments are sets of pairs written
238: $x:\sigma$, where $x$ is a variable and $\sigma$ is a type. Let
239: $\Dom{\Gamma}=\{x \mid x:\sigma\in\Gamma \mbox { for some type }
240: \sigma\}$. We assume there is a unique pair of the form $x:\sigma$
241: for every variable $x\in\Dom{\Gamma}$. Our typing judgments are
242: written as $\Gamma \turnstyle M : \sigma$ if the term $M$ can be
243: proved to have the type $\sigma$ in the environment $\Gamma$. A term
244: $M$ has type $\sigma$ in the environment $\Gamma$ if $\Gamma
245: \turnstyle M : \sigma$ is provable in the inference system of
246: Figure~\ref{f:typing}. A term $M$ is typable in the environment
247: $\Gamma$ if there exists a type
248: $\sigma$ such that $M$ has type $\sigma$ in the environment
249: $\Gamma$. A term $M$ is typable if it is typable in some environment
250: $\Gamma$. Note that function symbols are uncurried, hence must come
251: along with all their arguments.
252:
253: \begin{figure}
254: \begin{center}
255: \fbox{
256: $
257: \begin{array}{ccc}
258: \begin{array}{c}
259: \newinfRULE
260: {Variables}
261: {x : \sigma \in \Gamma}
262: {\Gamma \turnstyle x : \sigma}
263: \end{array}
264: &\quad&
265: \begin{array}{c}
266: \newinfRULE
267: {Functions}
268: {\begin{array}{c}
269: f : \sigma_1 \times \ldots \times \sigma_n \ra \sigma\\
270: \Gamma \turnstyle t_1 : \sigma_1 ~\ldots~ \Gamma \turnstyle t_n : \sigma_n
271: \end{array}}
272: {\Gamma \turnstyle f(t_1,\ldots,t_n): \sigma}
273: \end{array}
274: \\\\
275: \begin{array}{c}
276: \newinfRULE
277: {Abstraction}
278: {\Gamma \cup \{x : \sigma \} \turnstyle t : \tau}
279: {\Gamma \turnstyle (\lambda x:\sigma.t) : \sigma \ra \tau}
280: \end{array}
281: &&
282: \begin{array}{c}
283: \newinfRULE
284: {Application}
285: {\Gamma \cup \{x : \sigma \} \turnstyle s : \sigma \ra \tau~~~~
286: \Gamma \turnstyle t : \sigma }
287: {\Gamma \turnstyle @(s, t) : \tau}
288: \end{array}
289: \\\\
290: \end{array}
291: $
292: }
293: \end{center}
294: \caption{Typing judgments in higher-order algebras}\label{f:typing}
295: \end{figure}
296:
297: \subsection{Higher-Order Rewrite Rules}
298: Substitutions are written as in $\{x_1:\sigma_1 \mapsto (\Gamma_1,
299: t_1),\ldots, x_n:\sigma_n \mapsto (\Gamma_n,t_n)\}$ where, for every
300: $i\in[1..n]$, $t_i$ is assumed different from $x_i$ and
301: $\Gamma_i\turnstyle t_i:\sigma_i$. We also assume that
302: $\bigcup_i{\Gamma_i}$ is an environment.
303: We often write $x\mapsto t$ instead of
304: $x:\sigma\mapsto (\Gamma,t)$, in particular when $t$ is ground. We
305: use the letter $\gamma$ for substitutions and postfix notation for
306: their application. Substitutions behave as endomorphisms defined on
307: free variables.
308:
309: \noindent%
310: A (possibly higher-order) {\it term rewriting system} is a set of
311: rewrite rules $R=\{\Gamma_i \turnstyle l_i \ra r_i:\sigma_i\}_i$,
312: where $l_i$ and $r_i$ are higher-order terms such that $l_i$ and $r_i$
313: have the same type $\sigma_i$ in the environment $\Gamma_i$. Given a
314: term rewriting
315: system $R$, a term $s$ rewrites to a term $t$ at position
316: $p$ with the rule $l\ra r$ and the substitution $\gamma$, written
317: $\displaystyle s \lrps{p}{l\ra r} t$, or simply $s \ra_R t$, if $s|_p
318: = l\gamma$ and $t = s[r\gamma]_p$.
319:
320: A term $s$ such that $\displaystyle s\lrps{p}{R} t$ is called {\em
321: $R$-reducible}. The subterm $s|_p$ is a \emph{redex} in $s$, and $t$
322: is the \emph{reduct} of $s$. Irreducible terms are said to be in {\it
323: $R$-normal form}. A substitution $\gamma$ is in $R$-normal form if
324: $x\gamma$ is in $R$-normal form for all $x$. We denote by
325: $\displaystyle \lrps{*}{R}$ the reflexive, transitive closure of the
326: rewrite relation $\displaystyle \lrps{}{R}$.
327:
328: Given a rewrite relation $\lrps{}{}$, a term $s$ is strongly
329: normalizing if there is no infinite sequence of rewrites issuing from
330: $s$. The rewrite relation itself is {\it strongly normalizing}, or
331: {\it terminating}, if all terms are strongly normalizing, in which case
332: it is called a \emph{reduction}.
333:
334: Three particular higher-order equation schemas originate from the $\lambda$-calculus,
335: $\alpha$-, $\beta$- and $\eta$-equality:
336: \begin{center}
337: $
338: \begin{array}{rcll}
339: \lambda x . v & =_\alpha & \lambda y . v\{x\mapsto y\}
340: & \mbox{if}~ y\not\in\BVar{v}~\cup~ (\Var{v}\setminus\{x\})\\
341: @(\lambda x . v, u) & \lrps{}{\beta} & v\{x \mapsto u\} &\\
342: \lambda x . @(u, x) & \lrps{}{\eta} & u & \mbox{if}~ x\not\in\Var{u}
343: \end{array}
344: $
345: \end{center}
346:
347: As usual, we do not distinguish $\alpha$-convertible terms.
348: $\beta$- and $\eta$-equalities are used as reductions, which is
349: indicated by the long-arrow symbol instead of the equality symbol.
350: The above rule-schemas define a rewrite system which is known to be
351: terminating, a result proved in Section~\ref{s:computability}.
352:
353: \subsection{Higher-Order Reduction Orderings}
354: \label{ro}
355: We will make intensive use of well-founded orderings, using the
356: vocabulary of rewrite systems for orderings, for proving strong
357: normalization properties. For our purpose, an \emph{ordering}, usually
358: denoted by $\geq$, is a reflexive, symmetric, transitive relation
359: compatible with $\alpha$-conversion, that is, $s=_\alpha t\geq
360: u=_\alpha v$ implies $s\geq v$, whose strict part $>$ is itself
361: compatible. We will essentially use strict orderings, and hence, the
362: word ordering for them too. We will also make use of order-preserving
363: operations on relations, namely multiset and lexicographic extensions,
364: see~\cite{dershowitz88}.
365:
366: \emph{Rewrite orderings} are \emph{monotonic} and \emph{stable}
367: orderings, \emph{reduction orderings} are in addition {\em
368: well-founded}, while \emph{higher-order reduction orderings} must also
369: contain $\beta$- and $\eta$-reductions. Monotonicity of $>$ is defined
370: as $u > v$ implies $s[u]_p > s[v]_p$ for all contexts
371: $s[~]_p$. Stability of $>$ is defined as $u > v$ implies $s\gamma >
372: t\gamma$ for all substitutions $\gamma$. Higher-order reduction
373: orderings are used to prove termination of rewrite systems including
374: $\beta$- and $\eta$-reductions by simply comparing the left hand and
375: right hand sides of the remaining rules.
376:
377:
378:
379: \section{Computability}
380: \label{s:computability}
381:
382: Simply minded arguments do not work for showing the strong
383: normalization property of the simply typed lambda-calculus, for
384: $\beta$-reduction increases the size of terms, which precludes
385: an induction on their size, and preserves their types, which seems to
386: preclude an induction on types.
387:
388: Tait's idea is to generalize the strong normalization property in
389: order to enable an induction on types. To each type $\sigma$, we
390: associate a subset $\cand{\sigma}$ of the set of terms, called the
391: \emph{computability predicate} of type $\sigma$, or set of
392: \emph{computable terms} of type $\sigma$. Whether $\cand{\sigma}$
393: contains only typable terms of type $\sigma$ is not really important,
394: although it can help intuition. What is essential are the properties
395: that the family of predicates should satisfy:
396:
397: \begin{compactenum}[(i)]
398: \item computable terms are strongly normalizing;
399: \item reducts of computable terms are computable;
400: \item a neutral term $u$ is computable iff all its reducts are
401: computable;
402: \item $u:\sigma\ra\tau$ is computable iff so is $@(u,v)$ for all
403: computable $v$.
404: \end{compactenum}
405:
406:
407:
408:
409:
410: A (non-trivial) consequence of all these properties can be added to
411: smooth the proof of the coming Main Lemma:
412:
413: \begin{compactenum}[(i)]\setcounter{enumi}{4}
414: \item \label{fifth}
415: $\lambda x.u$ is computable iff so is $u\{x\mapsto
416: v\}$ for all computable $v$.
417: \end{compactenum}
418:
419:
420: Apart from (\ref{fifth}), the above properties refer to
421: $\beta$-reduction via the notions of \emph{reduct} and \emph{strong
422: normalization} only. Indeed, various computability predicates found
423: in the literature use the same definition parametrized by the
424: considered reduction relation.
425:
426: There are several ways to define a computability predicate by taking
427: as its definition some of the properties that it should satisfy. For
428: example, a simple definition by induction on types is this:
429:
430: $s:\sigma\in\cand{\sigma}$ for $\sigma$ basic iff $s$ is strongly normalizing;
431:
432: $s:\theta\ra\tau\in\cand{\sigma\ra\tau}$ iff
433: $@(s,u):\tau\in\cand{\tau}$ for every $u:\theta\in\cand{\theta}$.
434:
435: \noindent
436: An alternative for the case of basic type is:
437: \begin{displaymath}
438: s:\sigma\in\cand{\sigma} \mbox{~iff~} \forall t:\tau~.~s\lrps{}{}t
439: \mbox{~then~}
440: t\in\cand{\tau} .
441: \end{displaymath}
442: This formulation defines the predicate as a
443: fixpoint of a monotonic functional. Once the predicate is defined, it
444: becomes necessary to show the computability properties. This uses an induction on
445: types in the first case or an induction on the definition of the
446: predicate in the fixpoint case.
447:
448: Tait's strong normalization proof is based on the following key lemma:
449:
450: \begin{lemma}[Main Lemma]
451: Let $s$ be an arbitrary term and $\gamma$ be an arbitrary computable
452: substitution. Then $s\gamma$ is computable.
453: \end{lemma}
454:
455: \begin{proof}
456: By induction on the structure of terms.
457: \begin{enumerate}
458: \item
459: $s$ is a variable: $s\gamma$ is computable by assumption on $\gamma$.
460: \item
461: $s=@(u,v)$. Since $u\gamma$ and $v\gamma$ are computable by induction
462: hypothesis, $s\gamma=@(u\gamma,v\gamma)$ is computable by
463: computability property (iv).
464: \item
465: $s=\lambda x . u$. By computability property (v), $s\gamma=\lambda
466: x.u\gamma$ is computable iff $u\gamma\{x\mapsto v\}$ is computable for
467: an arbitrary computable $v$. Let now $\gamma'=\gamma\cup\{x\mapsto
468: v\}$. By definition of substitutions for abstractions,
469: $u\gamma\{x\mapsto v\}=u\gamma'$, which is usually ensured by
470: $\alpha$-conversion. By assumptions on $\gamma$ and $v$, $\gamma'$ is
471: computable, and $u\gamma'$ is therefore computable by the main induction
472: hypothesis.
473: \qed
474: \end{enumerate}
475: \end{proof}
476:
477: Since an arbitrary term $s$ can be seen as its own instance by the
478: identity substitution, which is computable by computability property
479: (iii), all terms are computable by the Main Lemma, hence strongly
480: normalizing by computability property (i).
481:
482:
483: \section{The Recursive Path Ordering and Computability}
484: \label{s:rpo}
485:
486: In this section, we restrict ourselves to first-order algebraic terms.
487: Assuming that the set of function symbols is equipped with an ordering
488: relation $\geF$, called \emph{precedence}, and a status function $stat$,
489: writing $stat_f$ for $stat(f)$, we recall the definition of the
490: recursive path ordering:
491:
492: \begin{definition}
493: \label{d:rpo}
494: $s\gtrpo t$ iff
495: \begin{enumerate}
496: \item
497: \label{rposubt}
498: $s=f(\vect{s})$ with $f\in\F$,
499: and
500: $ u \displaystyle{\gerpo} t$ for some
501: $u\in\vect{s}$
502:
503: \item
504: \label{rpoprec}
505: $s=f(\vect{s})$ with $f\in\F$, and
506: $t=g(\vect{t})$ with $f\gtF g$, and $A$
507:
508: \item
509: \label{rpomul}
510: $s=f(\vect{s})$ and $t=g(\vect{t})$ with $f=_\F g\in\Mul$, and
511: $\vect{s}~(\displaystyle{\gtrpo})_{mul}~ \vect{t}$
512:
513: \item
514: \label{rpolex}
515: $s=f(\vect{s})$ and $t=g(\vect{t})$ with $f=_\F g\in\Lex$, and
516: $\vect{s}~(\displaystyle{\gtrpo})_{lex}~ \vect{t}$ and $A$
517: \end{enumerate}
518: $$\mbox{where } A=\forall v\in\vect{t}. ~ s\gtrpo v \quad\mbox{ and }\quad
519: s\gerpo t \mbox{ iff } s\gtrpo t \mbox{ or } s=t$$
520: \end{definition}
521:
522: We now show the well-foundedness of $\gtrpo$ by using Tait's
523: method. Computability is defined here as strong normalization,
524: implying computability property (i). We prove the computability
525: property:
526:
527: (vii) Let $f\in\F_n$ and $\vect{s}$ be computable terms.
528: Then $f(\vect{s})$ is computable.
529:
530:
531: \begin{proof}
532: The restriction of $\succ_{rpo}$ to terms smaller than or equal to the
533: terms in $\vect{s}$ w.r.t. $\succ_{rpo}$ is a well-founded ordering
534: which we use for building an outer induction on the pairs
535: $(f,\vect{s})$ ordered by $(>_\F, (\succ_{rpo})_{stat_f})_{lex}$. This
536: ordering is well-founded, since it is built from well-founded
537: orderings by using mappings that preserve well-founded orderings.
538:
539: We now show that $f(\vect{s})$ is computable by proving that $t$ is
540: computable for all $t$ such that $f(\vect{s}) \succ_{rpo} t$. This
541: property is itself proved by an (inner) induction on $|t|$, and by
542: case analysis upon the proof that $f(\vect{s}) \succ_{rpo} t$.
543: \begin{enumerate}
544: \item
545: subterm case: $\exists u\in\vect{s}$ such that $u \succ_{rpo} t$. By assumption,
546: $u$ is computable, hence so is its reduct $t$.
547: \item
548: precedence case: $t=g(\vect{t})$, $f>_\F g$, and $\forall v\in\vect{t}$,
549: $s\succ_{rpo} v$. By inner induction, $v$ is computable, hence
550: so is $\vect{t}$. By outer induction, $g(\vect{t})=t$ is computable.
551: \item
552: multiset case: $t=f(\vect{t})$ with $f\in Mul$, and
553: $\vect{s}(\succ_{rpo})_{mul} \vect{t}$. By definition of the multiset
554: extension, $\forall v\in\vect{t},~\exists u\in\vect{s}$ such that
555: $u\succeq_{rpo} v$. Since $\vect{s}$ is a vector of computable terms
556: by assumption, so is $\vect{t}$. We conclude by outer induction that
557: $f(\vect{t})=t$ is computable.
558: \item
559: lexicographic case: $t=f(\vect{t})$ with $f\in Lex$,
560: $\vect{s}(\succ_{rpo})_{lex} \vect{t}$, and $\forall
561: v\in\vect{t},~s\succ_{rpo} v$. By inner induction, $\vect{t}$ is strongly
562: normalizing, and by outer induction, so is $f(\vect{t})=t$.
563: \qed
564: \end{enumerate}
565: \end{proof}
566:
567: \noindent
568: The well-foundedness of $\gtrpo$ follows from computability property (vii).
569:
570:
571:
572: \section{The General Schema and Computability}
573: \label{s:closure}
574:
575: As in the previous section, we assume that the set of function symbols
576: is equipped with a precedence relation $\geF$ and a status function $stat$.
577:
578: \begin{definition}
579: \label{d:closure}
580: The \emph{computability closure} $\CS(t=f(\vect{t}))$, with $f\!\in\!\F$,
581: is the set $\CS(t,\emptyset)$, s.t. $\CS(t,{\cal V})$, with ${\cal
582: V}\cap\Var{t}=\emptyset$, is the smallest set of typable terms
583: containing all variables in ${\cal V}$ and terms in $\vect{t}$,
584: closed under:
585: \begin{enumerate}
586: \item
587: \label{csubterm}
588: subterm of basic type: let $s\in\CS(t,{\cal V})$, and $u$ be a subterm
589: of $s$ of basic type $\sigma$ such that $\Var{u}\subseteq \Var{t}$;
590: then $u\in\CS(t,{\cal V})$;
591: \item
592: \label{cprecedence}
593: precedence: let $f\gtF g$, and
594: $\vect{s}\in\CS(t,{\cal V})$; then $g(\vect{s})\in\CS(t,{\cal V})$;
595: \item
596: \label{crecursive}
597: recursive call: let $f(\vect{s})$ be a term such that terms in $\vect{s}$
598: belong to $\CS(t,{\cal V})$ and $\vect{t}
599: (\lrps{}{\beta}\cup\gtsubt)_{stat_f} \vect{s}$; then
600: $g(\vect{s})\in\CS(t,{\cal V})$ for every $g =_\F f$;
601: \item
602: \label{capplication}
603: application: let $s :
604: \sigma_1\ra\ldots\ra\sigma_n\ra\sigma\in\CS(t,{\cal V})$ and
605: $u_i:\sigma_i \in\CS(t,{\cal V})$ for every $i\in[1..n]$; then
606: $@(s,u_1,\ldots,u_n)\in\CS(t,{\cal V})$;
607: \item
608: \label{cabstraction}
609: abstraction: let $s\in\CS(t,{\cal V}\cup\{x\})$ for some
610: $x\notin\Var{t}\cup{\cal V}$;
611: then $\lambda x . s \in\CS(t,{\cal V})$;
612: \item
613: \label{creduction}
614: reduction: let $u \in \CS(t,{\cal V})$, and
615: $u\lrps{}{\beta\cup\gtsubt} v$; then $v\in \CS(t,{\cal V})$.
616: \end{enumerate}
617: \end{definition}
618:
619: We say that a rewrite system $R$ satisfies the \emph{general schema} iff
620: $$\mbox{$r\in\CS(f(\vect{l}))$ for all $f(\vect{l})\ra r\in R$}
621: $$
622:
623: We now consider computability with respect to the rewrite relation
624: $\lrps{}{R}\cup\lrps{}{\beta}$, and add the computability property (vii)
625: whose proof can be easily adapted from the previous one.
626: We can then add a new case in Tait's Main Lemma, for terms headed by
627: an algebraic function symbol. As a consequence, the relation
628: $\lrps{}{\beta}\cup\lrps{}{R}$ is strongly normalizing.
629:
630: \begin{example}[System T]
631: \label{recursor}
632: We show the strong normalization of G{\"o}del's system $T$ by showing that
633: its rules satisfy the general schema. This is clear for the first rule
634: by the base Case of the definition. For the second rule, we have:
635: $V\in\CS(rec(s(X),U,V))$ by base Case; $s(X)\in\CS(rec(s(X),U,V))$ by
636: base Case again, and
637: $X\in\CS(rec(s(X),U,V))$ by Case~\ref{cprecedence}, assuming $rec\gtF s$; $U\in\CS(rec(s(X),U,V))$
638: by base Case, hence all arguments of the recursive call are in
639: $\CS(rec(s(X),U,V))$. Since $s(X)\gtsubt X$ holds, we have
640: $rec(X,U,V)\in\CS(rec(s(X),U,V))$. Therefore, we conclude with
641: \mbox{$@(V,X,rec(X,U,V))\in\CS(rec(s(X),U,V))$} by Case~\ref{capplication}.
642: \end{example}
643:
644:
645: \section{The Higher-Order Recursive Path Ordering}
646: \label{s:horpo}
647:
648: \subsection{The Ingredients}
649: \label{ssto}
650:
651: \begin{itemize}
652: \item
653: A quasi-ordering on types $\geS$ called \emph{the type ordering}
654: satisfying the following properties:
655: \begin{enumerate}
656: \item
657: \label{wf}
658: \emph{Well-foundedness}: $\gtS$ is well-founded;
659:
660: \item
661: \label{poa}
662: \emph{Arrow preservation}:
663: $\tau\ra\sigma \eqS \alpha~\mbox{iff}~
664: \alpha=\tau'\ra\sigma',~\tau'\eqS \tau~\mbox{and}~\sigma \eqS \sigma';$
665:
666: \item
667: \label{sa}
668: \emph{Arrow decreasingness}:
669: $\tau\ra\sigma \gtS \alpha ~\mbox{implies}~ \sigma \geS \alpha \mbox{ or }
670: \alpha=\tau'\ra\sigma', \tau'\eqS \tau$ \mbox{ and $\sigma \gtS \sigma'$;}
671:
672: \item
673: \label{ma}
674: \emph{Arrow monotonicity}:
675: $\tau\geS\sigma~\mbox{implies}~ \alpha\ra\tau\geS\alpha\ra\sigma ~\mbox{and}~
676: \tau\ra\alpha\geS\sigma\ra\alpha;$
677: \end{enumerate}
678: A convenient type ordering is obtained by restricting the subterm
679: property for the arrow in the RPO definition.
680:
681: \item
682: A quasi-ordering $\geF$ on ${\cal F}$, called the \emph{precedence},
683: such that $\gtF$ is well-founded.
684:
685: \item
686: A \emph{status} $stat_f\in\{Mul,Lex\}$ for every symbol $f\in\F$.
687: \end{itemize}
688:
689: The higher-order recursive path ordering (HORPO) operates on typing
690: judgments. To ease the reading, we will however forget the
691: environment and type unless necessary. Let
692: \[A=\forall v \in\vect{t}~~
693: s \displaystyle{\gthorpo} v ~\mbox{or}~
694: u \displaystyle{\gthorpo} v
695: ~\mbox{for some}~u\in\vect{s}\]
696:
697: \begin{definition}
698: \label{horpodef}
699: Given two judgments $\Gamma \judgF s: \sigma$ and $\Sigma \judgF t: \tau$,
700: \[
701: s \gthorpo t ~\mbox{iff}~ \sigma \geS \tau ~\mbox{and}
702: \]
703: \begin{enumerate}
704: \item
705: \label{horposubterm}
706: $s=f(\vect{s})$ with $f\in\F$,
707: and
708: $u \displaystyle{\gehorpo} t$ for some
709: $u\in\vect{s}$
710:
711: \item
712: \label{horpoprec}
713: $s=f(\vect{s})$ with $f\in\F$, and
714: $t=g(\vect{t})$ with $f\gtF g$, and $A$
715:
716: \item
717: \label{horpomul}
718: $s=f(\vect{s})$ and $t=g(\vect{t})$ with $f=_\F g\in\Mul$, and
719: $\vect{s}~(\displaystyle{\gthorpo})_{mul}~\vect{t}$
720:
721: \item
722: \label{horpolex}
723: $s=f(\vect{s})$ and $t=g(\vect{t})$ with $f=_\F g\in\Lex$, and
724: $\vect{s}~(\displaystyle{\gthorpo})_{lex}~\vect{t}$ and $A$
725:
726: \item
727: \label{horposubtapp}
728: $s=@(s_1,s_2)$, and $s_1 \displaystyle{\gehorpo} t$
729: or $s_2 \displaystyle{\gehorpo} t$
730:
731: \item
732: \label{horposubtlam}
733: $s=\lambdax:\alpha.u$ with $x\not\in\Var{t}$, and
734: $u \displaystyle{\gehorpo} t$
735:
736: \item
737: \label{horpoprecapp}
738: $s=f(\vect{s})$ with $f\in\F$,
739: $t=@(\vect{t})$ is a partial left-flattening of $t$, and $A$
740:
741: \item
742: \label{horpopreclam}
743: $s=f(\vect{s})$ with $f\in\F$,
744: $t=\lambdax:\alpha.v$ with $x\not\in\Var{v}$ and
745: $s\displaystyle{\gthorpo} v$
746:
747: \item
748: \label{horpoapp}
749: $s=@(s_1,s_2)$, $t=@(\vect{t})$, and $\{s_1, s_2\}
750: (\displaystyle{\gthorpo})_{mul}~ \vect{t}$
751:
752: \item
753: \label{horpolambda}
754: $s=\lambdax:\alpha.u,~t=\lambdax:\beta.v$, $\alpha\eqS\beta$, and
755: $u \displaystyle{\gthorpo} v$
756:
757: \item
758: \label{horpobeta}
759: $s=@(\lambdax:\alpha.u,v)$ and
760: $u\{x\mapsto v\} \displaystyle{\gehorpo} t$
761:
762: \item
763: \label{horpoeta}
764: \label{number}
765: $s=\lambdax:\alpha. @(u,x), ~x\not\in\Var{u}$ and
766: $u \displaystyle{\gehorpo} t$
767: \end{enumerate}
768: \end{definition}
769:
770: \begin{example}[System T]
771: The new proof of strong normalization of System $T$ is even simpler.
772: For the first rule, we apply Case~\ref{horposubterm}. For the second,
773: we apply Case~\ref{horpoprecapp}, and show recursively
774: that $rec(s(X),U,V)\gthorpo V$ by Case~\ref{horposubterm},
775: $rec(s(X),U,V)\gthorpo X$ by Case~\ref{horposubterm} applied twice,
776: and $rec(s(X),U,V)\gthorpo rec(X,U,V)$ by Case~\ref{horpomul},
777: assuming a multiset status for $rec$, which follows from the comparison
778: $s(X)\gthorpo X$ by Case~\ref{horposubterm}.
779: \end{example}
780:
781: The strong normalization proof of HORPO is in the same style as the
782: previous strong normalization proofs, although technically more
783: complex~\cite{jouannaud06jacm}. This proof shows that HORPO and the
784: general schema can be combined by replacing the membership
785: $u\in\vect{s}$ used in case~\ref{horposubterm} by the more general
786: membership $u\in\CS(f(\vect{s}))$. It follows that the HORPO mechanism
787: is inherently more expressive than the closure mechanism.
788:
789: Because of Cases~\ref{horpobeta} and~\ref{horpoeta}, HORPO is not
790: transitive. Indeed, there are examples for which the proof of
791: $s\gthorpo^+ t$ requires guessing a middle term $u$ such that
792: $s\gthorpo u$ and $u\gthorpo t$. Guessing a middle term when necessary
793: is automated in the implementations of HORPO and HORPO with closure
794: available from the web page of the first two authors.
795:
796:
797: \section{Unifying HORPO and the Computability Closure}
798: \label{s:newhorpo}
799:
800: A major advantage of HORPO over the general schema is its recursive
801: structure. In contrast, the membership to the computability closure is
802: undecidable due to its Case~\ref{crecursive}, but does not involve any
803: type comparison. To combine the advantages of both, we now incorporate
804: the closure construction into the HORPO as an ordering. Besides, we
805: also incorporate the property that arguments of a type constructor are
806: computable when the \emph{positivity condition} is satisfied as it is
807: the case for inductive types in the Calculus of Inductive
808: Constructions~\cite{paulin93tlca,blanqui05fi}.
809:
810: \[
811: \begin{array}{lcl}
812: \begin{array}{@{}c@{}}
813:
814: {\displaystyle s: \sigma \gthorpo t: \tau}\quad\mbox{iff}\\
815: \Var{t}\subseteq\Var{s}\quad\mbox{and}\\\\
816:
817: \begin{array}{@{}ll@{}}
818: 1.&
819: s=f(\vect{s}) \mbox{ and } {\displaystyle s\gtchorpoX{\emptyset} t}\\
820:
821: 2.&
822: s=f(\vect{s}) \mbox{ and } \sigma\geS\tau \mbox{ and}\\
823:
824: &\begin{array}{@{}ll@{}}
825:
826: (a)&
827: t=g(\vect{t}),~ f\gtF g \mbox{ and } A\\
828:
829: (b)&
830: t=g(\vect{t}),~ f=_\F g,\\
831: & {\displaystyle \vect{s}(\gthorpo)_{stat_f}\vect{t}} \mbox{ and } A\\
832:
833: (c)&
834: t=@(t_1,t_2) \mbox{ and } A
835: \end{array}\\
836:
837: 3.&
838: s=@(s_1,s_2), \sigma\geS\tau \mbox{ and}\\
839:
840: &\begin{array}{@{}ll@{}}
841: (a)&
842: t=@(t_1,t_2) \mbox{ and}\\
843: & {\displaystyle \{s_1,s_2\} (\gthorpo)_{mul} \{t_1,t_2\}}\\
844:
845: (b)&
846: {\displaystyle s_1\gehorpo t}$ or ${\displaystyle s_2\gehorpo t}\\
847:
848: (c)&
849: s_1=\lambda x.u \mbox{ and}\\
850: &{\displaystyle u\{x\mapsto s_2\}\gehorpo t}
851: \end{array}\\
852:
853: 4.&
854: s=\lambdax:\alpha.u, \sigma\geS\tau \mbox{ and}\\
855: &\begin{array}{ll}
856:
857: (a)&
858: t=\lambdax:\beta.v, \alpha\eqS\beta\\
859: & \mbox{and } {\displaystyle u\gthorpo v}\\
860:
861: (b)&
862: x\not\in\Var{t}$ and ${\displaystyle u\gehorpo t}\\
863:
864: (c)&
865: u=@(v,x), x\not\in\Var{v}\\
866: & \mbox{and } {\displaystyle v\gehorpo t}
867: \end{array}
868: \end{array}\\\\
869:
870:
871: \mbox{where } A=\forall v \in\vect{t}:\\
872: s \displaystyle{\gthorpo} v \mbox{ or }
873: \exists u\in\vect{s}:~u \displaystyle{\gthorpo} v
874: \end{array}
875:
876: &\quad&
877:
878: \begin{array}{@{}c@{}}
879:
880: {\displaystyle s=f(\vect{s})\gtchorpoX{\vect{X}} t}\quad\mbox{iff}\\\\
881:
882: \begin{array}{@{}ll@{}}
883: 1.&
884: t\in\vect{X}\\
885:
886: 2.&
887: \exists s_i\in Acc(s):~ s_i \gechorpoX{\vect{X}} t\\
888:
889: 3.&
890: t=g(\vect{t}),~ f\gtS g \mbox{ and}\\
891: & \forall v\in\vect{t}:~
892: {\displaystyle s\gtchorpoX{\vect{X}}v}\\
893:
894: 4.&
895: t=g(\vect{t}),~ f\eqS g,\\
896: & \forall v\in\vect{t}~:
897: {\displaystyle s\gtchorpoX{\vect{X}}v} \mbox{ and}\\
898: & {\displaystyle Acc(s) (\gthorpo)_{stat_f} \lambda\vect{X}.\vect{t}}\\
899:
900: 5.&
901: t=@(u,v),\\
902: & {\displaystyle s\gtchorpoX{\vect{X}} u} \mbox{ and }
903: {\displaystyle s\gtchorpoX{\vect{X}} v}\\
904:
905: 6.&
906: t=\lambdax:\alpha.u \mbox{ and}\\
907: & {\displaystyle s\gtchorpoX{\vect{X}\cdot\{x:\alpha\}} u}
908: \end{array}\\\\
909:
910: \mbox{where } s_i \in Acc(f(\vect{s}))\\
911: (s_i \mbox{ is accessible in } s)\\
912: \mbox{ iff}\\
913:
914: \begin{array}{@{}ll@{}}
915: 1.&
916: s \mbox{ is the left hand side of}\\
917: & \mbox{an ancestor goal } s\gthorpo u\\
918:
919: 2.&
920: s \mbox{ is the left hand side of the}\\
921: & \mbox{current goal } s\gtchorpoX{} u, \mbox{ and,}\\
922: & \mbox{either} f:\vect{\sigma}\ra\sigma \mbox{ and}\\
923: & \sigma \mbox{ occurs only positively in } \sigma_i.
924: \end{array}
925: \end{array}
926: \end{array}
927: \]
928:
929: \begin{example}
930: \label{ex:brouwer}
931: We consider now the type of Brouwer's ordinals defined from the type
932: $\Nat$ by the equation $Ord=0 \uplus s(Ord) \uplus lim(\Nat\ra
933: Ord)$. Note that $Ord$ occurs positively in the type $\Nat\ra Ord$,
934: and that $\Nat$ must be smaller or equal to $Ord$.
935: The recursor for the type $Ord$ is defined as:
936:
937: \begin{eqnarray*}
938: rec(0,U,V,W) &\ra& U\\
939: rec(s(X),U,V,W) &\ra& @(V,X,rec(X,U,V,W))\\
940: rec(lim(F),U,V,W) &\ra& @(W,F,\lambda n.rec(@(F,n),U,V,W))
941: \end{eqnarray*}
942:
943: \noindent
944: We skip the first two rules and concentrate on the third:
945: \begin{compactenum}
946: \item \label{goal:1}
947: $rec(lim(F),U,V,W) \gthorpo @(W,F,\lambda n.rec(@(F,n),U,V,W))$\\
948: which, by Case~1 of $\gthorpo$ is replaced by the new goal:
949: \item \label{goal:2}
950: $rec(lim(F),U,V,W) \gtchorpoX{\emptyset} @(W,F,\lambda
951: n.rec(@(F,n),U,V,W))$\\
952: By Case~5 of $\gtchorpoX{}$, these three goals become:
953: \item \label{goal:3}
954: $rec(lim(F),U,V,W) \gtchorpoX{\emptyset} W$
955: \item \label{goal:4}
956: $rec(lim(F),U,V,W) \gtchorpoX{\emptyset} F$
957: \item \label{goal:5} $rec(lim(F),U,V,W) \gtchorpoX{\emptyset}
958: \lambda
959: n.rec(@(F,n),U,V,W)$\\
960: Since $rec(lim(F),U,V,W)$ originates from Goal~\ref{goal:1},\\
961: Goal~\ref{goal:3} disappears by Case~2, while
962: Goal~\ref{goal:4} becomes:
963: \item \label{goal:6}
964: $lim(F)\gtchorpoX{\emptyset} F$\\
965: which disappears by the same Case since $F$ is accessible in
966: $lim(F)$.\\
967: thanks to the positivity condition. By Case~6, Goal~\ref{goal:5}
968: becomes:
969: \item \label{goal:7}
970: $rec(lim(F),U,V,W) \gtchorpoX{\{n\}} rec(@(F,n),U,V,W)$\\
971: Case~4 applies with a lexicographic status for $rec$, yielding 5 goals:
972: \item \label{goal:8}
973: $rec(lim(F),U,V,W) \gtchorpoX{\{n\}} @(F,n)$
974: \item \label{goal:9}
975: $rec(lim(F),U,V,W) \gtchorpoX{\{n\}} U$
976: \item \label{goal:10}
977: $rec(lim(F),U,V,W) \gtchorpoX{\{n\}} V$
978: \item \label{goal:11}
979: $rec(lim(F),U,V,W) \gtchorpoX{\{n\}} W$
980: \item \label{goal:12} $\{lim(F),U,V,W\} (\gthorpo)_{lex}
981: \{\lambda n.@(F,n), \lambda n.U, \lambda n.V, \lambda n.W\}$\\
982: Goals~\ref{goal:9}, \ref{goal:10}, \ref{goal:11} disappear by
983: Case~2, while, by Case~5\\
984: Goal~\ref{goal:8} generates (a variation of) the solved
985: Goal~\ref{goal:4} and the new sub-goal:
986: \item \label{goal:13}
987: $rec(lim(F),U,V,W) \gtchorpoX{\{n\}} n$\\
988: which disappears by Case~1. We are left with Goal~\ref{goal:12},
989: which reduces to:
990: \item \label{goal:14}
991: $lim(F) \gthorpo \lambda n.@(F,n)$\\
992: which, by Case~1 of $\gthorpo$, then~6 and~5 of $\gtchorpoX{}$
993: yields successively:
994: \item \label{goal:15}
995: $lim(F) \gtchorpoX{\emptyset} \lambda n.@(F,n)$
996: \item \label{goal:16}
997: $lim(F) \gtchorpoX{\{n\}} @(F,n)$\\
998: which, by Case~5, generates (a variation of) the Goal~\ref{goal:6} and the last goal:
999: \item \label{goal:17}
1000: $lim(F) \gtchorpoX{\{n\}} n$\\
1001: which succeeds by Case~1, ending the computation.
1002: \end{compactenum}
1003: \end{example}
1004:
1005:
1006: To show the strong normalization property of this new definition of
1007: $\horpo$, we need a more sophisticated predicate combining the
1008: predicates used for showing the strong normalization of
1009: HORPO~\cite{jouannaud06jacm} and CAC~\cite{blanqui05mscs}. We have not
1010: done any proof yet, but we believe that it is well-founded.
1011:
1012: It is worth noting that the ordering $\horpo$ defined here is in one
1013: way less powerful than the one defined in Section~\ref{s:horpo} using
1014: the closure definition of Section~\ref{s:closure} because it does not
1015: accumulate computable terms for later use anymore. Instead, it
1016: deconstructs its left hand side as usual with rpo, and remembers very
1017: few computable terms: the accessible ones only. On the other hand, it
1018: is more powerful since the recursive case~4 of the closure uses now
1019: the full power of $\horpo$ for its last comparison instead of simply
1020: $\beta$-reduction (see~\cite{jouannaud06jacm}). Besides, there is no
1021: more type comparison in Case~1 of the definition of $\horpo$, a key
1022: improvement which remains to be justified formally.
1023:
1024:
1025:
1026:
1027:
1028: \section{Related Work}
1029: \label{s:related}
1030:
1031: Termination of higher-order calculi has recently attracted quite a lot
1032: of attention. The area is building up, and mostly, although not
1033: entirely, based on reducibility techniques.
1034:
1035: The case of conditional rewriting has been recently investigated by
1036: Blanqui~\cite{blanqui06lpar}. His results are presented in this
1037: conference.
1038:
1039: Giesl's dependency pairs method has been generalized to higher-order
1040: calculi by using reducibility techniques as described
1041: here~\cite{sakai06,blanqui06hodp}. The potential of this line of work
1042: is probably important, but more work in this direction is needed to
1043: support this claim.
1044:
1045: Giesl~\cite{giesl06rta} has achieved impressive progress for the case of
1046: combinator based calculi, such as Haskell programs, by transforming
1047: all definitions into a first-order framework, and then proving
1048: termination by using first-order tools. Such transformations do not
1049: accept explicit binding constructs, and therefore, do not apply to
1050: rich $\lambda$-calculi such as those considered here. On the other hand,
1051: the relationship of these results with computability deserves investigation.
1052:
1053: An original, interesting work is Jones's analysis of the flux of
1054: redexes in pure lambda-calculus~\cite{jones04rta}, and its use for
1055: proving termination properties of functional programs. Whether this
1056: method can yield a direct proof of finite developments in pure
1057: $\lambda$-calculus should be investigated. We also believe that his
1058: method can be incorporated to the HORPO by using an interpretation on
1059: terms instead of a type comparison, as mentioned in Conclusion.
1060:
1061: Byron Cook, Andreas Podelski and Andrey Ribalchenko~\cite{podelski}
1062: have developed a quite different and impressive method based on
1063: abstract interpretations to show termination of large imperative
1064: programs. Their claim is that large programs are more likely to be
1065: shown terminating by approximating them before to make an
1066: analysis. Note that the use of a well-founded ordering can be seen as
1067: a particular analysis. Although impressive, this work is indeed quite
1068: far from our objectives.
1069:
1070:
1071:
1072: \section{Conclusion}
1073: \label{s:conclusion}
1074:
1075:
1076: We give here a list of open problems which we consider important. We
1077: are ourselves working on some of these. The higher-order recursive
1078: path ordering should be seen as a firm step to undergo further
1079: developments in different directions, some of which are listed below.
1080: \begin{itemize}
1081: \item Two of them have been investigated in the first order framework:
1082: the case of associative commutative operators, and the use of
1083: interpretations as a sort of elaborated precedence operating on
1084: function symbols. The first extension has been carried out for the
1085: general schema~\cite{blanqui03rta}, and the second for a weak form
1086: of HORPO~\cite{rubio01}. Both should have an important impact for
1087: applications, hence deserve immediate attention.
1088: \item Enriching the type system with dependent types, a problem
1089: considered by Wa\-{\l}u\-kie\-wicz~\cite{walukiewicz00lfm} for the
1090: original version of HORPO in which types were compared by a
1091: congruence. Replacing the congruence by HORPO recursively called on
1092: types as done in~\cite{jouannaud06jacm} for a simpler type
1093: discipline raises technical difficulties. The ultimate goal here is
1094: to generalize the most recent versions of the ordering including the
1095: present one, for applications to the Calculus of Inductive
1096: Constructions.
1097: \item HORPO does not contain and is not a well-order for the subterm
1098: relationship. However, its definition shows that it satisfies a weak
1099: subterm property, namely property $A$. It would be theoretically
1100: interesting to investigate whether some Kruskal-like theorem holds
1101: for higher-order terms with respect to the weak subterm property.
1102: This could yield an alternative, more abstract way of hiding away
1103: computability arguments.
1104: \end{itemize}
1105:
1106:
1107:
1108: \begin{thebibliography}{10}
1109:
1110: \bibitem{barbanera90}
1111: F.~Barbanera.
1112: \newblock Adding algebraic rewriting to the calculus of constructions: Strong
1113: normalization preserved.
1114: \newblock In \emph{Proc. 2nd Int. Workshop on Conditional and Typed Rewriting
1115: Systems, Montreal, LNCS 516}, 1990.
1116:
1117: \bibitem{barbanera94lics}
1118: F.~Barbanera, M.~Fern{\'a}ndez, and H.~Geuvers.
1119: \newblock Modularity of strong normalization and confluence in the
1120: $\lambda$-algebraic-cube.
1121: \newblock In \emph{Proc. 9th IEEE Symp. Logic in Computer Science}, pages
1122: 406--415, 1994.
1123:
1124: \bibitem{blanqui99rta}
1125: F.~Blanqui, J.-P. Jouannaud, and M.~Okada.
1126: \newblock The {C}alculus of {A}lgebraic {C}onstructions.
1127: \newblock In Paliath Narendran and Michael Rusinowitch, editors, \emph{10th
1128: International Conference on Rewriting Techniques and Applications}, volume
1129: 1631 of \emph{Lecture Notes in Computer Science}, Trento, Italy, July 1999.
1130: Springer Verlag.
1131:
1132: \bibitem{blanqui02tcs}
1133: F.~Blanqui, J.-P. Jouannaud, and M.~Okada.
1134: \newblock Inductive-{D}ata-{T}ype {S}ystems.
1135: \newblock \emph{Theoretical Computer Science}, 272(1-2):41--68, 2002.
1136:
1137: \bibitem{blanqui03rta}
1138: F.~Blanqui.
1139: \newblock Rewriting modulo in {D}eduction modulo.
1140: \newblock In \emph{Proc. of the 14th International Conference on Rewriting
1141: Techniques and Applications}, volume 2706 of \emph{LNCS}, 2003.
1142:
1143: \bibitem{blanqui05mscs}
1144: F.~Blanqui.
1145: \newblock Definitions by rewriting in the {C}alculus of {C}onstructions.
1146: \newblock {\em Mathematical Structures in Computer Science}, 15(1):37--92,
1147: 2005.
1148:
1149: \bibitem{blanqui05fi}
1150: F.~Blanqui.
1151: \newblock Inductive types in the {C}alculus of {A}lgebraic {C}onstructions.
1152: \newblock {\em Fundamenta Informaticae}, 65(1-2):61--86, 2005.
1153:
1154: \bibitem{blanqui06lpar}
1155: F.~Blanqui and C.~Riba.
1156: \newblock Combining typing and size constraints for checking termination of
1157: higher-order conditional rewriting systems.
1158: \newblock In \emph{Proc. LPAR, to appear in LNAI}, LNCS, 2006.
1159:
1160: \bibitem{blanqui06horpo}
1161: F.~Blanqui.
1162: \newblock {(HO)RPO} revisited, 2006.
1163: \newblock Manuscript.
1164:
1165: \bibitem{blanqui06hodp}
1166: F.~Blanqui.
1167: \newblock Higher-order dependency pairs.
1168: \newblock In {\em Proceedings of the 8th International Workshop on Termination,
1169: 2006}.
1170:
1171: \bibitem{rubio01}
1172: Cristina Borralleras and Albert Rubio.
1173: \newblock A monotonic, higher-order semantic path ordering.
1174: \newblock In \emph{Proceedings LPAR}, Lecture Notes in Computer Science.
1175: Springer Verlag, 2006.
1176:
1177: \bibitem{BTG90}
1178: Val Breazu-Tannen and Jean Gallier.
1179: \newblock Polymorphic rewriting conserves algebraic strong normalization.
1180: \newblock \emph{Theoretical Computer Science}, 1990.
1181:
1182: \bibitem{podelski}
1183: Andreas~Podelski Byron~Cook and Andrey Rybalchenko.
1184: \newblock Termination proofs for systems code, 2004.
1185: \newblock Manuscript.
1186:
1187: \bibitem{coq8.0}
1188: {Coq Development Team}.
1189: \newblock {\em The {C}oq Proof Assistant Reference Manual, Version 8.0}.
1190: \newblock INRIA Rocquencourt, France, 2004.
1191: \newblock \url{http://coq.inria.fr/}.
1192:
1193: \bibitem{dershowitz88}
1194: Nachum Dershowitz and Jean-Pierre Jouannaud.
1195: \newblock Rewrite systems.
1196: \newblock In J.~van Leeuwen, editor, \emph{Handbook of Theoretical Computer
1197: Science}, volume~B, pages 243--309. North Holland, 1990.
1198:
1199: \bibitem{jones04rta}
1200: Neil Jones and Nina Bohr.
1201: \newblock Termination analysis of the untyped $\lambda$-calculus.
1202: \newblock In \emph{Rewriting techniques and Applications}, pages 1--23. Springer
1203: Verlag, 2004.
1204: \newblock LNCS 3091.
1205:
1206: \bibitem{jouannaud91lics}
1207: Jean-Pierre Jouannaud and Mitsuhiro Okada.
1208: \newblock Executable higher-order algebraic specification languages.
1209: \newblock In \emph{Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam},
1210: pages 350--361, 1991.
1211:
1212: \bibitem{jouannaud97tcs}
1213: Jean-Pierre Jouannaud and Mitsuhiro Okada.
1214: \newblock Abstract data type systems.
1215: \newblock \emph{Theoretical Computer Science}, 173(2):349--391, February 1997.
1216:
1217: \bibitem{jouannaud99lics}
1218: Jean-Pierre Jouannaud and Albert Rubio.
1219: \newblock The higher-order recursive path ordering.
1220: \newblock In Giuseppe Longo, editor, \emph{Fourteenth Annual {IEEE} Symposium on
1221: Logic in Computer Science}, Trento, Italy, July 1999.
1222:
1223: \bibitem{jouannaud06rta}
1224: Jean-Pierre Jouannaud and Albert Rubio.
1225: \newblock Higher-order orderings for normal rewriting.
1226: \newblock In \emph{Proc. 17th International Conference on Rewriting Techniques
1227: and Applications, Seattle, Washington, USA}, 2006.
1228:
1229: \bibitem{jouannaud06jacm}
1230: Jean-Pierre Jouannaud and Albert Rubio.
1231: \newblock Polymorphic higher-order recursive path orderings.
1232: \newblock \emph{Journal of the ACM}, submitted.
1233:
1234: \bibitem{giesl06rta}
1235: Peter Scneider-Kamp J{\"u}rgen~Giesl, Stephan~Swiderski and Ren{\'e} Thiemann.
1236: \newblock Automated termination analysis for haskell: Form term rewriting to
1237: programming languages.
1238: \newblock In \emph{Rewriting techniques and Applications}, pages 297--312.
1239: Springer Verlag, 2006.
1240: \newblock LNCS 4098.
1241:
1242: \bibitem{okada89issac}
1243: Mitsuhiro Okada.
1244: \newblock Strong normalizability for the combined system of the typed lambda
1245: calculus and an arbitrary convergent term rewrite system.
1246: \newblock In \emph{Proc. of the 20th Int. Symp. on Symbolic and Algebraic
1247: Computation, Portland, Oregon, USA}, 1989.
1248:
1249: \bibitem{paulin93tlca}
1250: Christine Paulin-Mohring.
1251: \newblock Inductive definitions in the system {COQ}.
1252: \newblock In \emph{Typed Lambda Calculi and Applications}, pages 328--345.
1253: Springer Verlag, 1993.
1254: \newblock LNCS 664.
1255:
1256: \bibitem{sakai06}
1257: Masahiko Sakai and Keiichirou Kusakari.
1258: \newblock On dependency pairs method for proving termination of higher-order
1259: rewrite systems.
1260: \newblock \emph{IEICE-Transactions on Information and Systems}, E88-D
1261: (3):583--593, 2005.
1262:
1263: \bibitem{walukiewicz00lfm}
1264: Daria Wa{\l}ukiewicz-Chrzaszcz.
1265: \newblock Termination of rewriting in the {C}alculus of {C}onstructions.
1266: \newblock In \emph{Proceedings of the Workshop on Logical Frameworks and
1267: Meta-languages, {S}anta {B}arbara, {C}alifornia}, 2000.
1268: \newblock Satellite workshop of LICS'2000.
1269:
1270: \end{thebibliography}
1271:
1272: \end{document}
1273:
1274: