J.R. Kennaway, J.W. Klop, M.R. Sleep And F.J. De Vries

2y ago
18 Views
2 Downloads
1.93 MB
13 Pages
Last View : 19d ago
Last Download : 2m ago
Upload by : Wren Viola
Transcription

4An Infinitary Church-Ro sserProperty for Non-collap singOrthogona l Term RewritingSystemsJ.R. Kennaway, J.W. Klop, M.R. Sleep and F.J. de Vries4.1INTRODUCTIONThere are at least two good reasons to study infinitary term rewriting. First, we believethat infinitary term rewriting is of interest for its own sake, as a natural extension offinitary term rewriting. Second, infinitary term rewriting provides a sound and thorough basis for term graph rewriting, a fruitful theoretical model for implementations offunctional programming languages. Term graph rewriting has been defined by Barendregt and co-workers in [BvEG 87] and has been adopted as the central model bythe ESPRIT BRA project SemaGraph.Term rewriting is a general model of computation. Computations can be finite andinfinite. The usual focus is on successful finite computations: finite derivations endingin finite normal form. However, infinite computations computing a possible infiniteanswer are of interest as well: recursive procedures enumerating some infinite set: e.g.the natural numbers or the Fibonacci numbers. Until recently, infinite computationshave hardly seriously been considered in the theory of term rewriting.In functional programming languages like Miranda or ML it is possible to manipulate with lazy expressions representing infinite objects, like lists. Graph rewriting hasbeen introduced as a theoretical framework to show the soundness of such computing.Term Graph Rewriting: Theory and Practice.Eds. Ronan Sleep, Rinus Plasmeijer and Marko van Eekelen.@1993 John Wiley & Sons Ltd

48NON-COLLAPSING ORTHOGONAL TERM REWRITING SYSTEMSlnfinitary term rewriting is a foundation for graph rewriting ( cf. [KKSdV93] for anelaboration of this point): some instances of graph rewriting on shared graphs actuallyrepresent infinite computations on infinite terms.At present the theory of infinitary rewriting for orthogonal Term Rewriting Systemsis rapidly emerging in a series of papers. Dershowitz, Kaplan and Plaisted have openedthe series with [DK89, DKP89, DKP91]. They take a rather topological approach andstudy Cauchy converging reduction sequences. A number of their results (CompressionLemma, Infinitary Projection Lemma, Infinitary Church-Rosser property) depend onthe rather strong notion of a top-terminating orthogonal Term Rewriting System.Dropping the condition of top-termination introduces problems. Farmer and Watro[FW91] observed the necessity of strong convergence for some instances of compressingand pointed out the link between infinitary term rewriting and graph rewriting.In [KKSdV90b] we developed the theory of infinite term rewriting based on stronglyconverging reductions after presenting counter-examples to the desired general resultsfor Cauchy converging sequences. For the theory involving strong convergence thelnfinitary Projection Lemma, the Compressing Lemma and the Unique Normal FormProperty are provable, whereas counter-examples exist for these results in case ofCauchy convergence. We also showed that despite the nice theory one can developfor strongly converging reductions the infinitary Church-Rosser property does nothold. The presented counter-example shows that also for Cauchy-converging reductionsthere is no infinitary Church-Rosser property for arbitrary orthogonal infinitary TermRewriting Systems.In this chapter we will prove the infinitary Church-Rosser property for stronglyconverging reductions for orthogonal infinitary Term Rewriting Systems of which allrules are non-collapsing, except for at most one rule of the form I(x) - x. We thinkthat our proof is instructive and conceptually clear.The present account improves our treatment in the early version [KKSdV90a].4.1.1Overview of this chapterIn section 4.2 we briefly introduce infinitary Term Rewriting Systems (TRS). Then, insection 4.3, we define depth-preserving orthogonal Term Rewriting Systems and provethe infinitary Church-Rosser property for strongly converging sequences in such systems. Using Park's idea of hiaton we show in section 4.4 that any orthogonal TRS canbe transformed into a depth-preserving orthogonal TRS, via the so called -completion.This enables us to prove the infinitary Church-Rosser property for orthogonal TRSconsisting of non-collapsing rules with at most one unary collapsing rule. Finally, wediscuss our results and relate them with those of Dershowitz, Kaplan and Plaisted.4.2INFINITARY ORTHOGONAL TERM REWRITINGSYSTEMSWe briefly recall the definition of a finitary Term Rewriting System, before we defineinfinitary orthogonal Term Rewriting Systems involving both finite and infinite terms.For more details the reader is referred to [DJ90] and [Klo92].

