1: % Document Type: LaTeX
2:
3: \documentclass[hyperref]{acmtrans2e}
4: %\usepackage[pdfmark]{hyperref}
5:
6:
7: %\newdisplay{guess}{Conjecture}
8:
9: %% mes packages utilises dans le .llncs
10: \usepackage[all]{xy}
11: \usepackage{amssymb,alltt}
12: %\pagestyle{plain}
13:
14:
15:
16: \newcommand{\HK}[1]{\textbf{[?}~#1~\textbf{?]}}
17:
18: \newcommand{\OUT}[1]{\ignorespaces}
19:
20:
21: \newcommand{\TXF}{{\cal T}({\cal F},{\cal X})}
22: \newcommand{\TFN}{{\cal T}({\cal F},{\cal N})}
23: \newcommand{\TFXA}{{\cal T}({\cal F},{\cal X}_A)}
24: \newcommand{\TFXN}{{\cal T}({\cal F},{\cal X \cup \cal N})}
25: \newcommand{\TFXXA}{{\cal T}({\cal F},{\cal X} \cup {\cal X}_A)}
26:
27: \newcommand{\TF}{{\cal T}({\cal F})}
28: \newcommand{\XA}{{\cal X}_A}
29: \newcommand{\C}{{\cal C}}
30: \newcommand{\R}{{\cal R}}
31: \newcommand{\U}{{\cal U}}
32: \newcommand{\OC}{{\cal O}}
33:
34: \newcommand{\OS}{{\overline{\cal O}}}
35: \newcommand{\F}{{\cal F}}
36: \newcommand{\X}{{\cal X}}
37: \newcommand{\N}{{\cal N}}
38: \newcommand{\ra}{\rightarrow}
39: %\newcommand{\longra}{\longrightarrow}
40: \newcommand{\Longra}{\Longrightarrow}
41: \newcommand{\da}{\mathord{\downarrow}}
42: \newcommand{\rain}{\stackrel{in}{\longrightarrow}_{R}^{*}}
43: \newcommand{\rip}{\stackrel{in}{\longrightarrow}_{R}^{+}}
44: \newcommand{\surred}{\leadsto}
45:
46: \newcommand{\narrow}{\leadsto}
47: \newcommand{\con}{\da =}
48: \newcommand{\longra}[1]{\stackrel{#1}{\longrightarrow}}
49: \newcommand{\red}{\twoheadrightarrow^*}
50: \newcommand{\sur}{/}
51:
52:
53: \newcommand{\Pos}{{\cal P}{\it os}}
54: \newcommand{\Var}{{\cal V}{\it ar}}
55: \newcommand{\Root}{{\cal R}{\it oot}}
56: \newcommand{\Cons}{{\cal C}{\it ons}}
57: \newcommand{\Def}{{\cal D}{\it ef}}
58: \newcommand{\om}{{\it outermost }}
59:
60: \newcommand{\ttree}[2]{#1} % textual tree
61: \newcommand{\gtree}[2]{#2} % graphical tree
62: \newcommand{\comment}[1]{}
63:
64:
65: % INFERENCE RULES
66:
67: \newcommand{\rname}[1]{\mbox{$\bf #1$}} % rule name
68:
69: \newcommand{\HSpace}{\hspace{1em}}
70: \newlength{\Labelwidth}\setlength{\Labelwidth}{5em} % was 5em
71: \newcommand{\ainfr}[2]
72: {\makebox[\Labelwidth][l]{\bf #1:}\
73: \(\displaystyle {#2}\)}
74: \newcommand{\infr}[3]
75: {\makebox[\Labelwidth][l]{\bf #1:}\
76: \(\displaystyle {#2} \over \displaystyle {#3}\)}
77: \newcommand{\acinfr}[3]
78: {\makebox[\Labelwidth][l]{\bf #1:}\
79: \(\displaystyle {#2} \)\(~~{\rm if}\;{#3}\)}
80: \newcommand{\cinfr}[4]
81: {\makebox[\Labelwidth][l]{\bf #1:}\
82: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
83: \(\displaystyle ~~{\rm if}\;{#4}\)}
84: \newcommand{\wcinfr}[5]
85: {\makebox[\Labelwidth][l]{\bf #1:}\
86: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
87: \(\displaystyle {#4}\) \\[1mm]
88: \(\displaystyle {#5}\)}
89: \newcommand{\owcinfr}[4]
90: {\makebox[\Labelwidth][l]{\bf #1:}\
91: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
92: \(\displaystyle {#4}\)}
93: \newcommand{\dubblewcinfr}[6]
94: {\makebox[\Labelwidth][l]{\bf #1:}\
95: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
96: \(\displaystyle {#4}\) \\[1mm]
97: \(\displaystyle {#5}\) \\[1mm]
98: \(\displaystyle {#6}\)}
99:
100: \newcommand{\triplewcinfr}[7]
101: {\makebox[\Labelwidth][l]{\bf #1:}\
102: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
103: \(\displaystyle {#4}\) \\[1mm]
104: \(\displaystyle {#5}\) \\[1mm]
105: \(\displaystyle {#6}\) \\[1mm]
106: \(\displaystyle {#7}\)}
107:
108: \newcommand{\fivecinfr}[8]
109: {\makebox[\Labelwidth][l]{\bf #1:}\
110: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
111: \(\displaystyle {#4}\) \\[1mm]
112: \(\displaystyle {#5}\) \\[1mm]
113: \(\displaystyle {#6}\) \\[1mm]
114: \(\displaystyle {#7}\) \\[1mm]
115: \(\displaystyle {#8}\)}
116:
117: \newcommand{\sixcinfr}[9]
118: {\makebox[\Labelwidth][l]{\bf #1:}\
119: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
120: \(\displaystyle {#4}\) \\[1mm]
121: \(\displaystyle {#5}\) \\[1mm]
122: \(\displaystyle {#6}\) \\[1mm]
123: \(\displaystyle {#7}\) \\[1mm]
124: \(\displaystyle {#8}\) \\[1mm]
125: \(\displaystyle {#9}\)}
126:
127:
128: \newcommand{\longcinfr}[4]
129: {\makebox[\Labelwidth][1]{\bf #1:}\
130: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
131: \(\displaystyle ~~{\rm if}\;{#4}\)}
132:
133: \newcommand{\bcinfr}[4]
134: {\makebox[\Labelwidth][l]{\bf #1:}\
135: \(\displaystyle {#2} \over \displaystyle {#3}\)\(~~{\rm
136: if}\;{#4}\)}
137:
138: \newcommand{\dubblecinfr}[5]
139: {\makebox[\Labelwidth][l]{\bf #1:}\
140: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
141: \(\displaystyle ~~{\rm if}\;{#4}\) \\[1mm]
142: \(\displaystyle {#5}\)}
143:
144: \newcommand{\memelignedubblecinfr}[5]
145: {\makebox[\Labelwidth][l]{\bf #1:}\
146: \(\displaystyle {#2} \over \displaystyle {#3}\)
147: \(\displaystyle ~~{\rm if}\;{#4}\) \\[1mm]
148: \(\displaystyle {#5}\)}
149:
150: \newcommand{\triplecinfr}[6]
151: {\makebox[\Labelwidth][l]{\bf #1:}\
152: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
153: \(\displaystyle ~~{\rm if}\;{#4}\) \\[1mm]
154: \(\displaystyle {#5}\) \\[1mm]
155: \(\displaystyle {#6}\)}
156:
157: \newcommand{\quadruplecinfr}[7]
158: {\makebox[\Labelwidth][l]{\bf #1:}\
159: \(\displaystyle {#2} \over \displaystyle {#3}\) \\[3mm]
160: \(\displaystyle ~~{\rm if}\;{#4}\) \\[1mm]
161: \(\displaystyle {#5}\) \\[1mm]
162: \(\displaystyle {#6}\) \\[1mm]
163: \(\displaystyle {#7}\)
164: }
165:
166: \newcommand{\triifline}[4]
167: {\makebox[\Labelwidth][l]{\bf #1:}\
168: \(\displaystyle {#2} \over \displaystyle {#3}\)
169: \(\displaystyle ~~~~~~{\rm if}\;{#4}\)}
170:
171:
172: % THEOREMS
173: \newtheorem{lemma}{Lemma}[section]
174: \newtheorem{sublemma}{Lemma}[subsection]
175: \newtheorem{proposition}{Proposition}[section]
176: \newtheorem{subproposition}{Proposition}[subsection]
177: \newtheorem{theorem}{Theorem}[section]
178: \newtheorem{subtheorem}{Theorem}[subsection]
179: \newdef{definition}[theorem]{Definition}
180: \newdef{subdefinition}[subtheorem]{Definition}
181: \newdef{example}[theorem]{Example}
182: \newdef{subexample}[subtheorem]{Example}
183:
184:
185: %---------------------------ACM
186: \newcommand{\BibTeX}{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
187: T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}
188:
189: \firstfoot{ACM Transactions on Computational Logic,
190: Vol.\ X, No.\ X, Date XXXX, Pages xxx-xxx.}
191:
192: \runningfoot{ACM Transactions on Computational Logic,
193: Vol.\ X, No.\ X, Date XXXX.}
194:
195: \markboth{Isabelle Gnaedig and H\'el\`ene Kirchner}{Termination of rewriting strategies: a generic approach}
196:
197: \title{Termination of rewriting strategies:
198: a generic approach}
199: \author{ISABELLE GNAEDIG\\Loria-INRIA
200: \and
201: HELENE KIRCHNER\\Loria-CNRS}
202: \begin{abstract}
203: We propose a generic termination proof method for rewriting under strategies,
204: based on an explicit induction on the termination property.
205: Rewriting trees on ground terms are modeled by proof trees, generated by
206: alternatively applying narrowing and abstracting steps.
207: The induction principle is applied through the abstraction mechanism,
208: where terms are replaced by variables representing any
209: of their normal forms.
210: The induction ordering is not given a priori, but defined with ordering constraints,
211: incrementally set during the proof. Abstraction constraints can be used to control
212: the narrowing mechanism, well known to easily diverge.
213: The generic method is then instantiated for the innermost, outermost and
214: local strategies.
215: \end{abstract}
216:
217:
218: %--------------------Les fameuses categories ACM !----------------------------------------------
219:
220: \category{F.3.1}{LOGICS AND MEANINGS OF PROGRAMS}{Specifying and Verifying and Reasoning about Programs}
221: [Logics of programs, Mechanical verification, Specification
222: techniques]
223:
224: \category{F.4.2}{MATHEMATICAL LOGIC AND FORMAL LANGUAGES}{Grammars and Other Rewriting Systems}
225:
226: \category{F.4.3}{MATHEMATICAL LOGIC AND FORMAL LANGUAGES}{Formal
227: Languages}
228: [Algebraic language theory]
229:
230: \category{I.1.3}{SYMBOLIC AND ALGEBRAIC MANIPULATION}{Languages and
231: Systems}
232: [Evaluation stra\-tegies, Substitution mechanisms]
233:
234: \category{I.2.2}{ARTIFICIAL INTELLIGENCE}{Automatic Programming}
235: [Automatic analysis of algorithms, Program verification]
236:
237: \category{I.2.3}{ARTIFICIAL INTELLIGENCE}{Deduction and Theorem Proving}
238: [Deduction, Inference engines, Mathematical induction]
239:
240: \category{D.3.1}{PROGRAMMING LANGUAGES}{Formal Definitions and Theory}
241:
242: \category{D.2.4}{SOFTWARE ENGINEERING}{Software/Program
243: Verification}[Correctness proofs, Formal methods, Validation]
244:
245: %--------------------------------------------------------------------------------------------
246:
247:
248: \terms{Algorithms, Languages, Verification}
249:
250: \keywords{abstraction, innermost, local strategy, narrowing,
251: ordering constraint, outermost, termination}
252:
253: \begin{document}
254:
255: \setcounter{page}{1}
256:
257: \begin{bottomstuff}
258: Author's address: Isabelle Gnaedig, H\'el\`ene
259: Kirchner,
260: LORIA, 615, rue du Jardin Botanique, BP 101, F-54602 Villers-l\`es Nancy
261: Cedex ,
262: Fax: + 33 3 83 27 83 19 \\
263: {\tt e-mail:~Isabelle.Gnaedig@loria.fr,Helene.Kirchner@loria.fr}
264: \permission
265: \copyright\ 2005 ACM ... \$00.75
266: \end{bottomstuff}
267: \maketitle
268:
269: \bibliographystyle{acmtrans}
270:
271:
272:
273:
274: \section{Introducing the problem}
275: %OUTERMOST/out-inn.tex
276:
277: Rewriting techniques are now widely used in automated deduction,
278: especially to handle equality, as well as in programming, in
279: functional, logical or rule-based languages.
280: Termination of rewriting is a crucial property, important in itself
281: to guarantee a result in a finite number of steps, but it is also
282: required to decide properties like confluence and sufficient
283: completeness, or to allow proofs by
284: consistency. Existing methods for proving termination of
285: rewrite systems essentially tackle the
286: termination problem on free term algebras for rewriting without strategies.
287:
288: Most are based on
289: syntactic or semantic noetherian orderings containing the rewriting
290: relation induced by the
291: rewrite system~\cite{Plaisted-well-founded-78,Lankford-79,Kamin-Levy,DershowitzTCS-1982,Cherifa-Lescanne-SCP87,Dershowitz-Hoot-1995,BorFerRubio-SPO-CADE-2000}.
292: Other methods consist in transforming the termination problem of a rewrite system
293: into the decreasingness problem of another rewrite system or of pairs of terms,
294: then handled with
295: techniques of the previous category. Examples are
296: semantic labelling \cite{Zantema-1995}, and the dependency pair
297: method~\cite{Arts-Giesl-TCS-2000,Giesl-Thi-all-improvingDP-2003}. For most approaches, finding an
298: appropriate ordering is the key problem, that often comes down
299: to solving a set of ordering constraints.
300: %Automating theseS
301: %termination proof techniques then requires ordering
302: %constraint solving, which remains difficult and costly, despite the
303: %existence of some efficient
304: %solvers~\cite{Giesl-RTA95,Contejean-Marche-2000}.
305:
306:
307: In the context of proof environments for rule-based programming
308: languages, such as ASF+SDF \cite{Klint-ACM93},
309: Maude~\cite{Maude-RwLg1996}, Cafe\-OBJ~\cite{FutatsugiN-IEEE97},
310: ELAN~\cite{BorovanskyKKMR-WRLA98}, or TOM~\cite{MoreauRV-2003},
311: where a program is a rewrite system
312: and the evaluation of a query consists in rewriting a ground
313: expression, more specific termination proof tools are required, to
314: allow termination proofs on ground terms, and
315: under specific reduction strategies. There
316: are still few results in this domain. To our knowledge, methods have
317: only been given on the free term algebra with the innermost
318: strategy~\cite{Arts-Giesl-inner-tech-96,Giesl-Mid-inn-context-sens-2003}
319: and for the context-sensitive
320: rewriting~\cite{LucasIC02}, which involves particular kinds of local
321: strategies~\cite{Luc01}. In previous works, we already have obtained
322: termination results on ground terms for the innermost
323: strategy~\cite{GKF-in-out-2001,FGK-PPDP-2002}, for general local
324: strategies on the operators~\cite{FGK-local-strat-ENTCS-2001}, and for
325: the outermost strategy~\cite{FGK-WRLA-2002}.
326:
327:
328: In this paper, we propose a generic proof principle, based on an
329: explicit induction mechanism on the termination property, which is
330: a generalization of our three previous results.
331: We then show how it can be instantiated to give an effective
332: termination proof algorithm for the innermost strategy, the outermost
333: strategy, and local strategies on operators.
334: This generalizing work allowed not only to propose a generic version
335: of our proof method, but also to considerably simplify the technical
336: features of the algorithms initially designed for the different strategies.
337:
338: The three above strategies have been chosen for their
339: relevance to programming languages.
340: The most widely used innermost strategy consists in rewriting always
341: at the lowest possible positions. It is often used as a built-in
342: mechanism in evaluation of rule-based or functional languages. In
343: addition, for non-overlapping or locally confluent overlay systems
344: \cite{Gramlich-FI96}, or systems satisfying critical peak conditions
345: \cite{Gramlich-RTA96}, innermost termination is equivalent to standard
346: termination (i.e. termination for standard rewriting, which consists
347: in rewriting without any strategy). As proved in
348: \cite{Rao-innermost-TCS-2000}, termination of rewriting is equivalent
349: for the leftmost innermost and the innermost strategies.
350:
351: The outermost strategy for evaluating expressions in the context of
352: programming is essentially used when one knows that computations can
353: be non-terminating. The intuition suggests that rewriting a term at
354: the highest possible position gives more chance than with another
355: strategy to lead to an irreducible form. Indeed, outermost rewriting
356: may succeed when innermost fails, as illustrated by the expression
357: $\mathit{second}(\mathit{dec}(1), 0)$, with the rewrite rules
358: $\mathit{second}(x,y) \ra y$ and
359: $\mathit{dec}(x) \ra \mathit{dec}(x-1)$ on integers. Innermost rewriting fails to
360: terminate, because it first evaluates $\mathit{dec}(1)$ into $\mathit{dec}(0)$,
361: $\mathit{dec}(-1)$, and so on. Outermost rewriting, however, gives $0$ in one
362: rewriting step. Moreover, outermost derivations are often shorter~:
363: in our example, to reduce $\mathit{second}(u,v)$, one does not need to reduce
364: $u$, which can lead to infinite computations or, at least, to a
365: useless evaluation. This advantage makes the outermost strategy an
366: interesting strategy for rule-based languages, by allowing the
367: interpreters to be more efficient, as well as for theorem proving, by
368: allowing the rewriting-based proofs to be shorter.
369:
370:
371: Outermost computations are of interest in particular for functional
372: languages,
373: %like Miranda, Haskell, or Clean,
374: where interpreters or compilers generally involve a strategy for call
375: by name. Often, lazy evaluation is used instead: operators are
376: labelled in terms as lazy or eager, and the strategy consists in
377: reducing the eager subterms only when their reduction allows a
378: reduction step higher in the term~\cite{NG01a}. However, lazy
379: evaluation may diverge while the outermost computation terminates,
380: which gives an additional motivation for studying outermost
381: termination. For instance, let us consider the evaluation of the
382: expression $\mathit{inf}(0)$ with the following two rules~:
383: $\mathit{cons}(x,\mathit{cons}(y,z))
384: \ra \mathit{big}, \; \; \mathit{inf}(x) \ra \mathit{cons}(x, \mathit{inf}(s(x)))$.
385: If $\mathit{inf}$ is
386: labelled as eager, $\mathit{inf}(0)$ is reduced to
387: $\mathit{cons}(0, \mathit{inf}(s(0)))$, and
388: then, since application of the first rule fails, the sub-expression
389: $\mathit{inf}(s(0))$ has to be evaluated before considering the whole
390: expression, which leads to an infinite evaluation. Evaluated in an
391: outermost manner, $\mathit{inf}(0)$ is also reduced to
392: $\mathit{cons}(0, \mathit{inf}(s(0)))$,
393: but then $\mathit{inf}(s(0))$ is reduced to $\mathit{cons}(s(0), \mathit{inf}(s(s(0))))$,
394: and the
395: whole expression is reduced to $\mathit{big}$. Lazy termination of functional
396: languages has already been studied (see for
397: example~\cite{Panitz-Schmidt-Schauss-1997}), but to our knowledge,
398: except our previously cited work, no
399: termination proof method exists for specifically proving outermost
400: termination of rewriting.
401:
402: Local strategies on operators are used
403: in particular to force the evaluation of expressions
404: to terminate. A famous example is the evaluation of a recursive function
405: defined with an $\mathit{if\_then\_else}$ expression, for which evaluating the
406: first argument in priority may allow to avoid divergence.
407:
408: This kind of strategy is allowed by languages such that
409: OBJ3, Cafe\-OBJ or Maude, and studied
410: in~\cite{Eker98} and~\cite{Nakamura-Ogata-2000}.
411: It is defined
412: in the following way:
413: to any operator $f$ is attached an ordered list
414: of integers, giving the positions of the subterms to be
415: evaluated in a given term, whose top operator is $f$. For example, the
416: rewrite system
417:
418: {\footnotesize
419: \[
420: \begin{array}{ll}
421: f(i(x)) & \ra if\_then\_else(zero(x),g(x),f(h(x)))\\
422: zero(0) & \ra true\\
423: zero(s(x)) & \ra false\\
424: if\_then\_else(true,x,y) & \ra x\\
425: if\_then\_else(false,x,y) & \ra y\\
426: h(0) & \ra i(0)\\
427: h(x) & \ra s(i(x))
428: \end{array}
429: \]
430: }
431: \noindent
432: using the conditional expression,
433: does not terminate for the standard rewriting relation, but does with
434: the following strategy:
435: $\mathit{LS}(\mathit{ite}) = [1 ; 0]$, $\mathit{LS}(f) = \mathit{LS}(\mathit{zero}) =$
436: $\mathit{LS}(h) = [1 ; 0]$ and
437: $\mathit{LS}(g) = \mathit{LS}(i) = [1]$, where $\mathit{ite}$ denotes
438: $\mathit{if\_then\_else}$ for short.
439:
440: Local strategies have to be compared with context-sensitive rewriting,
441: where rewriting is also allowed at some specified positions only in
442: the terms: as local strategies specify in addition an ordering on these
443: rewriting positions, they are more specific.
444:
445: The termination problem for these various strategies is always
446: different: in~\cite{FGK-out-interne-2002}, the interested reader can
447: find examples showing that termination for one of these strategies
448: does not imply termination for any other of them. A better knowledge
449: of these differences would be interesting, and could help to choose the good
450: one when programming in these languages.
451:
452: %------------------------------------------------------------------------
453:
454: Despite of these distinct behaviours, the termination proofs we
455: propose rely on
456: a generic principle and a few common concepts, that are emphasized in
457: this paper.
458: Our approach
459: is based on an explicit induction mechanism on the termination
460: property. The main idea is to proceed by induction on the ground term
461: algebra with a noetherian ordering
462: $\succ$, assuming that for any $t'$ such that $t \succ t'$,
463: $t'$
464: terminates, i.e. there is no infinite derivation
465: chain starting from $t'$.
466: The general proof principle relies on the simple idea that
467: for establishing termination of a ground term $t$, it
468: is enough to suppose that subterms of $t$ are smaller than $t$ for
469: this ordering, and that rewriting the context only leads to
470: terminating chains. Iterating this process until a non-reducible context
471: is obtained establishes termination
472: of $t$.
473:
474: Unlike classical induction
475: proofs, where the ordering is given, we do not need to define it {\em
476: a priori}. We only have to check its existence by ensuring
477: satisfiability of ordering constraints incrementally set along the
478: termination proof.
479: Thanks to the power of induction, the generated constraints are often simpler
480: to solve than for other approaches, and even, in many cases, do not need any
481: constraint solving algorithm.
482:
483: Directly using the termination notion on terms has also been proposed
484: in~\cite{Goubault-Larrecq-well-found-2001},
485: but for inductively proving well-founded\-ness of
486: binary relations, among which path orderings.
487:
488: In order to explain the basic idea of this work, let us consider
489: the classical example, due to Toyama, of a rewrite system
490: that does not terminate, but terminates with the innermost strategy:
491:
492: {\footnotesize
493: \[
494: \begin{array}{ll}
495: f(0,1,x) & \ra f(x,x,x) \\
496: g(x,y) & \ra x\\
497: g(x,y) & \ra y
498: \end{array}
499: \]
500: }
501: \noindent
502:
503: Let us prove by induction on the set $\TF$ of ground terms
504: built on ${\cal F}=\{0,1,f,g\}$
505: with a noetherian
506: ordering $\succ$, that any term
507: $t$ innermost terminates (i.e. there is no infinite innermost rewriting
508: chain starting from $t$). The terms of
509: $\mathit{\TF}$ are $0$, $1$, or terms of the form
510: $f(t_1,t_2,t_3)$, or
511: $g(t_1,t_2)$, with $t_1,t_2,t_3 \; \in \TF$. The terms
512: $0$ and $1$
513: are obviously terminating.
514:
515: Let us now prove that $f(t_1,t_2,t_3)$ is innermost terminating.
516: First, $f(t_1,t_2,t_3) \succ$ $t_1, t_2, t_3$ for any term ordering with
517: the subterm property (i.e. any term is greater than any of its subterms).
518: Then, by induction
519: hypothesis, assume that $t_1, t_2$ and $t_3$ innermost terminate. Let
520: $t_1\da, t_2\da, t_3\da$ be respectively any of their normal forms.
521: The problem is then reduced to innermost termination of all
522: $f(t_1\da, t_2\da, t_3\da)$.
523: If $t_1\da = 0 \; ,\; t_2\da = 1$, then $f(0,1, t_3\da)$
524: only rewrites at the top position into $f(t_3\da, t_3\da,$ $t_3\da)$,
525: which is in normal form.
526: Else $f(t_1\da, t_2\da, t_3\da)$ is already in normal form.
527:
528:
529: Let us finally prove that $g(t_1,t_2)$ is innermost terminating.
530: First, $g(t_1,t_2) \succ t_1,$ $t_2$. Then, by induction
531: hypothesis, assume that $t_1$ and $t_2$ innermost terminate.
532: Let $t_1\da, t_2\da$ be respectively any of their normal forms.
533: It is then sufficient to prove that $g(t_1\da, t_2\da)$ is innermost
534: terminating.
535: The term $g(t_1\da, t_2\da)$ rewrites either into $t_1\da$ or into
536: $t_2\da$ at the
537: top position, with both $t_1\da$ and $t_2\da$ in normal form.
538: Remark that for $\succ$ in this proof, any ordering having the subterm
539: property is convenient.
540: Our goal is to provide a procedure implementing such a reasoning.
541:
542:
543: The paper is organized as follows: in Section~\ref{sec:background},
544: the background is presented. Section~\ref{sec:inductive} introduces
545: the inductive proof principle of our approach.
546: Section~\ref{sec:abstraction-narrowing-constraints} gives the basic
547: concepts of our inductive proof mechanism based on abstraction and
548: narrowing, and the involved constraints.
549: Section~\ref{sec:generic-algoritm} presents the generic termination
550: proof procedure that is further applied to different rewriting
551: strategies. In Section \ref{sec:innermost}, the mechanism is
552: instantiated for the case of innermost termination. In Section
553: \ref{sec:outermost}, the procedure is applied to outermost
554: termination. Finally, in section \ref{sec:local-strat}, the same
555: method is adapted to the case of local strategies.
556:
557:
558: \section{The background}
559: \label{sec:background}
560: %OUTERMOST/out-inn.tex
561:
562:
563: We assume that the reader is familiar with the basic definitions and notations
564: of term rewriting given for instance in~\cite{DershowitzJ-1989}.
565: $\TXF$ is the set of terms built from a given finite set $\F$
566: of function symbols $f$ having arity $n \in \mathbb N$ (denoted $f:n$), and a set $\X$ of
567: variables denoted $x, y \ldots $.
568: $\TF$ is the set of ground terms (without variables). The
569: terms reduced to a symbol of arity $0$ are called {\em constants}.
570: Positions in a term are represented as sequences of integers.
571: The empty sequence $\epsilon$ denotes the top position.
572: The symbol at the top position of a term $t$ is written $top(t)$.
573: Let $p$ and $p'$ be two positions. The position $p$ is said to be (a strict)
574: prefix of $p'$ (and $p'$ suffix of $p$) if $p'=p \lambda$, where
575: $\lambda$ is a non-empty sequence of integers.
576: Given a term $t$, $Var(t)$ is the set of variables of $t$,
577: $\OC(t)$ is the set of positions in $t$, inductively
578: defined as follows:
579: $\OC(t) =
580: \{\epsilon\} \; if \; t \in \X, \;
581: \OC(t) = \{\epsilon\} \cup \{i.p \mid 1 \leq i \leq n \mbox{ and } p \in \OC(t_i)\}
582: \; if \; t = f(t_1, \ldots ,t_n)$.
583: This set is partitioned into $\OS(t) = \{p \in \OC(t) \mid t|_p \not \in \X\}$
584: and $\OC_{\cal V}(t) = \{p \in \OC(t) \mid t|_p \in \X \}$ where the notation
585: $t|_p$ stands for the subterm of $t$ at position $p$.
586: If $p \in \OC(t)$, then $t[t']_p$ denotes the term obtained from $t$
587: by replacing the subterm at position $p$ by the term $t'$.
588:
589: A substitution is an assignment from $\X$ to $\TXF$,
590: written $\sigma = (x \mapsto t) \ldots (y \mapsto u)$.
591: It uniquely extends to an endomorphism of $\TXF$.
592: The result of applying
593: $\sigma$ to a term $t \in \TXF$ is written $\sigma(t)$ or $\sigma t$.
594: The domain of $\sigma$, denoted $Dom(\sigma)$ is the finite subset of
595: $\X$ such
596: that $\sigma x \neq x$. The range of $\sigma$, denoted $Ran(\sigma)$, is
597: defined by $Ran(\sigma) = \bigcup_{x \in Dom(\sigma)} Var(\sigma x)$.
598: We have in addition $Dom(\sigma) \cap Ran(\sigma) = \emptyset$.
599: A ground substitution or instantiation is an assignment from $\X$ to
600: $\TF$.
601: $Id$ denotes the identity substitution. The composition of substitutions
602: $\sigma_1$ followed by $\sigma_2$ is denoted $\sigma_2 \sigma_1$.
603: %Given two substitutions $\sigma _1$ and $\sigma _2$, we write
604: %$\sigma _1 \leq \sigma _2 [X]$
605: %iff $\exists \theta$ such that $\sigma _2 = \theta \sigma _1[X]$ i.e.
606: %$\forall x \in X, \sigma_2 x = \theta \sigma_1 x$
607: %($\sigma_1$ is said more general than $\sigma_2$).
608: Given a subset ${\cal X}_1$ of $\cal X$, we write
609: ${\sigma}_{{\cal X}_1}$ for the {\em restriction} of
610: $\sigma$
611: to the variables of ${\cal X}_1$, i.e. the substitution such that
612: $Dom({\sigma}_{{\cal X}_1}) \subseteq {\cal X}_1$ and
613: $\forall x \in Dom({\sigma}_{{\cal X}_1}):{\sigma}_{{\cal X}_1} x = \sigma x.$
614:
615:
616:
617: Given a set $\R$ of rewrite rules (a set of pairs of terms of $\TXF$, denoted
618: $l \ra r$, such that $Var(r) \subseteq Var(l)$) or rewrite system
619: on $\TXF$, a function symbol in $\F$
620: is called a {\em constructor} iff it does not occur in $\R$ at the top position
621: of a left-hand side of rule, and is called a {\em defined function symbol}
622: otherwise.
623: The set of defined function symbols of $\F$ for $\R$ is denoted
624: by $\Def_R$ ($\R$ is omitted when there is no ambiguity).
625:
626:
627: The rewriting relation induced by $\R$ is denoted by $\ra^{\R}$ ($\ra$ if
628: there is no ambiguity on $\R$), and defined by $s \ra t$ iff there exists a
629: substitution $\sigma$ and a position $p$ in $s$ such that $s|_p = \sigma l$
630: for some rule $l \ra r$ of $\R$, and $t=s[\sigma r]_p$.
631: This is written $ s \ra^{p, l \ra r, \sigma}_{\cal R} t$
632: where either $p$ either $l \ra r$ either $\sigma$ or ${\cal R}$ may be omitted;
633: $s|_p$ is called a redex.
634: The reflexive transitive closure of the rewriting
635: relation induced by $\R$ is denoted by
636: $\stackrel{*}{\ra}_{\R}$.
637: If $t \stackrel{*}{\ra} t'$ and $t'$ cannot be rewritten anymore, then $t'$ is
638: called a normal form of $t$ and denoted by $t\da$. Remark that given $t$,
639: $t\da$ may be not unique.
640:
641: Let $\cal R$ be a rewrite system on $\TXF$. A term $t$ is {\em narrowed} into $t'$, at
642: the non-variable position
643: $p$, using the rewrite rule $l\ra r$ of $\R$ and the substitution
644: $\sigma$, when $\sigma$ is a most general unifier of $t|_p$ and $l$,
645: and $t'=\sigma(t[r]_p)$.
646: This is denoted
647: $t\surred_{R}^{p,l\ra r,\sigma}t'$ where either $p$, either $l\ra r$ or $\sigma$
648: may be omitted.
649: It is always assumed that there is no variable in common
650: between the rule and the term, i.e. that $Var(l) \cap Var(t) = \emptyset$.
651:
652:
653:
654:
655: An ordering $\succ$ on $\TXF$ is said to be noetherian iff there is no
656: infinite decreasing chain for this ordering. It is
657: $\F$-stable iff for any pair of terms $t, t'$ of $\TXF$, for any
658: context $f( \ldots \; \ldots )$, $t \succ t'$ implies $f( \ldots t \ldots
659: )$ $ \succ f( \ldots t' \ldots )$. It
660: has the subterm property iff for any $t$ of $\TXF$, $f( \ldots t \ldots ) \succ
661: t$.
662: Observe that, for $\F$ and $\X$ finite, if $\succ$ is $\F$-stable and has the subterm
663: property, then it is noetherian~\cite{Kruskal60}. If, in addition,
664: $\succ$ is stable under substitution (for any
665: substitution $\sigma$, any pair of terms $t, t' \in \TXF, \; t \succ t'$
666: implies $\sigma t \succ \sigma t'$), then it is called a simplification
667: ordering.
668: Let $t$ be a term of $\TF$; let us recall that $t$ terminates
669: if and only if any rewriting
670: derivation (or derivation chain) starting from $t$ is finite.
671:
672:
673: Rewriting strategies are in general aimed at reducing the derivation
674: tree (for standard rewriting) of terms. The following definition
675: expresses that rewriting a term with a strategy $S$ can only give a
676: term that would be obtained with the standard rewriting relation.
677:
678: \begin{definition}[\thetheorem\ (rewriting strategy)]
679: Let $\R$ a rewrite system on $\TXF$.
680: A {\em rewriting strategy} $S$ for $\R$ is
681: a mapping $S : \TXF \ra \TXF$ such that for every $t \in \TXF$,
682: $S(t)=t'$ (we write $t \ra^S t'$) where $t'$ is such that $t
683: \ra_{\R} t'$.
684: \end{definition}
685:
686: %A position strategy is completely defined, for every term, by a
687: %position in the term, where the term is allowed to be rewritten.
688:
689: %\begin{definition}[position strategy]
690: %Let $\R$ a rewrite system on $\TXF$.
691: %A rewriting strategy $S$ is a {\em position strategy} for $\R$ iff
692: %there exists a mapping $Pos : \TXF \ra N^*$ such that for every $t \in
693: %\TXF$, $Pos(t) \in {\cal O}(t)$, and $S(t) =t'$ with $t' =t$ or $t\ra_{\cal
694: %R}^{Pos(t)} t'$.
695:
696: %\end{definition}
697:
698: %The strategies studied in this paper are position strategies.
699:
700: \begin{definition}[\thetheorem\ (innermost/outermost strategy)]
701: Let $\R$ a rewrite system on $\TXF$. The innermost (resp. outermost) strategy is a
702: rewriting strategy written $\mathit{S=Innermost}$ \ (resp. $\mathit{S=Outermost}$)
703: such that
704: for any term $t \in \TXF$, if $t \ra^S t'$, the rewriting position
705: $p$ in $t$ is such that
706: there is no suffix (resp. prefix) position $p'$ of $p$ such
707: that $t$ rewrites at position $p'$.
708: \end{definition}
709:
710: Rewriting strategies may be more complex to define. This is the case
711: for local strategies on operators, used in the OBJ-like languages.
712: We use here the notion of local strategy as expressed in \cite{OBJ3}
713: and studied in \cite{Eker98}.
714:
715: \begin{definition}[\thetheorem\ (LS-strategy)]
716: \label{def:local-strat}
717: An {\em LS-strategy}
718: is given by a function $LS$
719: from ${\cal F}$ to the set of lists of integers ${\cal L}(\Bbb{N})$,
720: that induces a rewriting strategy as follows.
721:
722: Given a LS-strategy such that $LS(f) = [p_1, \ldots ,p_k]$,
723: $p_i \in [0..arity(f)]$ for all $i \in [1..k]$,
724: for some symbol $f \in {\cal F}$,
725: normalizing a term $t =f(t_1, \ldots ,t_m) \in \TXF$ with
726: respect to $LS(f) = [p_1, \ldots,$ $p_k]$, consists in normalizing all subterms of $t$ at
727: positions $p_1, \ldots ,p_k$ successively, according to the strategy.
728: If there exists $i \in [1..k]$ such that $p_1, \ldots ,p_{i-1} \neq 0$
729: and $p_i=0$ ($0$ is the top position), then
730:
731: \begin{itemize}
732: \item if the current term $t'$ obtained
733: after normalizing $t|_{p_1},$ $ \ldots ,t|_{p_{i-1}}$ is reducible at the top
734: position into a term $g(u_1,$ $ \ldots ,u_n)$, then $g(u_1, \ldots ,u_n)$ is
735: normalized with respect to $LS(g)$ and the rest of the strategy
736: $[p_{i+1}, \ldots ,$ $p_k]$ is ignored,
737:
738:
739: \item if $t'$ is not reducible at the top
740: position, then $t'$ is normalized with respect to
741: $p_{i+1}, \ldots ,p_k$.
742: \end{itemize}
743:
744: \end{definition}
745:
746:
747: Let $t$ be a term of $\TF$; we say that $t$ terminates (w.r.t. to
748: the strategy $S$) if and only if every rewriting
749: derivation (or derivation chain) (w.r.t. to the strategy $S$)
750: starting from $t$ is finite.
751: Given a term $t$, we call normal form (w.r.t. to the strategy $S$)
752: or S-normal form of $t$, denoted $t\da$, any irreducible term, if it
753: exists, such that $t \stackrel{*}{\ra}^{S} t\da$.
754:
755:
756: \section{The inductive proof process}
757: \label{sec:inductive}
758:
759: \subsection{Lifting rewriting trees into proof trees}
760:
761: For proving that a term $t$ of $\TF$ terminates (for the considered
762: strategy), we proceed by induction on $\TF$ with a noetherian ordering
763: $\succ$, assuming that for any $t'$ such that $t \succ t'$, $t'$
764: terminates. To warrant non emptyness of $\TF$, we assume that $\F$
765: contains at least a constructor constant.
766:
767:
768: The main intuition is to observe the rewriting derivation tree (for
769: the considered strategy) starting from a ground term $t \in \TF$ which is any
770: instance of a term $g(x_1, \ldots ,x_m)$, for some defined function
771: symbol $g \in \Def$, and variables $x_1, \ldots ,x_m$. Proving
772: termination on ground terms amounts proving that all rewriting
773: derivation trees have only finite branches, using the same induction
774: ordering $\succ$ for all trees.
775:
776: Each rewriting derivation tree is simulated, using a lifting mechanism,
777: by a proof tree, developed from $g(x_1,\ldots,x_m)$ on $\TXF$,
778: for every $g \in \Def$, by
779: alternatively using two main operations, namely narrowing and
780: abstraction, adapted to the considered rewriting strategy.
781: More precisely, narrowing schematizes all rewriting
782: possibilities of terms. The abstraction process simulates the
783: normalization of subterms in the derivations, according to the
784: strategy. It consists in replacing these subterms by special
785: variables, denoting one of their normal forms, without computing
786: them. This abstraction step is performed on subterms that can be
787: assumed terminating by induction hypothesis.
788:
789: The schematization of ground rewriting derivation trees is achieved
790: through constraints. The nodes of the developed proof trees are
791: composed of a current term of $\TXF$, and a
792: set of ground substitutions represented by a constraint progressively
793: built along the successive abstraction and narrowing steps.
794: Each node in a proof tree schematizes a set of ground terms:
795: the ground instances of the current term, that are solutions of the constraint.
796:
797: The constraint is in fact composed of two kinds of formulas: ordering
798: constraints, set to warrant the validity of the inductive steps, and
799: abstraction constraints combined to narrowing substitutions, which
800: effectively define the relevant sets of ground terms. The latter are
801: actually useful for controlling the narrowing process, well known to
802: easily diverge.
803:
804: The termination proof procedures given in this paper are described by
805: deduction rules applied with a special control $\mathit{Strat{-}Rules(S)}$,
806: depending on the studied rewriting strategy $S$.
807: To prove termination of $\R$
808: on any term $t \in \TF$ w.r.t. the strategy $S$, we consider a so-called
809: reference term $t_{\mathit{ref}} = g(x_1, \ldots , x_m)$ for each
810: defined symbol $g \in \Def$, and empty
811: sets $\top$ of constraints. Applying the deduction rules according to the
812: strategy $\mathit{Strat{-}Rules(S)}$ to the initial state $(\{g(x_1, \ldots ,
813: x_m)\}, \top, \top)$ builds a proof tree, whose nodes are the states
814: produced by the inference rules. Branching is produced by the
815: different possible narrowing steps.
816:
817:
818: Termination is established when the procedure terminates because the
819: deduction rules do not apply anymore and all terminal states of all proof trees
820: have an empty set of terms.
821:
822:
823:
824: \subsection{A generic mechanism for strategies}
825: \label{subsec:generic}
826:
827: As said previously, we consider any term of $\TF$ as a ground
828: instance of
829: a term $t$ of $\TXF$ occurring in a proof tree issued from
830: a reference term $t_{\mathit{ref}}$.
831: Using the termination induction hypothesis on $\TF$ naturally
832: leads us to simulate the rewriting relation by two mechanisms:
833:
834: \begin{itemize}
835: \item
836: first, some subterms $t_j$
837: of the current term $t$ of the proof tree are supposed
838: to have only terminating ground instances, by induction hypothesis, if $\theta
839: t_{\mathit{ref}} \succ \theta t_j$ for the induction ordering $\succ$
840: and for every $\theta$ solution of the constraint associated to $t$.
841: They are replaced in $t$
842: by {\em abstraction variables} $X_j$ representing respectively one
843: of their normal forms $t_j \da$.
844: Reasoning by induction allows us to
845: only suppose the existence of the $t_j \da$
846: {\em without explicitly computing them};
847:
848:
849: \item
850: second, narrowing (w.r.t. to the strategy $S$) the resulting term
851: $u=t[X_j]_{j\in \{i_1,\ldots,i_p\}}$ (where
852: $i_1,\ldots,i_p$ are the positions of the abstracted subterm $t_j$ in
853: $t$) into terms $v$, according to the
854: possible instances of the $X_j$.
855: This corresponds to rewriting (w.r.t. to the strategy $S$)
856: the possible ground instances of $u$ (characterized
857: by the constraint associated to $u$) in all possible ways.
858:
859: In general, the narrowing step of $u$ is not unique. We
860: obviously have to consider all terms $v$ such that $\theta u$
861: rewrites into $\theta v$, which
862: corresponds to considering all narrowing steps from $u$.
863:
864:
865: \end{itemize}
866:
867: Then the termination problem of the ground instances of $t$ is reduced
868: to the termination problem of the ground instances of $v$. If
869: $\theta t_{\mathit{ref}} \succ \theta v$ for every ground
870: substitution $\theta$ solution of the constraint associated to $v$,
871: by induction hypothesis, $\theta v$ is supposed to be terminating.
872: Else, the process is iterated on $v$, until getting
873: a term $t'$ such that either $\theta t_{\mathit{ref}} \succ \theta t'$, or
874: $\theta t'$ is irreducible.
875:
876: We introduce in the next section the necessary concepts to formalize and automate
877: this technique.
878:
879:
880:
881:
882: \section{Abstraction, narrowing, and the involved constraints}
883: \label{sec:abstraction-narrowing-constraints}
884:
885:
886: \subsection{Ordering constraints}
887:
888: The induction ordering is constrained
889: along the proof by imposing constraints between terms that must be
890: comparable, each time the induction hypothesis is used in the
891: abstraction mechanism.
892: As we are working with a lifting mechanism on the proof trees
893: with terms of $\TXF$, we directly work with an ordering $\succ_{\cal
894: P}$ on $\TXF$
895: such that $t\succ _{\cal P} u$ implies $\theta t \succ \theta u$,
896: for every $\theta$ solution of the constraint associated to $u$.
897:
898:
899: So inequalities of
900: the form $t > u_1, \ldots ,u_m$ are accumulated, which are called
901: {\em ordering constraints}. Any ordering $\succ_{\cal P}$ on $\TXF$
902: satisfying them and which is stable under substitution fulfills the
903: previous requirements on ground terms. The ordering $\succ_{\cal P}$,
904: defined on $\TXF$,
905: can then be seen as an extension of the induction ordering $\succ$,
906: defined on $\TF$. For convenience, the ordering $\succ_{\cal P}$
907: will also be written $\succ$.
908:
909:
910: It is important to remark that, for establishing the inductive
911: termination proof, it is sufficient to decide whether
912: there exists such an ordering.
913:
914:
915:
916: \begin{subdefinition}[\thesubtheorem\ (ordering constraint)]
917: \label{def:ordering-constraint}
918: {\em An ordering constraint} is a pair of terms of $\TXF$ noted $(t>t')$.
919: It is said to be {\em satisfiable} if there exists an ordering
920: $\succ$, such that for every instantiation $\theta$ whose domain
921: contains $\Var(t) \cup \Var(t')$, we have
922: $\theta t \succ \theta t'$. We say that $\succ$ satisfies $(t>t')$.
923:
924: A conjunction $C$ of ordering constraints is
925: satisfiable if there exists an ordering
926: satisfying all conjuncts.
927: The empty conjunction, always satisfied, is denoted by $\top$.
928: \end{subdefinition}
929:
930:
931: Satisfiability of a constraint conjunction $C$ of this form is undecidable.
932: But a sufficient condition for an ordering $\succ$ to satisfy $C$
933: is that $\succ$ is stable under substitution
934: %%%(the induction ordering is then a simplification ordering)
935: and $t \succ t'$ for any constraint $t > t'$ of $C$.
936:
937:
938: \subsection{Abstraction}
939: \label{subsec:generic-abstraction}
940:
941: To abstract a term $t$ at positions $i_1,\ldots,i_p$,
942: where
943: the $t|_j$ are supposed to have a normal
944: form $t|_j \da$, we replace the $t|_j$ by abstraction variables $X_j$
945: representing respectively one of their possible normal forms.
946: Let us define these special variables more formally.
947:
948:
949:
950: \begin{subdefinition}
951: \label{def:abstraction-var}
952: Let $\XA$ be a set of variables disjoint from ${\cal X}$.
953: Symbols of $\XA$ are called {\em abstraction variables}.
954: Substitutions and instantiations are extended to $\TFXXA$
955: in the following way:
956: let $X \in \XA$; for any substitution $\sigma$
957: (resp. instantiation $\theta$)
958: such that $X \in Dom(\sigma)$, $\sigma X$ (resp. $\theta X$)
959: is in S-normal form.
960: \end{subdefinition}
961:
962: %%DEBAT
963: %{\bf Pourquoi les variables d'abstraction ne sont pas toujours
964: %instantiees par les termes clos en forme normale pour l'out et les
965: %strat lo ?\\
966: %Reponse: au moment de l'abstraction, les var representent bien des fn,
967: %mais si le terme se reecrit, les var peuvent se retrouver a des
968: %positions redex...\\
969: %Non, pas pour l'outermost, puisque l'abstraction est une phase
970: %terminale de la chaine de reduction. Pour les strat lo non plus,
971: %puisque une fois qu'un sous-terme a ete normalise, il le reste quel
972: %que soit le contexte.\\
973: %A BIEN REVOIR ENSEMBLE
974: %REVU: les var d'abstraction le restent definitivement (quelle que sout
975: %la strat).
976: %La ou il faut faire attention, c'est aux mgu qui peuvent introduire
977: %des var normales, pour les strat lo. Pour l'outermost, on ne narrowe
978: %jamais un terme avec des var d'abstraction
979:
980:
981:
982: \begin{subdefinition}[\thesubtheorem\ (term abstraction)]
983: \label{def:abstraction}
984: The term $t[t|_j]_{j \in \{i_1, \ldots , i_p\}}$ is said to be
985: {\em abstracted} into the term $u$ (called {\em abstraction} of $t$) at
986: positions $\{i_1, \ldots, i_p\}$ iff
987: $u =$ $t[X_j]_{j \in \{i_1, \ldots, i_p\}}$, where the $X_j, j \in \{i_1,
988: \ldots, i_p\}$ are fresh distinct abstraction variables.
989: \end{subdefinition}
990:
991:
992: Termination on $\TF$ is proved by reasoning on terms with
993: abstraction variables, i.e. on terms of $\TFXXA$. Ordering constraints
994: are extended to pairs of terms of $\TFXXA$. When subterms $t|_j$
995: are abstracted by $X_j$, we state constraints on abstraction
996: variables, called {\em abstraction constraints} to express that their
997: instances can only be normal forms of the corresponding instances
998: of $t|_j$. Initially, they are of the form $t \con X$ where $t \in
999: \TFXXA$, and $X \in \XA$, but we will see later how they are
1000: combined with the substitutions used for the narrowing process.
1001:
1002:
1003:
1004:
1005: \subsection{Narrowing}
1006: \label{sub:narrowing}
1007:
1008: After abstraction of the current term $t$ into $t[X_j]_{j \in \{i_1, \ldots , i_p\}}$,
1009: we check whether the possible ground instances of $t[X_j]_{j \in \{i_1, \ldots , i_p\}}$
1010: are reducible, according to the possible values of the instances of
1011: the $X_j$. This is achieved by narrowing $t[X_j]_{j \in \{i_1, \ldots , i_p\}}$.
1012:
1013: The narrowing relation depends on the considered strategy $S$ and
1014: the usual definition needs to be refined. The first idea is to use
1015: innermost (resp. outermost) narrowing. Then, if a position $p$ in a term
1016: $t$ is a narrowing position, a suffix (resp. prefix) position of $p$
1017: cannot be a narrowing position too.
1018: However, if we consider ground instances of $t$, we can have
1019: rewriting positions $p$ for some instances, and $p'$ for some other
1020: instances, such that $p'$ is a suffix (resp. a prefix) of $p$.
1021: So, when narrowing at some position $p$, the
1022: set of relevant ground instances of $t$ is defined by excluding the
1023: ground instances that would be narrowable at some suffix (resp. prefix)
1024: position of $p$, that we call $S$-better position:
1025: a position $S$-better than a position $p$ in $t$ is a suffix
1026: position of $p$ if $S$ is the innermost strategy, a prefix position of
1027: $p$ if $S$ is the outermost strategy.
1028: Note that local strategies are not of the same nature, and there is no
1029: $S$-better position in this case.
1030:
1031: %{\bf Moreover, in order a narrowing step of the current term $t$
1032: %schematizes a rewriting step of its possible ground instances, the
1033: %redexes of these ground instances must correspond to narrowable
1034: %positions of $t$. In other words, the redexes of the
1035: %possible ground instances of $t$ must not be in the instances of the
1036: %variables of $t$.
1037: %
1038: %So each narrowing step has to be preceded by a variable renaming in $t$,
1039: %schematizing any longest rewriting chain of any ground instance of
1040: %$t$, whose redexes are in the instances of the
1041: %variables of $t$.}
1042:
1043:
1044: Moreover, to preserve the fact that a narrowing step of $t$ schematizes a
1045: rewriting step of possible ground instances of $t$,
1046: we have to be sure that an innermost (resp. outermost) narrowing redex in $t$
1047: corresponds to the same rewriting redex in a ground instance of $t$.
1048: This is the case only if, in the rewriting chain of the ground instance of $t$,
1049: there is no rewriting redex at a suffix position of variable of $t$ anymore.
1050: So before each narrowing step, we schematize the
1051: longest rewriting chain of any ground instance of $t$, whose redexes
1052: occur in the variable part of the instantiation, by a linear variable renaming.
1053: Linearity is crucial to express that, in the previous rewriting chain,
1054: ground instances of the same variables can be reduced in different ways.
1055: For the innermost strategy, abstraction of variables performs
1056: this schematization. For the outermost strategy, a reduction renaming
1057: will be introduced.
1058: For local strategies however, this variable renaming is not relevant.
1059:
1060: The $S$-narrowing steps applying to a given term $t$ are computed in
1061: the following way.
1062: After applying the variable renaming to $t$,
1063: we look at every position $p$ of $t$ such that $t|_p$
1064: unifies with the left-hand side of a rule using a substitution
1065: $\sigma$. The position $p$ is a $S$-narrowing position of $t$,
1066: iff there is no $S$-better position $p'$
1067: of $t$ such that $\sigma t|_{p'}$ unifies with a left-hand side of
1068: rule. Then we look for every $S$-better position $p'$ than $p$ in $t$ such that
1069: $\sigma t|_{p'}$ narrows with some substitution $\sigma'$ and
1070: some rule $l' \ra r'$, and we set a constraint to exclude these
1071: substitutions.
1072: So the substitutions used to narrow a
1073: term have in general to satisfy a set
1074: of disequalities coming from the negation of previous substitutions.
1075: To formalize this point, we need the following notations
1076: and definitions.
1077:
1078: In the following, we identify a substitution
1079: $\sigma = (x_1 \mapsto t_1) \ldots (x_n \mapsto t_n)$ on $\TFXXA$
1080: with the finite set
1081: of solved equations $(x_1 = t_1) \wedge \ldots \wedge (x_n = t_n)$,
1082: also denoted by the equality formula $\bigwedge_i (x_i=t_i)$,
1083: with $x_i \in {\cal X} \cup \XA$, $t_i \in \TFXXA$, where $=$ is
1084: the syntactic equality. Similarly, we call {\em negation
1085: $\overline{\sigma}$} of the substitution $\sigma$ the formula
1086: $\bigvee_i (x_i \neq t_i)$.
1087:
1088:
1089: \begin{subdefinition}
1090: [\thesubtheorem\ (constrained substitution)]
1091: %An instantiation $\theta$ is said {\em to satisfy} a constraint
1092: %$\bigwedge_j \bigvee_{i_j}$ $ (x_{i_j} \neq t_{i_j})$, iff
1093: %$\bigwedge_j \bigvee_{i_j} (\theta x_{i_j} \neq \theta t_{i_j})$.
1094: A {\em constrained substitution} $\sigma$ is a formula $\sigma_0
1095: \wedge \bigwedge_j \bigvee_{i_j} (x_{i_j} \neq t_{i_j})$, where
1096: $\sigma_0$ is a substitution.
1097: \end{subdefinition}
1098:
1099:
1100:
1101: \begin{subdefinition}[\thesubtheorem\ ($S$-narrowing)]
1102: \label{def:narrowing}
1103: A term $t \in \TFXXA$ {\em $S$-narrows} into a term $t' \in \TFXXA$ at
1104: the non-variable position $p$ of $t$, using the rule $l \ra r \in \R$ with
1105: the constrained substitution
1106: $\sigma = \sigma_0 \wedge \bigwedge_{j \in [1..k]} \overline{\sigma_j}$,
1107: which is written $t \leadsto^{S}_{p, l \ra r, \sigma} t'$ iff
1108: \begin{center}
1109: $ \sigma_0(l) = \sigma_0(t|_p)$ and $ t' = \sigma_0(t[r]_p)$
1110: \end{center}
1111: \noindent
1112: where $\sigma_0$ is the most general unifier of $t|_p$ and $l$ and
1113: $\sigma_j, j \in [1..k]$ are
1114: all most general unifiers of $\sigma_0 t|_{p'}$ and a left-hand side
1115: $l'$ of a rule of $\R$, for all position $p'$ which are $S$-better
1116: positions than $p$ in $t$.
1117: \end{subdefinition}
1118:
1119:
1120: It is always assumed that there is no variable in common
1121: between the rule and the term, i.e. that $Var(l) \cap Var(t) =
1122: \emptyset$.
1123: This requirement of disjoint variables is easily fulfilled by an
1124: appropriate renaming of variables in the rules when narrowing is
1125: performed.
1126: The most general unifier $\sigma_0$ used in
1127: the above definition can be taken such that its
1128: range only contains fresh variables.
1129: Since we are interested in the
1130: narrowing substitution applied to the current term $t$, but not in its
1131: definition on the variables of the left-hand side of the rule, the
1132: narrowing substitutions can be restricted to the variables of
1133: the narrowed term $t$.
1134:
1135:
1136: The following lifting lemma, generalized from~\cite{MiddeldorpH-AAECC94},
1137: ensures the correspondence between the narrowing relation, used during the
1138: proof, and the rewriting relation.
1139:
1140: \begin{sublemma}[\thesubtheorem\ ($S${-}lifting Lemma)]
1141: \label{lemma:surred-S}
1142: Let $\R$ be a rewrite system.
1143: Let $s \in \TXF$, $\alpha$ a ground
1144: substitution such that $\alpha s$ is $S${-}reducible
1145: at a non variable position $p$ of $s$, and ${\cal Y} \subseteq {\cal X}$
1146: a set of variables
1147: such that $Var(s) \cup Dom(\alpha) \subseteq {\cal Y}$.
1148: If $\alpha s \ra^{S}_{p, l \ra r} t'$, then there exist a term
1149: $s' \in \TXF$ and substitutions
1150: $\beta, \sigma = \sigma_0 \wedge \bigwedge_{j \in [1..k]} \overline{\sigma_j}$
1151: such that:
1152:
1153: \[
1154: \begin{array}{ll}
1155:
1156: 1.~s \surred^{S}_{p, l \ra r, \sigma} s', \\
1157: 2.~\beta s' = t', \\
1158: 3.~\beta \sigma_0 = \alpha [{\cal Y}]\\
1159: 4.~\beta {\rm ~satisfies~} \bigwedge_{j \in [1..k]} \overline{\sigma_j}
1160:
1161: \end{array}
1162: \]
1163: where $\sigma_0$ is the most general unifier of $s|_p$ and $l$ and
1164: $\sigma_j, j \in [1..k]$ are
1165: all most general unifiers of $\sigma_0 s|_{p'}$ and a left-hand side
1166: $l'$ of a rule of $\R$, for all position $p'$ which are $S$-better
1167: positions than $p$ in $s$.
1168:
1169: \end{sublemma}
1170:
1171:
1172: \subsection{Cumulating constraints}
1173: \label{subsec:cumulating-constraints}
1174:
1175: Abstraction constraints have to be combined with the narrowing
1176: constrained substitutions to characterize the ground terms schematized
1177: by the proof trees.
1178: %A narrowing step with constrained substitution $\sigma$ effectively corresponds to a rewriting step
1179: %of ground instances if $\sigma$ is compatible with the previous
1180: %abstraction constraints.
1181: A narrowing step effectively corresponds to a
1182: rewriting step of ground instances of $u$
1183: if the narrowing constrained substitution $\sigma$
1184: is {\em compatible} with the abstraction constraint formula A associated to
1185: $u$ (i.e. $A \wedge \sigma$ is satisfiable). Else, the narrowing step
1186: is meaningless.
1187: So the narrowing constraint attached to the narrowing step is added
1188: to $A$.
1189: Hence the introduction of abstraction constraint formulas.
1190:
1191: %%%%{\bf Faut-il expliquer alors que les contraintes de la forme $t \con X$
1192: %%%ne donnent des contraintes $t \con t'$ que si on propage dans $A$ ?}
1193:
1194:
1195: %To the abstraction constraints of the form $t \con X$, disequations
1196: %coming from narrowing substitutions are added.
1197:
1198: \begin{subdefinition}[\thesubtheorem\ (abstraction constraint formula)]
1199: An {\em abstraction constraint formula} (ACF in short) is a formula
1200: $\bigwedge_i (t_i \con t'_i) \wedge \bigwedge_j (x_j = t_j) \wedge
1201: \bigwedge_k \bigvee_{l_k} (u_{l_k} \neq v_{l_k})$,
1202: where $t_i, t'_i, t_j, u_{l_k}, v_{l_k} \in \TFXXA$, $x_j
1203: \in \X \cup \XA$.
1204: \end{subdefinition}
1205:
1206:
1207: \begin{subdefinition}[\thesubtheorem\ (satisfiability of an ACF)]
1208: \label{def:satACF}
1209: An {\em abstraction constraint formula}
1210: $\bigwedge_i (t_i \con t'_i) \wedge \bigwedge_j (x_j = t_j) \wedge
1211: \bigwedge_k \bigvee_{l_k} (u_{l_k} \neq v_{l_k})$,
1212: is {\em satisfiable} iff there exists at least one instantiation $\theta$ such
1213: that $\bigwedge_i (\theta t_i \con \theta t'_i) \wedge
1214: \bigwedge_j (\theta x_j = \theta t_j) \wedge
1215: \bigwedge_k \bigvee_{l_k} (\theta u_{l_k} \neq \theta v_{l_k})$.
1216: The instantiation
1217: $\theta$ is then said to satisfy the ACF $A$ and is called solution of
1218: $A$.
1219: \end{subdefinition}
1220:
1221: Integrating a constrained substitution $\sigma = \sigma_0
1222: \wedge \bigwedge_i \bigvee_{j_i} (x_{j_i} \neq t_{j_i})$ to an ACF $A$
1223: is done by adding the formula defining $\sigma$ to $A$, thus giving the formula
1224: $A \wedge \sigma$.
1225: For a better readability on examples,
1226: we can propagate $\sigma$ into $A$ (by applying $\sigma_0$ to $A$),
1227: thus getting instantiated abstraction constraints of the form $t_i \con t'_i$
1228: from initial abstraction constraints of the form $t_i \con X_i$.
1229:
1230:
1231: An ACF $A$ is attached to each term $u$ in the proof trees;
1232: its solutions characterize the interesting ground instances of this
1233: term, i.e. the $\theta u$ such that $\theta$ is a solution of $A$.
1234: When $A$ has no solution, the current node of the proof tree
1235: represents no ground term. Such nodes are then irrelevant for the
1236: termination proof.
1237: Detecting and suppressing them during a narrowing step allows to control
1238: the narrowing mechanism.
1239: So we have the choice between
1240: generating only the relevant nodes of the
1241: proof tree, by testing satisfiability of $A$ at each step, or stopping the
1242: proof on a branch on an irrelevant node, by testing unsatisfiability
1243: of $A$. These are both facets of the same question, but in practice,
1244: they are handled in different ways.
1245:
1246: Checking satisfiability of $A$ is in general undecidable.
1247: The disequality part of an ACF is a particular instance of a
1248: disunification problem (a quantifier free equational formula), whose satisfiability
1249: has been addressed in~\cite{Comon-rob91}, that provides rules
1250: to transform any disunification problem into a solved form.
1251: Testing satisfiability of the equational part of an ACF is
1252: undecidable in general, but sufficient conditions can be given,
1253: relying on a characterization of normal forms.
1254: %But as we will see on examples, SCFs are simple to handle in
1255: %practice, and the use of the previously cited algorithms can often be
1256: %avoided.
1257:
1258: Unsatisfiability of $A$ is also undecidable in general, but simple sufficient conditions
1259: can be used, very often applicable in practice. They rely
1260: on reducibility, unifiability, narrowing and constructor tests.
1261:
1262: According to Definition~\ref{def:satACF}, %Def 7 au 25/03/04
1263: an ACF
1264: $\bigwedge_i (t_i \con t'_i) \wedge \bigwedge_j (x_j = t_j) \wedge
1265: \bigwedge_k \bigvee_{l_k} (u_{l_k} \neq v_{l_k})$
1266: is unsatisfiable if for instance, one of its conjunct $t_i \con t'_i$ is
1267: unsatisfiable, i.e. is such that $\theta t'_i$ is not a normal form of
1268: $\theta t_i$ for any ground substitution $\theta$.
1269: Hence, we get four automatable conditions for unsatisfiability of
1270: an abstraction constraint $t \con t'$:
1271: \begin{description}
1272:
1273: \item[Case 1:]
1274: $t \con t'$, with $t'$ reducible.
1275: Indeed, in this case, any ground instance of $t'$ is reducible, and hence
1276: cannot be a normal form.
1277:
1278: \item[Case 2:]
1279: $t \con t' \wedge \ldots \wedge t' \con t''$, with $t'$ and $t''$ not unifiable.
1280: Indeed, any ground substitution $\theta$ satisfying the above conjunction is
1281: such that (1)~$\theta t \con \theta t'$ and (2)~$\theta t' \con \theta t''$.
1282: In particular, (1) implies that $\theta t'$ is in normal form and hence
1283: (2) imposes $\theta t' = \theta t''$, which is impossible if $t'$ and $t''$
1284: are not unifiable.
1285:
1286: \item[Case 3:]
1287: $t \con t'$ where $top(t)$ is a constructor, and $top(t) \neq top(t')$.
1288: Indeed, if the top symbol of $t$ is a constructor $s$, then any normal form
1289: of any ground instance of $t$ is of the form $s(u)$, where $u$ is a
1290: ground term in normal form.
1291: The above constraint is therefore unsatisfiable if the top symbol of $t'$
1292: is $g$, for some
1293: $g \neq s$.
1294:
1295: \item[Case 4:]
1296: $t \con t'$ with $t,t' \in \TFXA$ not unifiable and
1297: $\bigwedge_{t \surred^S v} v \con t'$ unsatisfiable.
1298: This criterion is of interest if unsatisfiability of each conjunct $v \con t'$
1299: can be shown with one of the four criteria we present here.
1300:
1301: \end{description}
1302:
1303: So both satisfiability and unsatisfiability checks need to use
1304: sufficient conditions.
1305: But in the first case, the proof process stops with failure as soon as satisfiability
1306: of $A$ cannot be proved. In the second one, it can go on, until $A$ is
1307: proved to be unsatisfiable, or until other stopping conditions are fulfilled.
1308:
1309: Let us now come back to ordering constraints. If we check satisfiability
1310: of $A$ at each step, we only generate states in the proof trees, that
1311: represent non empty sets of ground terms. So in fact, the ordering
1312: constraints of $C$ have not to be satisfied for every ground
1313: instance, but only for those instances that are solution of $A$, hence
1314: the following definition, that can be used instead of
1315: Definition~\ref{def:ordering-constraint},
1316: when constraints of this definition cannot be proved satisfiable,
1317: and solutions of $A$ can easily be characterized.
1318:
1319: \begin{subdefinition}[\thesubtheorem\ (constraint problem)]
1320: \label{def:constraint-problem}
1321: Let $A$ be an abstraction constraint formula
1322: and $C$ a conjunction of ordering constraints.
1323: The constraint problem $C \sur A$ is satisfied by an ordering $\succ$
1324: iff for every instantiation $\theta$
1325: satisfying $A$, then $\theta t \succ \theta t'$ for
1326: every conjunct $t>t'$ of $C$.
1327: $C \sur A$ is satisfiable iff there exists an
1328: ordering $\succ$ as above.
1329: \end{subdefinition}
1330:
1331: Note that $C \sur A$ may be satisfiable even if $A$ is not.
1332:
1333:
1334: \subsection{Relaxing the induction hypothesis}
1335: \label{subsec:relaxing}
1336:
1337: \newcommand{\APos}{{\cal AP}{\it os}}
1338:
1339: It is important to point out the flexibility of the proof method
1340: that allows the combination with auxiliary termination proofs using
1341: different techniques: when the induction hypothesis cannot be applied
1342: on a term $u$, i.e. when it is not possible to decide whether the
1343: ordering constraints are satisfiable, it is often possible to
1344: prove termination
1345: (for the considered strategy) of any ground instance of $u$ by another way. In
1346: the following we use a predicate $\mathit{TERMIN(S,u)}$ that is true iff
1347: every ground instance of $u$ terminates for the considered strategy
1348: $S$.
1349:
1350: In particular, $\mathit{TERMIN(S,u)}$ is true when every instance of $u$ is in
1351: normal form. This is the case when $u$ is not narrowable, and all
1352: variables of $u$ are in $\XA$. Indeed, by Lemma~\ref{lemma:surred-S}
1353: and Definition~\ref{def:abstraction-var}, every instance of $u$ is in
1354: normal form. This includes the cases where $u$ itself is an
1355: abstraction variable, and where $u$ is a non narrowable ground term.
1356:
1357:
1358: Every instance of a narrowable $u$ whose variables are all in $\XA$,
1359: and whose narrowing substitutions are not compatible with $A$, is also in
1360: normal form. As said in Section~\ref{subsec:cumulating-constraints},
1361: these narrowing possibilities do not represent any reduction step for
1362: the ground instances of $u$, which are then in normal form.
1363:
1364: %%%%% Attention quand meme au cas des strat lo...
1365:
1366: Otherwise, in many cases, for proving that $\mathit{TERMIN(S,u)}$ is true, the
1367: notion of usable rules~\cite{Arts-Giesl-inner-tech-96} is relevant.
1368: Given a rewrite system $\R$ on $\TXF$ and a term $t \in \TFXXA$, the {\em usable
1369: rules} of $t$ are a subset of $\R$, which is a computable superset of the
1370: rewrite rules that are likely to be used in any rewriting chain
1371: (for the standard strategy) starting from any ground instance of $t$,
1372: until its ground normal forms are reached, if they exist.
1373:
1374: Proving termination of any ground instance of $u$ then comes
1375: down to proving termination of its usable rules, which is in general
1376: much easier than proving termination of the whole rewrite system $\R$. In
1377: general, we try to find a simplification ordering $\succ_N$ that
1378: orients these rules. Thus any ground instance $\alpha t$ is bound to
1379: terminate for the standard rewriting relation, and then for the
1380: rewriting strategy $S$. Indeed, if $\alpha t \ra t_1 \ra t_2 \ra
1381: \ldots $, then, thanks to the previous hypotheses, $\alpha t \succ_N
1382: t_1 \succ_N t_2 \succ_N \ldots $ and, since the ordering $\succ_N$ is
1383: noetherian, the rewriting chain cannot be infinite. As a particular
1384: case, when a simplification ordering can be found to orient the whole rewrite system,
1385: it also orients the usable rules of any term, and our inductive approach
1386: can also conclude to termination.
1387: If an appropriate
1388: simplification ordering cannot be found, termination of the usable
1389: rules may also be proved with our inductive process itself. The fact
1390: that the induction ordering used for usable rules is independent of
1391: the main induction ordering, makes the proof very flexible.
1392: Complete results on usable rules for the innermost strategy are given in
1393: Section~\ref{subsec:relaxing-innermost}. For the outermost and local
1394: strategies, this is developed in~\cite{FGK-WRLA-2002} and \cite{FGK-local-strat-ENTCS-2001}.
1395:
1396:
1397: \section{The termination proof procedure}
1398: \label{sec:generic-algoritm}
1399:
1400: \subsection{Strategy-independent proof steps}
1401: \label{sec:proof-steps}
1402:
1403: We are now ready to describe the different steps of the proof
1404: mechanism presented in Section~\ref{sec:inductive}.
1405:
1406: The proof steps generate proof trees in transforming 3-tuples $(T,A,C)$ where
1407: \begin{itemize}
1408: \item
1409: $T$ is a set of terms of $\TFXXA$, containing the current term $u$ whose termination
1410: has to be proved. $T$ is either a singleton or the empty set.
1411: For local strategies, the term is enriched by
1412: the list of positions where $u$ has to be evaluated, $LS(top(u))$.
1413: This is denoted by $u^{LS(top(u))}$.
1414:
1415:
1416: \item
1417: $A$ is a conjunction of abstraction constraints. At each abstraction
1418: step, constraints of the form
1419: $u \con X, u \in \TFXXA, X \in {\XA}$ are stated for each subterm term $t$
1420: abstracted into a new abstraction variable $X$.
1421: At each narrowing step with narrowing substitution $\sigma$, $A$ is replaced by
1422: $A \wedge \sigma$.
1423:
1424:
1425: \item
1426: $C$ is a conjunction of ordering constraints stated by the
1427: abstraction steps.
1428: \end{itemize}
1429:
1430: Starting from initial states
1431: $(T=\{t_{\mathit{ref}}=g(x_1,\ldots,x_m)\},A=\top,C=\top)$, where $g
1432: \in \Def$,
1433: the proof process consists in iterating
1434: the following generic steps:
1435:
1436: \begin{itemize}
1437: \item
1438: The first step abstracts the current term $t$ at
1439: given positions $i_{1}, \ldots,$ $i_{p}$.
1440: If the conjunction of ordering constraints
1441: $\bigwedge_j t_{\mathit{ref}}>t|_j$ is satisfiable for some $j
1442: \in \{i_{1}, \ldots ,i_{p}\}$, we
1443: suppose, by induction, the existence of irreducible
1444: forms for the $t|_j$.
1445: We must have $\mathit{TERMIN(S,t|_j)}$ for the other $t|_j$.
1446: Then, $t|_{i_1}, \ldots ,t|_{i_p}$ are
1447: abstracted into abstraction variables $X_{i_{1}}, \ldots ,$
1448: $X_{i_{p}}$.
1449: The abstraction constraints $t|_{i_1} \con X_{i_{1}}, \ldots ,t|_{i_p} \con
1450: X_{i_{p}}$ are added to the ACF $A$.
1451: We call that step the \emph{abstract} step.
1452:
1453: \item The second step narrows the resulting term $u$
1454: in one step with all
1455: possible rewrite rules of the rewrite system $\R$, and all possible
1456: substitutions $\sigma$, into terms $v$, according to Definition~\ref{def:narrowing}.
1457: This step is a branching step,
1458: creating as many states as narrowing possibilities.
1459: The substitution $\sigma$ is added to $A$.
1460: This is the \emph{narrow} step.
1461:
1462:
1463: \item We then have a \emph{stop} step halting the proof process on the
1464: current branch of the proof tree, when $A$ is detected to be unsatisfiable,
1465: or when the ground instances of the current term
1466: can be stated terminating for the considered strategy. This happens
1467: when the whole
1468: current term $u$ can be abstracted, i.e. when the induction hypothesis applies
1469: on it, or when we have $\mathit{TERMIN(S,u)}$.
1470:
1471: \end{itemize}
1472:
1473:
1474: The satisfiability and unsatisfiability tests of $A$ are integrated in
1475: the previously presented steps. If testing unsatisfiability of $A$ is
1476: chosen, the unsatisfiability test is integrated in the \emph{stop} step. If
1477: testing the satisfiability of $A$ is chosen, the test is made at each
1478: attempt of an abstraction or a narrowing step, which are then
1479: effectively performed only if $A$ can be proved
1480: satisfiable. Otherwise, the proof cannot go on anymore and stops with
1481: failure.
1482:
1483: As we will see later, for a given rewriting strategy $S$,
1484: these generic proof steps are instantiated by more
1485: precise mechanisms, depending on $S$,
1486: and taking advantage of its specificity.
1487: We will define these specific instances by inference rules.
1488:
1489: \subsection{Discussion on abstraction and narrowing positions}
1490: \label{sec:discussion}
1491:
1492: There are different ways to simulate the rewriting relation on ground
1493: terms, using abstraction and narrowing.
1494:
1495: For example, the abstraction positions can be chosen so that the
1496: abstraction mechanism captures the greatest possible number of
1497: rewriting steps. For that, we abstract the greatest subterms in the term, that
1498: are the immediate subterms of the term. Then, if a narrowing step
1499: follows, the abstracted term has to be narrowed in all possible ways
1500: at the top position only. This strategy may yield a deadlock if some
1501: of the direct subterms cannot be abstracted. We can instead abstract
1502: all greatest possible subterms of $t=f(t_1, \ldots , t_n)$. More
1503: concretely, we try to abstract $t_1, \ldots, t_n$ and, for each $t_i =
1504: g(t'_1,\ldots,t'_p)$ that cannot be abstracted, we try to abstract
1505: $t'_1,\ldots,t'_p$, and so on. In the worst case, we are driven to
1506: abstract leaves of the term, which are either variables, that do not
1507: need to be abstracted if they are abstraction variables, or constants.
1508:
1509: On the contrary, we can choose in priority the smallest
1510: possible subterms $u_i$, that are constants or variables. The ordering
1511: constraints $t > u_i$ needed to apply the induction hypothesis, and
1512: then to abstract the term, are easier to satisfy than in the previous
1513: case since the $u_i$ are smaller.
1514:
1515: Between these two cases, there are a finite
1516: but possibly big number of ways to choose the positions where terms
1517: are abstracted.
1518: Anyway it is not useful to abstract the subterms, whose
1519: ground instances are in normal form. Identifying these subterms is
1520: made in the same way that for the study of $\mathit{TERMIN(S,u)}$ (see
1521: Section~\ref{subsec:relaxing}).
1522:
1523: From the point of view of the narrowing step following the abstraction,
1524: there is no general optimal abstracting strategy either:
1525: the greater the term to be narrowed,
1526: the greater is the possible number of narrowing positions.
1527: On another side, more general the term to be narrowed,
1528: greater is the possible number of narrowing substitutions for a given redex.
1529:
1530:
1531:
1532: \subsection{How to combine the proof steps}
1533:
1534: The previous proof steps, applied to every
1535: reference term $t_{\mathit{ref}}=g(x_1,$ $\ldots ,x_m)$, where $x_1, \ldots ,x_m \in
1536: {\cal X}$ and $g \in \Def$,
1537: can be combined in the same way whatever $\mathit{S \in
1538: \{Innermost, Outermost, Local{-}Strat\}}$:
1539:
1540: \begin{center}
1541: %$\forall S \in \{Innermost, Outermost, Local{-}Strat\}$,\\
1542: $\mathit{Strat{-}Rules(S) = repeat^*(try(abstract), \; try(narrow), \; try(stop))}$.
1543: \end{center}
1544: \noindent
1545:
1546: $\mathit{"repeat^*}(T_1, \ldots, T_n)"$ repeats the strategies of the set
1547: $\{T_1, \ldots, T_n\}$ until it is not possible anymore.
1548: The operator $"try"$ is a generic operator that can be instantiated,
1549: following $S$, by
1550: $\mathit{try{-}skip(T)}$, expressing that the strategy or rule $T$
1551: is tried, and skipped when it cannot be applied, or by $\mathit{try{-}stop(T)}$,
1552: stopping the strategy if $T$ cannot be applied.
1553:
1554:
1555: \subsection{The termination theorem}
1556: For each strategy $\mathit{S \in \{Innermost, Outermost, Local{-}Strat\}}$,
1557: we write $\mathit{SUCCESS(g,}$ $\mathit{\succ)}$ if the application of $\mathit{Strat{-}Rules(S)}$
1558: on $(\{g(x_1, \ldots,$ $ x_m)\}, \top,\top)$
1559: gives a finite proof tree, whose sets $C$ of ordering constraints
1560: are satisfied by a same ordering $\succ$, and
1561: whose leaves
1562: are either states of the form $(\emptyset,A,C)$ or states
1563: whose set of constraints $A$ is unsatisfiable.
1564:
1565:
1566:
1567: \begin{subtheorem}
1568: \label{theo:termin}
1569: Let $R$ be a rewrite system on a set $\F$ of symbols containing at least a
1570: constructor constant. If there exists an $\F$-stable ordering $\succ$
1571: having the subterm property, such that for each symbol $g \in \Def$,
1572: we have $\mathit{SUCCESS(g,\succ)}$, then every term of $\TF$ terminates with
1573: respect to the strategy $S$.
1574:
1575: \end{subtheorem}
1576:
1577: %Remark that the noetherian property of $\succ$
1578: %is implied by $\F$-stability and the subterm property.
1579: %{\bf Peut-on supprimer la condition sur les constantes dans le cas des
1580: %strat lo? et pour l'outermost?(c'est fait ds le thme - a confirmer avec la preuve.)}\\
1581:
1582:
1583: We are now ready to instantiate this generic proof process, according
1584: to the different rewriting strategies.
1585:
1586: \section{The innermost case}
1587: \label{sec:innermost}
1588:
1589: %innermost.tex
1590: % IN-OUTERMOST/in-out-interne.tex
1591:
1592: \subsection{Abstraction and narrowing}
1593:
1594:
1595: When rewriting a ground instance of the current term according to the innermost
1596: principle, the ground instances of variables in the current term have to be
1597: normalized before a redex appears higher in the term. So the variable
1598: renaming performed before narrowing corresponds here to abstracting variables
1599: in the current term.
1600: Then, here, narrowing has only to be performed on terms of $\TFXA$.
1601:
1602: Moreover for the most general unifiers $\sigma$ produced during the proof process,
1603: all variables of $Ran(\sigma)$ are abstraction variables.
1604: Indeed, by Definition~\ref{def:abstraction-var},
1605: if $X \in Dom(\sigma)$, $\sigma X$ is in normal form,
1606: as well as $\theta X$ for any instantiation $\theta$.
1607: By definition of the innermost strategy, this requires that
1608: variables of $\sigma X$ can only be instantiated by terms in normal
1609: form, i.e. variables of $\sigma X$ are abstraction variables.
1610:
1611: Then, since before the first narrowing step, all variables are renamed into
1612: variables of $\XA$, and the narrowing steps only introduce variables of $\XA$,
1613: it is superfluous to rename the variables of the current term after the
1614: first narrowing step.
1615:
1616:
1617:
1618:
1619: \subsection{Relaxing the induction hypothesis}
1620: \label{subsec:relaxing-innermost}
1621:
1622: To establish $\mathit{TERMIN(Innermost,u)}$, a simple narrowing test of $u$ can
1623: first be tried. Except for the initial state, the variables of $u$ are
1624: in $\XA$. So if $u$ is not narrowable, or if $u$ is narrowable with a
1625: substitution $\sigma$ that is not compatible with $A$,
1626: then every ground instance of
1627: $u$ is in innermost normal form. Else, we compute the usable
1628: rules.
1629:
1630: When $t$ is a variable of $\X$, the usable
1631: rules of $t$ are $\R$ itself.
1632: When $t \in \XA,$ the set of usable rules of $t$ is
1633: empty, since the only possible instances of such a variable are ground terms
1634: in normal form.
1635:
1636: \begin{subdefinition}[\thesubtheorem\ Usable rules]
1637: Let $\R$ be a rewrite system on a set $\F$ of symbols.
1638: Let $Rls(f) = \{l \ra r \in \R \mid root(l)~= f\}$.
1639: For any $t \in \TFXXA$, the set of usable rules of $t$, denoted $\U(t)$,
1640: is defined by:
1641:
1642: \begin{itemize}
1643: \item $\U(t) = \R$ if $t \in \X$,
1644: \item $\U(t) = \emptyset$ if $t \in \XA$,
1645: \item $\U(f(u_1, \ldots ,u_n)) =
1646: Rls(f) \cup \bigcup_{i=1}^n \U(u_i) \cup \bigcup_{l \ra r \in Rls(f)} \U(r)$.
1647: \end{itemize}
1648: \end{subdefinition}
1649:
1650:
1651: \begin{sublemma}\label{lemma:U-correction}
1652: Let $\R$ be a rewrite system on a set $\F$ of symbols and $t \in \TFXXA$.
1653: Whatever $\alpha t$ ground instance of $t$ and
1654: $\alpha t \ra_{p_1,l_1 \ra r_1} t_1 \ra_{p_2,l_2 \ra r_2} t_2
1655: \ra \ldots \ra_{p_n,l_n \ra r_n} t_n$ rewrite chain starting from $\alpha t$,
1656: then $l_i \ra r_i \in \U(t), \; \forall i \in [1..n]$.
1657: \end{sublemma}
1658:
1659:
1660: A sufficient criterion for ensuring standard
1661: termination (and then innermost termination) of
1662: {\ any ground instance of} a term $t$ can be given.
1663:
1664: \begin{subproposition}\label{prop:TC}
1665: Let $\R$ be a rewrite system on a set $\F$ of symbols, and $t$ a term of $\TFXN$.
1666: If there exists a simplification ordering $\succ$ such that
1667: $\forall l \ra r \in \U(t): l \succ r$, then any ground instance of $t$
1668: is terminating.
1669: \end{subproposition}
1670:
1671:
1672: \subsection{The innermost termination proof procedure}
1673:
1674: The inference rules \rname{Abstract}, \rname{Narrow} and \rname{Stop}
1675: instantiate respectively the proof steps
1676: \emph{abstract}, \emph{narrow}, and \emph{stop} defined in
1677: Section~\ref{sec:proof-steps}.
1678: They are given in Table~\ref{innermost-inference}.
1679: Their application conditions depend on whether
1680: satisfiability of $A$ or unsatisfiability of $A$ is checked. These conditions are
1681: specified in Tables~\ref{conditions-satisfiability-A} and
1682: \ref{conditions-unsatisfiability-A} respectively.
1683:
1684:
1685:
1686: \begin{table*}
1687: \centering
1688: \caption{Inference rules for the innermost strategy}
1689: \label{innermost-inference}
1690: \framebox[\textwidth]{
1691: %\framebox[30pc]{
1692: \begin{minipage}{\textwidth}
1693: \setlength{\parindent}{0pt}
1694: \setlength{\parskip}{2ex}
1695:
1696: %\linewidth
1697:
1698:
1699:
1700: \wcinfr{~Abstract}
1701: { \{t\},~~A,~~C }
1702: { \{u\},~A \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con X_{i_p},
1703: ~C \wedge H_C(t|_{i_1}) \ldots \wedge H_C(t|_{i_p})}
1704: {{\rm ~where~} t {\rm ~is~abstracted~into~}
1705: u {\rm~at~positions~} i_1, \ldots ,i_p \neq \epsilon}
1706: {\rm ~if~ \mathit{COND{-}ABSTRACT}}
1707:
1708:
1709:
1710: \cinfr{~Narrow}
1711: { \{t\},~~A,~~C }
1712: { \{u\},~~A \wedge \sigma, ~~ C}
1713: {t \surred_{R}^{Inn,\sigma} u {\rm ~and~} {\rm \mathit{COND{-}NARROW}}}
1714:
1715:
1716:
1717: \cinfr{~Stop}
1718: { \{t\},~~A,~~C }
1719: { \emptyset,~~A \wedge H_A(t),~~C \wedge H_C(t)}
1720: {\mathit{COND{-}STOP}}
1721:
1722: %\begin{tabular}{lcr}
1723: ${\rm ~and~} H_A(t) =
1724: \left\{
1725: \begin{array}{ll}
1726: \mathit{\top} & {\rm ~if~any~ground~instance~of~} t \\
1727: & {\rm ~is~in~normal~form}\\
1728: t \con X & {\rm ~otherwise.}
1729: \end{array}
1730: \right.
1731: $
1732: \\
1733: %&
1734: %~
1735: %&
1736: $ ~~~~~~~~H_C(t) =
1737: \left\{
1738: \begin{array}{ll}
1739: \mathit{\top} & {\rm ~if~} \mathit{TERMIN(Innermost,t)}\\
1740: t_{\mathit{ref}}>t & {\rm ~otherwise.}
1741: \end{array}
1742: \right.
1743: $
1744: %\end{tabular}
1745:
1746:
1747: \end{minipage}}
1748: \end{table*}
1749:
1750: %
1751: %{\bf Les ip sont des positions ds les termes a abstraire plutot que
1752: %des indices...}\\
1753:
1754: %{\bf Attention: j'ai reintroduit le $H_A(t)$ dans Stop (pour les 3 strategies),
1755: %car dans les cas
1756: %particulier ou le terme courant a toutes ses instances closes en forme normale,
1757: %on n'abstrait pas (en effet, c'est stipule dans les tactiques d'abstraction),
1758: %donc on ne doit pas poser $t \con X$.}
1759:
1760: %Il y a toutefois une petite inexactitude car j'ai mis ``if TERMIN(t)'',
1761: %et c'est seulement si ``toutes les instances closes de $t$ sont en forme normale''.
1762: %Ce qu'on ne peut mettre dans les regles d'inference, car ce sont les conditions - op%erationnelles- dans lesquelles on n'abstrait pas (voir Section 5.1).}
1763:
1764: As said above, the ground terms whose termination is studied are
1765: defined by the solutions of $A$.
1766: When satisfiability of $A$ is checked at each inference step, the nodes of the proof
1767: tree exactly model the ground terms generated during the rewriting
1768: derivations. Satisfiability of $A$, although undecidable in general,
1769: can be proved by exhibiting a ground substitution satisfying the
1770: constraints of $A$.
1771:
1772:
1773: When satisfiability of $A$ is not checked, nodes are generated in the
1774: proof tree, that can represent empty sets of ground terms, so the
1775: generated proof trees can have branches that do not represent any derivation on the
1776: ground terms. The unsatisfiability test of $A$ is only used to stop
1777: the development of meaningless branches as soon as possible, with
1778: the sufficient conditions presented in Section~\ref{subsec:cumulating-constraints}.
1779:
1780: \begin{table*}
1781: \centering
1782: \caption{Conditions for inference rules dealing with satisfiability of
1783: $A$}
1784: \label{conditions-satisfiability-A}
1785: \framebox[\textwidth]{
1786: %\framebox[30pc]{
1787: \begin{minipage}{\textwidth}
1788: \setlength{\parindent}{0pt}
1789: \setlength{\parskip}{2ex}
1790:
1791:
1792: %\begin{itemize}
1793: ${\rm \mathit{~COND{-}ABSTRACT:~~}}
1794: { (A \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con X_{i_p})}\\
1795: {\rm ~and~} (C \wedge H_C(t|_{i_1}) \ldots \wedge H_C(t|_{i_p})) \;
1796: {\rm ~are~satisfiable}$
1797:
1798: ${\rm \mathit{~COND{-}NARROW:~~}}
1799: {A \wedge \sigma} {\rm { ~is~satisfiable}}$
1800:
1801: ${\rm \mathit{~COND{-}STOP:~~}}
1802: { (A \wedge H_A(t))} {\rm ~and~} (C \wedge H_C(t))
1803: {\rm ~are~satisfiable}$
1804: %\end{itemize}
1805:
1806: \end{minipage}}
1807: \end{table*}
1808:
1809:
1810: \begin{table*}
1811: \centering
1812: \caption{Conditions for inference rules dealing with unsatisfiability of $A$}
1813: \label{conditions-unsatisfiability-A}
1814: \framebox[\textwidth]{
1815: %\framebox[30pc]{
1816: \begin{minipage}{\textwidth}
1817: \setlength{\parindent}{0pt}
1818: \setlength{\parskip}{2ex}
1819:
1820: %\linewidth
1821: %\begin{itemize}
1822: ${\rm \mathit{~COND{-}ABSTRACT:~~}}
1823: C \wedge H_C(t|_{i_1}) \ldots \wedge H_C(|t_{i_p}) {\rm ~is~satisfiable}$
1824:
1825: ${\rm \mathit{~COND{-}NARROW:~~}}
1826: true $
1827:
1828: ${\rm \mathit{~COND{-}STOP:~~}}
1829: (C \wedge H_C(t)) {\rm ~is~satisfiable~or~} {A} {\rm ~is~unsatisfiable}. $
1830:
1831: %\end{itemize}
1832:
1833: \end{minipage}}
1834: \end{table*}
1835:
1836:
1837:
1838: Once instantiated, the generic strategy $\mathit{Strat{-}Rules(S)}$ simply becomes:
1839:
1840: \begin{center}
1841: $\mathit{repeat*(try{-}skip(\rname{Abstract}); try{-}stop(\rname{Narrow});
1842: try{-}skip(\rname{Stop}))}$
1843: \end{center}
1844: with conditions of Table~\ref{conditions-satisfiability-A}, and
1845: \begin{center}
1846: $\mathit{repeat*(try{-}skip(\rname{Abstract}); try{-}skip(\rname{Narrow});
1847: try{-}skip(\rname{Stop}))}$
1848: \end{center}
1849: with conditions of Table~\ref{conditions-unsatisfiability-A}.
1850: Note that \rname{Narrow} with conditions of
1851: Table~\ref{conditions-satisfiability-A} is the only rule stopping the
1852: proof procedure when it cannot be applied: in this case, when $A \wedge \sigma$
1853: is satisfiable, the narrowing step can be applied, while, if
1854: satisfiability of $A \wedge \sigma$ cannot be proved, the procedure must
1855: stop.
1856:
1857: The procedure can diverge, with infinite alternate applications
1858: of \rname{Abstract} and \rname{Narrow}. With conditions of
1859: Table~\ref{conditions-satisfiability-A}, it can stop on \rname{Narrow} with
1860: at least in a branch of the proof tree, a state of the form $(\{t\} \neq
1861: \emptyset,A,C)$. In both cases, nothing can be said on termination.
1862: Termination is proved when, for all proof trees, the procedure stops with an
1863: application of \rname{Stop} on each branch, generating only final
1864: states of the form $(\emptyset,A,C)$.\\
1865:
1866:
1867: According to the strategy $\mathit{Strat{-}Rules(Innermost)}$, testing satisfiability of $A$ in conditions of
1868: Table~\ref{conditions-satisfiability-A}
1869: can be optimized on the basis of the following remarks.
1870: In the first application of \rname{Abstract} for each initial state,
1871: $(A \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con X_{i_p}) =
1872: (\top \wedge x_1 \con X_1 \ldots \wedge x_m \con X_m)$, which is
1873: always satisfiable, since the signature admits at least a constructor constant.
1874: Moreover, the following possible current application of \rname{Abstract}
1875: comes after an application of \rname{Narrow}, for which it has been
1876: checked that $A \wedge \sigma {\rm {\bf ~is~satisfiable}}$. So
1877: $(A \wedge \sigma \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con
1878: X_{i_p})$ is also satisfiable since $X_{i_1}, \ldots, X_{i_p}$ are
1879: fresh variables, not used in $A \wedge \sigma$.
1880: So it is useless to verify satisfiability of
1881: $(A \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con X_{i_p})$
1882: in $\mathit{COND{-}ABSTRACT}$.
1883:
1884: In a similar way, as \rname{Stop} is applied with a current
1885: abstraction constraint formula $A$, which is satisfiable,
1886: $A \wedge t \con X$ is also satisfiable since $X$ is a
1887: fresh variable, not used in $A$.
1888: So it is also useless to verify that $A \wedge t \con X$
1889: is satisfiable in $\mathit{COND{-}STOP}$.
1890:
1891: This leads to the conditions expressed in
1892: Table~\ref{conditions-satisfiability-A-optimized}, simplifying those
1893: of Table~\ref{conditions-satisfiability-A}.
1894:
1895:
1896: \begin{table*}
1897: \centering
1898: \caption{Conditions for inference rules dealing with satisfiability of
1899: $A$}
1900: \label{conditions-satisfiability-A-optimized}
1901: \framebox[\textwidth]{
1902: %\framebox[30pc]{
1903: \begin{minipage}{\textwidth}
1904: \setlength{\parindent}{0pt}
1905: \setlength{\parskip}{2ex}
1906:
1907:
1908: %\begin{itemize}
1909: ${\rm \mathit{~COND{-}ABSTRACT:~~}}
1910: (C \wedge H_C(t|_{i_1}) \ldots \wedge H_C(t|_{i_p})) \;
1911: {\rm ~is~satisfiable}$
1912:
1913: ${\rm \mathit{~COND{-}NARROW:~~}}
1914: A \wedge \sigma {\rm ~is~satisfiable}$
1915:
1916: ${\rm \mathit{~COND{-}STOP:~~}}
1917: (C \wedge H_C(t))
1918: {\rm ~is~satisfiable}$
1919: %\end{itemize}
1920:
1921: \end{minipage}}
1922: \end{table*}
1923:
1924:
1925:
1926:
1927: \subsection{Examples}
1928:
1929: For a better readability, when a constrained substitution $\sigma$ is
1930: added to the ACF $A$, we propagate the new constraint $\sigma$ into $A$
1931: in applying the substitution part $\sigma_0$ of $\sigma$ to $A$.
1932:
1933:
1934:
1935:
1936: \begin{subexample}
1937:
1938: Let \(R\) be the previous example of Toyama.
1939: We prove that $R$ is innermost terminating on $\TF$, where $\F =\{f\!:\!3, g\!:\!2, 0\!:\!0, 1\!:\!0\}$.
1940:
1941: \[
1942: \begin{array}{ll}
1943: f(0,1,x) \ra f(x,x,x)\\
1944: g(x,y) \ra x \\
1945: g(x,y) \ra y\\
1946: \end{array}
1947: \]
1948:
1949:
1950: The defined symbols of $\F$ are here $f$ and $g$.
1951: Applying the rules on $f(x_1,x_2,x_3)$, we get:
1952:
1953: \footnotesize{
1954: $$
1955: \xymatrix{
1956: \txt{
1957: $t_{ref} = f(x_1, x_2, x_3)$\\
1958: $A = \top$\\
1959: $C = \top$
1960: } \ar[d]|-{\txt{\footnotesize \rname{Abstract}}}\\
1961: \txt{
1962: $f(X_1,X_2,X_3)$\\
1963: $A = (x_1 \con X_1 \wedge x_2 \con X_2 \wedge x_3 \con X_3)$\\
1964: $C = (f(x_1,x_2,x_3) > x_1, x_2, x_3)$
1965: }
1966: \ar[d]^-{\txt{\footnotesize \rname{Narrow}}}_-{\sigma = (X_1 = 0 \wedge X_2 = 1)}\\
1967: \txt{
1968: $f(X_3,X_3,X_3)$\\
1969: $A = (x_1 \con X_1 \wedge x_2 \con X_2 \wedge x_3 \con X_3)$\\
1970: $C = (f(x_1,x_2,x_3) > x_1, x_2, x_3)$
1971: }
1972: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}\\
1973: \txt{
1974: $\emptyset$\\
1975: $A = (x_1 \con X_1 \wedge x_2 \con X_2 \wedge x_3 \con X_3)$\\
1976: $C = (f(x_1,x_2,x_3) > x_1, x_2, x_3)$
1977: }
1978: }
1979: $$
1980: }
1981: \normalsize
1982:
1983:
1984: \rname{Abstract} applies since $f(x_1,x_2,x_3) > x_1,x_2,x_3$
1985: is satisfiable by any simplification ordering.
1986:
1987:
1988: If we are using the conditions for inference rules dealing with satisfiability of $A$
1989: given in Table~\ref{conditions-satisfiability-A-optimized}, we have to justify the \rname{Narrow} application.
1990: Here, \rname{Narrow} applies because $A \wedge \sigma= (x_1 \con 0 \wedge x_2 \con 1 \wedge x_3 \con X_3)$, where
1991: $\sigma = (X_1=0 \wedge X_2=1)$,
1992: is satisfiable by any ground instantiation $\theta$ such that
1993: $\theta x_1 = 0$, $\theta x_2 = 1$ and $\theta x_3 = \theta X_3 = 0$.
1994:
1995: Then \rname{Stop} applies because $f(X_3,X_3,X_3)$ is a non narrowable term whose all variables
1996: are abstraction variables, and hence we have
1997: $\mathit{TER\-MIN(Innermost, f(X_3,X_3,}$ $\mathit{X_3))}$.
1998:
1999: Considering now $g(x_1,x_2)$, we get:
2000:
2001:
2002: \footnotesize{
2003: $$
2004: \xymatrix{
2005: & \txt{
2006: $t_{ref} = g(x_1,x_2)$\\
2007: $A = \top$\\
2008: $C = \top$
2009: }
2010: \ar[d]|-{\txt{\footnotesize \rname{Abstract}}}
2011: &\\
2012: & \txt{
2013: $g(X_1, X_2)$\\
2014: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2015: $C = (g(x_1,x_2) > x_1,x_2)$
2016: }
2017: \ar[dl]_-{\txt{\footnotesize \rname{Narrow}}}^-{\sigma = Id}
2018: \ar[dr]^-{\txt{\footnotesize \rname{Narrow}}}_-{\sigma = Id} & \\
2019: \txt{}
2020: && \txt{}
2021: }
2022: $$
2023: \vspace{-4mm}
2024: $$
2025: \xymatrix{
2026: \txt{
2027: $X_1$\\
2028: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2029: $C = (g(x_1,x_2) > x_1,x_2)$
2030: }
2031: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}
2032: &&
2033: \txt{
2034: $X_2$\\
2035: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2036: $C = (g(x_1,x_2) > x_1,x_2)$
2037: }
2038: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}\\
2039: \txt{
2040: $\emptyset$\\
2041: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2042: $C = (g(x_1,x_2) > x_1,x_2)$
2043: }
2044: &&
2045: \txt{
2046: $\emptyset$\\
2047: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2048: $C = (g(x_1,x_2) > x_1,x_2)$
2049: }
2050: }
2051: $$
2052: }
2053: \normalsize
2054:
2055: %Attention au renommage des variables. Que fait-on au final ?
2056: %Quand $\sigma$ n'est pas l'identite, on introduit automatiquement des variables
2057: %fraiches (voir remarque apres Def. 8).
2058: %Mais quand c'est l'identite, ne devrait-on pas plutot mettre un renommage?
2059: %NON! finalement... voir narrowing lemmma.
2060:
2061: \rname{Abstract} applies since $g(x_1,x_2) > x_1,x_2$
2062: is satisfiable by any simplification ordering.
2063:
2064: Again, we have to justify the \rname{Narrow} application.
2065: Here, \rname{Narrow} applies because $A \wedge \sigma =
2066: (x_1 \con X_1 \wedge x_2 \con X_2)$, where
2067: $\sigma = Id$,
2068: is satisfiable by any ground instantiation $\theta$ such that
2069: $\theta x_1 = \theta X_1 = 0$ and $\theta x_2 = \theta X_2 = 0$.
2070:
2071: Then \rname{Stop} applies on both branches because $X_1$ and $X_2$
2072: are abstraction variables,
2073: hence we trivially have $\mathit{TERMIN(Innermost, X_1)}$ and
2074: $\mathit{TERMIN(Innermost,}$ $\mathit{X_2)}$.
2075:
2076: \end{subexample}
2077:
2078:
2079:
2080: %Let us cite the example $\{f(f(x)) \ra f(f(x)), f(a) \ra a\}$,
2081: %that is innermost terminating on the ground term algebra,
2082: %while it is not on the free term one. To our knowledge, our method is
2083: %the only one to treat such examples.
2084: %{\bf le garder ?}
2085:
2086: \begin{subexample}
2087: Let us now give an example illustrating how the usable rules can be helpful and why detecting
2088: unsatisfiability of $A$ can be important.
2089: Let us consider the following system $\R$:
2090: \[
2091: \begin{array}{lll}
2092: plus(x,0) & \ra x & (1)\\
2093: plus(x,s(y)) & \ra s(plus(x,y)) & (2)\\
2094: f(0,s(0),x) & \ra f(x,plus(x,x),x) & (3)\\
2095: g(x,y) & \ra x & (4)\\
2096: g(x,y) & \ra y & (5)
2097: \end{array}
2098: \]
2099: Let us first remark that $\R$ is not terminating, as illustrated by
2100: the following cycle, where successive redexes are underlined:\\
2101:
2102: \footnotesize{
2103: $
2104: \begin{array}{ll}
2105: \underline{f(0,s(0),g(0,s(0)))}
2106: & \ra^{(3)} f(\underline{g(0,s(0))}, plus(g(0,s(0)),g(0,s(0))), g(0,s(0)))\\
2107: & \ra^{(4)} f(0, plus(\underline{g(0,s(0))},g(0,s(0))), g(0,s(0)))\\
2108: & \ra^{(5)} f(0, plus(s(0),\underline{g(0,s(0))}), g(0,s(0)))\\
2109: & \ra^{(4)} f(0, \underline{plus(s(0),0)}, g(0,s(0)))\\
2110: & \ra^{(1)} \underline{f(0, s(0), g(0,s(0)))}\\
2111: & \ra^{(3)} \ldots
2112: \end{array}
2113: $
2114: }
2115: \normalsize
2116:
2117: Let us prove the innermost termination of $\R$ on $\TF$,
2118: where $\F = \{0\!:\!0, s\!:\!1, plus\!:\!2, g\!:\!2, f\!:\!3\}$.
2119: The defined symbols of $\F$ are $f, plus$ and $g$.
2120:
2121: Let us apply the inference rules checking unsatisfiability of $A$,
2122: whose conditions are given in Table~\ref{conditions-unsatisfiability-A}.
2123: Applying the rules on $f(x_1,x_2,x_3)$, we get:
2124:
2125: \footnotesize{
2126: $$
2127: \xymatrix{
2128: \txt{
2129: $f(x_1,x_2,x_3)$\\
2130: $A = \top$\\
2131: $C = \top$
2132: }
2133: \ar[d]|-{\txt{\footnotesize \rname{Abstract}}}
2134: \\
2135: \txt{
2136: $f(X_1,X_2,X_3)$\\
2137: $A = (x_1 \con X_1 \wedge x_2 \con X_2 \wedge x_3 \con X_3)$\\
2138: $C = f(x_1,x_2,x_3) > x_1,x_2,x_3$
2139: }
2140: \ar[d]^-{\txt{\footnotesize \rname{Narrow}}}_-{\sigma = (X_1=0 \wedge X_2 = s(0))}
2141: \\
2142: \txt{
2143: $f(X_3,plus(X_3,X_3),X_3)$\\
2144: $A = (x_1 \con 0 \wedge x_2 \con s(0) \wedge x_3 \con X_3)$\\
2145: $C = f(x_1,x_2,x_3) > x_1,x_2,x_3$
2146: }
2147: \ar[d]|-{\txt{\footnotesize \rname{Abstract}}}
2148: \\
2149: \txt{
2150: $f(X_3,X_4,X_3)$\\
2151: $A = (x_1 \con 0 \wedge x_2 \con s(0) \wedge x_3 \con X_3 \wedge plus(X_3,X_3) \con X_4)$\\
2152: $C = f(x_1,x_2,x_3) > x_1,x_2,x_3$
2153: }
2154: \ar[d]^-{\txt{\footnotesize \rname{Narrow}}}_-{\sigma = (X_3=0 \wedge X_4 = s(0))}
2155: \\
2156: \txt{
2157: $f(0,plus(0,0),0)$\\
2158: $A = (x_1 \con 0 \wedge x_2 \con s(0) \wedge x_3 \con 0 \wedge plus(0,0) \con s(0))$\\
2159: $C = f(x_1,x_2,x_3) > x_1,x_2,x_3$
2160: }
2161: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}
2162: \\
2163: \txt{
2164: $\emptyset$\\
2165: $A = (x_1 \con 0 \wedge x_2 \con s(0) \wedge x_3 \con 0 \wedge plus(0,0) \con s(0))$\\
2166: $C = f(x_1,x_2,x_3) > x_1,x_2,x_3$
2167: }
2168: }
2169: $$
2170: }
2171: \normalsize
2172:
2173: The first \rname{Abstract} applies since $f(x_1,x_2,x_3) > x_1,x_2,x_3$
2174: is satisfiable by any simplification ordering.
2175:
2176: Since we are using the inference rules checking unsatisfiability of $A$
2177: given in Table~\ref{conditions-unsatisfiability-A}, we do not have to justify
2178: the \rname{Narrow} applications.
2179:
2180: The second \rname{Abstract} applies by using the $\mathit{TERMIN}$ predicate.
2181: Indeed, the usable rules of $plus(X_3,X_3)$ consist of the system
2182: $\{plus(x,0)$ $ \ra x, plus(x,s(y)) \ra s(plus(x,y))\}$, that can be
2183: proved terminating with any precedence based ordering,
2184: independent of the induction ordering, with the
2185: precedence $plus \succ_{\F} s$, which ensures the property
2186: $\mathit{TERMIN(Innermost, plus(X_3,X_3))}$.
2187: Without abstraction here, the process would have generated a branch
2188: containing an infinite number of \rname{Narrow} applications.
2189:
2190: Finally, \rname{Stop} applies because the constraint $A$ becomes unsatisfiable.
2191: Indeed, it contains the abstraction constraint $plus(0,0) \con s(0)$, which is
2192: not true since the unique normal form of $plus(0,0)$ is $0$.
2193: Note that if we would have chosen to apply the inference rules checking
2194: satisfiability of $A$, whose conditions are given in
2195: Table~\ref{conditions-satisfiability-A-optimized},
2196: then the last narrowing step would not have applied, and would have been
2197: replaced by a \rname{Stop} application.
2198:
2199: Considering now $g(x_1,x_2)$, we get:
2200:
2201: \footnotesize{
2202: $$
2203: \xymatrix{
2204: & \txt{
2205: $t_{ref} = g(x_1,x_2)$\\
2206: $A = \top$\\
2207: $C = \top$
2208: }
2209: \ar[d]|-{\txt{\footnotesize \rname{Abstract}}}
2210: &\\
2211: & \txt{
2212: $g(X_1, X_2)$\\
2213: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2214: $C = (g(x_1,x_2) > x_1,x_2)$
2215: }
2216: \ar[dl]_-{\txt{\footnotesize \rname{Narrow}}}^-{\sigma = Id}
2217: \ar[dr]^-{\txt{\footnotesize \rname{Narrow}}}_-{\sigma = Id} & \\
2218: \txt{}
2219: && \txt{}
2220: }
2221: $$
2222: \vspace{-4mm}
2223: $$
2224: \xymatrix{
2225: \txt{
2226: $X_1$\\
2227: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2228: $C = (g(x_1,x_2) > x_1,x_2)$
2229: }
2230: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}
2231: &&
2232: \txt{
2233: $X_2$\\
2234: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2235: $C = (g(x_1,x_2) > x_1,x_2)$
2236: }
2237: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}\\
2238: \txt{
2239: $\emptyset$\\
2240: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2241: $C = (g(x_1,x_2) > x_1,x_2)$
2242: }
2243: &&
2244: \txt{
2245: $\emptyset$\\
2246: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2247: $C = (g(x_1,x_2) > x_1,x_2)$
2248: }
2249: }
2250: $$
2251: }
2252: \normalsize
2253:
2254: \rname{Abstract} applies since $g(x_1,x_2) > x_1,x_2$
2255: is satisfiable by the previous precedence based ordering.
2256: \rname{Stop} applies on both branches because $X_1$ and $X_2$
2257: are abstraction variables,
2258: so we trivially have $\mathit{TERMIN(Innermost, X_1)}$ and
2259: $\mathit{TERMIN(Innermost,}$ $\mathit{X_2)}$.
2260:
2261: Let us finally apply the inference rules of Table~\ref{conditions-unsatisfiability-A}
2262: on $plus(x_1,x_2)$:
2263:
2264: \footnotesize{
2265: $$
2266: \xymatrix{
2267: &
2268: \txt{
2269: $plus(x_1,x_2)$\\
2270: $A = \top$\\
2271: $C = \top$
2272: }
2273: \ar[d]|-{\txt{\footnotesize \rname{Abstract}}}
2274: &
2275: \\
2276: &
2277: \txt{
2278: $plus(X_1,X_2)$\\
2279: $A = (x_1 \con X_1 \wedge x_2 \con X_2)$\\
2280: $C = plus(x_1,x_2) > x_1,x_2$
2281: }
2282: \ar[dl]_-{\txt{\footnotesize \rname{Narrow}}}^{\sigma = (X_2=0)}
2283: \ar[dr]^-{\txt{\footnotesize \rname{Narrow}}}_{\sigma = (X_2=s(X_3))~~~~}
2284: &
2285: \\
2286: \txt{}
2287: && \txt{}
2288: }
2289: $$
2290: \vspace{-4mm}
2291: $$
2292: \xymatrix{
2293: \txt{
2294: $X_1$\\
2295: $A = (x_1 \con X_1 \wedge x_2 \con 0)$\\
2296: $C = plus(x_1,x_2) > x_1,x_2$
2297: }
2298: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}
2299: &&
2300: \txt{
2301: $s(plus(X_1,X_3))$\\
2302: $A = (x_1 \con X_1 \wedge x_2 \con s(X_3))$\\
2303: $C = plus(x_1,x_2) > x_1,x_2$
2304: }
2305: \ar[d]|-{\txt{\footnotesize \rname{Stop}}}
2306: \\
2307: \txt{
2308: $\emptyset$\\
2309: $A = (x_1 \con X_1 \wedge x_2 \con 0)$\\
2310: $C = plus(x_1,x_2) > x_1,x_2$
2311: }
2312: &&
2313: \txt{
2314: $\emptyset$\\
2315: $A = (x_1 \con X_1 \wedge x_2 \con s(X_3))$\\
2316: $C = plus(x_1,x_2) > x_1,x_2$
2317: }
2318: }
2319: $$
2320: }
2321: \normalsize
2322:
2323: \rname{Abstract} applies since $g(x_1,x_2) > x_1,x_2$
2324: is satisfiable by the previous precedence based ordering.
2325: \rname{Stop} applies on the left branch because $X_1$ is an abstraction variable,
2326: hence we trivially have $\mathit{TERMIN(Innermost, X_1)}$.
2327: \rname{Stop} applies on the right branch by using the $\mathit{TER\-MIN}$ predicate.
2328: Indeed, the usable rules of $s(plus(X_1,X_3))$ consist of the previous
2329: terminating system
2330: $\{plus$ $(x,0) \ra x, plus(x,s(y)) \ra s(plus(x,y))\}$.
2331:
2332:
2333: \end{subexample}
2334:
2335:
2336:
2337: \section{The outermost case}
2338: \label{sec:outermost}
2339:
2340:
2341: %outermost.tex
2342: % OUTERMOST/out-wrla.tex
2343:
2344: \subsection{Abstraction}
2345: \label{subsec:abstraction}
2346:
2347:
2348: %% {\bf On a supprime la strat d'abstraction. Faut-il en parler pour
2349: %% les exemples ? Non c'est dit ailleurs.}
2350:
2351:
2352: According to the outermost strategy, abstraction can be performed on
2353: subterms $t_i$ only if
2354: during their normalization, the $t_i$ do not introduce outermost
2355: redexes higher in the term $t$.
2356: More formally, the induction hypothesis is applied to the subterms
2357: $t|_{p_1}, \ldots ,t|_{p_n}$ of the current term $t$, provided
2358: $\alpha t_{\mathit{ref}} \succ \alpha t|_{p_1}, \ldots ,\alpha t|_{p_n}$
2359: for every ground substitution $\alpha$,
2360: for the induction ordering $\succ$
2361: and provided $u = t[y_1]_{p_1}$ $ \ldots [y_n]_{p_n}$ is not narrowable
2362: at prefix positions of $p_1,\ldots, p_n$, for
2363: the outermost narrowing relation defined below.
2364:
2365: As already mentioned in Section~\ref{subsec:relaxing}, if in addition,
2366: the variables of
2367: $u$ are all in $\XA$, and $u$ is not narrowable, then every ground
2368: instance of the term $u$ outermost terminates.
2369:
2370:
2371:
2372: \subsection{The narrowing mechanism}
2373:
2374:
2375: Outermost narrowing is defined by Definition~\ref{def:narrowing},
2376: where a $S$-better position is a prefix position.
2377: In order to support intuition, let us consider for instance the
2378: system $\{f(g(a))\ra a, f(f(x)) \ra b, g(x) \ra f(g(x))\}$.
2379: With the standard narrowing relation used at the outermost position,
2380: $f(g(x_1))$ only narrows into $a$ with the first rule and the
2381: substitution $\sigma=(x_1=a)$.
2382: With the outermost narrowing relation,
2383: $f(g(x_1))$ narrows into $a$ with the first rule and $\sigma=
2384: (x_1=a)$, and into $f(f(g(x_2)))$ with the third rule and
2385: the constrained substitution
2386: $\sigma=(x_1=x_2 \wedge x_2 \neq a)$.
2387:
2388: The variables of the narrowed terms are in $\X \cup \XA$:
2389: as we will see, renaming variables
2390: of $\X$ still gives variables of $\X$, and abstraction,
2391: replacing subterms by variables of $\XA$, may not cover all
2392: variables of $\X$ in the abstracted term.
2393:
2394:
2395: In the outermost termination proof,
2396: the variable renaming performed before the narrowing step
2397: has a crucial meaning for the schematization of outermost derivations.
2398: %{\bf Mais pourquoi est-ce plus qu'un renommage? parce qu'on linearise!}
2399: This renaming, applied on the current term $g(x_1, \ldots ,x_m)$,
2400: replaces the variable occurrences $x_1,\ldots,x_m$ by new and all
2401: different variables $x'_1,\ldots,$ $x'_m$, defined as follows.
2402: Given any ground instance $\alpha g(x_1, \ldots ,x_m)$ of
2403: $g(x_1, \ldots ,$ $x_m)$, the $x'_1,\ldots,x'_m$ represent
2404: the first reduced form of $\alpha x_1,\ldots, \alpha x_m$
2405: generating an outermost reduction higher
2406: in the term (here, at the top),
2407: in any outermost rewriting chain starting from
2408: $\alpha g(x_1, \ldots ,x_m)$.
2409: This replacement is memorized in a reduction formula before applying
2410: a step of outermost narrowing to $g(x'_1,$ $\ldots ,x'_m)$.
2411: The abstraction variables are not renamed: since their ground instances
2412: are in normal form, they are not concerned by the rewriting chain schematized by
2413: the variable renaming.
2414:
2415: Formally, the definition of the variable replacement
2416: performed before a narrowing step is the following.
2417:
2418: \begin{subdefinition}
2419: \label{def:renaming-red}
2420: Let $t \in \TXF$ be a term whose variable occurrences from left to
2421: right in $t$ are $x_1,\ldots,x_m$.
2422: The reduction renaming of $t$, noted $\rho = (x_1 \red x'_1)...(x_m \red x'_m)$,
2423: consists in replacing the $x_i$ by new and all different variables $x'_i$ in
2424: $t$, giving a term $t^\rho$. This is denoted by the so-called reduction formula
2425: \begin{center}
2426: $ R(t)= t \red t^\rho$.
2427: \end{center}
2428: \end{subdefinition}
2429:
2430: Notice that the reduction renaming linearizes the term. For instance,
2431: the two occurrences of $x$ in $g(x,x)$ are respectively renamed into
2432: $x'_1$ and $x'_2$, and $g(x,x) \red g(x'_1, x'_2)$.
2433:
2434:
2435: \begin{subdefinition}
2436: \label{sat-red-formula}
2437: Let $t \in \TXF$ be a term whose variable occurrences from left to
2438: right are $x_1,\ldots,x_m$,
2439: at positions $p_1,\ldots,p_m$ respectively.
2440: A ground substitution $\theta$ satisfies the reduction formula
2441: $ R(t)= t \red t^\rho$, where $\rho = (x_1 \red x'_1)...(x_m \red x'_m)$,
2442: iff there exists an outermost rewriting chain
2443: $\theta t \ra^{* out}_{p \not \in \OS(t)} \theta t^\rho
2444: \ra^{out}_{p \in \OS(t)} u$, i.e. such that:
2445: \begin{itemize}
2446: \item either $t [\theta x'_1]_{p_1} \ldots [\theta x'_m]_{p_m}$
2447: is the first reduced form of
2448: $\theta t = t [\theta x_1]_{p_1}$ $ \ldots [\theta x_m]_{p_m}$
2449: on this chain
2450: having an outermost rewriting position
2451: at a non variable position of $t$, if this position exists,
2452:
2453: \item or
2454: $\theta x'_1 = (\theta x_1\da), \ldots, \theta x'_m = (\theta x_m\da)$
2455: if there is no such position.
2456: \end{itemize}
2457:
2458: \end{subdefinition}
2459:
2460:
2461:
2462:
2463: Before going on, a few remarks on this definition can be made.
2464: In the second case of satisfiability, $t[\theta x_1 \da]_1 \ldots
2465: [\theta x_m \da]_m$ is in normal form.
2466: In any case, $ R(t)$ is always satisfiable~:
2467: it is sufficient to take a ground substitution $\theta$ such that
2468: $t[\theta x_1]_{p_1} \ldots [\theta x_m]_{p_m}$ has an outermost
2469: rewriting position at a non variable position of $t$,
2470: and then to extend its domain $\{x_1, \ldots, x_m\}$ to
2471: $\{x_1, \ldots, x_m, x'_1, \ldots, x'_m\}$ by choosing
2472: for each $i \in \{1,...,m\}$, $\theta x'_i = \theta x_i$.
2473: If such a substitution does not exist, then every ground instance
2474: of $t$ has no outermost rewriting position at a non variable
2475: position of $t$, and it is sufficient to take a ground substitution
2476: $\theta$ such that
2477: $\theta x_1 = \ldots = \theta x_m = \theta x'_1 = \ldots = \theta x'_m =
2478: u$, with $u$ any ground term in normal form.
2479:
2480:
2481: However, there may exist several instantiations solution of such constraints.
2482: Let us consider for instance the rewrite system
2483: $R= \{f(a) \ra f(c), b \ra a\}$ and the reduction formula
2484: $R(f(x)) = f(x) \red f(x')$. The substitution
2485: $\theta_1(x) = \theta_1(x') = a$ and
2486: $\theta_2(x) = b, \theta_2(x') = a$ are two distinct solutions.
2487: With the substitution $\theta_2$, $f(a)$ is the first reduced form
2488: of $f(b)$ having an outermost rewriting position at a non variable
2489: position of $f(x)$ (here at top).
2490:
2491: %% ATTENTION: avec theta2, la reecriture outermost a lieu a la position d'une variable!
2492: %% Faut-il modifier la definition ou l'exemple n'est-il pas bon?
2493:
2494: Notice also that if $t$ is outermost reducible at position $p$,
2495: variables of $t$ whose position is a suffix of $p$ are not affected
2496: by the reduction renaming.
2497:
2498: Indeed, if $t$ is reducible at position $p$, a ground instance $\alpha t$ of $t$
2499: cannot be outermost reduced in the instance of $x$, whose positions are suffix
2500: of $p$.
2501: So $x'$, representing the first reduced form of $\alpha x$
2502: in any outermost rewriting chain starting from
2503: $\alpha t$, such that the reduction is performed higher
2504: in the current term, is equal to $x$.
2505:
2506:
2507:
2508: %Finally, when $t$ is outermost reducible,
2509: %{\bf the reduction renaming does not affect all
2510: %variable occurrences $x_1,\ldots,x_m$ of a term $t$.
2511: %Indeed, let $p_1,\ldots,p_m$ the respective positions of
2512: %$x_1,\ldots,x_m$ in $t$,
2513: %and let us denote $I_t = \{i \in [1..m] | t$
2514: %outermost rewrites at a prefix position $p'_i$ of $p_i\}$.
2515:
2516: %Let us consider $\rho = (x_1 \red x'_1)...(x_m \red x'_m)$.
2517: %By definition of the reduction renaming, the $x'_i$ represent
2518: %the first reduced form of $\alpha x_1,\ldots, \alpha x_m$
2519: %generating an outermost reduction higher
2520: %in the term,
2521: %in any outermost rewriting chain starting from
2522: %$\alpha t$, for any $\alpha$.
2523: %As the $p'_i$ are prefix positions of the $p_i$,
2524: %$\alpha t$ is outermost reduced at positions $p'_i$,
2525: %so we have $\bigwedge_{i \in I_t} x'_i = x_i$.
2526: %Then $R(t)$ is equivalent (in the sense that the
2527: %same set of ground substitutions satisfies both formulas) to
2528: %$R(t) \bigwedge_{i \in I_t} x'_i = x_i$.
2529: %So $R(t)$ can be reduced to $t \red t^{\rho}$ with $\rho =
2530: %\bigwedge_{i \in \{1,\ldots,m\} \setminus I_t} (x_i \red x'_i)$.}\\
2531:
2532: %{\bf ATTENTION: je crois que c'est encore plus que ca: quand il y a un redex
2533: %dans $t$, tous les $x'_i$ sont les $x_i$ eux-memes... c'est vrai ?}
2534: %NON!!!!!
2535:
2536:
2537: To illustrate this, let us consider the system $\{g(x) \ra x, f(x,x) \ra x\}$
2538: (the right-hand sides of the rules are not important here).
2539: Then, since $f(x,g(y))$ outermost rewrites at the position of $g$,
2540: the variable $y$ does not need to be renamed.
2541: So $R(f(x,g(y))) = (f(x,g(y)) \red f(x',g(y)))$.
2542:
2543: %is equivalent to
2544: %$R'(f(x,g(y))) = (f(x,g(y)) \red f(x',g(y'))) \wedge y=y'$, and then to
2545: %$R'(f(x,g(y))) = (f(x,g(y)) \red f(x',g(y)))$.
2546:
2547: %Indeed, whatever the
2548: %ground instance $\theta y$, the term $g(\theta y)$ outermost rewrites
2549: %only at the top position, and there is no outermost reduction of $\theta y$.
2550: %Then, following Definition~\ref{sat-red-formula}, $\theta y' = \theta y$.
2551: %Finally, note that if $I_t = \{1, \ldots, m\}$, then $R(t)$ is
2552: %the identity.\\
2553:
2554:
2555:
2556:
2557:
2558: Because of the previously defined renaming process, the formula $A$ for
2559: cumulating constraints has to be completed in the following way.
2560:
2561:
2562: \begin{subdefinition}%[renaming-abstraction constraint formula]
2563: A {\em renaming-abstraction constraint formula} (RACF for short) is a
2564: formula \\
2565: $\bigwedge_m u_m \red u_m^\rho
2566: \bigwedge_i (t_i \con t'_i) \wedge \bigwedge_j (x_j = t_j) \wedge
2567: \bigwedge_k \bigvee_{l_k} (u_{l_k} \neq v_{l_k})$,
2568: where
2569: $u_m, u_m^\rho, t_i, t'_i, t_j,$ $ u_{l_k}, v_{l_k} \in \TFXXA$, $x_j
2570: \in \X \cup \XA$.
2571: The empty formula is denoted $\top$.
2572: \end{subdefinition}
2573:
2574:
2575: \begin{subdefinition}
2576: A renaming-abstraction constraint formula \\
2577: $\bigwedge_m u_m \red u_m^\rho
2578: \bigwedge_i (t_i \con t'_i) \wedge \bigwedge_j (x_j = t_j) \wedge
2579: \bigwedge_k \bigvee_{l_k} (u_{l_k} \neq v_{l_k})$
2580: is said to be {\em satisfiable} iff there
2581: exists at least one instantiation $\theta$ such that
2582: $\bigwedge_i (\theta t_i \con \theta t'_i)
2583: \wedge \bigwedge_j (\theta x_j = \theta t_j)
2584: \wedge \bigwedge_k \bigvee_{l_k} (\theta u_{l_k} \neq \theta v_{l_k})$
2585: and $\theta$ satisfies
2586: $\bigwedge_m u_m \red u_m^\rho$.
2587: \end{subdefinition}
2588:
2589:
2590:
2591: In practice, one can solve the equality and disequality part of the constraint
2592: and then check whether the solution $\theta$ satisfies the reduction
2593: formulas.
2594: This is trivial when $\theta$ only instantiates the $x'_i$, since it
2595: can be extended by setting $\theta(x_i) = \theta(x'_i)$. Unfortunately, when
2596: $\theta$ also instantiates the $x_i$, we get the undecidable problem of
2597: reachability: given two
2598: ground terms $t$ and $t'$, can $t$ be transformed into $t'$ by repeated
2599: application of a given set of rewriting rules?
2600:
2601: So here again, we can either test satisfiability of the formula of
2602: cumulated constraints, or unsatisfiability.
2603: As satisfiability is in general more difficult to show than in the
2604: innermost case, we only present here inference rules checking unsatisfiability.
2605:
2606:
2607:
2608: \OUT{
2609: {\bf Est-ce que ca peut servir commme dans le cas innermost, ou on
2610: decide de la supprimer?}
2611: Je propose de supprimer.
2612:
2613:
2614: To Definition~\ref{def:constraint-problem} corresponds the following
2615: definition, specific to the outermost case.
2616:
2617:
2618: \begin{definition}
2619: Let $t,u_1,\ldots,u_m \in \TXF$ and $\Sigma$ an SCF. The constraint
2620: $(t>u_1,\ldots,u_m) \sur \Sigma$ is said to be satisfiable iff
2621: there exists an $\F$-stable ordering $\succ$ on $\TF$ having the subterm property
2622: such that $\theta t \succ \theta u_i, i \in [1..m]$,
2623: for every ground substitution
2624: $\theta$ satisfying $\Sigma$, and whose domain contains the variables of $t$ and of
2625: the $u_i, i \in [1..m]$.
2626: Such an ordering $\succ$ is said to satisfy $(t>u_1,\ldots,u_m) \sur \Sigma$.
2627: \end{definition}
2628:
2629:
2630: The satisfiability of $(t>u_1,\ldots,u_m) \sur \Sigma$ is undecidable.
2631: But here again, a sufficient condition for an
2632: ordering $\succ$ to satisfy this constraint is that $\succ$ is stable under
2633: substitution (the induction ordering is then a simplification
2634: ordering) and $t \succ u_1,\ldots,u_m $.
2635: Remark that consequently, $(t>u_1,\ldots,u_m) \sur \Sigma$ may be proved
2636: satisfiable, even if $\Sigma$ is not.
2637: }
2638:
2639:
2640:
2641:
2642: \subsection{Inference rules for the outermost case}
2643:
2644:
2645: The inference rules \rname{Abstract}, \rname{Narrow} and \rname{Stop}
2646: instantiate respectively the proof steps \emph{abstract}, \emph{narrow}, and
2647: \emph{stop}.
2648:
2649: They work as follows:
2650:
2651: \begin{itemize}
2652: \item
2653: The narrowing step is expressed by a rule \rname{Narrow} applying on
2654: $(\{t\}, A, C)$:
2655: the variables of $t$ are renamed as specified in Definition~\ref{def:renaming-red}.
2656: Then $t^\rho$ is outermost narrowed in all possible ways in one step, with all
2657: possible rewrite rules of the rewrite system $\R$,
2658: into terms $u$. For any possible $u$, we generate the state
2659: $(\{u\}, R(t) \wedge A \wedge \sigma, C)$
2660: where $\sigma$ is the constrained substitution allowing outermost narrowing
2661: of $t^\rho$ into $u$.
2662:
2663:
2664: \item
2665: The rule \rname{Abstract} works as in the innermost case, except that the
2666: abstraction positions are such that the abstracted term is not narrowable
2667: at prefix positions of the abstraction positions.
2668:
2669: \item
2670: The rule \rname{Stop} also works as in the innermost case.
2671: \end{itemize}
2672:
2673: \begin{table*}
2674: \centering
2675: \caption{Inference rules for the outermost strategy}
2676: \label{outermost-inference}
2677: \framebox[\textwidth]{
2678: %\framebox[30pc]{
2679: \begin{minipage}{\textwidth}
2680: \setlength{\parindent}{0pt}
2681: \setlength{\parskip}{2ex}
2682:
2683: %\linewidth
2684:
2685:
2686:
2687: \dubblewcinfr{~Abstract}
2688: { \{t\},~~A,~~C }
2689: { \{u\},~A \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con X_{i_p},
2690: ~C \wedge H_C(t|_{i_1}) \ldots \wedge H_C(t|_{i_p})}
2691: {{\rm ~where~} t {\rm ~is~abstracted~into~}
2692: u {\rm~at~positions~} i_1, \ldots ,i_p \neq \epsilon}
2693: {{\rm ~if~} C \wedge H_C(t|_{i_1}) \ldots \wedge H_C(|t_{i_p}) {\rm
2694: ~is~satisfiable}}
2695: {{\rm ~and~} u {\rm ~is~not~narrowable~at~prefix~positions~of~} i_1, \ldots ,i_p }
2696:
2697:
2698:
2699:
2700:
2701: \cinfr{~Narrow}
2702: { \{t\},~~A,~~C }
2703: { \{u\},~~R(t) \wedge A \wedge \sigma , ~~ C}
2704: {t^\rho \surred_{R}^{Out,\sigma} u }
2705:
2706:
2707:
2708: \cinfr{~Stop}
2709: { \{t\},~~A,~~C }
2710: { \emptyset,~~A \wedge H_A(t),~~C \wedge H_C(t)}
2711: {C \wedge H_C(t) {\rm ~is~satisfiable~or~} {A} {\rm ~is~unsatisfiable}}
2712:
2713: %\begin{tabular}{lcr}
2714: ${\rm ~and~} H_A(t) =
2715: \left\{
2716: \begin{array}{ll}
2717: \mathit{\top} & {\rm ~if~any~ground~instance~of~} t \\
2718: & {\rm ~is~in~normal~form}\\
2719: t \con X & {\rm ~otherwise.}
2720: \end{array}
2721: \right.
2722: $
2723: \\
2724: %&
2725: %~
2726: %&
2727: $ ~~~~~~~~H_C(t) =
2728: \left\{
2729: \begin{array}{ll}
2730: \mathit{\top} & {\rm ~if~} \mathit{TERMIN(Outermost,t)}\\
2731: t_{\mathit{ref}}>t & {\rm ~otherwise.}
2732: \end{array}
2733: \right.
2734: $
2735: %\end{tabular}
2736:
2737:
2738: \end{minipage}}
2739: \end{table*}
2740:
2741:
2742:
2743: To prove outermost termination of $\R$
2744: on every term $t \in \TF$, for each defined symbol
2745: $g \in \Def$, we apply the rules on the initial state
2746: $(\{t_{\mathit{ref}}=g(x_1, \ldots , x_m)\}, \top, \top)$, with the strategy:
2747: \begin{center}
2748: $\mathit{Strat{-}Rules(Outermost) = repeat*(try{-}skip(\rname{Abstract}); try{-}skip(\rname{Narrow});}$
2749: $\mathit{try{-}skip(\rname{Stop}))}$.
2750: \end{center}
2751:
2752: There are three cases for the behavior of the strategy: either
2753: there is a branch in the proof tree with infinite applications of
2754: \rname{Abstract} and \rname{Narrow}, in which case we cannot say anything
2755: about termination, or the procedure stops on each branch with the rule
2756: \rname{Stop}. Then,
2757: outermost termination is established, if all proof trees are finite.
2758:
2759: According to the remark following Definition~\ref{sat-red-formula},
2760: the reduction formulas in $A$ may often be reduced to simple variable renamings.
2761: In this case, $A$ only contains variable renamings and constrained
2762: substitutions, that can be used to show that the ordering constraint
2763: needed to apply \rname{Abstract} or \rname{Stop} is satisfiable
2764: (see Examples B.1 and B.4 in ~\cite{FGK-out-interne-2002}).
2765: The following lemma can also be used, if satisfiability of $C$
2766: is considered with Definition~\ref{def:constraint-problem}
2767: (see Examples B.2, B.3 and B.4 in ~\cite{FGK-out-interne-2002}).
2768: %It enables in particular to apply \rname{Stop} when the current term is either
2769: %a variable, or a non narrowable term.
2770:
2771:
2772:
2773: \begin{sublemma}
2774: \label{lemme:var}
2775: Let $(\{t_i\}, A_i, C_i)$ be the $i^{th}$ state of any
2776: branch of the derivation tree obtained by applying
2777: the strategy $S$ on $(\{t_{\mathit{ref}}\}, \top, \top)$,
2778: and $\succ$ an $\F$-stable ordering having the subterm property.
2779: If every reduction formula in $A_i$ can be reduced to a formula
2780: $\bigwedge_j x_j = x'_j$, then
2781: we have:
2782: \begin{center}
2783: for all variable $x$ of $t_i$ in $\X$:
2784: $(t_{\mathit{ref}} > x)/A_i$ is satisfiable by $\succ$.
2785: \end{center}
2786: \end{sublemma}
2787:
2788:
2789:
2790: \subsection{Examples}
2791:
2792: \begin{subexample}
2793:
2794: Consider the previous example $\R= \{f(g(a)) \ra a, f(f(x)) \ra b ,
2795: g(x)$ $\ra f(g(x))\}$, that is outermost
2796: terminating, but not terminating for the standard rewriting relation.
2797: We prove that $\R$ is outermost terminating on $\TF$ where $\F =\{f:1, g:1, a:0, b:0\}$.
2798:
2799: The defined symbols of $\F$ for $\R$ are $f$ and $g$.
2800: Applying the rules on $f(x_1)$, we get:
2801:
2802: \footnotesize{
2803: $$
2804: \xymatrix{
2805: & *{\txt{$f(x_1)$\\$A = \top, \; C=\top$\\$$}} \ar_{\rname{Narrow}}[dl]^{\sigma = (x'_1 = g(a))} \ar^{\rname{Narrow}}[dr]_{\sigma = (x'_1 = f(x_2))} &\\
2806: *{\txt{$a$\\$A = (f(x_1) \red f(x'_1)$\\$~~~~~~ \wedge x'_1 = g(a))$\\$C=\top$}} \ar|-{\rname{Stop}}[d]
2807: && *{\txt{$b$\\$A = (f(x_1) \red f(x'_1)$\\$~~~~~~ \wedge x'_1 = f(x_2))$\\$C=\top$}} \ar|-{\rname{Stop}}[d]\\
2808: *{\txt{$ $\\$\emptyset$\\$A = (f(x_1) \red f(x'_1)$\\$~~~~~~ \wedge x'_1 = g(a))$\\$C=\top$}} &&
2809: *{\txt{$ $\\$\emptyset$\\$A = (f(x_1) \red f(x'_1)$\\$~~~~~~ \wedge x'_1 = f(x_2))$\\$C=\top$}}\\
2810: }
2811: $$
2812: }
2813: \normalsize
2814:
2815: %The SCF $A = (x_1 = g(a))$ is satisfiable by $\theta$ such that
2816: %$\theta x_1 = g(a)$, and the SCF $A = (x_1 = f(x_2))$ by $\theta$
2817: %such that $\theta x_1 = f(a)$ and $\theta x_2 = a$.
2818: The first \rname{Stop} is applied because $a$ is in normal form,
2819: the second \rname{Stop} because $b$ is in normal form.
2820: Applying the rules on $g(x_1)$, we get:
2821:
2822: \gtree{
2823: \[
2824: \begin{array}{lll}
2825: \epsilon & ~~~g(x_1) & ~~~A = \top & ~~~C=\top \\
2826:
2827: \rname{Narrow} & &\\
2828: 1 & ~~~f(g(x'_1)) & ~~~A = \top (g(x_1) \red g(x'_1))\\
2829: & & ~~~(\sigma = (x' = x'_1)) \\
2830:
2831: \rname{Narrow} & &\\
2832: 1.1 & ~~~a & ~~~A = (x_1 \red x'_1)[g(x_1)] \wedge x'_1 \red x'_2)[f(g(x'_1))] \wedge x'_2 = a)\\
2833: & & ~~~(\sigma = (x'_2 = a))\\
2834: 1.2 & ~~~f(f(g(x'_2))) & ~~~A = (x_1 \red x'_1)[g(x_1)] \wedge x'_1 \red x'_2)[f(g(x'_1))] \wedge x'_2 \neq a)\\
2835: && ~~~(\sigma = (x'' = x'_2) \mbox{ satisfies } (x'_2 \neq a)) \\
2836:
2837: \rname{Abstract} & &\\
2838: 1.1.1 & ~~~\emptyset & ~~~A =\\$A = \top$ (x_1 \red x'_1)[g(x_1)] \wedge x'_1 \red x'_2)[f(g(x'_1))] \wedge x'_2 = a)\\
2839: 1.2 & ~~~f(f(g(x_3))) & ~~~A = (x_1 \red x_2)[g(x_1)] \wedge x_2 \red x_3)[f(g(x_2))] \wedge x_3 \neq a)\\
2840:
2841: \rname{Narrow} & &\\
2842: 1.1.1 & ~~~\emptyset & ~~~A = (x_1 \red x_2)[g(x_1)] \wedge x_2 \red x_3)[f(g(x_2))] \wedge x_3 = a)\\
2843: 1.2.1 & ~~~b & ~~~A = (x_1 \red x_2)[g(x_1)] \wedge x_2 \red x_3)[f(g(x_2))] \wedge x_3 \red x_4)[f(f(g(x_3)))] \wedge x_3 \neq a)\\
2844: && ~~~(\sigma = (x''' = g(x_4))\\
2845:
2846: \rname{Abstract} & &\\
2847: 1.1.1 & ~~~\emptyset & ~~~A = (x_1 \red x_2)[g(x_1)] \wedge x_2 \red x_3)[f(g(x_2))] \wedge x_3 = a)\\
2848: 1.2.1.1 &~~~\emptyset & ~~~A = (x_1 \red x_2)[g(x_1)] \wedge x_2 \red x_3)[f(g(x_2))] \wedge x_3 \red x_4)[f(f(g(x_3)))] \wedge x_3 \neq a)\\
2849:
2850: \end{array}
2851: \]
2852: }
2853:
2854:
2855: \footnotesize{
2856: \begin{center}
2857: {
2858: $$
2859: \xymatrix{
2860: & *{\txt{$ $ \\$g(x_1)$\\$A = \top, \; C = \top$\\$ $}}
2861: \ar_{\rname{Narrow}}[d]^{\sigma = Id}& \\
2862: & *{\txt{$ $\\$f(g(x_1))$\\$A = \top, \; C = \top$\\$ $}}
2863: \ar_{\rname{Narrow}}[dl]^{\sigma = (x_1 = a)}
2864: \ar^{\rname{Narrow}}[dr]_{\sigma = (x_1 \neq a)}
2865: &\\
2866: *{\txt{$ $ \\$a$\\$A = (x_1 = a)$\\$C = \top$}}
2867: \ar|-{\rname{Stop}}[d]
2868: && *{\txt{$ $ \\$f(f(g(x_1)))$\\$A = (x_1 \neq a)$\\$C = \top$}}
2869: \ar^{\rname{Narrow}}[d]_{\sigma = Id}\\
2870: *{\txt{$ $\\$\emptyset$\\$A = (x_1 = a)$\\$C = \top$}}
2871: && *{\txt{$ $\\$b$\\$A = (x_1 \neq a)$\\$C = \top$}} \ar|-{\rname{Stop}}[d]\\
2872: && *{\txt{$ $\\$\emptyset$\\$A = (x_1 \neq a)$\\$C = \top$}}
2873: }
2874: $$
2875: }
2876: \end{center}
2877: }
2878: \normalsize
2879:
2880:
2881: There is no reduction renaming before the \rname{Narrow} steps,
2882: since $g(x_1)$, $f(g(x_1))$ and $f(f(g(x_1)))$ are reducible at prefix positions
2883: of the position of $x_1$.
2884:
2885: When narrowing $f(g(x_1))$, we first try the top position,
2886: and find a possible unification with the first rule (the left
2887: branch).
2888: One also must consider
2889: the third rule if $x_1$ is such that $x_1 \neq a$ (second branch).
2890: \rname{Stop} is applied on $a$ and $b$
2891: as previously.
2892:
2893:
2894: %The SCF $A = (x_1 = x_2 \wedge x_2 = a)$ is satisfiable by $\theta$
2895: %such that $\theta x_1 = \theta x_2 = a$, and the SCF
2896: %$A = (x_1 = x_2 \wedge x_2 = x_3 \wedge x_3 \neq a)$ is satisfiable
2897: %by $\theta$ such that $\theta x_1 = \theta x_2 = \theta x_3 = b$.
2898: \end{subexample}
2899:
2900:
2901: \begin{subexample}
2902:
2903:
2904: Let $\R$ be the rewrite system cited in the introduction, built
2905: on $\F = \{cons:2, inf:1, big:0\}$ :
2906: \[
2907: \begin{array}{ll}
2908: cons(x,cons(y,z)) & \ra big\\
2909: inf(x) & \ra cons(x, inf(s(x)))
2910: \end{array}
2911: \]
2912:
2913: Applying the inference rules on $inf(x_1)$, we get :
2914:
2915: \footnotesize{
2916: $$
2917: \xymatrix{
2918: *{\txt{$inf(x_1)$\\$A = \top, \; C = \top$\\$ $}}
2919: \ar[d]^{\rname{Narrow}}_{\sigma = Id}\\
2920: *{\txt{$ $\\$cons(x_1, inf(s(x_1)))$\\$A = \top, \;C = \top$\\$ $}}
2921: \ar[d]^{\rname{Narrow}}_{\sigma = Id}\\
2922: *{\txt{$ $\\$cons(x'_1,cons(s(x_1),inf(s(s(x_1)))))$\\
2923: $A = (cons(x_1,inf(s(x_1))) \red cons(x'_1,inf(s(x_1))))$\\$C = \top$\\$ $}}
2924: \ar[d]^{\rname{Narrow}}_{\sigma = Id}\\
2925: *{\txt{$ $\\$big$\\$A = (cons(x_1,inf(s(x_1))) \red cons(x'_1,inf(s(x_1))))$\\$C = \top$\\$ $}}
2926: \ar|-{\rname{Stop}}[d]\\
2927: *{\txt{$ $\\$\emptyset$\\
2928: $A = (cons(x_1,inf(s(x_1))) \red cons(x'_1,inf(s(x_1))))$\\
2929: $C = \top$\\$ $}}\\
2930: }
2931: $$
2932: }
2933: \normalsize
2934:
2935: Applying the inference rules on $cons(x_1,x_2)$, we get~:
2936:
2937: \footnotesize{
2938: $$
2939: \xymatrix{
2940: *{\txt{$cons(x_1,x_2)$\\$A = \top, \; C = \top$\\$ $}}
2941: \ar^{\rname{Narrow}}[d]_{\sigma = (x'_2 = cons(x_3,x_4))}\\
2942: *{\txt{$ $\\$big$\\$A = (cons(x_1,x_2) \red cons(x'_1,x'_2))$\\
2943: $ \wedge~ x'_2 = cons(x_3, x_4))$\\$C = \top$}}
2944: \ar|-{\rname{Stop}}[d]\\
2945: *{\txt{$ $\\$\emptyset$\\$A = (cons(x_1,x_2) \red cons(x'_1,x'_2))$\\
2946: $ \wedge~ x'_2 = cons(x_3, x_4))$\\$C = \top$}}
2947: }
2948: $$
2949: }
2950: \normalsize
2951:
2952:
2953:
2954:
2955: \end{subexample}
2956:
2957:
2958: Other examples can be found in~\cite{FGK-out-interne-2002}.
2959:
2960:
2961:
2962: \section{Local strategies on operators}
2963: \label{sec:local-strat}
2964:
2965: %strat-locales.tex
2966:
2967: We now address the termination problem for rewriting with local
2968: strategies on operators.
2969:
2970: \subsection{Abstraction and narrowing}
2971:
2972: %A subtle point related to local strategies is that some subterms may
2973: %never be rewritten according to the LS-strategy. Identifying reducible
2974: %subterms according to the LS-strategy is thus an important point, and
2975: %the notion of LS-position is introduced to denote possible reducible
2976: %positions of any instantiation of $t$, with respect to the
2977: %LS-strategy.
2978:
2979: %\begin{definition}
2980: %\label{def:LS-position}
2981: %A position $p$ of a term $t \in \TXF$ is an LS-position in $t$
2982: %if the LS-strategy allows rewriting $t$ at position $p$, or
2983: %if the LS-strategy allows rewriting any ground instance of $t$ at
2984: %position $p$ or at a suffix position of $p$.
2985: %\end{definition}
2986:
2987: %This notion helps to characterize which variables may be replaced by
2988: %abstraction variables.
2989: The information that variables are abstraction
2990: variables can be very important to conclude the proofs here:
2991: if the current term is an
2992: abstraction variable, its strategy is set to $[]$ in the \emph{Narrow}
2993: step, and then the \emph{Stop} step applies. This information can be
2994: easily deduced when new variables are introduced: the abstracting
2995: process directly introduces abstraction variables, by definition.
2996: But the resulting term may still have variables of $\cal X$ since
2997: the abstracted subterms of a term may not cover all variables of
2998: the term.
2999:
3000: Moreover, narrowing is performed on terms of $\TFXXA$.
3001: Indeed, there is no variable renaming before the narrowing steps, that
3002: could transform all variables into abstraction variables.
3003: In addition, even if the variables of a narrowed term are all in $\XA$,
3004: the range of the narrowing substitution can introduce variables of
3005: $\X$, according to the LS-strategies, if these variables do not appear at
3006: LS-positions.
3007:
3008: However some variable occurrences can be particularized into variables
3009: of $\XA$ in the narrowing process:
3010: the narrowing substitution $\sigma$, whose range only contains new
3011: variables of ${\cal X}$, can be transformed into a new substitution
3012: $\sigma_A$ by replacing some of these variables by abstraction
3013: variables. Let us consider an equality of the form $X=u$, introduced
3014: by the narrowing substitution $\sigma$, where $X \in \XA$,
3015: and $u \in \TXF$.
3016: As $X$ is an abstraction variable, every
3017: ground instance of $u$ must be in normal form. So the variables in
3018: $u$ that occur at an LS{-}position can be replaced by abstraction
3019: variables.
3020: Let now $\mu$ be the
3021: substitution $(x_i = X_i)$, for all $x_i \in Var(u)$ such that
3022: $X=u$ is an equality of $\sigma$ with $X \in \XA, \; u \in \TFXXA$,
3023: and $x_i$ occurs at an LS{-}position in $u$.
3024: Then $\sigma_A = \mu
3025: \sigma$.\\
3026:
3027:
3028:
3029:
3030: Combining abstraction and narrowing is achieved here in the following
3031: way. The abstraction positions are chosen so that the abstraction
3032: mechanism captures the greatest possible number of rewriting steps: we
3033: try to abstract the immediate subterms of the current term. If the
3034: abstraction is possible, then a narrowing step is applied, only at the
3035: top position, which limits the number of narrowing steps, more
3036: complicated here than for the other strategies, since, as we will see
3037: later, they involve complementary branches.
3038:
3039: If \rname{Abstract} cannot be applied at all LS-positions of the term,
3040: the process is stopped, and nothing can be concluded about termination.
3041:
3042:
3043: \subsection{The termination proof procedure for local strategies}
3044: \label{sec:rules}
3045:
3046: The inference rules \rname{Abstract}, \rname{Narrow} and \rname{Stop}
3047: instantiate respectively the proof steps \emph{abstract}, \emph{narrow}, and
3048: \emph{stop}.
3049: They work in the following way on a state $(\{t^{[p_1,\ldots,p_n]}\},A,C)$,
3050: where $top(t)=f$ and $LS(f)=[p_1,\ldots,p_n]$.
3051:
3052:
3053:
3054:
3055: \begin{itemize}
3056:
3057: \item The rule \rname{Abstract} processes the abstracting step. It
3058: can apply:
3059:
3060: \begin{itemize}
3061: \item
3062: when there exists $k \in
3063: [2..n]$, $p_j \neq 0$ for $ 1 \leq j \leq k-1$ and $p_k=0$.
3064: The term $t$ is abstracted at positions
3065: $p_j \neq 0$ for $ 1 \leq j< k$ if
3066: there exists an $\F$-stable ordering having the subterm property and
3067: such that $C \wedge (t_{\mathit{ref}}> t|_{p_j}, 1 \leq j< k)$
3068: is satisfiable. Indeed, by induction hypothesis,
3069: all ground instances of $t|_{p_j}, 1 \leq j< k$ LS-terminate.
3070: We can instead have $\mathit{TERMIN(Local{-}Strat, t|_{p_j})}$ for some of the previous $t|_{p_j}$.
3071: The list of positions then becomes $[0, p_{k+1}, \ldots ,p_n]$.
3072:
3073: \item
3074: when there is no position $0$ in the strategy of the current term. Any ground
3075: instance of the term obtained after abstraction is irreducible, by
3076: definition of the LS-strategy, which ends the proof on the
3077: current derivation chain. The set containing the current term is then
3078: replaced by the empty set.
3079:
3080: \item when $p_1=0$. The rule applies but does not change the
3081: state on which the {\emph narrow} step can be applied.
3082:
3083: %{\bf Remark that, if the above abstracting process fail,
3084: %reducible subterms could remain in the current term, leading the
3085: %narrowing step to be applied at position $p>\epsilon$.
3086: %As narrowing is only applied at the top position,
3087: %the process stops on the rule \rname{Abstract}, hence the
3088: %following rule.}
3089: \end{itemize}
3090:
3091: %\item The rule \rname{Stop{-}A} allows to stop the inference process
3092: %when $p_1 \neq 0$ and neither \rname{Abstract} nor \rname{Abstract{-}Stop} applies,
3093: %replacing $u$ by the particular symbol $\sharp$.
3094:
3095:
3096: \item The rule \rname{Narrow} works as follows:
3097: \begin{itemize}
3098: \item
3099: if the current term $t$ is narrowable at position 0,
3100: $t$ is narrowed in all possible ways in one step, with all
3101: possible rewrite rules of the rewrite system $R$, and all possible
3102: substitutions $\sigma_i$, into $u_i, i \in [1..l]$.
3103: Then from the state $(\{t^{[0,p_1, \ldots ,p_n]}\}, A, C)$ we generate the states
3104: $(\{u_i^{LS(top(u_i))}\}, A \wedge \sigma_i , C),$ $i \in [1..l]$,
3105: where the $\sigma_i$ are all most general unifiers
3106: allowing narrowing of $t$ into terms $u_i$, such that $A \wedge \sigma_i$ is satisfiable.
3107: This narrowing step means that $\sigma_1 t, \ldots , \sigma_l t$ are all
3108: most general instances of $t$ that are reducible at the top position.
3109: As a consequence, if
3110: $\Phi = \overline{\sigma_1} \wedge \ldots \wedge \overline{\sigma_l}$
3111: is satisfiable, for each {\bf instantiation} $\mu$ satisfying
3112: $\Phi$, $\mu t$ is not reducible at the top position.
3113: Then, as these $\mu t$ have to be reduced at positions
3114: $[p_1, \ldots ,p_n]$, we also generate the complementary state
3115: $(\{t^{[p_1, \ldots ,p_n]}\}, A \wedge \bigwedge_{i=1}^l \overline{\sigma_i}, C)$.
3116:
3117: Let us also notice that if $u_i$ is a variable $x \in {\cal X}$, we
3118: cannot conclude anything about termination of ground instances of
3119: $x$.
3120: Setting $LS(x)$ to $[0]$ or $[]$ would wrongly lead to conclude, with the rule
3121: \rname{Narrow}, that ground instances of $x$ are terminating.
3122: So we force the proof process to stop in setting $LS(x)$ to
3123: a particular symbol $\sharp$.
3124: However, if $u_i = X \in {\XA}$,
3125: $LS(X)$ is set to $[]$, which is coherent with the fact that any
3126: ground instance of $X$ is in LS- normal form.
3127:
3128:
3129:
3130: \item if $t$ is not narrowable at position $0$ or is narrowable with a
3131: substitution {\bf that is not compatible with} the current constraint
3132: formula $A$, then no narrowing
3133: is applied and the current term is evaluated at positions following
3134: the top position in the strategy. The list of positions then becomes
3135: $[p_1, \ldots ,p_n]$.
3136: \end{itemize}
3137:
3138: \item
3139: We also can check for the current term whether there
3140: exists an ordering having the subterm property such that
3141: $C \wedge t_{\mathit{ref}}>t$ is satisfiable. Then, by induction
3142: hypothesis, any ground instance of $t$ terminates for the LS-strategy,
3143: which ends the proof on the current derivation chain.
3144: The \rname{Stop} rule then replaces the set containing the current term by
3145: the empty set.
3146:
3147: The rule \rname{Stop} also allows to stop the inference process
3148: when the list of positions is empty.
3149:
3150:
3151: \end{itemize}
3152:
3153:
3154:
3155:
3156: The set of inference rules is given in Table \ref{tab:inference-strat-lo}.
3157: In the conditions of these rules, satisfiability of $A$ is checked.
3158: Working with unsatisfiability of $A$ would be more technical to
3159: handle here than in the innermost case, because of the complementary
3160: branches generated by the \rname{Narrow} rule.
3161:
3162:
3163:
3164: \begin{table*}
3165: \centering
3166: \caption{Inference rules for $t_{\mathit{ref}}$ LS-termination}
3167: \label{tab:inference-strat-lo}
3168: %\framebox[150mm]{
3169: \framebox[\textwidth]{
3170: \begin{minipage}{\textwidth}
3171: \setlength{\parskip}{6ex}
3172:
3173: \sixcinfr{Abstract}
3174: {\{t^{[p_1, \ldots ,p_n]}\},~~A,~~C}
3175: {\{u^S\},~~A \wedge \bigwedge_{j
3176: \in \{i_1, \ldots ,i_p\}} (t|_j \da = X_j),~~C \wedge \bigwedge_{j \in \{i_1, \ldots ,i_p\}} H_C(t|_j)}
3177: {{\rm ~where~} t {\rm ~is~abstracted~into~}
3178: u {\rm ~at~the~positions~}
3179: i_1,\ldots,i_p \in \mathit{POS}}
3180: {{\rm ~if~} A \wedge \bigwedge_{j \in \{i_1, \ldots ,i_p\}} (t|_j \da = X_j), \; C
3181: \wedge \bigwedge_{j \in \{i_1, \ldots ,i_p\}} H_C(t|_j){\rm
3182: ~are~satisfiable~and~}}
3183: {\mathit{~POS} = \{p_1,\ldots,p_{k-1}\},S=[0,p_{k+1}, \ldots ,p_n]
3184: {\rm ~if~} \exists k \in [2..n] : p_1,\ldots,p_{k-1} \neq 0}
3185: {{\rm ~~~~~~~~~~~~and~} p_k = 0}
3186: {\mathit{~POS} = \{p_1,\ldots,p_n\}, S=[]
3187: {\rm ~if~} p_1,\ldots,p_n \neq 0 {\rm ~or~} [p_1, \ldots ,p_n]=[]}
3188: {\mathit{~POS} = \emptyset, S=[p_1, \ldots ,p_n]
3189: {\rm ~if~} p_1=0}
3190:
3191:
3192:
3193: \fivecinfr{Narrow}
3194: {\{t^{[0,p_1, \ldots ,p_n]}\},~~A,~~C}
3195: {\{u^S\}, ~~A',~~C }
3196: {{\rm where~} u=u_i, S=LS(top(u_i)), A'= A \wedge \sigma_i {\rm ~if~}
3197: t \leadsto^{\epsilon, \sigma_i}_\R u_i {\rm ~and~} A \wedge \sigma_i {\rm ~is~satisfiable~}}
3198: {{\rm ~~or~} u^S = t^{[p_1, \ldots ,p_n]},
3199: A'=A \wedge (\bigwedge_{i=1}^l \overline{\sigma_i}),
3200: {\rm ~and~} \sigma_i, i \in [1..l] {\rm ~are~all~nar.~subst.~as~above~}}
3201: {{\rm ~~or~} u^S = t^{[p_1, \ldots ,p_n]}, A'=A }
3202: {{\rm ~~~~~~~~~if~} t {\rm ~is~not~narrowable~at~the~top~position}}
3203: {{\rm ~~~~~~~~~or~} \forall \sigma {\rm ~nar.~subst.~of~} t
3204: {\rm ~at~the~top~position}, ~~A \wedge \sigma {\rm ~is~not~satisfiable}}
3205:
3206:
3207: \cinfr{Stop}
3208: {\{t^{[p_1, \ldots ,p_n]}\},~~A,~~C}
3209: {\emptyset,~~A \wedge H_A(t),~~C \wedge H_C(t)}
3210: {A \wedge H_A(t), \; C \wedge H_C(t) {\rm ~are~satisfiable}
3211: }
3212:
3213: %\begin{tabular}{lcr}
3214: ${\rm ~and~} H_A(t) =
3215: \left\{
3216: \begin{array}{ll}
3217: \mathit{\top} & {\rm ~if~} [p_1, \ldots ,p_n]=[] \\
3218: & {\rm ~or~any~ground~instance~of~} t \\
3219: & {\rm ~is~in~normal~form}\\
3220:
3221: t \da = X & {\rm ~otherwise.}
3222: \end{array}
3223: \right.
3224: $
3225: \\
3226: %&
3227: %~
3228: %&
3229: $~~~~~~~~H_C(t) =
3230: \left\{
3231: \begin{array}{ll}
3232: \mathit{\top} & {\rm ~if~} [p_1, \ldots ,p_n]=[] \\
3233: & {\rm ~or~} \mathit{TERMIN(Local{-}Strat,t)}\\
3234: t_{\mathit{ref}}>t & {\rm ~otherwise.}
3235: \end{array}
3236: \right.
3237: $
3238: %\end{tabular}
3239:
3240: \end{minipage}}
3241: \end{table*}
3242:
3243:
3244:
3245:
3246: %When \rname{Abstract} does not apply, and the evaluation list's first element
3247: %is not $0$, then \rname{Stop{-}A} applies, and then no rule applies
3248: %anymore.
3249: %As in the innermost case, $\rname{Narrow}$ can fail, if the current
3250: %term is narrowable, and we cannot say anything about satisfiability of
3251: %$\sigma A$.
3252:
3253: %%DEBAT
3254: % CE QU'ON DIT DANS LE PAPIER SUR LES STRAT LO EST FAUX: ON N'A PAS
3255: % SOIT NARROW-N SOIT NARROW-Y.
3256:
3257: The strategy for applying these rules is:
3258:
3259:
3260: %\begin{center}
3261: %repeat*\\
3262: %(try-skip(\rname{Abstract}); try-skip(\rname{Stop{-}A}); try-stop(\rname{Narrow}); try-skip(\rname{Stop}))
3263: %\end{center}
3264:
3265: \begin{center}
3266: $\mathit{repeat*
3267: (try{-}stop(\rname{Abstract}); try{-}stop(\rname{Narrow}); try{-}skip(\rname{Stop}))}$.
3268: \end{center}
3269:
3270: %{\bf Pourquoi pas try-stop(\end{document}\rname{Abstract}) ?
3271: %Parce qu'il y a un cas ou on ``skip'' la regle Abstract: c'est quand
3272: %LS commece par 0... A REVOIR: on peut le traiter}
3273:
3274: There are here also three cases for
3275: the behavior of the proof process. It can diverge as previously, or
3276: stop and the states in the leaves have then to be considered.
3277: %on a failure state $(\sharp,A,C)$.
3278: The good case is when
3279: the process stops and all final states of all proof trees are of the
3280: form $(\emptyset,A,C)$. \\
3281:
3282: %{\bf Peut-on ici aussi optimiser le test de sat de A en ne le faisant
3283: %que dans Narrow ?}\\
3284:
3285:
3286:
3287: %%%%%%%%LE CAS DES VARIABLES QUI SONT DES NF-VAR
3288:
3289:
3290: \subsection{Examples}
3291:
3292: \begin{subexample}
3293: Let us recall the rules of the example given in the introduction.
3294:
3295: {\footnotesize
3296: \[
3297: \begin{array}{ll}
3298: f(i(x)) & \ra ite(zero(x),g(x),f(h(x)))\\
3299: zero(0) & \ra true\\
3300: zero(s(x)) & \ra false\\
3301: ite(true,x,y) & \ra x\\
3302: ite(false,x,y) & \ra y\\
3303: h(0) & \ra i(0)\\
3304: h(x) & \ra s(i(x))
3305: \end{array}
3306: \]
3307: }
3308: The LS-strategy is the following :
3309:
3310: {\footnotesize
3311: \begin{itemize}
3312: \item $LS(ite) = [1 ; 0]$,
3313: \item $LS(f) = LS(zero) = LS(h) = [1 ; 0]$ and
3314: \item $LS(g) = LS(i) = [1]$.
3315: \end{itemize}
3316: }
3317:
3318: Let us prove the termination of this system on the signature
3319: $\F = \{f:1, zero:1, ite:3, h:1, s:1, i:1, g:1, 0:0\}$.
3320:
3321: %%% Obviously, the constant $0$ LS-terminates.
3322: Applying the inference rules on $f(x_1)$, we get :
3323:
3324:
3325: \footnotesize{
3326: $$
3327: \xymatrix{
3328: & \txt{$f(x_1)^{[1,0]}$\\$A = \top, \; C = \top$\\$ $}
3329: \ar|-{\rname{Abstract}}[d] & \\
3330: & \txt{$ $\\$f(X_1)^{[0]}$\\$A = (x_1 \con X_1)$\\$C = (f(x_1)>x_1)$\\$ $}
3331: \ar_-{\rname{Narrow}}^{\sigma_A = (X_1=i(X_2))}[dl]
3332: \ar^-{\rname{Narrow}}[dr] &\\
3333: \txt{}
3334: && \txt{}
3335: }
3336: $$
3337: $$
3338: \xymatrix{
3339: *{\txt{$ $\\$ite(zero(X_2),g(X_2),f(h(X_2)))^{[1,0]}$\\$A = (x_1 \con i(X_2))$\\$C = (f(x_1)>x_1)$}}
3340: \ar|-{\rname{Abstract}}[d]
3341: && *{\txt{$ $\\$f(X_1)^{[]}$\\$A = (x_1 \con X_1) \wedge (X_1\neq i(X_2))$\\$C = (f(x_1)>x_1)$}}
3342: \ar|-{\rname{Stop}}[d]\\
3343: *{\txt{$ $\\$ite(X_3,g(X_2),f(h(X_2)))^{[0]}$\\$A = (x_1 \con i(X_2) \wedge zero(X_2) \con X_3)$\\$C = (f(x_1)>x_1)$}}
3344: && *{\txt{$ $\\$\emptyset$\\$A = (x_1 \con X_1) \wedge (X_1\neq i(X_2))$\\$C = (f(x_1)>x_1)$}}
3345: }
3346: $$
3347: }
3348:
3349: \normalsize
3350:
3351:
3352:
3353:
3354:
3355: \rname{Abstract} applies on $f(x_1)$, since $C$ is satisfiable by any
3356: ordering having the subterm property.
3357: $A$ is satisfiable with any instantiation $\theta$ such that
3358: $\theta x_1 = \theta X_1 = 0$.
3359:
3360: \rname{Narrow} expresses the fact that $\sigma f(X_1)$ is reducible
3361: if $\sigma$ is such that $\sigma X_1 = i(X_2)$, and that
3362: the other instances ($\sigma' f(X_1)$ with $\sigma' X_1 \neq i(X_2)$)
3363: cannot be reduced.
3364:
3365: The renaming of $x_2$ into $X_2$ in $\sigma_A$ comes from the fact that
3366: $x_2$ occurs in $i(x_2)$ at an LS-position in $\sigma = (X_1 = i(x_2))$.
3367:
3368: Then, the constraint formula $A$ on the left branch is satisfiable by any
3369: instantiation $\theta$ such that $\theta X_2 = 0$ and $\theta x_1 = i(0)$.
3370: The constraint formula on the complementary branch
3371: is satisfied by any instantiation
3372: $\theta$ such that $\theta x_1 = \theta X_1 = \theta X_2 = 0$.
3373:
3374: \rname{Abstract} applies here on the first branch, since $zero(X_2)$ can be
3375: abstracted, thanks to a version of Proposition~\ref{prop:TC} adapted to local
3376: strategies~\cite{FGK-local-strat-ENTCS-2001}.
3377: Indeed, $\U(zero(X_2)) = \{zero(0) \ra true, zero(s(x)) \ra false\}$,
3378: and both rules can be oriented by a LPO $\succ$
3379: with the precedence $zero \succ_{\F} true$ and $zero \succ_{\F} false$.
3380: Then we have $\mathit{TERMIN}(Local{-}strat, zero(X_2))$.
3381:
3382: The next constraint formula $A$ is satisfiable with any instantiation $\theta$
3383: such that $\theta X_2 = 0$, $\theta X_3 = true$ and
3384: $\theta x_1 = i(0)$.
3385:
3386: Then, \rname{Narrow} applies on the left branch:
3387:
3388:
3389: \footnotesize{
3390: {
3391: $$
3392: \xymatrix{
3393: & *{\txt{$ $\\$ite(X_3,g(X_2),f(h(X_2)))^{[0]}$\\$A = (x_1 \con i(X_2) \wedge zero(X_2) \con X_3)$\\$C = (f(x_1)>x_1)$\\$ $}}
3394: \ar_-{\rname{Narrow}}^{\sigma_A = (X_3 = true)}[dl]
3395: \ar|-{\sigma_A = (X_3 = false)}[d]
3396: \ar^{Complementary~state}[dr] & \\
3397: *{\txt{$ $\\ $ $\\ $g(X_2)^{[1]}$\\$A = (x_1 \con i(X_2) \wedge$ \\$zero(X_2) \con true)$\\$C = (f(x_1)>x_1)$}}
3398: \ar|-{\rname{Abstract}}[d]
3399: & *{\txt{$ $\\ $ $ \\ $f(h(X_2))^{[1,0]}$\\$A = (x_1 \con i(X_2) \wedge$ \\ $zero(X_2) \con false)$\\$C = (f(x_1)>x_1)$}}
3400: \ar|-{\rname{Abstract}}[d]
3401: && *{\txt{$ $\\ $\bullet$}}\\
3402: *{\txt{$g(X_2)^{[]}$\\$A = (x_1 \con i(X_2) \wedge$ \\$zero(X_2) \con true)$\\$C = (f(x_1)>x_1)$}}
3403: \ar|-{\rname{Stop}}[d]
3404: & *{\txt{$ $\\ $f(X_4)^{[0]}$\\$A = (x_1 \con i(X_2) \wedge$ \\ $zero(X_2) \con false \wedge h(X_2) \con X_4)$\\$C = (f(x_1)>x_1)$}}
3405: \ar|-{\rname{Narrow}}[d]\\
3406: *{\txt{$\emptyset$\\$A = (x_1 \con i(X_2) \wedge$ \\$zero(X_2) \con true)$\\$C = (f(x_1)>x_1)$}}
3407: & *{\txt{$ $\\ $f(X_4)^{[]}$\\$A = (x_1 \con i(X_2) \wedge$ \\ $zero(X_2) \con false \wedge h(X_2) \con X_4)$\\$C = (f(x_1)>x_1)$}}
3408: \ar|-{\rname{Stop}}[d] \\
3409: & *{\txt{$ $\\ $\emptyset$\\$A = (x_1 \con i(X_2) \wedge$ \\ $zero(X_2) \con false \wedge h(X_2) \con X_4)$\\$C = (f(x_1)>x_1)$}}
3410: }
3411: $$
3412: }
3413: }
3414: \normalsize
3415:
3416:
3417:
3418: The first constraint formula $A$ is satisfiable by any
3419: instantiation $\theta$ such that
3420: $\theta X_2 = 0$ and $\theta x_1 = i(0)$.
3421: The second one is satisfiable by any instantiation $\theta$ such that
3422: $\theta X_2 = s(0)$ and $\theta x_1 = i(s(0))$.
3423: The third one (see below) is satisfiable by any instantiation $\theta$ such that
3424: $\theta X_3 = zero(i(0))$, $\theta X_2 = i(0)$ and $\theta x_1 = i(i(0))$.
3425:
3426: \rname{Abstract} trivially applies on $g(X_2)$: since $X_2$ is an abstraction
3427: variable, there is no need to abstract it.
3428:
3429: The second \rname{Abstract} applies on $f(h(X_2))$, thanks to
3430: the previous adaptation of Proposition~\ref{prop:TC} to local strategies.
3431: Indeed, $\U(h(X_2)) = \{h(0) \ra i(0), h(x) \ra s(i(x))\}$, and both rules
3432: can be oriented by the same LPO as previously with the additional precedence
3433: $h \succ_{\F} i$ and $h \succ_{\F} s$.
3434: Then we have $\mathit{TERMIN}(Local{-}strat,$ $ h(X_2))$.
3435:
3436: The constraint formula associated to $f(X_4)^{[0]}$
3437: is satisfiable by any instantiation $\theta$ such that
3438: $\theta X_4 = s(i(s(0)))$, $\theta X_2 = s(0)$ and $\theta x_1 = i(s(0))$.
3439:
3440: One could have tried to narrow $f(X_4)$, by using the first rule
3441: and the narrowing substitution
3442: $\sigma_A = (X_4=i(X_5))$.
3443: But then $A \wedge \sigma_A$ would lead to $(x_1 \con i(X_2)
3444: \wedge zero(X_2) \con false \wedge h(X_2) \con i(X_5))$.
3445: For any $\theta$ satisfying $A \wedge \sigma_A$, $\theta$ must be such that
3446: $\theta h(X_2) \con h(\theta X_2 \da) \con i(\theta X_5)$.
3447: If $\theta X_2 \da \neq 0$, then, according to $\R$,
3448: $h(\theta X_2 \da) \ra s(i(\theta X_2 \da))$, where $s$ is a constructor.
3449: Then we cannot have $h(\theta X_2 \da) \con i(\theta X_5)$, so
3450: $\theta$ must be such that $\theta X_2 \con 0$.
3451: But then $\theta zero(X_2) \con true$, which makes $A \wedge \sigma_A$
3452: unsatisfied.
3453: Therefore there is no narrowing.
3454:
3455: For the third branch, we have:
3456: \footnotesize{
3457: {
3458: $$
3459: \xymatrix{
3460: & *{\txt{$ $\\ $ $ \\ $\bullet$ \\$ite(X_3,g(X_2),f(h(X_2)))^{[]}$\\$A = (x_1 \con i(X_2) \wedge$ \\ $zero(X_2) \con X_3$ \\$\wedge X_3 \neq true \wedge X_3 \neq false)$\\$C = (f(x_1)>x_1)$\\$ $}}
3461: \ar|-{\rname{Stop}}[d] \\
3462: & *{\txt{$ $\\ $\emptyset$\\$A = (x_1 \con i(X_2) \wedge$ \\ $zero(X_2) \con X_3 \wedge $ \\$X_3 \neq true \wedge X_3 \neq false)$\\$C = (f(x_1)>x_1)$\\$ $}} \\
3463: }
3464: $$
3465: }
3466: }
3467:
3468:
3469: \normalsize
3470:
3471:
3472: Like for the defined symbols $ite, zero, h$, the inference rules apply
3473: successfully through one \rname{Abstract}, \rname{Narrow},
3474: \rname{Abstract} with no abstraction position, \rname{Narrow} and
3475: \rname{Stop} application.
3476: Therefore $\R$ is LS-terminating.
3477:
3478: \end{subexample}
3479:
3480:
3481:
3482: Let us now give an example that cannot be handled with the
3483: context-sensitive approach.
3484:
3485: \begin{subexample}
3486:
3487: Let \(\R\) be the following rewrite system
3488: {\footnotesize
3489: \[
3490: \begin{array}{lll}
3491:
3492: f(a,g(x)) \ra f(a,h(x)) \\
3493: h(x) \ra g(x)
3494: \end{array}
3495: \]
3496: }
3497: with the LS-strategy :
3498: {\footnotesize
3499: $LS(f) = [0 ; 1 ; 2], \; LS(h) = [0]$ and
3500: $LS(g) = [1]$.
3501: }
3502:
3503: The context-sensitive strategy would allow to permute the reducible
3504: arguments of $f$, so that we also could evaluate terms with $LS(f) =
3505: [1; 2; 0]$.
3506: We let the user check that, with this strategy, \(\R\) does not terminate.
3507:
3508: Applying the rules on $f(x_1,x_2)$, we get:
3509: \newpage
3510:
3511:
3512: \footnotesize{
3513: {
3514: $$
3515: \xymatrix{
3516: & *{\txt{$f(x_1,x_2)^{[0,1,2]}$\\$A = \top, \; C = \top$\\$ $}}
3517: \ar_{\rname{Narrow}}^{\sigma = (x_1 = a \wedge x_2 = g(x_3))}[dl]
3518: \ar^{\rname{Narrow}}[dr] &\\
3519: \txt{}
3520: &&\txt{}
3521: }
3522: $$
3523: $$
3524: \xymatrix{
3525: *{\txt{$ $\\$f(a,h(x_3))^{[0,1,2]}$\\
3526: $A = (x_1 = a \wedge x_2 = g(x_3))$\\$C = \top$\\$ $}}
3527: \ar|-{\rname{Narrow}}[d]
3528: && *{\txt{$ $\\$f(x_1,x_2)^{[1,2]}$\\$A = (x_1 \neq a \vee x_2 \neq g(x_3))$\\$C = \top$\\$ $}}
3529: \ar|-{\rname{Abstract}}[d] \\
3530: *{\txt{$ $\\$f(a,h(x_3))^{[1,2]}$\\
3531: $A = (x_1 = a \wedge x_2 = g(x_3))$\\$C = \top$\\$ $}}
3532: \ar|-{\rname{Abstract}}[d]
3533: && *{\txt{$ $\\$f(X_1,X_2)^{[]}$\\$A = (x_1 \con X_1 \wedge x_2 \con X_2 $\\ $x_1 \neq a \wedge x_2 \neq g(x_3))$\\$C = (f(x_1,x_2) > x_1,x_2)$\\$ $}}
3534: \ar|-{\rname{Stop}}[d] \\
3535: *{\txt{$ $\\$f(a,X_3)^{[]}$\\
3536: $A = (x_1 = a \wedge x_2 = g(x_3) \wedge$ \\$h(x_3) \con X_3)$\\$C = (f(x_1,x_2) > h(x_3))$\\$ $}}
3537: \ar|-{\rname{Stop}}[d]
3538: && *{\txt{$ $\\$\emptyset$\\
3539: $A = (x_1 \con X_1 \wedge x_2 \con X_2 $\\ $x_1 \neq a \wedge x_2 \neq g(x_3))$\\$C = (f(x_1,x_2) > x_1,x_2)$\\$ $}} \\
3540: *{\txt{$ $\\$\emptyset$\\
3541: $A = (x_1 = a \wedge x_2 = g(x_3) \wedge$ \\$h(x_3) \con X_3)$\\$C = (f(x_1,x_2) > h(x_3))$\\$ $}}
3542: &&
3543: }
3544: $$
3545: }
3546: }
3547:
3548: \normalsize
3549:
3550:
3551: Applying the rules on $h(x_1)$, we get:
3552:
3553: \footnotesize{
3554: \begin{center}
3555: {
3556: $$
3557: \xymatrix{
3558: & *{\txt{$h(x_1)^{[0]}$\\$A = \top, \; C = \top$\\$ $}}
3559: \ar^{\rname{Narrow}}_{\sigma = Id}[d] &\\
3560: & *{\txt{$ $\\$g(x_1)^{[1]}$\\ $A = \top, \; C = \top$\\$ $}}
3561: \ar|-{\rname{Abstract}}[d] &\\
3562: & *{\txt{$ $\\ $g(X_1)^{[]}$\\ $A = (x_1 \con X_1), \; C = (h(x_1) > x_1)$\\$ $}}
3563: \ar|-{\rname{Stop}}[d] &\\
3564: & *{\txt{$ $\\ $\emptyset$\\ $A = (x_1 \con X_1), \; C = (h(x_1) > x_1)$\\$ $}} &
3565: }
3566: $$
3567: }
3568: \end{center}
3569: }
3570:
3571: \normalsize
3572:
3573: \end{subexample}
3574:
3575:
3576: \OUT{
3577: {\bf Choisir ce qu'on garde et developpe:}
3578: Let us finally give another example, that cannot be be handled with the
3579: context-sensitive approach:the rewrite system
3580: $\{f(b) \ra c, g(x) \ra h(x), h(c) \ra g(f(a)), a \ra b\}$
3581: with the LS-strategy $LS(f) =[0 ; 1], LS(g) = LS(h) = [1 ; 0], LS(a) = [0]$, and two
3582: examples of innermost rewriting: the well-known Toyamas'example
3583: $\{f(0,1,x) \ra f(x, x, x), g(x,y) \ra x, g(x,y) \ra y\}$
3584: with the LS-strategy $LS(f) = [1 ; 2 ; 3 ; 0], LS(g) = [1 ; 2 ; 0],
3585: LS(0) = LS(1) = [0]$, and $\{f(f(x)) \ra f(f(x)), f(a) \ra a\}$
3586: with the LS-strategy $LS(f) = [1 ; 0], LS(a) = [0]$, that is
3587: innermost terminating on $\TF$, but is not on $\TXF$. The complete development of these
3588: examples can be found in the \cite{FGK-local-strat-2001-interne}.
3589: }
3590:
3591:
3592:
3593: \section{Conclusion}
3594:
3595: The generic termination proof method presented in this paper is based
3596: on the simple ideas of schematizing and observing the derivation trees
3597: of ground terms and of using an induction ordering to stop
3598: derivations as soon as termination is ensured by induction.
3599: The method makes clear the schematization power of narrowing,
3600: abstraction and constraints. Constraints are heavily used on one hand
3601: to gather conditions that the induction ordering must satisfy, on the
3602: other hand to represent the set of ground instances of generic terms.
3603:
3604:
3605:
3606: Our technique is implemented in a system named
3607: CARIBOO~\cite{FGK-PPDP-2002,Fissore-These-2003,CARIBOO-APP-2004},
3608: providing a termination proof tool for the innermost, the outermost,
3609: and the local strategies~\footnote{Available at http://protheo.loria.fr/softwares/cariboo/}.
3610: CARIBOO consists of two main parts~:
3611: \begin{enumerate}
3612:
3613: \item The proof procedure, written in ELAN,
3614: which is a direct translation of the inference rules. It generates
3615: the proof trees, dealing with the ordering and the abstraction constraints.
3616: It is worth emphasizing the reflexive aspect of this proof procedure,
3617: written in a rule-based language, to allow termination of rule-based programs.
3618:
3619: \item A graphical user interface (GUI), written in Java.
3620: It provides an edition tool to define specifications of rewrite systems
3621: which are then transformed into an ELAN specification
3622: used by the proof procedure.
3623: It also displays the detailed results of the proof process~:
3624: which defined symbols have already been treated and, for
3625: each of them, the proof tree together with the detail of each state.
3626: Trace files can be generated in different formats (HTML, ps, pdf...)
3627:
3628: \end{enumerate}
3629:
3630: To deal with the generated constraints,
3631: the proof process of CARIBOO can use integrated features,
3632: like the computation of usable rules,
3633: the use of the subterm ordering or the Lexicographic Path ordering
3634: to satisfy ordering constraints, and the test of sufficient conditions of
3635: Section~\ref{subsec:cumulating-constraints} for detecting unsatisfiability of
3636: $A$.
3637:
3638: It can also delegate features, as solving the ordering constraints or
3639: orienting the usable rules when the LPO fails, proving termination of a term,
3640: or testing satisfiability of $A$. Delegation is either proposed to the user,
3641: or automatically ensured by the ordering constraint solver C{\it i}me2.
3642:
3643: CARIBOO provides several automation modes for dealing with constraints.
3644: Dealing with unsatisfiability of $A$ allows a complete automatic mode,
3645: providing a termination proof for a large class of examples
3646: (a library is available with the distribution of CARIBOO).
3647:
3648: It is interesting to note that thanks to the power of induction,
3649: and to the help of usable rules,
3650: the generated ordering constraints are often simple, and are easily
3651: satisfied by the subterm ordering or an LPO.
3652:
3653: Finally, the techniques presented here have also been applied to weak
3654: termination in~\cite{FGK-ter-faible-ICTAC-2004}.
3655:
3656: As our proof process is very closed to the rewriting mechanism, it could easily
3657: be extended to conditional, equational and typed rewriting,
3658: by simply adapting the narrowing definition.
3659: Our approach is also promising to tackle inductive proofs of other term
3660: properties like confluence or ground reducibility.
3661:
3662: \appendix
3663: \section*{APPENDIX}
3664: %\setcounter{section}{1}
3665:
3666: \section{The lifting lemma}
3667:
3668: The lifting lemma for standard narrowing~\cite{MiddeldorpH-AAECC94}
3669: can be locally adapted to $S${-}rewriting with non-normalized substitutions
3670: provided they fulfill some constraints on the positions of rewriting.
3671: To do so, we need the following
3672: two propositions (the first one is obvious).
3673:
3674: \begin{proposition}\label{prop:obvious}
3675: Let $t \in \TXF$ and $\sigma$ a substitution of $\TXF$.
3676: Then $Var(\sigma t) = (Var(t) - Dom(\sigma)) \cup Ran(\sigma_{Var(t)})$.
3677: \end{proposition}
3678:
3679: \begin{proposition}\label{prop:congruence}
3680: Suppose we have substitutions $\sigma, \mu, \nu$ and sets $A,B$ of variables
3681: such that
3682: $(B - Dom(\sigma)) \cup Ran(\sigma) \subseteq A$.
3683: If $\mu = \nu [A]$ then $\mu \sigma = \nu \sigma [B]$.
3684: \end{proposition}
3685:
3686: \begin{proof}
3687: Let us consider $(\mu \sigma)_B$, which can be divided as follows:
3688: $(\mu \sigma)_B = (\mu \sigma)_{B \cap Dom(\sigma)} \cup
3689: (\mu \sigma)_{B - Dom(\sigma)}$.\\
3690: For $x \in B \cap Dom(\sigma)$, we have $\Var(\sigma x)
3691: \subseteq Ran(\sigma)$, and then
3692: $(\mu \sigma) x = \mu(\sigma x) = \mu_{Ran(\sigma)}(\sigma x) =
3693: (\mu_{Ran(\sigma)} \sigma) x$.
3694: Therefore $(\mu \sigma)_{B \cap Dom(\sigma)} =$\\
3695: $(\mu_{Ran(\sigma)} \sigma)_{B \cap Dom(\sigma)}$.\\
3696: For $x \in B - Dom(\sigma)$, we have $\sigma x = x$, and then
3697: $(\mu \sigma) x = \mu(\sigma x) = \mu x$.
3698: Therefore we have $(\mu \sigma)_{B-Dom(\sigma)} = \mu_{B - Dom(\sigma)}$.
3699: Henceforth we get
3700: $(\mu \sigma)_B = (\mu_{Ran(\sigma)} \sigma)_{B \cap Dom(\sigma)}$
3701: $\cup \mu_{B - Dom(\sigma)}$.\\
3702: By a similar reasoning, we get
3703: $(\nu \sigma)_B = (\nu_{Ran(\sigma)} \sigma)_{B \cap Dom(\sigma)}
3704: \cup \nu_{B - Dom(\sigma)}$.\\
3705: By hypothesis, we have $Ran(\sigma) \subseteq A$ and $\mu = \nu [A]$. Then
3706: $\mu_{Ran(\sigma)} = \nu_{Ran(\sigma)}$. Likewise, since $B - Dom(\sigma)
3707: \subseteq A$, we
3708: have $\mu_{B - Dom(\sigma)} = \nu_{B - Dom(\sigma)}$.\\
3709: Then we have $(\mu \sigma)_B = (\mu_{Ran(\sigma)} \sigma)_{B \cap Dom(\sigma)}
3710: \cup \mu_{B - Dom(\sigma)}=$\\
3711: $({\nu}_{Ran(\sigma)} \sigma)_{B \cap Dom(\sigma)}
3712: \cup {\nu}_{B - Dom(\sigma)} = (\nu \sigma)_B$.
3713: Therefore $(\mu \sigma)= (\nu \sigma) [B]$.
3714: \end{proof}
3715:
3716:
3717: \begin{lemma}[\ref{lemma:surred-S}\ ($S${-}lifting Lemma)]
3718:
3719: Let $\R$ be a rewrite system.
3720: Let $s \in \TXF$, $\alpha$ a ground
3721: substitution such that $\alpha s$ is $S${-}reducible
3722: at a non variable position $p$ of $s$, and ${\cal Y} \subseteq {\cal X}$
3723: a set of variables
3724: such that $Var(s) \cup Dom(\alpha) \subseteq {\cal Y}$.
3725: If $\alpha s \ra^{S}_{p, l \ra r} t'$, then there exist a term $s' \in
3726: \TXF$ and substitutions
3727: $\beta, \sigma = \sigma_0 \wedge \bigwedge_{j \in [1..k]} \overline{\sigma_j}$
3728: such that:
3729:
3730: \[
3731: \begin{array}{ll}
3732:
3733: 1.~s \surred^{S}_{p, l \ra r, \sigma} s', \\
3734: 2.~\beta s' = t', \\
3735: 3.~\beta \sigma_0 = \alpha [{\cal Y}]\\
3736: 4.~\beta {\rm ~satisfies~} \bigwedge_{j \in [1..k]} \overline{\sigma_j}.
3737:
3738: \end{array}
3739: \]
3740:
3741:
3742: where $\sigma_0$ is the most general unifier of $s|_p$ and $l$ and
3743: $\sigma_j, j \in [1..k]$ are
3744: all most general unifiers of $\sigma_0 s|_{p'}$ and a left-hand side
3745: $l'$ of a rule of $\R$, for all position $p'$ which are $S$-better
3746: positions than $p$ in $s$.
3747: \end{lemma}
3748:
3749: \begin{proof}
3750: In the following, we assume that ${\cal Y} \cap \Var(l) = \emptyset$ for every
3751: $l \ra r \in \R$.\\
3752: If $\alpha s \ra^{S}_{p, l \ra r} t'$, then there exists a substitution $\tau$
3753: such that $Dom(\tau) \subseteq \Var(l)$ and $(\alpha s)|_p = \tau l$.
3754: Moreover, since $p$ is a non variable position of $s$, we have $(\alpha s)|_p
3755: = \alpha(s|_p)$.
3756: Denoting $\mu = \alpha \tau$, we have:
3757: \\
3758: \begin{tabular}{lll}
3759: $\mu(s|_p)$ & $= \alpha(s|_p)$ & for $Dom(\tau) \subseteq \Var(l)$ and
3760: $\Var(l) \cap \Var(s) = \emptyset$\\
3761: & $= \tau l$ & by definition of $\tau$\\
3762: & $= \mu l$ & for $Dom(\alpha) \subseteq {\cal Y}$ and ${\cal Y} \cap
3763: \Var(l) = \emptyset$,
3764: \end{tabular}
3765: \\
3766: and therefore $s|_p$ and $l$ are unifiable.
3767: Let us note $\sigma_0$ the most general unifier of $s|_p$ and $l$, and
3768: $s' = \sigma_0(s[r]_p)$.
3769:
3770: Since $\sigma_0$ is more general than $\mu$, there exists a substitution
3771: $\rho$ such that $\rho \sigma_0 = \mu$.
3772: Let ${\cal Y}_1 = ({\cal Y} - Dom(\sigma_0)) \cup Ran(\sigma_0)$.
3773: We define $\beta = \rho_{{\cal Y}_1}$.
3774: Clearly $Dom(\beta) \subseteq {\cal Y}_1$.\\
3775: We now show that $\Var(s') \subseteq {\cal Y}_1$, by the following reasoning:
3776: \begin{itemize}
3777: \item since $s' = \sigma_0(s[r]_p)$, we have
3778: $\Var(s') = \Var(\sigma_0(s[r]_p))$;
3779: \item the rule $l \ra r$ is such that $\Var(r) \subseteq \Var(l)$,
3780: therefore we have
3781: $\Var(\sigma_0(s[r]_p)) \subseteq \Var(\sigma_0(s[l]_p))$, and then,
3782: thanks to the previous point,
3783: $\Var(s') \subseteq \Var(\sigma_0(s[l]_p))$;
3784: \item since $\sigma_0(s[l]_p) = \sigma_0 s [\sigma_0 l]_p$ and
3785: since $\sigma_0$ unifies $l$ and $s|_p$, we get
3786: $\sigma_0(s[l]_p) = (\sigma_0 s) [\sigma_0(s|_p)]_p = \sigma_0 s[s|_p]_p =
3787: \sigma_0 s$ and, thanks to the
3788: previous point: $\Var(s') \subseteq \Var(\sigma_0 s)$;
3789: \item according to Proposition \ref{prop:obvious}, we have
3790: $\Var(\sigma_0(s)) = (\Var(s)$ $ - Dom(\sigma_0)) \cup Ran(\sigma_{0\Var(s)})$;
3791: by hypothesis, $\Var(s) \subseteq {\cal Y}$. Moreover, since
3792: $Ran(\sigma_{0\Var(s)}) \subseteq Ran(\sigma_0)$, we have \\
3793: $\Var(\sigma_0(s)) \subseteq ({\cal Y} - Dom(\sigma_0)) \cup Ran(\sigma_0)$,
3794: that is
3795: $\Var(\sigma_0 s) \subseteq {\cal Y}_1$.
3796: Therefore, with the previous point, we get $Var(s') \subseteq {\cal Y}_1$.
3797: \end{itemize}
3798:
3799: From $Dom(\beta) \subseteq {\cal Y}_1$ and
3800: $Var(s') \subseteq {\cal Y}_1$, we infer
3801: $Dom(\beta) \cup Var(s') \subseteq {\cal Y}_1$.
3802:
3803: Let us now prove that $\beta s' = t'$.\\
3804: Since $\beta = \rho_{{\cal Y}_1}$, we have $\beta = \rho [{\cal Y}_1]$.
3805: Since $Var(s') \subseteq {\cal Y}_1$, we get
3806: $\beta s' = \rho s'$.
3807: Since $s' = \sigma_0(s[r]_p)$, we have
3808: $\rho s' = \rho \sigma_0(s[r]_p) = \mu(s[r]_p) = \mu s[\mu r]_p$.
3809: Then $\beta s' = \mu s[\mu r]_p$.\\
3810: We have $Dom(\tau) \subseteq \Var(l)$ and ${\cal Y} \cap \Var(l) = \emptyset$,
3811: then we have ${\cal Y} \cap Dom(\tau) = \emptyset$. Therefore,
3812: from $\mu = \alpha \tau$, we get $\mu = \alpha [{\cal Y}]$.
3813: Since $\Var(s) \subseteq {\cal Y}$, we get $\mu s = \alpha s$.\\
3814: Likewise, by hypothesis we have $Dom(\alpha) \subseteq {\cal Y}$,
3815: $\Var(r) \subseteq \Var(l)$ and ${\cal Y} \cap \Var(l) = \emptyset$, then we get
3816: $Var(r) \cap Dom(\alpha) = \emptyset$, and then we have $\mu = \tau [Var(r)]$,
3817: and therefore $\mu r = \tau r$.\\
3818: From $\mu s = \alpha s$ and $\mu r = \tau r$ we get $\mu s [\mu r]_p =
3819: \alpha s [\tau r]_p$.
3820: Since, by hypothesis, $\alpha s \ra^p t'$, with $\tau l = (\alpha s)|_p$,
3821: then $\alpha s [\tau r]_p = t'$.
3822: Finally, as $\beta s' = \mu s[\mu r]_p$, we get $\beta s' = t'$ (2).
3823:
3824: Next let us prove that $\beta \sigma_0 = \alpha [{\cal Y}]$.
3825: Reminding that ${\cal Y}_1 = ({\cal Y} - Dom(\sigma_0)) \cup Ran(\sigma_0)$,
3826: Proposition \ref{prop:congruence} (with the notations $A$ for ${\cal Y}_1$,
3827: $B$ for $\cal Y$, $\mu$ for $\beta$, $\nu$ for $\rho$ and $\sigma$ for $\sigma_0$)
3828: yields $\beta \sigma_0 = \rho \sigma_0 [{\cal Y}]$.
3829: We already noticed that $\mu = \alpha [{\cal Y}]$.
3830: Linking these two equalities via the equation $\rho \sigma_0 = \mu$ yields
3831: $\beta \sigma_0 = \alpha [{\cal Y}]$ (3).
3832:
3833:
3834: Let us now suppose that there exist a rule $l' \ra r' \in \R$, a
3835: position $p'$ $S${-}better than $p$ and a substitution $\sigma_i$ such
3836: that $\sigma_i(\sigma_0(s|_{p'})) = \sigma_i l'$.
3837:
3838: Let us now suppose that $\beta$ does not satisfy
3839: $\bigwedge_{j \in [1..k]} \overline{\sigma_j}$.
3840: There exists $i \in [1..k]$ such that $\beta$ satisfies $\sigma_i =
3841: \bigwedge _{i_l \in [1..n]} (x_{i_l} = u_{i_l})$. So $\beta$ is such that
3842: $\bigwedge _{i_l \in [1..n]} (\beta x_{i_l} = \beta u_{i_l})$.
3843:
3844: Thus, on $Dom(\beta) \cap Dom(\sigma_i) \subseteq \{x_{i_l}, i_l
3845: \in[1..n]\}$, we have $(\beta x_{i_l} = \beta u_{i_l})$, so $\beta
3846: \sigma_i = \beta$.
3847: Moreover, as $\beta$ is a ground substitution, $\sigma_i \beta = \beta$. Thus,
3848: $\beta \sigma_i = \sigma_i \beta$.
3849:
3850: On $Dom(\beta) \cup Dom(\sigma_i) -(Dom(\beta) \cap Dom(\sigma_i))$,
3851: either $\beta = Id$, or $\sigma_i = Id$, so $\beta \sigma_i = \sigma_i
3852: \beta$.
3853:
3854:
3855: %NON
3856: %By construction, we
3857: %may choose $Ran(\sigma_i) \cap Dom(\beta) = \emptyset$. With this
3858: %condition, and since $\beta$ is a ground substitution, we get:
3859: %$\beta \sigma_i = \sigma_i \beta = \beta [\Var(\sigma_0(s))]$.
3860: As a consequence,
3861: $\alpha(s) = \sigma_i \alpha(s) = \sigma_i \beta \sigma_0(s) = \beta
3862: \sigma_i \sigma_0 (s)$ is reducible at position $p'$ with the rule
3863: $l'$, which is impossible by definition of S-reducibility of
3864: $\alpha(s)$ at position $p$.
3865: So the ground substitution $\beta$ satisfies
3866: $\bigwedge_{i \in [1..k]} \overline{\sigma_i}$
3867: for all most general unifiers $\sigma_i$ of $\sigma_0 s$ and a left-hand side of
3868: rule of $\R$ at $S${-}better positions of $p$ (4).
3869:
3870: Therefore, denoting $\sigma = \sigma_0 \wedge \bigwedge_{i \in [1..k]}
3871: \overline{\sigma_i}$,
3872: from the beginning of the proof,
3873: we get $s \surred^{S}_{[p, l \ra r, \sigma]} s'$, and
3874: then the point (1) of the current lemma holds.
3875: \end{proof}
3876:
3877:
3878: \section{Proof of the generic termination result}
3879:
3880: Let us remind that $\mathit{SUCCESS(g,\succ)}$ means that
3881: the application of $\mathit{Strat{-}Rules(S)}$
3882: on $(\{g(x_1, \ldots , x_m)\},$ $\top,\top)$
3883: gives a finite proof tree, whose sets $C$ of ordering constraints
3884: are satisfied by a same ordering $\succ$, and
3885: whose leaves
3886: are either states of the form $(\emptyset,A,C)$ or states
3887: whose set of constraints $A$ is unsatisfiable.
3888:
3889:
3890:
3891: \begin{subtheorem}
3892: [\ref{theo:termin}]
3893:
3894: Let $R$ be a rewrite system on a set $\F$ of symbols containing at least a
3895: constructor constant. If there exists an $\F$-stable ordering $\succ$
3896: having the subterm property, such that for each symbol $g \in \Def$,
3897: we have $\mathit{SUCCESS(g,\succ)}$, then every term of $\TF$ terminates with
3898: respect to the strategy $S$.
3899:
3900: \end{subtheorem}
3901:
3902: \begin{proof}
3903: We use an emptyness lemma, an abstraction lemma, a narrowing lemma,
3904: and a stopping lemma, which are given after this main proof.
3905:
3906: We prove by induction on $\TF$ that any ground instance
3907: $\theta f(x_1, \ldots,$ $x_m)$ of
3908: any term $f(x_1, \ldots ,x_m) \in \TXF$ S-terminates.
3909: The induction ordering is constrained along the proof. At the
3910: beginning, it has at least to be $\F$-stable and to have the
3911: subterm property, which ensures its noetherianity.
3912: Such an ordering always exists on $\TF$ (for instance the embedding
3913: relation). Let us denote it $\succ$.\\
3914:
3915: %Cas constructeur
3916:
3917: If $f$ is a constructor, then $\theta f(x_1, \ldots ,x_m) \da =
3918: f(\theta x_1, \ldots ,\theta x_m) \da =
3919: [f(\theta x_1, \ldots,\theta x_m)$
3920: $[\theta x_{i_1} \da]_{i_1}\ldots[\theta x_{i_p} \da]_{i_p}]\da$,
3921: where $\{i_1, \ldots, i_p\} \in [1..m]$
3922: are the highest positions in $f(\theta x_1,$ $ \ldots,\theta x_m)$, where
3923: subterms can be normalized, according to the strategy $S$.
3924: (More specifically, $\{i_1, \ldots, i_p\} = [1..m]$ if $\mathit{S = Innermost}$
3925: or $\mathit{S = Outermost}$, $\{i_1, \ldots,
3926: i_p\}$ $ = \{j|$ $j \in \{p_1, \ldots p_n\}, j \neq 0\}$ where $[p_1,
3927: \ldots, p_n]=LS(f)$ if $\mathit{S = Local{-}Strat}$.)
3928: % and $\{i_1, \ldots, i_p\}$
3929: %are the highest positions such that $f(\theta x_1, \ldots ,\theta
3930: %x_m)[x_{i_1}]_{i_1}\ldots[x_{i_p}]_{i_p}$ is not narrowable if $S =
3931: %Outermost$.)
3932:
3933: By subterm property of $\succ$, we have $\theta f(x_1, \ldots ,x_m) =
3934: f(\theta x_1, \ldots ,\theta x_m)$ $ \succ \theta x_{i_1},$ $ \ldots ,\theta
3935: x_{i_p}$. Then, by induction hypothesis, we suppose that $\theta
3936: x_{i_1},$ $\ldots ,\theta x_{i_p}$ S-terminate, and so their respective
3937: normal forms $\theta x_{i_1} \da, \ldots,$ $\theta x_{i_p} \da$ exist
3938: and $f(\theta x_1, \ldots,\theta x_m)$ $[\theta x_{i_1}
3939: \da]_{i_1}\ldots[\theta x_{i_p} \da]_{i_p}$ is in normal form. We may
3940: thus restrict our attention to terms headed by a defined symbol.\\
3941:
3942:
3943: %Cas non constructeur
3944:
3945: If $f$ is not a constructor, let us denote it $g$ and prove that
3946: $g(\theta x_1 , \ldots,$ $\theta x_m)$ S-terminates for any $\theta$
3947: satisfying $A$ $= \top$ if we have $\mathit{SUCCESS{-}S(h,\succ)}$ for every
3948: defined symbol $h$. Let us denote $g(x_1 , \ldots ,x_m)$ by
3949: $t_{\mathit{ref}}$ in the sequel of the proof.
3950:
3951: To each state $s$ of the proof tree of $g$, characterized by a current
3952: term $t$ and the set of constraints $A$, we associate the set of
3953: ground terms $G = \{\alpha t ~|~ \alpha {\rm ~satisfies~} A\}$, that
3954: is the set of ground instances represented by $s$.
3955:
3956: Inference rule \rname{Abstract} (resp. \rname{Narrow}) transforms
3957: $(\{t\},A)$ into $(\{t'\},A')$ to which is associated $G' = \{\beta t'
3958: ~|~ \beta {\rm ~satisfies~} A'\}$ (resp. into $(\{t'_i\},A'_i), i
3959: \in [1..l]$ to which are associated $G' = \{\beta_i t'_i ~|~
3960: \beta_i {\rm ~satisfies}$ $A'_i\}$).
3961:
3962: By abstraction (resp. narrowing) Lemma, applying \rname{Abstract}
3963: (resp. \rname{Narrow}), for each $\alpha t$ in
3964: $G$, there exists a
3965: $\beta t'$ (resp. $\beta_i t'_i$) in $G'$ and such that
3966: S-termination of $\beta t'$ (resp. of the $\beta_i t'_i$) implies
3967: S-termination of $\alpha t$.
3968:
3969: When the inference rule \rname{Stop} applies on $(\{t\},A,C)$:
3970: \begin{itemize}
3971: \item either $A$ is satisfiable, in which case,
3972: by stopping lemma, every term of
3973: $G = \{\alpha t ~|~ \alpha {\rm ~satisfies~} A\}$
3974: is S-terminating,
3975:
3976: \item {or $A$ is unsatisfiable.} In this case, $G$ is empty.
3977: By emptyness lemma, all previous states on the branch correspond
3978: to empty sets $G_i$, until an ancestor state $(\{t_p\},A_p,C_p)$,
3979: where $A_p$ is satisfiable.
3980: Then every term $\alpha t$ of $G_p$ is irreducible, otherwise, by
3981: Abstraction and Narrowing lemmas, $G_{p+1}$ would not be empty.
3982: \end{itemize}
3983:
3984: Therefore, S-termination is ensured for all terms in all sets $G$
3985: of the proof tree.\\
3986:
3987:
3988: As the process is initialized with $\{t_{\mathit{ref}}\}$ and a
3989: constraint problem satisfiable by any ground substitution, we get that
3990: $g(\theta x_1, \ldots , \theta x_m)$ is S-terminating, for any
3991: $t_{\mathit{ref}}=g(x_1, \ldots , x_m)$, and any ground instance
3992: $\theta$.
3993: \end{proof}
3994:
3995:
3996:
3997:
3998: \vspace{3mm}
3999:
4000: \begin{lemma}
4001: [(Emptyness lemma)]
4002: Let $(\{t\}, A,C)$ be a state of any proof tree, giving
4003: $(\{t'\}, A',C')$ by application of \rname{Abstract} or \rname{Narrow}.
4004: If $A$ is unsatisfiable, then so is $A'$.
4005: \end{lemma}
4006:
4007: \begin{proof}
4008: If \rname{Abstract} is applied, then if $A$ is unsatisfiable,
4009: $A' = A \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con
4010: X_{i_p}$ is also unsatisfiable.
4011:
4012: If \rname{Narrow} is applied, then
4013: if $A$ is unsatisfiable (which does not occur for local strategies),
4014: $A'=A \wedge \sigma$ in the innermost case, and $A'=R(t) \wedge A \wedge \sigma$
4015: in the outermost case are also unsatisfiable.
4016: \end{proof}
4017: \vspace{3mm}
4018:
4019:
4020: \begin{lemma}
4021: [(Abstraction lemma)]
4022: Let $(\{t\}, A,C)$ be a state of any proof tree, giving
4023: the state
4024: $(\{t'= t[X_j]_{j \in \{i_1,\ldots,i_p\} }\},$ $ A',C')$
4025: by application of \rname{Abstract}.
4026:
4027: For any ground substitution $\alpha$ satisfying $A$,
4028: if $\alpha t$ is reducible, there exists $\beta$ such that S-termination of
4029: $\beta t'$ implies S-termination of $\alpha t$.
4030: Moreover, $\beta$ satisfies $A'$.
4031: \end{lemma}
4032:
4033: \begin{proof}
4034:
4035: We prove that $\alpha t \ra^{* S} \beta
4036: t'$, where $\beta = \alpha \cup \bigcup_{j \in \{i_1,\ldots,i_p\}} X_j =
4037: \alpha t|_j \da$.
4038:
4039: First, whatever the strategy $S$, the abstraction positions in $t$ are
4040: chosen so that the $\alpha t|_j$ can be supposed terminating w.r.t. $S$.
4041: Indeed, each term $t|_{i_j}$ is such that:
4042: \begin{itemize}
4043:
4044: \item
4045: either $\mathit{TERMIN(S,t|_j)}$ is true, and then by definition of the predicate
4046: $\mathit{TERMIN}$, $\alpha t|_j$ S-terminates;
4047:
4048: \item
4049: or $t_{ref} > t|_j$ is satisfiable by $\succ$, and then, by induction
4050: hypothesis, $\alpha t|_j$ S-terminates.
4051:
4052: \end{itemize}
4053: So the $\alpha t|_j \da exist.$
4054:
4055: Then, let us consider the different choices of abstraction positions w.r.t
4056: the strategy S:
4057: \begin{itemize}
4058: \item either $\mathit{S=Innermost}$, and whatever the positions $i_1,\ldots,i_p$ in
4059: the term $t$, we have $\alpha t \ra^{* Inn}$ $ \alpha t[\alpha t|_{i_1} \da]_{i_1}\ldots$
4060: $[\alpha t|_{i_p} \da]_{i_p} = \beta t'$;
4061:
4062: \item either $\mathit{S=Outermost}$ and $t$ is abstracted
4063: at positions $i_1,\ldots,i_p$ if $t[X_j]_{j\in \{i_1,\ldots,i_p\} }$
4064: is not outermost narrowable at prefix positions of $i_1,\ldots,i_p$,
4065: which warrants that the only redex positions of
4066: $\alpha t$ are suffixes of the $j$, and then that
4067: $\alpha t \ra^{* Outermost}
4068: \alpha t[\alpha t|_{i_1} \da]_{i_1}\ldots$
4069: $[\alpha t|_{i_p} \da]_{i_p} = \beta t'$;
4070:
4071: \item or $\mathit{S=Local{-}Strat}$ and $top(t)=f$ with $LS(f)=[p_1,\ldots,p_n]$.
4072: The term $t$ is abstracted
4073: at positions $i_1,\ldots,i_p \in \{p_1,\ldots,p_{k-1}\}$,
4074: if $\exists k \in [2..n] : p_1,\ldots,p_{k-1} \neq 0,
4075: p_k = 0$, or at positions $i_1,\ldots,i_p \in \{p_1,\ldots,p_n\}$
4076: if $p_1,\ldots,p_n \neq 0$.
4077: According to the definition of local strategies, $\alpha t \ra^{* Local{-}Strat}
4078: \alpha t[\alpha t|_{i_1} \da]_{i_1}\ldots$
4079: $[\alpha t|_{i_p} \da]_{i_p} = \beta t'$.
4080:
4081: If $LS(f)=[]$ or $LS(f)=[0,p_2,\ldots,p_n]$, then $t=t'$ and $A=A'$,
4082: so $\alpha t = \beta t'$.\\
4083:
4084: So $\alpha t \ra^{* S} \beta t'$ for any normal form $\alpha t|_j \da$ of
4085: $\alpha t|_j$, for $j \in \{i_1,\ldots,i_p]\}$.
4086: Then, S-termination of
4087: $\beta t'$ implies S-termination of $\alpha t$.
4088:
4089: Clearly in all cases, $\beta$ satisfies
4090: $A' = A \wedge t|_{i_1} \con X_{i_1} \ldots \wedge t|_{i_p} \con
4091: X_{i_p}$,
4092: provided the $X_i$ are not in $Dom(\alpha)$, which is true
4093: since the $X_i$ are fresh variables not appearing in $A$.
4094:
4095: \end{itemize}
4096: \end{proof}
4097: \vspace{3mm}
4098:
4099: \begin{lemma}
4100: [(narrowing lemma)]
4101: Let $(\{t\}, A,C)$ be a state of any proof tree, giving
4102: the states
4103: $(\{v_i\}, $ $A'_i, C'_i), i \in [1..l]$,
4104: by application of \rname{Narrow}.
4105: For any ground substitution $\alpha$ satisfying $A$,
4106: if $\alpha t$ is reducible, then, for each $i \in [1..l]$,
4107: there exist $\beta_i$
4108: such that S-termination of the $\beta_i v_i, i \in [1..l]$,
4109: implies S-termination of $\alpha t$.
4110: Moreover, $\beta_i$ satisfies $A'_i$ for each $i \in [1..l]$.
4111: \end{lemma}
4112:
4113: \begin{proof}
4114: \vspace{1mm}
4115:
4116: We reason by case on the different strategies.
4117:
4118: \begin{itemize}
4119: \item
4120: Either $\mathit{S = Innermost}$, and
4121: By lifting lemma, there is a
4122: term $v$ and substitutions $\beta$ and
4123: $\sigma = \sigma_0 \wedge \bigwedge_{j \in [1..k]} \overline{\sigma_j}$,
4124: corresponding to each rewriting step
4125: $\alpha f(u_1,\ldots,u_m)$ $
4126: \ra^{Inn}_{p, l \ra r} t'$, such that:
4127:
4128: \[
4129: \begin{array}{ll}
4130: 1.~t=f(u_1,\ldots,u_m) \surred^{Inn}_{p, l \ra r,\sigma} v,\\
4131: 2.~\beta v = t', \\
4132: 3.~\beta \sigma_0 = \alpha [{\cal Y}]\\
4133: 4.~\beta {\rm ~satisfies~} \bigwedge_{j \in [1..k]} \overline{\sigma_j}.
4134: \end{array}
4135: \]
4136: where $\sigma_0$ is the most general unifier of $t|_p$ and $l$ and
4137: $\sigma_j, j \in [1..k]$ are
4138: all most general unifiers of $\sigma_0 t|_{p'}$ and a left-hand side
4139: $l'$ of a rule of $\R$, for all position $p'$ which are
4140: suffix positions of $p$ in $t$.
4141:
4142:
4143:
4144:
4145: These narrowing steps are effectively produced by the rule
4146: \rname{Narrow}, applied in all possible ways on $f(u_1, \ldots ,u_m)$.
4147: So a term $\beta v$ is
4148: produced for every innermost rewriting branch starting from
4149: $\alpha t$.
4150: Then innermost termination of the $\beta v$ implies
4151: innermost termination of $\alpha t$.
4152:
4153:
4154: Let us prove that $\beta$ satisfies
4155: $A'= A \wedge \sigma_0 \wedge \bigwedge_{j \in [1..k]}
4156: \overline{\sigma_j}$.
4157:
4158: By lifting lemma, we have $\alpha = \beta \sigma_0$ on ${\cal Y}$.
4159: As we can take ${\cal Y} \supseteq Var(A)$, we have $\alpha = \beta
4160: \sigma_0$ on $Var(A)$.
4161:
4162: More precisely, on $Ran(\sigma_0)$, $\beta$ is such that $\beta \sigma_0 = \alpha$
4163: and on $Var(A) \setminus Ran(\sigma_0)$, $\beta = \alpha$.
4164: As $Ran(\sigma_0)$ only contains fresh variables, we have $Var(A)
4165: \cap Ran(\sigma_0) = \emptyset$, so $Var(A) \setminus Ran(\sigma_0) =
4166: Var(A)$.
4167: So $\beta = \alpha$ on $Var(A)$ and then, $\beta$ satisfies $A$.
4168:
4169: Moreover, as $\beta \sigma_0 = \alpha$ on $Dom(\sigma_0)$,
4170: $\beta$ satisfies $\sigma_0$.
4171:
4172: So $\beta$ satisfies $A \wedge \sigma_0$.
4173: Finally, with the point 4. of the lifting lemma, we conclude that
4174: $\beta$ satisfies $A'= A \wedge \sigma_0 \wedge \bigwedge_{j \in [1..k]}
4175: \overline{\sigma_j}$.
4176:
4177:
4178: \vspace{3mm}
4179: \item Either $\mathit{S = Local{-}Strat}$, and
4180: \rname{Narrow} is applied on $\{t=f(u_1, \ldots, $ $u_m)\}$ with $l =
4181: [0,p_1, \ldots ,p_n]$.
4182: For any $\alpha$ satisfying $A$,
4183:
4184: \begin{itemize}
4185:
4186: \item either
4187: $\alpha f(u_1, \ldots ,u_m)$ is irreducible at the top position, but may
4188: be reduced at the positions $p_1, \ldots ,p_n$.
4189: In this case, either $f(u_1, \ldots ,u_m)$
4190: is not narrowable at the top position,
4191: either $ f(u_1, \ldots ,u_m)$ $ \leadsto_{\epsilon, \sigma_i} v_i$
4192: for $i \in [1..l]$ and
4193: $A \wedge \sigma_i$ is unsatisfiable for each $i$,
4194: or there exists $i \in [1..l]$ such that
4195: $ f(u_1, \ldots ,u_m) \leadsto_{\epsilon, \sigma_i} v_i$ and
4196: $A \wedge \sigma_i$ is satisfiable.
4197:
4198: In the first two cases, \rname{Narrow} produces the state
4199: $(\{t^{[p_1, \ldots ,p_n]}\},$ $A,C)$, and setting $\beta = \alpha$,
4200: we obtain that termination of $\beta t^{[p_1, \ldots ,p_n]}$ implies termination of
4201: $\alpha t^{[0,p_1, \ldots ,p_n]}$,
4202: and that $\beta$ satisfies $A'=A$.
4203:
4204: In the third case, \rname{Narrow} produces the state
4205: $(\{t^{[p_1, \ldots ,p_n]}\},
4206: A \wedge (\bigwedge_{i=1}^l \overline{\sigma_i}),C)$,
4207: and setting $\beta = \alpha$,
4208: we have termination of $\beta t^{[p_1, \ldots ,p_n]}$ implies termination of
4209: $\alpha t^{[0,p_1, \ldots ,p_n]}$.
4210: Moreover, as $\alpha t$ is not reducible at the top position,
4211: $\alpha = \beta$ satisfies $(\bigwedge_{i=1}^l \overline{\sigma_i})$.
4212: Thus, as $\alpha$ satisfies $A$, $\beta$ satisfies $A'=A
4213: \wedge (\bigwedge_{i=1}^l \overline{\sigma_i})$.
4214:
4215:
4216: \item or $\alpha f(u_1, \ldots ,u_m)$ is reducible at the top
4217: position,
4218: and by lifting lemma, there is a
4219: term $v$ and substitutions $\beta$ and
4220: $\sigma_0$ corresponding to each rewriting step $\alpha f(u_1,\ldots,u_m)
4221: \ra_{\epsilon, l \ra r} t'$, such that:
4222:
4223: \[
4224: \begin{array}{ll}
4225: 1.~t=f(u_1,\ldots,u_m) \surred_{\epsilon, l \ra r,\sigma_0} v,\\
4226: 2.~\beta v = t', \\
4227: 3.~\beta \sigma_0 = \alpha [{\cal Y}].
4228: \end{array}
4229: \]
4230:
4231: where $\sigma_0$ is the most general unifier of $t$ and $l$.
4232:
4233: These narrowing steps are effectively produced by
4234: \rname{Narrow}, which is applied in all possible ways on
4235: $f(u_1, \ldots ,u_m)$ at the top position.
4236: So a term $\beta v$ is
4237: produced for every LS-rewriting step applying on
4238: $\alpha t$ at the top position.
4239: Then termination of the $\beta v$ implies
4240: termination of $\alpha t$ for the given LS-strategy.
4241:
4242:
4243: %Finally,
4244: %since \rname{Narrow{-}Y} is applied with all possible substitutions and
4245: %all possible rewrite rules,
4246: %a term $\beta v$ is
4247: %produced on any LS-rewriting branch starting from $\alpha
4248: %f(u_1, \ldots ,u_m)$.
4249:
4250: We prove that $\beta$ satisfies $A \wedge \sigma_0$
4251: like in the innermost case, except that there is no negation of
4252: substitution here.
4253:
4254: \end{itemize}
4255: \vspace{3mm}
4256:
4257: %The domain of $\sigma$ can be extended in the same way
4258: %by setting $\sigma x = x$ for $x \in (Var(A) \cup Range(\sigma) \cup Var(C))-
4259: %Var(f(u_1, \ldots ,u_m))$.
4260:
4261:
4262: %Let $ A = (v_i=v'_i, i \in [1..p]) \wedge(v_i \da=v'_i, i \in [1..q] )$ and
4263: %$\sigma = (x_i=t_i, i \in [1..r])$.
4264: %We then have $A \wedge \beta \sigma = (v_i=v'_i, i \in [1..p]) \wedge(v_i \da=v'_i, i \in [1..q] )
4265: %\wedge (x_i= \beta t_i, i \in [1..r])$. This formula is true if
4266:
4267:
4268: %Let us split the domain $\{x_i, i \in [1..r]\}$
4269: %of $\sigma$ into $\{x_j, j \in \{i_1,\ldots, i-k\}, x_j \in Var(A)\}$ and
4270: %$\{x_j, j \in [1..r] \setminus \{i_1,\ldots, i-k\}, x_j \not \in Var(A)\}$.
4271: %Obviously, $A \wedge \{x_j = \beta t_j, j \in [1..r] \setminus \{i_1,\ldots, i-k\}, x_j
4272: %\not \in Var(A)\}$ is true.
4273: %$On another hand, $A \wedge \{x_j = \beta t_j, j \in
4274: %\{i_1,\ldots, i-k\}, x_j \in Var(A)\}$ is true if
4275:
4276:
4277: \vspace{3mm}
4278:
4279: \item Or $\mathit{S= Outermost}$, and
4280: in this case, $t=f(u_1, \ldots ,u_n)$ is renamed into $t_0=f(u_1,\ldots,u_n)^{\rho}$.
4281: $A$ then becomes
4282: $A_0 = A \cup R(f(u_1,\ldots,$ $u_n))$ where
4283: $\rho = (x_1 \red x'_1) \ldots (x_k \red x'_k)$.
4284:
4285: We first show that if every $\beta_0 t_0$ outermost
4286: terminates, for $\beta_0 {\rm ~satisfying~} A_0$,
4287: then every $\alpha t$ outermost terminates.
4288:
4289: If $A$ is satisfiable, then $A_0$ is satisfiable.
4290: Indeed, $A_0 = A \cup
4291: f(u_1, \ldots$ $ ,u_m) \red
4292: f(u_1, \ldots$ $ ,u_m)^{\rho}$, with $\rho = (x_1 \red x'_1)
4293: \ldots (x_k \red x'_k)$.
4294: In addition, the $x_i$ are the
4295: variables of $f(u_1,\ldots,u_n)$.
4296:
4297: If $A = \top$, then $A_0 = f(u_1, \ldots$ $ ,u_m) \red
4298: f(u_1, \ldots$ $ ,u_m)^{\rho}$,
4299: which is always satisfiable.
4300: If $A \neq \top$, since they are the variables of $f(u_1,\ldots,u_n)$,
4301: the $x_i$ can appear in $A$, either in abstracted subterms,
4302: either as new abstraction variables,
4303: either in the right hand-sides of equalities and disequalities defining
4304: the substitution of the previous narrowing step,
4305: or as new variables introduced by the previous reduction renaming step.
4306: In any case, the formula in which they appear is compatible with
4307: $f(u_1, \ldots$ $ ,u_m) \red f(u_1, \ldots, u_m)^{\rho}$.
4308: More precisely, for the $\theta x_i$ such that $\theta$ satisfies $A$,
4309: $\theta$ can be extended on the variables $x'_i$, in such a way that
4310: $A_0$ is satisfiable.
4311: Then $A_0 = A \cup f(u_1, \ldots, u_m) \red
4312: f(u_1, \ldots$ $ ,u_m)^{\rho}$ is satisfiable.\\
4313:
4314:
4315: By definition of $A_0$, the $\beta_0$ are the $\alpha$ verifying
4316: the reduction formula $f(u_1, \ldots, u_m)$ $\red
4317: f(u_1, \ldots, u_m)^{\rho}$, with $\rho = (x_1 \red x'_1)
4318: \ldots (x_k \red x'_k)$.
4319: We have $Dom(\alpha) = Var(A) \cup
4320: \{x_1,\ldots,x_k\}$.
4321: The domain of $\beta_0$ is $Dom(\alpha) \cup \{x'_1,\ldots,x'_k\}$.
4322: Then $\beta_0 = \alpha \; [Dom(\alpha)]$ and by definition of the
4323: reduction formula, the $\beta_0 x'_i$ are such that
4324: $t [\beta_0 x'_1]_{p_1} \ldots [\beta_0 x'_k]_{p_k}$ is
4325: the first reduced form of $\alpha f(u_1, \ldots ,u_n)$
4326: in any outermost rewriting chain starting from
4327: $\alpha f(u_1, \ldots ,u_n)$, having an outermost rewriting position
4328: at a non variable position of $f(u_1, \ldots ,u_n)$.
4329: %{\bf Therefore, $\beta_0$ satisfies $A_0$.}
4330:
4331: Then, by definition of the outermost strategy, the $\beta_0 t_0$
4332: represent any possible outermost reduced form of $\alpha t$
4333: just before the reduction occurs at a non variable occurence of
4334: $f(u_1,\ldots ,u_n)$. Thus, outermost termination of the $\beta_0 t_0$
4335: implies outermost termination of the $\alpha t$.\\
4336:
4337:
4338: Then $t_0$ is narrowed in all possible ways
4339: into terms $v_i$ at positions $p_i$
4340: with substitutions $\sigma_i$, provided $p_i$ and
4341: $\sigma_i$ satisfy the outermost
4342: narrowing requirements, as defined in Definition \ref{def:narrowing}.
4343: We now show that if $\beta_0 t_0$ is reducible,
4344: then there exist $\beta_i$ satisfying $A'$ such that
4345: outermost termination of the $\beta_i v_i$ implies
4346: outermost termination of $\beta_0 t_0$.
4347:
4348: We have $\beta_0 t_0 \ra^{Out}_{p, l \ra r}
4349: t'$ and $p \in \OS(t_0)$ since $t_0 = t^{\rho}$.
4350:
4351: By lifting lemma, there is a
4352: term $v$ and substitutions $\beta$ and
4353: $\sigma = \sigma_0 \wedge \bigwedge_{j \in [1..k]} \overline{\sigma_j}$,
4354: corresponding to each rewriting step $\alpha t_0
4355: \ra^{Out}_{p, l \ra r} t'$, such that:
4356:
4357:
4358: \[
4359: \begin{array}{ll}
4360: 1.~t_0 \surred^{Out}_{p, l \ra r,\sigma} v,\\
4361: 2.~\beta v = t', \\
4362: 3.~\beta \sigma_0 = \beta_0 [{\cal Y}]\\
4363: 4.~\beta {\rm ~satisfies~} \bigwedge_{j \in [1..k]} \overline{\sigma_j}.
4364: \end{array}
4365: \]
4366:
4367: where $\sigma_0$ is the most general unifier of $t_0|_p$ and $l$ and
4368: $\sigma_j, j \in [1..k]$ are
4369: all most general unifiers of $\sigma_0 t_0|_{p'}$ and a left-hand side
4370: $l'$ of a rule of $\R$, for all position $p'$ which are
4371: prefix positions of $p$ in $t_0$.
4372:
4373:
4374: These narrowing steps are effectively produced by the rule
4375: \rname{Narrow}, applied in all possible ways.
4376: So a term $\beta v$ is
4377: produced for every outermost rewriting branch starting from
4378: $\beta_0 t_0$.
4379: %(the other $\beta v$ correspond to the previous superfluous
4380: %narrowing steps).
4381: Then outermost termination of the $\beta v$ implies
4382: outermost termination of $\beta_0 t_0$.
4383:
4384:
4385:
4386: We prove that $\beta$ satisfies
4387: $A' = A_0 \wedge \sigma_0 \bigwedge_{j \in [1..k]} \overline{\sigma_j}$
4388: like in the innermost case.
4389: \end{itemize}
4390: \end{proof}
4391: \vspace{3mm}
4392:
4393:
4394:
4395: \begin{lemma}[(Stopping lemma)]
4396: Let $(\{t\}, A,C)$ be a state of any proof tree, {\bf with $A$ satisfiable,}
4397: and giving the state $(\emptyset, A',C')$ by application of an inference rule.
4398: Then for any ground substitution $\alpha$ satisfying $A$,
4399: $\alpha t$ S-terminates.
4400: \end{lemma}
4401:
4402: \begin{proof}
4403: The only rule giving the state $(\emptyset, A',C')$
4404: is \rname{Stop}.
4405: When \rname{Stop} is applied, then
4406:
4407: \begin{itemize}
4408: \item either $\mathit{TERMIN(S,t)}$ and then $\alpha t$ S-terminates for any
4409: ground substitution $\alpha$,
4410:
4411: \item or $(t_{\mathit{ref}} > t)$ is satisfiable.
4412: Then, for any ground substitution $\alpha$ satisfying $A$,
4413: $\alpha t_{\mathit{ref}} \succ \alpha t$.
4414: By induction hypothesis, $\alpha t$ S-terminates.
4415: \end{itemize}
4416: \end{proof}
4417:
4418: \section{The usable rules}
4419:
4420: To prove Lemma~\ref{lemma:U-correction}, we need the next three
4421: lemmas.
4422: The first two ones are pretty obvious from the definition of the
4423: usable rules.
4424:
4425: \begin{lemma}\label{lemma:U-def}
4426: Let $\R$ be a rewrite system on a set $\F$ of symbols and $t \in \TFXXA$.
4427: Then, every symbol $f \in \F$ occuring in $t$ is such that
4428: $Rls(f) \subseteq \U(t)$.
4429: \end{lemma}
4430:
4431: \begin{proof}
4432: We proceed by structural induction on $t$.
4433:
4434: \begin{itemize}
4435: \item If $t \in \X \cup \XA$, the property is trivially true;
4436: \item if $t$ is a constant $a$,
4437: $\U(t = a) = Rls(a) \cup_{l \ra r \in Rls(a)} \U(r)$; the only symbol
4438: of $t$ is $a$, and we have $Rls(a) \subseteq \U(t)$.
4439: \end{itemize}
4440:
4441: Let us consider a non-constant and non-variable term $t \in \TFXXA$,
4442: of the form $f(u_1, \ldots ,u_n)$.
4443: Then, by definition of $\U(t)$, we have
4444: $\U(t) = Rls(f) \cup_{i=1}^n \U(u_i) \cup_{l \ra r \in Rls(f)} \U(r)$.
4445: Then, whatever $g$ symbol of $t$, either $g = f$ and then
4446: $Rls(g) \subseteq \U(t)$, or $g$ is a symbol occuring in some $u_i$ and,
4447: by induction hypothesis on $u_i$, $Rls(g) \subseteq \U(u_i)$,
4448: with $\U(u_i) \subseteq \U(t)$.
4449: \end{proof}
4450:
4451: \begin{lemma}\label{lemma:U-rhs}
4452: Let $\R$ be a rewrite system on a set $\F$ of symbols and $t \in \TFXXA$.
4453: Then $l \ra r \in \U(t) \Rightarrow \U(r) \subseteq \U(t)$.
4454: \end{lemma}
4455:
4456: \begin{proof}
4457: According to the definition of the usable rules, if a term $t$
4458: is such that $\Var(t) \cap \X \neq \emptyset$, then $\U(t) = \R$,
4459: and then the property is trivially true.
4460: We will then suppose in the following that $t$ does not contain
4461: any variable of $\X$.
4462:
4463: Let $l \ra r \in \U(t)$.
4464: By definition of $\U(t)$, since $\Var(t) \cap \X = \emptyset$,
4465: among all recursive applications of the definition of $\U$ in
4466: $\U(t)$, there is an application $\U(t')$ of $\U$ to some term $t'$
4467: such that $\U(t') = Rls(g) \cup_i \U(t'|_i) \cup_{l' \ra r' \in Rls(g)} \U(r')$,
4468: with $\U(t') \subseteq \U(t)$, and $l \ra r \in Rls(g)$, with $g = top(l)$.
4469:
4470: Since $l \ra r \in Rls(g)$, by definition of $\U(t')$, we have
4471: $\U(r) \subseteq \cup_{l' \ra r' \in Rls(g)} \U(r')$, and then
4472: $\U(r) \subseteq \U(t') \subseteq \U(t)$.
4473: \end{proof}
4474:
4475: \begin{lemma}\label{lemma:U-reducible}
4476: Let $\R$ be a rewrite system on a set $\F$ of symbols and $t \in \TFXXA$.
4477: Whatever $\alpha$ ground normalized substitution and
4478: $\alpha t \ra_{p_1,l_1 \ra r_1} t_1 \ra_{p_2,l_2 \ra r_2} t_2
4479: \ra \ldots \ra_{p_n,l_n \ra r_n} t_n$ rewrite chain starting from $\alpha t$,
4480: the defined symbol of $t_k, 1 \leq k \leq n$ at a redex position
4481: of $t_k$ is either a symbol of $t$ or one of the $r_i, i \in [1..k]$.
4482: \end{lemma}
4483:
4484: \begin{proof}
4485: We proceed by induction on the length of the derivation.
4486: The property is obviously true
4487: for an empty derivation i.e. on $\alpha t$.
4488:
4489: Let us show the property for the first rewriting step
4490: $\alpha t \ra_{p_1, l_1 \ra r_1} t_1$.
4491: By definition of rewriting,
4492: $\exists \sigma : \sigma l_1 = \alpha t|_{p_1}$ and
4493: $t_1 = \alpha t[\sigma r_1]_{p_1}$.
4494: Let $f$ be the redex symbol of $t_1$ at a position $p$, and let us show
4495: that $f$ comes either from $t$ or from $r_1$.
4496:
4497: Since $t_1 = \alpha t[\sigma r_1]_{p_1}$, either $p$ is a position
4498: of the context $\alpha t[]_{p_1}$, which does not change by rewriting,
4499: so we already have $f$ as redex symbol of $\alpha t$ at position $p$.
4500: As $\alpha$ is normalized, $p$ is a position of $t$, so $f$ is a symbol of $t$.
4501:
4502: Either $p$ corresponds in $t_1$ to a non variable position of $r_1$,
4503: so $f$ is a symbol of $r_1$.
4504:
4505: Or $p$ corresponds in $t_1$ to a position $r$ in $\sigma x$,
4506: for a variable $x \in \Var(r_1)$ at position $q$ in $r_1$: we have $p=p_1qr$.
4507: In this case, since $\Var(r_1) \subseteq \Var(l_1)$, we have $x \in \Var(l_1)$,
4508: so $\sigma x$ is also a subterm of $\alpha t$, and $f$ occurs in $\alpha t$
4509: at position $p'=p_1q'r$, where $q'$ is a position of $x$ in $l_1$.
4510:
4511: Moreover, as $p$ is a redex position in $t_1$, then by definition of the innermost
4512: strategy, there is no suffix redex position of $p$ in $t_1$.
4513: As $t_1|_p = \alpha t|_{p'}$, then similarly $p'$ is a redex position in $\alpha t$.
4514: As $\alpha$ is normalized, $p'$ is a position of $t$, so $f$ is a symbol of $t$.
4515:
4516:
4517: Then, let us suppose the property true for any term of the rewrite chain
4518: $\alpha t$ $\ra_{p_1,l_1 \ra r_1} t_1 \ra \ldots \ra_{p_k, l_k \ra r_k}
4519: t_k$, i.e. any redex symbol $f$ of $t_k$ is also a symbol of $t$, or a symbol
4520: of one of the $r_i, i \in [1..k]$,
4521: and let us consider
4522: $t_k \ra_{p_{k+1}, l_{k+1} \ra r_{k+1}} t_{k+1}$.
4523:
4524: By a similar reasoning than previously, we establish that any
4525: redex symbol $f$ of $t_{k+1}$ is also a symbol of $t_k$, or a symbol of $r_{k+1}$.
4526: We then conclude with the previous induction hypothesis.
4527: \end{proof}
4528:
4529:
4530:
4531: We are now able to prove Lemma~\ref{lemma:U-correction}.
4532: \vspace{2mm}
4533:
4534: \begin{lemma}[\ref{lemma:U-correction}]
4535:
4536: Let $\R$ be a rewrite system on a set $\F$ of symbols and $t \in \TFXXA$.
4537: Whatever $\alpha t$ ground instance of $t$ and
4538: $\alpha t \ra_{p_1,l_1 \ra r_1} t_1 \ra_{p_2,l_2 \ra r_2} t_2
4539: \ra \ldots \ra_{p_n,l_n \ra r_n} t_n$ rewrite chain starting from $\alpha t$,
4540: then $l_i \ra r_i \in \U(t), \; \forall i \in [1..n]$.
4541: \end{lemma}
4542:
4543:
4544: \begin{proof}
4545: If a variable $x \in \X$ occurs in $t$, then $\U(t) = \R$ and the property
4546: is trivially true.
4547: We then consider in the following that $t \in \TFXA$,
4548: and then that $\alpha$ is a (ground) normalized substitution.\\
4549: We proceed by induction on $\TFXA$ and on the length of the derivation.
4550:
4551: The property is trivially true if $\alpha t$ is in normal form.
4552: For any $\alpha t$ $ \ra_{p_1, l_1 \ra r_1} t_1$,
4553: since $\alpha$ is normalized,
4554: $p_1$ corresponds in $\alpha t$ to a non-variable position of $t$.
4555: Let $f$ be the symbol at
4556: position $p_1$ in $t$.
4557: Since $f$ is the symbol at the redex position $p_1$ of $\alpha t$
4558: with the rule $l_1 \ra r_1$, then $l_1 \ra r_1 \in Rls(f)$.
4559: Moreover, thanks to
4560: Lemma~\ref{lemma:U-def}, $Rls(f) \subseteq \U(t)$. Therefore,
4561: $l_1 \ra r_1 \in \U(t)$.
4562:
4563: Let us now suppose the property is true for any derivation chain
4564: starting from $\alpha t$ whose
4565: length is less or equal to $k$, and consider the chain:
4566: $\alpha t \ra_{p_1,l_1 \ra r_1} t_1 \ra_{p_2,l_2 \ra r_2} t_2
4567: \ra \ldots \ra_{p_k,l_k \ra r_k} t_k \ra_{p_{k+1},l_{k+1} \ra r_{k+1}} t_{k+1}$.
4568: Let $f$ be the symbol at position $p_{k+1}$ in $t_k$.
4569: Since $p_{k+1}$ is a redex position of $t_k$ with the rule
4570: $l_{k+1} \ra r_{k+1}$, then
4571: $l_{k+1} \ra r_{k+1} \in Rls(f)$.
4572:
4573:
4574: By Lemma~\ref{lemma:U-reducible} with a derivation of length $k$,
4575: we have two cases:
4576: \begin{itemize}
4577: \item either the symbol $f$ at position $p_{k+1}$ in $t_k$ is
4578: a symbol of $t$;
4579: then, thanks to Lemma~\ref{lemma:U-def} on $t$, we get
4580: $Rls(f) \subseteq \U(t)$;
4581: henceforth $l_{k+1} \ra r_{k+1} \in
4582: \U(t)$;
4583:
4584:
4585: \item or the symbol $f$ at position $p_{k+1}$ in $t_k$ is
4586: a symbol of a $r_i, i \in [1..k]$;
4587: then, thanks to Lemma~\ref{lemma:U-def} on
4588: $r_i$, we get $Rls(f) \subseteq \U(r_i)$;
4589: henceforth $l_{k+1} \ra r_{k+1} \in \U(r_i)$;
4590: by induction hypothesis we have $l_i \ra r_i \in \U(t)$ and, thanks to
4591: Lemma~\ref{lemma:U-rhs}, we have $\U(r_i) \subseteq \U(t)$.
4592: Henceforth $l_{k+1} \ra r_{k+1} \in \U(t)$.
4593: \end{itemize}
4594: \end{proof}
4595:
4596: \begin{subproposition}[\ref{prop:TC}]
4597: Let $\R$ be a rewrite system on a set $\F$ of symbols, and $t$ a term of $\TFXXA$.
4598: If there exists a simplification ordering $\succ$ such that
4599: $\forall l \ra r \in \U(t): l \succ r$, then any ground instance of $t$
4600: is terminating.
4601: \end{subproposition}
4602:
4603: \begin{proof}
4604: As $\succ$ orients the rules used in any reduction chain starting from
4605: $\alpha t$ for any ground substitution $\alpha$,
4606: by properties of the simplification orderings,
4607: $\succ$ also orients the reduction chains, which are then finite.
4608: \end{proof}
4609:
4610:
4611:
4612:
4613: \section{A lemma specific to the outermost case}
4614:
4615: \begin{lemma}[\ref{lemme:var}]
4616: Let $(\{t_i\}, A_i, C_i)$ be the
4617: $i^{th}$ state of any branch of the derivation tree obtained by
4618: applying the strategy $S$ on $(\{t_{\mathit{ref}}\}, \top, \top)$, and
4619: $\succ$ an $\F$-stable ordering having the subterm property. If every
4620: reduction formula in $A_i$ can be reduced to a formula $\bigwedge_j
4621: x_j = x'_j$, then we have:
4622: \begin{center}
4623: for all variable $x$ of $t_i$ in $\X$: $(t_{\mathit{ref}} > x) \sur
4624: A_i$ is satisfiable by $\succ$.
4625: \end{center}
4626: \end{lemma}
4627:
4628:
4629: \begin{proof}
4630: The proof is made by induction on the number $i$ of applications of
4631: the inference rules from $(\{t_{\mathit{ref}}\}, \top, \top)$ to the
4632: state $(\{t_i\}, A_i, C_i)$.
4633:
4634: Let us prove that the property holds for $i=0$. We have $t_0 =
4635: t_{\mathit{ref}}$ and then $Var(t_0) = \Var(t_{\mathit{ref}})$.
4636: Consequently, for every $x \in Var(t_0)$, whatever the ground
4637: substitution $\alpha$ such that $\Var(t_{\mathit{ref}}) \subseteq
4638: Dom(\alpha)$, $\alpha x$ is a subterm of $\alpha t_{\mathit{ref}}$.
4639: The induction ordering $\succ$ satisfying the conditions of the rules
4640: before the application of these rules can be any $\F$-stable ordering
4641: having the subterm property. We then have $\alpha t_{\mathit{ref}}
4642: \succ \alpha x $.
4643:
4644: We now prove that if the property holds for $i-1$, it also holds for
4645: $i$.\\
4646:
4647: If the rule used at the $i^{th}$ step is \rname{Stop}, then $Var(t_i)
4648: = \emptyset$, and then, the property is trivially verified.\\
4649:
4650: If the rule used at the $i^{th}$ step is \rname{Abstract},
4651: as the rule \rname{Abstract} replaces subterms in $t_{i-1}$ by new
4652: variables of $\XA$, then $(Var(t_i) \cap \X) \subseteq (Var(t_{i-1}) \cap \X)$,
4653: so the property still holds.\\
4654:
4655: If the rule used at the $i^{th}$ step is \rname{Narrow} then,
4656: by hypothesis, the
4657: reduction renaming applied to $t_{i-1}$ and giving a term $t'_{i-1}$
4658: just consists in a mere
4659: renaming of the variables of $t_{i-1}$.
4660: Let $t_i$ be a term obtained
4661: by narrowing $t'_{i-1}$ with the substitution $\sigma$.
4662:
4663: %If $\sigma$ does not satisfy $A_{i-1} \wedge R(t_{i-1})$, then
4664: %$A_i = A_{i-1} \wedge R(t_{i-1}) \wedge \sigma_{\Var(Ren(t_{i-1}))} \wedge F_{\Var(\sigma Ren(t_{i-1}))}$
4665: %is not satisfiable and then the property is trivially true.
4666: %Let us now consider a narrowing substitution $\sigma$ satisfying
4667: %$A_{i-1} \wedge R(t_{i-1})$, if it exists so.\\
4668: Let $z \in \Var(t_i)$, and $\alpha$ a substitution satisfying $A_i$.
4669: We show that $\alpha t_{\mathit{ref}} \succ \alpha z$.
4670: We have two cases.
4671:
4672: Either $z$ is a fresh variable introduced by the narrowing step.
4673: Let $x' \in \Var(t'_{i-1})$ such that $z \in \Var(\sigma x')$,
4674: and $x \in \Var(t_{i-1})$ such that $x'$ is a renaming of $x$.
4675: By hypothesis, every reduction formula in $A_i$ can be reduced to a formula
4676: $\bigwedge_j x_j = x'_j$. This is then the same for
4677: $A_{i-1}$. Moreover, since $\alpha$ satisfies $A_i$,
4678: then it satisfies in particular $A_{i-1}$.
4679: Then, by induction hypothesis, $\alpha t_{\mathit{ref}} \succ \alpha x$ and,
4680: since $\alpha$ satisfies $x = x'$, we also have
4681: $\alpha t_{\mathit{ref}} \succ \alpha x'$.\\
4682: By hypothesis, $\sigma$ contains the equality $x' = C[z]$, with $C[z]$ a
4683: (possibly empty) context of $z$.
4684: Moreover, by definition of the rule \rname{Narrow},
4685: $A_i = A_{i-1} \wedge R(t_{i-1}) \wedge \sigma$.
4686: So $A_i$ contains the equality $x' = C[z]$.\\
4687: Then, as $\alpha$ satisfies $A_i$, $\alpha$ is such that
4688: $\alpha x' = \alpha C[z]$.
4689: Since $\alpha t_{\mathit{ref}} \succ \alpha x'$, we have
4690: $\alpha t_{\mathit{ref}} \succ \alpha C[z]$ and then, by subterm property,
4691: $\alpha t_{\mathit{ref}} \succ \alpha z$.
4692:
4693: Or $z \in \Var(t'_{i-1})$~;
4694: by the same reasoning as in the previous point
4695: for $x'$, we have $\alpha t_{\mathit{ref}} \succ \alpha z$.
4696: \end{proof}
4697:
4698: \begin{acks}
4699: We would like to thank Olivier Fissore for fruitful exchanges, we have had in
4700: previous works on the topic, the Protheo group for dynamically supporting our
4701: ideas, and Nachum Dershowitz for the interest he took in our approach, and for
4702: his advice on the manuscript of this paper.
4703: \end{acks}
4704:
4705: % biblio au Loria
4706: \bibliography{/local/protheo/bibtex/abbrev,/local/protheo/bibtex/protheo,/local/protheo/bibtex/gnaedig,/local/protheo/bibtex/hkirchne}
4707:
4708: % biblio sur le mac
4709: %\bibliography{/Users/gnaedig/HOME-LORIA/BIBTEX/abbrev,/Users/gnaedig/HOME-LORIA/BIBTEX/protheo,/Users/gnaedig/HOME-LORIA/BIBTEX/gnaedig-loria}
4710:
4711:
4712:
4713: \end{document}
4714:
4715:
4716:
4717: