Stream Productivity by Outermost Termination Hans Zantema DepartmentofComputerScience,TUEindhoven,P.O.Box513, 5600MBEindhoven,TheNetherlands [email protected] InstituteforComputingandInformationSciences,RadboudUniversity Nijmegen,P.O.Box9010,6500GLNijmegen,TheNetherlands MatthiasRaffelsieper DepartmentofComputerScience,TUEindhoven,P.O.Box513, 5600MBEindhoven,TheNetherlands [email protected] Streams are infinite sequences overa given data type. A stream specification is a set of equations intendedto define a stream. A corepropertyis productivity: unfoldingthe equationsproducesthe intended stream in the limit. In this paper we show that productivity is equivalent to termination withrespecttothebalancedoutermoststrategyofaTRSobtainedbyaddinganadditionalrule. For specificationsnotinvolvingbranchingsymbolsbalancednessisobtainedforfree,bywhichtoolsfor provingoutermostterminationcanbeusedtoproveproductivityfullyautomatically. 1 Introduction Streams are among the simplest data types in which the objects are infinite: they can be seen as maps from the natural numbers to some data type D. The basic constructor for streams is the operator ‘:’ mapping a data element d and a stream s to a new stream d :s by putting d in front of s. Using this operatorwecandefinestreamsbyequations. Forinstance,theThueMorsesequencemorseoverthedata elements0,1canbespecifiedbytherules morse → 0:zip(inv(morse),tail(morse)) tail(x:s ) → s inv(x:s ) → not(x):inv(s ) zip(x:s ,t ) → x:zip(t ,s ) together withthetworulesnot(0)→1andnot(1)→0. This stream specification is productive: for every n∈N there is a rewrite sequence morse→∗ u : 1 u :···:u :t, that is, by these rules every n-th element of the stream can be computed. This notion of 2 n productivity goes back to Sijtsma [6]. In [2] a nice and powerful approach has been described to prove productivity automatically for a restricted class of stream specifications. Here we follow a completely different approach: we do not have these restrictions, but show that productivity is equivalent to termi- nation with respect to a particular kind of outermost rewriting, after adding the rule x:s →overflow. The intuition of this equivalence is clear: productivity is equivalent to the claim that every ground term rewrites toaterm with’:’ on top. This kind of rewriting is forced by doing outermost rewriting, and as soonas’:’ isontop,thereduction tooverflowisforced,blocking furtherrewriting. However,therearesomepitfalls. Intheaboveexamplethetermtail(morse)admitsaninfiniteouter- mostreduction startingby tail(morse) → tail(0:zip(inv(morse),tail(morse))) → zip(inv(morse),tail(morse)) M.Fernandez(Ed.):9thInt.WorkshoponReductionStrategies inRewritingandProgramming(WRS’09) EPTCS15,2010,pp.83–95,doi:10.4204/EPTCS.15.7 84 StreamProductivitybyOutermostTermination and then repeating this reduction forever on the created subterm tail(morse). Sothe outermost strategy tobeconsideredneedsanextrarequirementdisallowingthisreduction. Thisrequirementiswhatwecall balanced: werequireeveryredexinthereductioneithertobereducedeventually,orrewrittenbyaredex closer to the root. In the given example the redex morse in zip(inv(morse),···) is never reduced, nor rewrittenbyahigherredex,sotheresulting infiniteoutermost reduction isnotbalanced. OurmainresultstatesthatastreamspecificationgivenbyaTRSRisproductiveforallgroundterms ifandonlyifR∪{x:s →overflow}doesnotadmitaninfinitebalanced outermostreduction. For the special case without rewrite rules for the data and without symbols having more than one argument of stream type, balancedness is obtained for free, and productivity of R on all ground terms is equivalent to outermost termination of R∪{x:s →overflow}. For this fully automatic tools can be used,forinstance basedontheapproaches of[3,5,7]. Asanexampleconsider c = 1:c f(0:s ) = f(s ) f(1:s ) = 1:f(s ) by which we want to compute f(c). Clearly c only consists of ones, and f only removes zeros, so the resultoff(c)willbetheinfinitestreamofones. Every1inthisstreamiseasilyproducedbythereduction f(c)→f(1:c)→1:f(c)→···, proving productivity of f(c). However, the approach from [2] fails, as this stream specification is not data-obliviously productive, i.e.,theidentity ofthedataisessential forproductivity. Asfarasweknow, and confirmed by the authors of [2], until now there were no techniques for proving productivity auto- matically if the productivity is not data-oblivious. This has changed by the approach we present in this paper. The above example does not directly fit the basic format of our approach. However, it is easily (andautomatically) unfolded tothesystemRconsisting oftherules c = 1:c f(x:s ) = g(x,s ) g(0,s ) = f(s ) g(1,s ) = 1:f(s ) fitting the basic format of our approach. Now outermost termination of R∪{x:s →overflow} can be proved by a tool. Due to the shape of the symbols and the fact that there are no rewrite rules for the data, also balanced outermost termination of R∪{x:s →overflow} can be concluded. Then the main theorem ofourpaperstatesproductivity, notonlyforf(c)butforallgroundtermsofsortstream. Theapproachworksforseveralotherexamples,forinstanceforanalternativedefinitionofthemorse stream. In [9] a related approach is described, while an implementation of that technique is described in [8]. However,theretheresultisonwell-definedness ofstream specifications, whichisaslightly weaker notion than productivity. Themainresult of[9]isthat well-definedness ofastream specification canbe concluded fromtermination ofsometransformed system: theobservational variant. 2 The Main Result Instreamspecificationswehavetwosorts: s(stream)andd(data). WeassumethesetDofdataelements to consist of the unique normal forms of ground terms over some signature S with respect to some d HansZantemaandMatthiasRaffelsieper 85 terminating orthogonal rewrite system R over S . Here all symbols of S are of type dn → d for d d d some n≥0. In the actual stream specification we have a set S of stream symbols, each being of type s dn×sm →sfor n,m≥0. Apartfrom that, weassumeaparticular symbol :6∈S having typed×s→s. s As a notational convention variables of sort d will be denoted by x,y, terms of sort d by u,u, variables i ofsortsbys ,t ,andtermsofsortsbyt,t. i Definition 1. A stream specification (S ,S ,R ,R ) consists of S ,S ,R as given before, and a set R d s d s d s d s ofrewriterulesoverS ∪S ∪{:}oftheshape d s f(u ,...,u ,t ,...,t )→t, 1 n 1 m where • f ∈S isoftypedn×sm→s, s • forevery i=1,...,mthe termt iseither avariable ofsort s, ort =x:s wherex isavariable of i i sortd ands isavariable ofsorts, • t isanywell-sorted termofsorts, • R ∪R isorthogonal, s d • Every term of the shape f(u ,...,u ,u :t ,...,u :t ) for f ∈S of type dn×sm →s, and 1 n n+1 1 n+m m s u ,...,u ∈DmatcheswiththelefthandsideofarulefromR . 1 n+m s Sometimes wecall R a stream specification: in that case S , S consist of the symbols of sort d, s, s d s respectively, occurring inR ,andR =0/. Rulesℓ→rinR areoftenwrittenasℓ=r. s d s Definition1isnearlythesameasin[9]. Itiscloselyrelatedtothedefinitionofstreamspecificationin [2]: byintroducing fresh symbols andrules fordefining these fresh symbols, every stream specification intheformatof[2]canbeunfoldedtoastreamspecificationinourformat. Intheendoftheintroduction, whereweunfolded f(x:s )tog(x,s ), wealready sawanexampleofthis. Fordefiningproductivitywefollowthedefinitionfrom[2]: astreamspecificationiscalledproductive foragroundtermtifforeveryn∈Nthereexistsareductionoftheshapet→∗u :u :···:u :t′. Instead 1 2 n of fixing the start ground term t we prefer to require this for all ground terms of sort s. In practice this will make hardly any difference: typically a stream specification consists of an intended stream to be defined and a few auxiliary functions for which productivity not only holds for the single stream to be definedbutalsoforanyground termbuiltfromitandtheauxiliary functions. Takingallgroundtermsofsortsinsteadofonlyonehasastrongadvantage: thenforprovingproduc- tivityitissufficienttoprovethatthefirstelementisproduced, ratherthanallelements. Thisisexpressed inthefollowingproposition thatwillserveasourcharacterization ofproductivity: Proposition 2. A stream specification (S ,S ,R ,R ) is productive for all ground terms of sort sif and d s d s onlyifeverygroundtermt ofsortsadmitsareductiont →∗ u′:t′. Rs∪Rd Proof. The “only if” direction of the proposition is obvious. To show the “if” direction, we show that if forall ground termsof sort swehavet →∗ u′ :t′, thent →∗ u :u :···:u :t for all n∈N. Rs∪Rd Rs∪Rd 1 2 n n Thisisdonebyinduction onn. Ifn=0,thentheproposition directlyholds. Otherwise, we get from the induction hypothesis that t →∗ u :u :···:u :t . Since t Rs∪Rd 1 2 n−1 n−1 n−1 isalsoaground term ofsorts, wehavet →∗ u′:t′ byassumption. Hence,t →∗ u :u :···: n−1 Rs∪Rd Rs∪Rd 1 2 u :t →∗ u :u :···:u :u′ :t′,provingtheproposition. n−1 n−1 Rs∪Rd 1 2 n−1 86 StreamProductivitybyOutermostTermination From now onweomitthe subscript R ∪R inrewrite steps →. Givenatermt, wedefine the setof s d positions Pos(t)⊆N∗ as the smallest set such that e ∈Pos(t) and ift = f(t ,...,t ), then i.p′ ∈Pos(t) 1 n forall1≤i≤nand p′∈Pos(t). Thereplacementofthesubtermoft atsomeposition p,denotedt| ,by i p another termt′ isdenotedt[t′]p anddefinedbyt[t′]e =t′ and f(t1,...,tn)[t′]i.p′ = f(t1,...,ti[t′]p′,...,tn). AcontextCisaspecialterm,inwhichthevariable(cid:3)occursexactlyonce. Then,wewriteC[t]todenote thetermthatisobtainedbyreplacing(cid:3)withthetermt. Ifinarewritestept→t′ theredexisonposition p∈Pos(t),wewritet → t′. Wealsowritet → toindicatethatthetermt hasaredexatposition p. For p p two positions p,q we write p≤q if p is a prefix of q, and p<q if p is a proper prefix of q, that is, the position p is above q. If neither p≤q nor q≤ p, then we call the two positions independent, which is denoted pkq. Arewritestept→ t′ iscalledoutermostift doesnotcontainaredexinapositionqwith p q< p. Areductioniscalledoutermostifeverystepisoutermost. Suchaninfiniteoutermostreductionis calledbalancedoutermost,ifeveryredexiseventuallyeitherreducedorconsumedbyaredexatahigher position, asformallydefinedbelow. Definition3. LetRbeanarbitrary TRS.Aninfiniteoutermostreduction t → t → t → t ··· 1 p1 2 p2 3 p3 4 with respect to R is called balanced outermost if for every i and every redex of t on position q there i exists j≥isuchthat p ≤q. TheTRSRiscalledbalancedoutermostterminatingifitdoesnotadmitan j infinitebalancedoutermost reduction. A direct consequence isthat for anyinfinite outermost reduction thatis notbalanced and contains a redexonposition pinsometerm,everytermlaterinthereduction hasaredexonposition p,too. AsanexampleweconsiderthestreamspecificationfortheThueMorsesequencefromtheintroduc- tion. Theinfinitereduction tail(morse) → tail(0:zip(inv(morse),tail(morse))) → zip(inv(morse),tail(morse)) continued by repeating this reduction forever on the created subterm tail(morse), is outermost, but not balanced, since theredex morseonposition 1.1inthetermzip(inv(morse),tail(morse))isneverrewrit- ten, and neither a higher redex. By forcing the infinite outermost reduction to be balanced, this redex shouldberewritten,afterwhichtheruleforinvcanbeapplied,andhastobeappliedduetobalancedness, afterwhichthefirstargumentofzipwillhave’:’asitsroot,afterwhichoutermostreduction willchoose thezipruleandcreatea’:’astheroot. Nowwearriveatthemaintheorem,showingthatproductivity ofastreamspecification isequivalent tobalanced outermosttermination ofthestreamspecification extended withtherulex:s →overflow. Theorem4. Astreamspecification(S ,S ,R ,R )isproductiveforallgroundtermsofsortsifandonly d s d s if R ∪ R ∪ {x:s →overflow} d s isbalanced outermostterminating. 3 Soundness In this section we show soundness of Theorem4, i.e., balanced outermost termination of the extended TRSimpliesproductivity ofthecorresponding streamspecification. Fordoingso,usingthespecialshapeofstreamspecifications,firstweprovealemmastatingthatany ground termnothaving’:’asrootsymbolcontainsaredexthatisnotbelowa’:’symbol. HansZantemaandMatthiasRaffelsieper 87 Lemma 5. Let (S ,S ,R ,R ) be a stream specification, and let t be a ground term of sort s with d s d s root(t)6=:. Thenthereexistsaposition p∈Pos(t)suchthatt → andforall p′< p,root(t| )6=:. p p′ Proof. Thislemmaisprovenbystructural induction ont. Ift isaconstant c∈S ,thenbyrequirement thereisarulec→r∈R forsometermr. s s Otherwise,t = f(u ,...,u ,t ,...,t )forsomesymbol f 6=:,groundtermsu ,...,u ofsortd,and 1 m 1 n 1 m ground termst1,...,tn of sort s. Ift →e , then the lemmaholds. Therefore, we assume in the rest of the proofthatthisisnotthecase. Ifthereisau suchthatu →,thenthisreduction isnotbelowa’:’since f 6=:. i i Otherwise, assume that u ∈NF(R ) for all 1≤i≤m. If there is a term t with root(t )6=:, then i d j j we get from the induction hypothesis that t → for some position p that is not below a ’:’. Hence, j p the position (m+ j).p is also not below a ’:’, since f 6=:. Finally, we have to consider the case where u ∈NF(R )andt =u :t′ for all 1≤ j≤n and some terms u ,t′. However, in this case it is required i d j j j j j bystreamspecifications thatt →e ,givingacontradiction toourassumption. Usingtheabovelemma,wecannowprovesoundness ofourmainresult, i.e.,wecanshowastream specification (S ,S ,R ,R ) to be productive by showing R ∪R ∪{x:s →overflow} to be balanced d s d s d s outermost terminating. ProofofSoundness ofTheorem4. Assume t is not productive, i.e., it does not rewrite to a term with ’:’ as its root symbol. This allows us to construct an infinite balanced outermost reduction w.r.t. R ∪ d R ∪{x :s →overflow}: According to Lemma5, there exists a position p such that t → and for all s p p′ < p, root(t| )6=:. Hence, there exists a position q ≤ p such that for some term t , t → t is an p′ 1 1 q1 1 outermoststepw.r.t.R ∪R . Sincealsoforallq′<q ,root(t| )6=:,thisisalsoanoutermoststepw.r.t. d s 1 q′ R ∪R ∪{x:s →overflow}. Alsot isnotproductive, otherwise, ift wouldrewrite toaterm with’:’ d s 1 1 as its root symbol, then so wouldt. Hence, we can repeat this argument to obtain an infinite outermost reductiont =t → t → t → .... 0 q1 1 q2 2 q3 There might however be a term t and a redex on a position p ∈ Pos(t) that is never reduced or i i consumed inthe constructed infinite outermost reduction. However, then there isnever areduction step above pinthe remaining reduction, i.e., for all j>i, q 6≤ p. Since the reduction consists of outermost j steps, we furthermore can conclude that q 6> p, otherwise t → t would not be outermost. Hence, j j−1 qj j q k pforall j>i. Let p′≤ psuchthatt → isanoutermoststep. Thenalso p′kq forall j>i,since j i p′ j q ≤p′≤pwouldcontradicttheassumptionthatq 6≤pandq >p′wouldcontradicttheassumptionthat j j j t → t is an outermost step. Therefore, we can reduce the redex at position p′ at any time, without j−1 qj j affecting reducibility of the redexes at positions q . These however might now become non-outermost j steps. So let t →∗t → ···→ t → t′ for some k>i such that t′ → is not an outermost 0 i qi+1 qk k p′ k+1 k+1 qk+1 step. Butthenwecanagainapply theabovereasoning thatthere isaredex onaposition notbelow a’:’ symbolint′ andfollowingterms,yieldinganother infiniteoutermostreduction forwhichtheredexof k+1 t atposition pisreducedorconsumed. Repeatingthisconstruction givesaninfinitebalancedoutermost i reduction, whichshowssoundness ofthetheorem. 4 Completeness In this section we show completeness of Theorem4, i.e., disproving balanced outermost termination allows us to conclude non-productivity. Before we can prove this however, we first have to introduce somenotation thatallowsustodistinguish betweenoutermostandnon-outermost rewritesteps. 88 StreamProductivitybyOutermostTermination Definition6. ForaTRSR,wedefinet→o t′ift→ t′ isanoutermostrewritestep. Otherwise,ift→ t′ p p p isnotanoutermostrewritestep,wedefinet →no t′. p Byconvention, wewill denote substitutions withV ,r , which are mappings from variables to terms, writtenas{x :=t ,...,x :=t }. Application ofasubstitution V toatermt isdenotedtV . GivenaTRS 1 1 n n R, c is called a constructor if root(ℓ)6=c for all rules ℓ→r∈R. Furthermore, given a term t, the tail of a position p∈Pos(t) w.r.t.another position p′ ∈Pos(t) with p′ ≤ pis denoted prp′ and defined as pre = p and i.pri.p′ = prp′. Thereby, prp′ is p after removing the prefix p′. Finally, we define theconcept ofparallelrewritesteps. k Definition 7. For a TRS R we define the parallel rewrite step t →t′ if there exists a set of positions {p ,...,p }⊆Pos(t)suchthatforall1≤i,j≤nwithi6= j, p k p andt → t → ···→ t′. 1 n i j p1 1 p2 pn AstandardlemmathatwewilluseistheParallelMovesLemma,whichisforexamplepresentedand proved in[1, Lemma6.4.4]. Wewillhoweveruse aslightly different form than presented there, but the proofof[1]easilyshowsthistobetrue. Parallel Moves Lemma. Let R be a TRSand ℓ→r∈R a left-linear rule. If for two substitutions V ,V ′ wehavethatxV →k xV ′ forallvariables x,thenℓV →k ℓV ′→rV ′ andℓV →rV →k rV ′. ItiseasytoseethatforanorthogonalTRS,theParallelMovesLemmaisalwaysapplicableincasea term isreducible attwodifferent positions. Thisholds, since there arenooverlaps ofthe rules, i.e.,any redexcontained inanother redexmustbebelowsomevariableposition, henceinthesubstitution part. We will now show that a non-outermost reduction step followed by an outermost reduction step is eitheronanindependent position oronaposition belowtheoutermost step. Lemma8. LetRbeanorthogonal TRS.Ift →no t →o t ,then pkqor p<q. 1 q 2 p 3 Proof. Lett →no t →o t . Therefore, aposition q′<qexistssuchthatt → . 1 ℓ1→r1,q 2 ℓ2→r2,p 3 1 ℓ′→r′,q′ Assumethat p∦qandq≤p(wherethelatterimpliestheformer). Thent =t [ℓ′V ′[ℓ V ] ] . Since 1 1 1 1 qrq′ q′ Risorthogonal, thereexistsavariablexandacontextCsuchthatt =t [ℓ′V ′′{x:=C[ℓ V ]}] ,whereV ′′ 1 1 1 1 q′ islikeV ′ exceptthatV ′′(x)=x. Therefore,t =t [ℓ′V ′′{x:=C[ℓ V ]}] →no t [ℓ′V ′′{x:=C[r V ]}] =t . 1 1 1 1 q′ q 1 1 1 q′ 2 In this last term, the redex at position p is contained, i.e., t =t [ℓ′V ′′{x :=C[r V ]}] =t [ℓ′V ′′{x := 2 1 1 1 q′ 1 C[r V [ℓ V ] ]}] foraposition p′suchthat p=q′.(qrq′).p′. However,thiscontradictsourassumption 1 1 2 2 p′ q′ t →o t ,sincet → andq′<q≤ p. 2 p 3 2 q′ The above lemma allows us to show that for such a sequence of steps, i.e., a non-outermost step followed by an outermost step, we can swap the evaluation order and still reach the same term. In the q no remainder of this section we denote with −−→ parallel non-outermost steps, i.e., a parallel reduction P whereallpositions inthesetPareonnon-outermost positions. Lemma9. Foranorthogonal TRSR,ift −q−n→o t →o t ,thent →o t →o ∗t′−q−n→o t forsometermst,t′. 1 2 p 3 1 p 3 Proof. Lett −q−n→o t →o t for some Q⊆Pos(t ). By Lemma8, we get that either qk p or q> p for 1 Q 2 p 3 1 allq∈Q. If qk p for all q∈Q, then we can swap the two reductions, i.e., t →o t → t for some term t. If 1 p q 3 t →no t , then we have the required shape. Otherwise, if t →o t then we also have the required shape, q 3 q 3 sincet →o t →o t −q−n→o t . 1 p q 3 0/ 3 Otherwise,amaximal0/ 6=Q′⊆Qexistssuchthat p<q′forallq′∈Q′. Lett −q−n→o t′ →o t′. Then, 1 Q′ 2 p 3 since R is orthogonal, we can apply the ParallelMovesLemma, showing that t →o t →k t′ for some t. 1 p 3 HansZantemaandMatthiasRaffelsieper 89 k Allredexesinthereductiont →t′ areonindependent positions, hencewecanfirstreducealloutermost 3 ones, thenallnon-outermost ones. Therefore, atermt′ existssuchthatt →o t →o ∗t′−q−n→o t′ forsome 1 p Q′′ 3 setQ′′,where p<q′′forallq′′∈Q′′. BecauseallpositionsinQ\Q′areindependentfromtheposition p, theyarealsoindependent fromthepositionsinQ′′. Thus,wegetthatt →o t→o ∗t′−q−n→o t . 1 p Q′′∪(Q\Q′) 3 Using the above lemma, we can prove that any reduction can be split into an outermost and a non- outermost reduction. Lemma10. LetRbeanorthogonal TRS. Ift →∗t′,thent →o ∗tˆ→no∗t′ forsometˆ. Proof. Lett →nt′. Weperform induction onthelengthnofthisreduction. Ifn=0,thent =t′ andnothinghastobeshown. Otherwise, lett →n−1t →t′. Wegetfrom theinduction hypothesis thatt →o ∗tˆ′→no∗t →t′ for n−1 n−1 some tˆ′. If t →no t′ then the lemma holds. So assume t →o t′. Then tˆ′ →no∗ t →o t′ and therefore n−1 n−1 n−1 tˆ′ −q−n→o ∗ t →o t′. Repeated application of Lemma9 shows that for some tˆ, tˆ′ →o ∗ tˆ−q−n→o ∗ t′, hence n−1 t →o ∗tˆ′→o ∗tˆ→no∗t′ byunfolding theparallel non-outermost steps,whichprovesthelemma. Thisallowsustoshowthatforchecking theproductivity criterion ofProposition 2,weonlyhaveto consider outermostreductions. Lemma11. LetRbeanorthogonal TRShavingabinarysymbol:initssignature. Ift →∗u:t ,thent →o ∗u′:t′ →∗u:t forsometermsu′,t′. u u u u Proof. Let t →∗ u :t . Then by Lemma10, t →o ∗ tˆ→no∗ u :t . If root(tˆ) = :, then the lemma holds. u u Otherwise, root(tˆ)6=:. Lettˆ=t →no t →no ···→no t =u:t . Thenforall1≤i≤k,root(t)=root(t ), 0 1 k u i i−1 sincenoneofthetermscanbereducedattherootposition asthiswouldbeanoutermost reduction step. Thishowevergivesacontradiction, because:6=root(tˆ)=root(t )=root(t )=···=root(t )=root(u: 0 1 k t )=:. u Next, weprove twotechnical lemmasthat willbeused toprovecompleteness ofourmaintheorem. Inthefirstwehandlethecasewherearedexinatermthatstartsaninfinitebalancedoutermostreduction is also reduced at that position later in the infinite balanced outermost reduction. In this case, we can bringforwardthisstepandstillgetaninfinitebalancedoutermost reduction. Lemma12. LetRbeanorthogonal TRSforwhich’:’isaconstructor. Ift →o t →o ···→o t →o ··· isaninfinitebalancedoutermostreduction, whereforalli∈N, 0 p1 1 p2 pj j pj+1 root(t) 6= :, t →o t′, and p 6≤ p for all 1 ≤ i < j, then an infinite balanced outermost reduction i 0 pj 1 i j t →o t′ →o ··· exists, whereforalli∈N,root(t′)6=:. 0 pj 1 i Proof. Firstweshowthat p k p forall1≤i< j. Forthis,weperforminductionon j−iandprovethat i j ifi< jandt → ,then p k p andt → . i−1 pj i j i pj o If j−i=0, then i= j and the claim vacuously holds. Otherwise, wehavet → t andt → . i−1 pi i i−1 pj If p ≤ p ,wehaveacontradiction totherequirement p 6≤ p ,sincei< j. If p > p ,thenwealsohave i j i j i j acontradiction, sincethent 6→o . Hence, p k p andtherefore alsot → . i−1 pi i j i pj Thisshowsthatallpositions p with1≤i< jareonindependent positions from p ,sincet → by i j 0 pj assumption. Therefore,wecanswaptheirorderandgetareductiont →o t′ → t′ → ···→ t′ =t . Due toLemma10, there exists atˆ such thatt →o t′ →o ∗tˆ →no∗t .0Letptj 1=t′p1→o2 t′p2→o ··p·j−→o1 j t′ =j 1 0 pj 1 1 j 0 0 q1 1 q2 qk k tˆ →no ···→no t′=t ,whereq = p . Furthermore, letq = p andt′ =t forallm≥1. We 1 qk+1 ql l j 1 j l+m j+m l+m j+m willnowshowthateveryredexinthisreduction iseventually reducedorconsumedbyahigherredex. 90 StreamProductivitybyOutermostTermination Assume not, i.e., there exists i≥0 such that for some q∈Pos(t′), t′ → and for all m>i, q 6≤q, i i q m i.e., either q > q or q k q. We can conclude that i < l, since t′ =t and t is part of the balanced m m l j j outermostreductiont →o ···. If0≤i<k,thent′→o t′ →o ···→o t′. Ifq >q,thenbecause 0 p1 i qi+1 i+1 qi+2 qk k i+1 of t → we would have t 6→o ; therefore this cannot occur. If q kq, then we also have t′ → . i q i qi+1 i+1 i+1 q Applying this repeatedly shows that t′ → , i.e., it suffices to investigate the case where i≥k. In this k q case, wehavet′ →no ···→no t′ =t . Ifq kq, then alsot′ → . Otherwise, if q >q, then due to i qi+1 ql l j i+1 i+1 q i+1 theParallelMovesLemma,wealsohavet′ → . Applyingthisrepeatedlyshowsthatt′=t → andfor i+1 q l j q allm>l wehaveq 6≤q. Thishoweverisacontradiction, sincet wascontained intheinitial balanced m j outermost reduction. Thisshowsourclaim. Furthermore, any non-outermost step of the above reduction, i.e., any step t′ →no t′ for i ℓi+1→ri+1,qi+1 i+1 k≤i<l, is below some position p for m> j. To show this, let t′ =t′[ℓ V ] . Then a position m i i i+1 i+1 qi+1 q′ <q exists such that t′ =t′[ℓV [ℓ V ] ] → for some ℓ→r ∈R. Since R is orthogonal, i+1 i i i+1 i+1 qi+1rq′ q′ q′ there must be a variable x and a contextC such that t′ =t′[ℓV ′{x:=C[ℓ V ]}] , where V ′ is like V , i i i+1 i+1 q′ except that V ′(x)=x. Thent′ =t′[ℓV ′{x:=C[ℓ V ]}] →no t′[ℓV ′{x:=C[r V ]}] =t′ → , i i i+1 i+1 q′ qi+1 i i+1 i+1 q′ i+1 q′ i.e., t′ still contains a redex at position q′. Repeating this argument, we see that for every reduced i+1 non-outermost redex,thereisastillaredexaboveitinthetermt′=t . However,foreverysuchredexat l j somepositionq′,thereisaposition p withm> jsuchthat p ≤q′duetotheinitialbalancedoutermost m m reduction, showingourclaim. Tothereduction t =t′ →o t′ →o ∗tˆ →no∗t →o ··· wecan now repeatedly apply Lemma9toget 0 0 pj 1 1 j pj+1 theoutermostreductiont =t′ →o t′ =t′′→o ∗tˆ →o t′′→o ∗tˆ →o ···. Thisisabalancedoutermost 0 0 pj 1 1 1 pj+1 2 2 pj+2 reduction due to the above observations, since every redex in areduction t′′ →o ∗tˆ is eventually reduced i i orconsumed andeveryredexinareductiontˆ →no∗t′′ isbelowsomeposition p thatisreduced laterin i i+1 m thereduction. Finally,wehavetoshowthatnoneofthetermsintheconstructed infinitebalancedoutermostreduc- tion has a’:’ symbol as itsroot. Ifthis wasnot the case, there would beatermt′′ with root(t′′)=:and t′′ →o ∗tˆ for some m. However, for every such termtˆ , we have thattˆ →no∗t for some n. Since ’:’ isa m m m n constructor of R, wewould have that :=root(t′′)=root(tˆ )=root(t )6=:, giving acontradiction and m n henceshowingthedesired property. Thesecondcasewehavetoconsider isthataredexinatermstarting aninfinitebalanced outermost reduction is strictly below some reduction step. But also in this case, we will show that we can reduce theredexandstillgetaninfinitebalanced outermostreduction. Lemma 13. Let R be an orthogonal TRS for which : is a constructor, t →o t →o ... be an infinite 0 p1 1 p2 balanced outermost reduction with root(t)6=: for all i≥0, t → t [rV ] =t′, and let p ≤q be i 0 ℓ→r,q1 0 q1 1 j 1 minimal,with p <q . j 1 Thenaninfinitebalancedoutermostreductiont [rV ] =t′ →o t′ →o ... existswithroot(t′)6=:for 0 q1 1 p′1 2 p′2 i alli≥1. Proof. Let t =t [r V ] ...[r V ] [ℓ V ] . Then for some variable x∈V(ℓ ) and some con- j−1 0 1 1 p1 j−1 j−1 pj−1 j j pj j textCwehavethatt =t [r V ] ...[r V ] [ℓ V ′{x:=C[ℓV ]}] →o t [r V ] ...[r V ] j−1 0 1 1 p1 j−1 j−1 pj−1 j j pj pj 0 1 1 p1 j−1 j−1 pj−1 [r V ′{x:=C[ℓV ]}] =t ,whereV ′ islikeV ,exceptthatV ′(x)=x. j j pj j j j j Ifx∈/V(r ),thenthelemmatriviallyholds. j Otherwise,let p(cid:3)∈Pos(C)suchthatC|p(cid:3)=(cid:3)andQj={q∈Pos(tj)|q=pj.p′.p(cid:3) andrj|p′ =x}= {qj,...,qj }. Thent → forallq∈Q . Furthermore, wedefineforallk> j,Q ={qk,...,qk }= 1 mj j ℓ→r,q j k 1 mk (Q \{q∈Q | p ≤q})∪{q′ ∈Pos(t ) |∃q∈Q :q= p .p.p′,ℓ | =y∈V, andq′ = p .p′′.p′ k−1 k−1 k k k−1 k k p k wherer | =y}, i.e., weupdate the set ofpositions such that independent positions are kept, positions k p′′ HansZantemaandMatthiasRaffelsieper 91 that are reduced are removed, andpositions below areduction ofthe infinite balanced outermost reduc- tionaremodifiedsuchthattheyreflecttheposition oftheredexintheright-hand side. Thiscanbedone since the TRS is orthogonal, which especially implies that a contained redex cannot overlap with the left-hand side of a rule that is applied above it, therefore it has to be below a variable position in the left-hand side. Hence, we have for all k > j either p kq for all q∈Q , p =q for some q∈Q , or p <q k k−1 k k−1 k for some q∈Q (p cannot be below someq, since otherwise itwould not beoutermost). Inthe first k−1 k case, the reduction t [rV ] ...[rV ] → is unaffected. In the second case, where p =q, we can k−1 qk1−1 qkm−1 pk k removethisreduction step. Inthethirdandfinalcase, where p <q,thisreduction isalsostillpossible, k sinceRisorthogonal andreductions insideanother redexcannotdestroy theouterredex. Hence,wecan again apply the argument and get aninfinite reduction t′ =t [rV ] → t′ → ..., where the positions 1 0 q1 p′1 2 p′2 p′ are the positions p after removing reduction steps as described above. This reduction is balanced, i i but not necessarily outermost. However, wecan repeatedly apply Lemma9 to get an infinite outermost reduction, which will defer non-outermost steps forever. To see that this reduction is balanced, assume the contrary. Then, a term t′ and a position q∈Pos(t′) exist such that t′| → and this redex is never a a a q reduced or consumed, and there exists h>a such that p ≤q since the non-outermost reduction was h balanced. Since Lemma9 only swaps non-outermost reductions to the end, it must be the case that all p ≤qarenon-outermost. Thenhowever anoutermost position p < p exists, hence itisnot deferred h h′ h forever. This gives a contradiction, since this position is reduced eventually, consuming the redex at position q. Finally, we show that root(t′) 6= : for all i ≥ 1. Assume this not to be the case, i.e., there is a i minimalt′ withroot(t′)=:. Then p′=e andfort′ → u:t′ itmustbethecasethatroot(r′)=:. i i i i−1 ℓ′→r′,p′i However, since this step was also contained in the original infinite balanced outermost reduction, this would contradict therequirement thatroot(t)6=:. Furthermore, since :isaconstructor, also reordering i thereductionsintoanoutermostreductioncannotintroduceatermwith:asrootsymbol,sinceotherwise this term could be reduced to a termt′ with root(t′)=:, which wehave shown to be false. This proves i i thelemma. Usingtheabovelemmas,wecanfinallyprovecompleteness ofourmaintheorem. ProofofCompleteness ofTheorem4. Assume R ∪R ∪{x:s →overflow} is not balanced outermost d s terminating, but(S ,S ,R ,R )isproductive. Thenatermt existsthatallowsaninfinitebalancedouter- d s d s mostreductiont=t′ →o t′ →o t′ →o ··· andthereexistsareductiont→∗u′:t′. Sincethesymboloverflow 0 1 2 u doesnotoccuronanyleft-handsideofR ∪R ,weconcludethatforalli≥0,root(t′)6=:,sinceotherwise d s i therulex:s →overflowwouldbeapplicable andnofurtherreductions wouldbepossible. We can also construct an infinite balanced outermost reduction w.r.t. R ∪R from the given one by d s removing allapplications oftherulex:s →overflow,sincethesymbol overflowdoesnotoccur onany left-hand sideofR ∪R . Thismightleavesomeredexesthatpreviously werecontained inaredexw.r.t. d s that rule. However, these redexes can only be on positions above which never a reduction step takes place, hence we can reduce them at any time. Thus, we have an infinite balanced outermost reduction t =t →o t →o t →o ··· w.r.t.theorthogonal TRSR ∪R ,whereforalli≥0,root(t)6=:. 0 p1 1 p2 2 p3 d s i ByLemma11wegetthatanoutermost reductiont →o tp→o ···→o tp=u:t exists. Duetothe q1 1 q2 qn n u definition of balanced outermost reductions, we have that a minimal j exists such that p ≤q . Case j 1 distinction onthe relation of p and q isperformed. If p =q then weget from Lemma12 aninfinite j 1 j 1 balanced outermost reduction t →o tp =t′ →o t′ →o .... Otherwise, if p <q , Lemma13 gives us an 0 pj 1 1 2 j 1 infinitebalancedoutermost reductiontp=t′ →o t′ →o .... 1 1 2 92 StreamProductivitybyOutermostTermination Inbothcases,wefurthermorehavethatroot(t′)6=:foralli>0. Hence,byinductiononnwegetan i o infinite balanced outermost reduction u:t →... inwhich noterm hasas root symbol ’:’, which yields u thedesiredcontradiction andtherefore completestheproof. 5 Using Outermost Termination Tools As stated in the introduction, balancedness is obtained for free in case there are no rewrite rules for the data,i.e.,R =0/,andtherearenorulesinR thathavemorethanoneargument ofstream types. Inthis d s sectionweprovethatclaim,whichallowsustoapplyautomatictoolsforprovingoutermosttermination toshowproductivity ofstreamspecifications. Proposition14. Let(S ,S ,R ,R )beastreamspecification withR =0/ andthetypeofall f ∈S isof d s d s d s theformdn×sm→sforsomen∈N,m∈{0,1}. Theneveryinfiniteoutermost reductiont →o t →o t →o ... isbalanced. 0 1 2 Proof. Weperform structural induction toshow thatforanyreduction stept →o t′,wehavethat p≤ p′ p forallpositions p′∈Pos(t)witht → . p′ If t =c∈S s, then by requirement of stream specifications we have that t →e , hence p=e . Since e ≤ p′ forall p′∈Pos(t),wehavenproventhiscase. Otherwise,ift= f(u ,...,u )(i.e.,thereisnoargumentofstreamtype),thenweagainconcludethat 1 n t →e . This is due to Rd =0/ and the requirements of stream specifications, note that no data operations areallowedwithargumentsofstreamtype. Sowehavealsoproventhiscase. Inthefinalcasetoconsider,wehavet= f(u1,...,un,t′). Ift→e ,thenagainwemusthavethat p=e andhencehaveproventhecase. Therefore, assumethat p>e . Sinceu ,...,u ∈D=NF(R ),because 1 n d R =0/, it must be the case that for all p′ ∈Pos(t) with t → , n+1≤ p′, hence this especially holds d p′ for p as well. Therefore, weget from the induction hypothesis that for the reduction stept′ →o t′′, prn+1 prn+1≤ p′′ forallpositions p′′ ∈Pos(t′)witht′ → . Becauset →o t′, p=(n+1).(prn+1), and p′′ p for all p′ ∈Pos(t) witht → we have p′ =(n+1).p′′, it also holds that p≤ p′, proving this final case p′ andtherefore theproposition. The specification of the Thue Morse sequence given in the introduction shows the necessity of re- quiring atmostoneargumenttobeofstreamtype. Itwasalready observedthattheinfinitereduction tail(morse)→tail(0:zip(inv(morse),tail(morse)))→zip(inv(morse),tail(morse))→..., continuedbyrepeatedlyreducingtheredextail(morse),isoutermostbutnotbalanced. Toshowthatalso therequirementR =0/ isneeded,weagaingiveanexamplethatallowstoconstructaninfiniteoutermost d reduction thatisnotbalanced. Considerthestream specification tail(x:s ) = s c = 0:f(not(1),tail(c)) f(0,s ) = 1:f(0,s ) f(1,s ) = 0:f(1,s ) together with the rules R ={not(0)→1,not(1)→0}. This stream specification is productive, as can d be checked withthe productivity tool of [2]. However, there also exists an infinite outermost reduction, namely tail(c)→tail(0:f(not(1),tail(c)))→f(not(1),tail(c))→...,