KENNAWAY ET AL4.2.149Finitary Term Rewriting SystemsA finitary Term Rewriting System over a signature E is a pair (Ter(E), R) consistingof the set Ter(E) of finite terms over the signature E and a set of rewrite rulesR Ter(E) x Ter(E).The signature E consists of a countably infinite set Var of variables ( x, y, z, . .) anda non-empty set of function symbols (A, B, C, . , F, G, . .) of various finite arities2:: 0. Constants are function symbols with arity 0. The set Ter(E) of finite terms(t, s, . .) over Eis the smallest set containing the variables and closed under functionapplication.The set O(t) of positions of a term t E Ter(E) is defined by induction on thestructure oft as follows: O(t) { .},if t is a variable and O(t) { .} U {i · ull i nand u E O(ti)}, ift is of the form F(t1, . .,tn)· Ifu E O(t) then the subterm t/u atposition u is defined as follows: t/ . t and F(t 1 , . , tn)/i · u t;fu. The depth of asubterm oft at position u is the length of u.Contexts are terms in Ter(E U {D} ), in which the special constant D, denotingan empty place, occurs exactly once. Contexts are denoted by C[) and the result ofsubstituting a term t in place of D is C[t] E Ter(E). A proper context is a context notequal to D.Substitutions are maps u: Var- Ter(E) satisfying the equation u(F(t 1 , , tn)) F(u(t1), . , u(tn)).The set R of rewrite rules contains pairs(/, r) of terms in Ter(E), written as l-- r,such that the left-hand side l is not a variable and the variables of the right-hand sider are contained in I. The result l" of the application of the substitution u to the term lis an instance of l. A redex (reducible expression) is an instance of a left-hand side of arewrite rule. A reduction step t -- s is a pair of terms of the form C[l"] -- [r"], whereI -- r is a rewrite rule in R. Concatenating reduction steps we get a finite reductionsequence ta -- t 1 -- . -- tn or an infinite reduction sequence ta - t1 -- . 4.2.2Infinitary orthogonal Term Rewriting SystemsAn infinitary Term Rewriting System (TRS, usually this abbreviation is reserved forthe finitary Term Rewriting Systems only) over a signature E is a pair (Ter 00 (:E), R)consisting of the set Ter 00 (E) of finite and infinite terms over the signature E and aset of rewrite rules R Ter(E) x Ter(E). It takes some elaboration to define the setTer 00 (E) of finite and infinite terms.The set Ter(E) of finite terms for a signature E can be provided with an metricd: Ter(E) x Ter(E)- [O, l]. The distance d(t, s) of two terms t and sis 0, if t and sare equal, and 2-k, otherwise, where k E w is the largest natural number such that allnodes of sand t at depth less than or equal to k are equally labeled. The set of infinitaryterms Ter 00 (E) is the metric completion of Ter(:E). (This is all well known, see forinstance [AN80]). Substitutions, contexts and reduction steps generalize trivially tothe set of infinitary terms Ter 00 (E).To introduce the prefix ordering on terms we extend the signature E with afresh symbol n. The prefix ordering on Ter 00 (E U {O}) is defined inductively:X X for any variable X, 0 t for any term t and, if t1 S1, . , tn Sn, thenF(t1, . ,tn) F(s1, . ,sn)· .

NON-COLLAPSING ORTHOGONAL TERM REWRITING SYSTEMS50If all function symbols of E occur in R we will write just R for (Ter 00 (:E), R). Theusual properties for finitary Term Rewriting Systems extend verbatim to infinitaryTerm Rewriting Systems:DEFINITION 4.2.la. A rewrite rule l - r is left-linear if no variable occurs more than once in theleft-hand side l.b. R is non-overlapping if for any two left-hand sides s and t, any position u in t, andany substitutions rand r: Var- Ter(E) it holds that if (t/u)a sr then eithert/u is a variable or t and s are left-hand sides of the same rewrite rule and u A(i. e. non-variable parts of different rewrite rules do not overlap and non-variableparts of the same rewrite rule overlap only entirely).c. A (in}finitary Term Rewriting System R is orthogonal if its rules are left-linearand non-overlapping.d. A rewrite rule I - r is collapsing, if r is a variable.It is well known ( cf. [Ros73, Klo92]) that finitary orthogonal Term Rewriting Systems satisfy the finitary Church-Rosser property, i.e., . o - * - * o * -, where - *is the transitive, reflexive closure of the relation- . It is not difficult to see that infinitary orthogonal Term Rewriting Systems inherit this finitary Church-Rosser property.In this chapter we consider a generalization of the finite Church-Rosser property toinfinite reductions. It is a rather subtle issue to decide on the appropriate class ofinfinite reductions. We will discuss this in the next section.4.2.3Projecting infinitary reductionsIn a complete metric space like Ter 00 p::), Cauchy sequences of any ordinal lengthhave a limit. (Such transfinite Cauchy sequences are an instance of Moore-Smith convergence over a net indexed by the ordinal length of the sequence, see e.g. the textbook [Kel55].) It is a natural idea to introduce (transfinite) converging reductions, asDershowitz, Kaplan and Plaisted have done in [DJ90]. These are transfinite reductionsequences whose elements form a Cauchy sequence.DEFINITION 4.2.2 A reduction of ordinal length a is a set (tp )/3 a of terms indexedby the ordinal O:' such that tp - t,13 1 for each f3 Q'.Note that when a is a limit ordinal, this definition does not stipulate any relationshipbetween ta and the earlier terms in the sequence. The obvious requirement to makeis that the earlier terms should converge to ta.DEFINITJON 4.2.3 A reduction(t,13)13 p isCauchy converging, written t 0 ,.;ta), inthe fallowing cases.- - h0ta,b. ta1 t,13 i if to- t,13,c. to- t;. if to- t13 for all f3a. to .and\:/c 03f3 .\:/1(f3 1 .A - d(t-y,t -.) ).However, despite being apparently so natural, converging reductions are not wellbehaved even for orthogonal TRS.

