JanisVoigtl¨ander∗
ArminK¨uhnemann
DepartmentofComputerScience,DresdenUniversityofTechnologyD–01062Dresden,Germany.E-mail:{voigt,kuehne}@tcs.inf.tu-dresden.de
Abstract
Aclassofrecursivefunctionswithaccumulatingparameterscanbemodeledby
macrotreetransducers.Wepresentaprogramtransformationtechniquethatcanbeusedtosolvetheefficiencyproblemsduetocreationandconsumptionofintermedi-atedatastructuresincompositionsofsuchfunctions,whereclassicaldeforestationtechniquesfail.
Inordertodoso,weconstructfortwogivenmacrotreetransducers,underappro-priaterestrictions,asinglemacrotreetransducerthatimplementsthecompositionofthetwooriginalones.Theimposedrestrictionsaremoreliberalthanthoseintheliteratureonmacrotreetransducercomposition,thusgeneralizingpreviousresults.
1Introduction
Animportantstyleofwritingprogramsinafunctionallanguageistodefinenewfunctionsbycompositionofexistingones.Thus,theresultofafunctionapplicationispassedasargumenttoanotherfunction.Thismodularprogrammingtechniqueofsolvinganoverallproblembycombiningsolutionsofpartialproblems—whichmightbesolvedbypredefinedorself-writtenfunctions—simplifiesthedesignandverificationofprograms,andencour-agesthereuseofexistingprogrammingsolutions.Unfortunately,modularprogramsoftenlackefficiencycomparedtoother—oftenlessunderstandable—programs,whichsolvethesametasks.Ifthecreatedintermediateresultsarestructuredobjects—forexamplelistsortrees—theircreationandeventualdestructionwillconsumetimeandmemoryspace.Furthermore,itispossiblethat,e.g.,listsaretraversedmoreoften,thanwouldreallybenecessaryforsolvingtheoverallproblem.Thus,wewouldliketohaveprogramtransfor-mationtechniques,whichenableustooptimizefunctionswritteninthemodularstyle,byeliminatingintermediatedatastructures.Severalsuchtechniqueshavebeenstudiedintheliterature,e.g.,thefold/unfold-techniquefrom[BD77],itsalgorithmicinstancessupercompilation[Tur86,SGJ96,SS99]anddeforestation[Wad90,Chi94],catamorphismfusion[Mal89,MFP91]andshortcutdeforestation[GLP93,Gil96].
Inthispaperwefollowanapproachforeliminatingintermediateresults,whichisbasedonthetheoryoftreetransducers[FV98].Particularly,weconsidermacrotreetransduc-ers[Eng80],whichrepresentalargeclassoffunctionalprograms.Macrotreetransducersareextendedschemesofprimitiverecursion,allowingsimultaneousdefinitionofseveralfunctionsandnestedfunctioncallsinparameterpositions.Compositionoffunctionsthencorrespondstoconsecutiveexecutionofmacrotreetransducers.Thegoalofavoidingin-termediatedatastructurescorrespondstotheproblemofreplacingsuchacompositionofmacrotreetransducersbyasinglemacrotreetransducer,whichcomputesthesamefunction.Itiswell-knownthatthisisnotpossibleingeneral,becausetheclassofmacro
2Introduction
3
Alsootherrestrictionsofmacrotreetransducersareknownthatallowthetransformationintoat-tributedtreetransducers,e.g.,therestricted-usecondition[KV01],whichgeneralizestheweaklysingle-useproperty,andthewell-presentedrestriction[CF82].
1
4Introduction
Anotherpossibilityisanewwayofapplyingresultsfrom[K¨uh98],byfirstdecomposingtreetrans-ducers,thusintroducingnewintermediateresults,butcreatingnewopportunitiesforcompositions,whichaltogethercanstillleadtoanoptimization.
2
5
6Preliminaries
2.2MacroTreeTransducers7
8Preliminaries
9
Althoughitwasobtainedin[Voi01]onlyafterestablishingthecompositionconstruction;theoriginalaimoftheformerpaperwastogiveadirectconstructionfortheweakerresultMACsu;MACwsu⊆MAC.4
MACnc;MACwp⊆TOP;ATTsu;ATT⊆MAC⊆TOP;YIELD⊆MACnc;MACwp,cf.Theo-rem5.10in[CF82]andtheconstructionfromExample4.5in[EV85]
3
10TheConstruction
,z1,...,zs),so
wewilltaketheright-handsideofthefirstmtt’sruleq(σ(x1,...,xk),y1,...,yr)→rhsq,σandtranslateitwithpbyreducingp(rhsq,σ
3.1TheIdea11
)
12TheConstruction
3.1TheIdea13
Thisshallnotdenoteindexedintegers,ratheritisusedasacompacternotationforthepairofpairs((h,q),(l,p)).
5
14TheConstruction
3.2FormalDevelopment15
16TheConstruction
3.2FormalDevelopment17
18TheConstruction
3.2FormalDevelopment19
20TheConstruction
3.2FormalDevelopment21
22TheConstruction
)),y1,p2,z1),
containingtwooccurrencesofnil.Thesecondone—inthezp2,1-positionofstate(1q1,1p1)—isofthekindintroducedintotheexpression(***)onpage15,wherewepromisedtheexamplegivennow.Wecanbynomeansassumethatstate(1q1,1p1)willneverneeditslastcontextparameterposition,infactwehavethat(1q1,1p1)(B(E),y1,p1,y1,p2,zp1,1,zp2,1)reducestozp2,1.Instead,wehavetoargueaccordingtotheplace,wherethe(1q1,1p1)-calloccurs,namelyinthefirstcontextparameterpositionofa(q1,p1)-callonthesametreeargument.Thus,weneedtoexplainwhytherecanbenoinputtreet,suchthat(q1,p1)calledontdependsonitsy1,p1-positionand(1q1,1p1)calledontdependsonitszp2,1-position.Wereasonintuitivelyasfollows.Ifthenormalformof(q1,p1)(t,y1,p1,y1,p2,z1)con-tainsy1,p1,thismeansthatreducingp1(q1(t,y1),z1)willleadtoacalltop1ony1.Bytheweaklysingle-usepropertyofM2,wehavearguedthattherecanbeonlyonestatep′suchthatreducingp′(q1(t,y1),···)leadstoap1-callony1.Forourparticulart,weknowthatp′=p1.Butthen,(1q1,1p1)calledont(whichcom-putesthefirstcontextparameterinacalltop1onthefirstcontextvariableofq1,resultingfromreductionofp′(q1(t,y1),···))willnotdependonzp2,1,because
3.2FormalDevelopment23
,z1)),y1,p2,z1).
2.Now,wewanttoconsiderthenil-symbols,whichoccurasfirstcontextparameterof(1q1,1p1)-callsinseveralrulesandtheinitialexpression:
(q1,p2)(x1,(1q1,1p1)(x1,nil
,nil,nil,zero),nil,nil,zero),
zero)
Thesearejustifiedbythefactthatfornoinputtreet,thestate(1q1,1p1)dependsonitsy1,p1-position(analogousforstate(1q1,1p2)andy1,p2).Thispropositionholds,because(1q1,1p1)ontcomputesthefirstcontextparameterpositionofap1-callony1,resultingfromreductionofsomep′(q1(t,y1),···).Ifthisvaluewoulddependonthep1-translationofy1,wewouldhavemetduringthereductionasituationlikep1(y1,···p1(y1,···)···),whichweargued—attheendofSubsection3.1—tobeimpossiblefornon-copyingM1andweaklysingle-useM2.3.Now,weexplainthenil-symbolinthey1,p2-positionofthesecond(1q1,1p1)-callintheinitialexpression:
(q1,p2)(x1,(1q1,1p1)(x1,nil,(1q1,1p2)(x1,nil,nil,nil,zero),nil,zero),
(1q1,1p2)(x1,(1q1,1p1)(x1,nil,nil
,zp1,1,zp2,1)),nil,zp1,1,zp2,1))
Toobtainthisright-handside,wecomputedctxp2,q1(x1,β(y1)),1,1(2,1)asdefinedin
24Aftermath
4.2ThesymmetricResultdoesnothold25
26Aftermath
4.3ASize-HeightPropertyfornon-copyingMacroTreeTransducers27
28Aftermath
o
appappx1(appy1(compoappapp1app
1app
app
app
29
appapp
30REFERENCES
REFERENCES31
32REFERENCES
REFERENCES33
34CorrectnessProof
35
)))
πp2,α(q1(x1,y1)),1,1(B(E),12,1)
=(bydefinitionofπp2,α(q1(x1,y1)),1,1)
(nf(⇒R2,(κ1,q1,1,p2(B(E)))[y1←nf(⇒R1,y1[x1←B(E)])]))
[zp1,1,zp2,1←πp1,α(q1(x1,y1)),1,1(B(E),1,1),πp2,α(q1(x1,y1)),1,1(B(E),1,1)]=(bydefinitionofκ1,q1,1,p2,withrhsq1,B=q1(x1,β(y1
36CorrectnessProof
)∈R2)
(ω(p1(y1,zp2,1),zp2,1))
[zp2,1←nf(⇒R2,z1[x1←nf(⇒R1,q1(x1,y1)[x1←B(E)]),
z1←πp1,α(q1(x1,y1)),1,1(B(E),ε,1)])]
=(bydefinitionofπp1,α(q1(x1,y1)),1,1)(ω(p1(y1,zp2,1),zp2,1))
[zp2,1←nf(⇒R2,z1[x1←nf(⇒R1,q1(x1,y1)[x1←B(E)]),
z1←zp1,1])]
=(bysubstitutionandnormalform)ω(p1(y1,zp1,1),zp1,1)
InExampleA.5wewillestablishhowthisresultcorrespondstothetwofoldunderlinedsubterminExample3.2.PThefollowingtheoremestablishesthekeypropertyofthefunctionsintroducedinDefini-tionA.1.
TheoremA.3Foreveryt∈TΣ,r,s∈N+,s′∈N,q∈Q(r+1),p∈P(s+1),p′∈P(s+1),h∈[r]andl∈[s]:ifduringareductionofp′(q(t,y1,...,yr),z1,...,zs′)with⇒R1∪R2acalloftheformp(yh,ξ1,...,ξs)occurs,thenwehaveκh,q,l,p(t)∈SEN(∅,Yr,{zp′,1,...,zp′,s′})
Pandnf(⇒R1∪R2,ξl)=(κh,q,l,p(t))[zp′,1,...,zp′,s′←z1,...,zs′].
ForprovingTheoremA.3,wewillusethefollowingprincipleofproofbysimultaneous
induction[EV85,KV94,FV98].
DefinitionA.4LetΣbearankedalphabet.Giventwostatements(I)and(II),where(I)hasafreevariablet∈TΣand(II)hasfreevariablesk∈Nandt1,...,tk∈TΣ,wesaythat(I)and(II)areprovenbysimultaneousinduction,ifwecanprovethefollowingtwoinductionsteps:
′
37
38CorrectnessProof
39
40CorrectnessProof
Itdoesnotmatter,whichvalueswereplaceforthevariablesfromZP\\{zp′′,1,...,zp′′,s′′},becausetheyanywaydonotoccurinκi−1,q,l,p(tb).Weonlyneedtoensurethatforthezp′′,1,...,zp′′,s′′thesamevaluesaresubstitutedasinthepreviousexpression.
6
41
42CorrectnessProof
)
43
44CorrectnessProof
45
46CorrectnessProof
47
48CorrectnessProof
49
50CorrectnessProof
51
Foreveryh′∈[a],s′∈Nandp′∈P(s+1),ifnot(h′,p′)≺∗q,tiC∪{(h,p)},then:
′′
nf(⇒R1;2,(nf(⇒R2∪Pair,(nestq(h,p,C∪{(h,p)}))[yu←φu,u∈[a]]))
[x←xi][x1,...,xk←t1,...,tk])=′
nf(⇒R2,p(yh′,κh′,q,1,p′(ti),...,κh′,q,s′,p′(ti))[yu←nf(⇒R1,φu[x1,...,xk←t1,...,tk]),u∈[a]])
7
′
52CorrectnessProof
53
54CorrectnessProof
因篇幅问题不能全部显示，请点此查看更多更全内容