KENNAWAY ET AL51 Converging reductions resist compression into converging reductions of length atmost w (cf. [FW91, KKSdV90b, DKP91]). Converging reductions do not project over finite reductions (cf. 4.2.4, [KKSdV90b,DKP91]). The infinitary Church-Rosser property does not hold (cf. 4.2.10, [KKSdV90b]).The next example shows that the projection of a infinite converging reduction overa finite converging reduction need not be a converging reduction.EXAMPLE4.2.4 {KKSdV90b, DKP91}.Rules : A(x, y)- A(y, x)C- DSequences : A(C, C)- A(C, C)- A(C, C)- A(C, C)- . - w A(C, C)A(C, D)- A(D, C) - A(C, D)- A(D, C)- . .Clearly A(C, C) - A(C, C). The second infinite reduction obtained by standardprojection over the one step reduction C - D is not a converging reduction, andhence has no limit.Strongly converging reductions, which generalize an idea in [FW91], have betterproperties. In [KKSdV90b] we have proved for orthogonal TRS that strongly converging reductions can be compressed and project over finite reductions. Informally, astrongly convergent reduction is such that for every depth d, there is some point in thereduction after which all contractions are performed at greater depth. By inductionon a we define when a converging reduction (tp )p:::;cr is strongly converging towardsthe limit t,. (notation to - er ta)· By dp we will denote the depth of the contractedredex in tp - t/3 1 ·DEFINITION4.2.5a. to - o to,b. to - 13 1 t13 1 if to - p i tp i and to - f3 tf3,c. to - ,i. t,i. if to - 1 t,i. and Vi ). (to - -r t-y) and 'rid 0 3,8 A 'V7 (/3 ")" A - d-y d).By t - er s we denote the existence of a strongly converging reduction from t withlimit s cl' length less than or equal to a.We end this section with some positive facts about strongly converging reductionsthat we will need in the sequel of this chapter.Farmer and Watro have provided a necessary and sufficient condition when an infinite sequence of strongly converging reductions of length w 1 itself is stronglyconverging.LEMMA 4.2.6 {FW91}. Let tn,o - tn,w tn 1,o be strongly converging for alln E w. Let dn,k denote the depth of the contracted redex Rn,k in tn,k - tn,k l· Iffor all n there is a dn such that for all k it holds that dn,k dn, and limk-oo dk oo,then there exists a term tw,w such that to,o - xw tw,w via the strongly converging0reduction to,o - :::;w to,w t1,o - :::;w t1,w t2,0 - :::;w . - xw tw,w.

52NON-COLLAPSING ORTHOGONAL TERM REWRITING SYSTEMSIn order to state the Infinitary Projection Lemma for strongly convergent reductionswe need the notion of descendant for transfinite reductions. We assume familiaritywith the notion in finitary term rewriting of the descendants of of a position or setof positions by a finite reduction (cf. [HL91]). The existence of infinite terms doesnot complicate the notion, but for infinite sequences we must extend the definition toaccount for what happens at limit points.a. Denote thesubsequence of R from tbeta to t-y by R13,-y For a set of positions v of to the set v \ R ofdescendants of v by R in ta is defined by induction on a. When a is finite, this is thestandard notion. If a is a limit ordinal, then v \ R is defined in terms of the sets v \ Ro,{3for all (3 a, as follows: u E v \ R if and only if 3/3 a 'Vr (/3 r a -- u E v \ 'Y) Ifa .A n for a limit ordinal A and a finite non-zero n, then v\R v\Ro, . \R ., . n.DEFINITION 4.2. 7 Let R be a reduction sequence to - a ta of length When contemplating this definition, note that the strong convergence of to - a taimplies that for any position u E O(t 0 ), either u is in every v \ 'Y for sufficiently larger, or u is in none of them. This is not the case for merely converging reductions, asExample 4.2.4 illustrates.(tn)new be a stronglyconverging reduction of t 0 with limit tw and let t 0 - so be a reduction of a red ex R ofto. Then there is a strongly converging reduction (sn)neA with limit Sw, where for allDn w, Sn is obtained by contraction of all descendants of R in tn.LEMMA 4.2.8 Infinitary Projection lemma [KKSdV90bj. Let4.2.4The infi.nitary Church-Rosser propertyIn the present infinitary context the natural generalization of the finite Church-Rosserproperty is to consider a peak of strongly converging reductions of arbitrary ordinallengths.DEFINITION 4.2.9 An infinitaryTerm Rewriting System satisfies the infinitaryChurch-Rosser property for strongly converging reductions if for any peak t - a 1 t 1 ,t -- a 2 t2 there exists a joining valley t 1 -- f3 1 s, t2 -- f3 2 s:ayt'{2tit2/31·., 's/32Since strongly converging reductions can be compressed into reductions of lengthat most w the infinitary Church-Rosser property follows if we can show that peaks oflength w can be joined:t:::;w/"-. wti w "'t2 's W

KENNAWAY ET AL53Despite the Infinitary Projection Lemma for strongly converging reductions, theinfinitary Church-Rosser property does not hold for strongly converging reductions(nor for converging reductions) in orthogonal TRS. The following TRS are counterexamples to the infinitary Church-Rosser property for both convergence and strongconvergence:4.2.10 [KKSdV90b}Rules : A(x)- xB(x)- xC- A(B(C))Sequences : C- A(B(C))- A(C) - w AwC- A(B(C))- B(C) - w BwEXAMPLEa.b.D(x,y)- xC- D(A, D(B, C))Sequences : C- D(A, D(B, C))- D(A, C) - * D(A, D(A, C)) - * .C- D(A, D(B, C))- D(B, C) - * D(B, D(B, C)) - * .Rules:Note that in these examples the rules involving Care not strictly necessary: e.g. forthe first example one may consider then the infinite term (AB)w A(B(A(B( . .))))instead.4.3DEPTH-PRESERVING ORTHOGONAL TERMREWRITING SYSTEMSIn this section and the next we consider two natural classes of orthogonal TRS inwhich the infinitary Church-Rosser property holds for strongly converging sequences.The counter-examples suggest that collapsing rules are destroying the Church-Rosserproperties. In the next section we will prove the Church-Rosser property for stronglyconverging reductions in orthogonal TRS without collapsing rules.In this section however we will consider the more restricted but easier to deal withorthogonal TRS whose rules are depth-preserving.DEFINITION 4.3.1 A depth-preserving TRS is a left-linear TRS such that for all rulesthe depth of any variable in a right-hand side is greater than or equal to the depth ofthe same variable in the corresponding left-hand side.THEOREM 4.3.2 Any depth-preserving orthogonal TRS has the infinitary ChurchRosser property for strongly converging sequences.PROOF. Let t 0 , 0convergent.- to, 1 - .- Sw to,w and to,o- t1,o- .- Sw iw,o be stronglya. Using the Infinitary Projection Lemma for strongly convergent reductions we construct the horizontal strongly converging sequences tn,O - * tn,1 - * . . . - Sw tn,wfor O n w, as depicted in figure 4.1. The vertical reductions are constructedsimilarly.

54NON-COLLAPSING ORTHOGONAL TERM REWRITING SYSTEMSltw,O---7 ltw,l---7 · · · --? tw,m --? · · · --? liw,w Figure 4.1b. The construction of the Transfinite Projection Lemma also implies that the reduction tn,w - tn l,w is strongly converging.By the depth-preserving property it holds for all m, n :::; w that the depth of thereduced redexes in tn,m - * tn,m 1, which are all descendants of the redex Ro,m into,m- to,m 1, is at least the depth of Ro,m itself. Because to,o- to,1 - . - Suto,w is strongly convergent we find by Lemma 4.2.6 that tw,o - Su tw,1 - Su tw,2 .is strongly converging. Let us call its limit tw,w.c. In the same way the terms tn,w are part of a strongly converging sequence. The limitof this sequence is also equal to iw,w, as can be seen with the following argument.Lett 0. Because (tw n)n w is a Cauchy sequence, there is an N 1 such that for allm?: N1 we have d(t.,, ,t ,w) 3-t.Because to,o - t1,o - . - w tw,o is strongly converging, there is an N 2 such thatfor n?: N2 we have that 2-4n 3-t where dn is the depth of the redex Rn reducedat step tn,o- tn i,O· Since the descendants of this redex Rn occur at least at thesame depth, and since the TRS R is depth-preserving, we get d(tn,m, tw,m) 3-tfor all m :::; w and all n ?: N2 For similar reasons there is an N3 such that for all n :::; w and all m N 3 we havethat d(tn,w, tn,m) {.Concluding: Let N be the maximum of Ni, N 2 and N3 . Then for n N we findusing the triangle inequality for metrics that-

SSKENNAWAY ET AL .0Observe that in this proof there are two places where it is essential that the reductionsare strongly convergent. The first is the appeal to the Infinitary Projection Lemma.The second is in the argument that the sequences (tw,n)nEw and (tn,w)nEw have thesame limit.4.4NON-COLLAPSING ORTHOGONAL TERM REWRITINGSYSTEMSTRS R is non-collapsing if all its rewrite rules are noncollapsing, i. e. there is no rewrite rule in R whose right-hand side is a single variable.DEFINITION 4.4.1 AWe will show that any non-collapsing orthogonal TRS satisfies the infinitary ChurchRosser property for strongly converging reductions. The proofs will use a variant ofPark's notion of hiaton ( cf. [Par83]). The idea is to replace a depth losing rule likeA(x, B(y)) -- B(y) by a depth-preserving variant A(x, B(y))-- B( (y)). In order tokeep the rewrite rules applicable to terms involving hiatons, we also have to add morevariants like A(x, m(B(y))) ,. B(

Term rewriting is a general model of computation. Computations can be finite and infinite. . A proper context is a context not equal to D. Substitutions are maps u: . To introduce the prefix ordering on terms we extend the signature E with a

Related Documents:

La paroi exerce alors une force ⃗ sur le fluide, telle que : ⃗ J⃗⃗ avec S la surface de la paroi et J⃗⃗ le vecteur unitaire orthogonal à la paroi et dirigé vers l’extérieur. Lorsque la

fructose, de la gélatine alimentaire, des arômes plus un conservateur du fruit – sorbate de potassium –, un colorant – E120 –, et deux édulco-rants – aspartame et acésulfame K. Ces quatre derniers éléments relèvent de la famille des additifs. Ils fleuris-sent sur la liste des ingrédients des spécialités laitières allégées .

The Dissident Daughter chronicles Sue’s process as she re-writes this narrative, and she maps the journey in four stages, shown here only in the most cursory of summaries: the recognition of a “feminine wound” and her struggle to conceive a “feminine self” (Part One: Awakening); her introduction to the

CBSE Sample Paper Class 11 Maths Set 2 Solution. 1 cos2 1 cos4 1 2 2 x x cos2x cos4x 0 2 cos3x cos x 0 Cos3x 0 6 3 0 2 6 3 x n Cosx x k n n is integer π π π π π π 8. Solution: 30 40 60 4 7 2 4 10 4 15 4 ( ) . ( ) ( ) 1 1 1 1 1 i i i i i i i i 9. Solution: Substituting the points (0, 0) and (5, 5) on the given line x y – 8 0 0 .

Studying astrology can evoke changes in how we see life and experience the world, and in our lives, and for this reason it is important that students take their time with their studies and view study as a journey rather than a destination. There are times where there is greater studying activity and other times of greater reflection or adjustment, both of which are of immense value. It is .

Department of Plant Biology, University of Newcastle upon Tyne, Newcastle upon Tyne, NEl 7RU, United Kingdom ABSTRACT: 200 taxa of algae were recovered from cultures of 24 "terres trial" and "hydro-terrestrialll soil and vegetation samples from Glerar dalur, northern Iceland. 22 of the samples were collected at heights of between 500 and 1300 m. The algae were divided between the classes .

One foggy night, Percy Shaw was driving on a dark winding road. His life was saved when a cat’s eyes reflected his car’s lights, which stopped him from going off the side of the hill. After his near-death experience, Percy Shaw decided to create something similar to cats’ eyes by inventing a small device (made of two marbles placed close together in a rubber case) which would reflect .

Events you have registered for will show up in your “My Learning” section of Bridge. If a Hub session for your Trust fills up, the option to register will be faded out and will show as “No Seats Available”. Please do not register for another Trusts tickets. Last edited: 29/07/2020 East of England Should there be no more spaces on your chosen event, you may need to register for the .