Under consideration for publication in Theory and

UnderonsiderationforpubliationinTheoryandPratieofLogiProgramming1TransformationsofLogiProgramswithGoalsasArgumentsALBERTOPETTOROSSIDipartimentodiInformatia,SistemieProduzione,UniversitadiRomaTorVergata,ViadelPolitenio1,I-00133Roma,Italy(e-mail:alberto.pettorossiuniroma2.it)MAURIZIOPROIETTIIASI-CNR,VialeManzoni30,I-00185Roma,Italy(e-mail:proiettiiasi.rm.nr.it)AbstratWeonsiderasimpleextensionoflogiprogrammingwherevariablesmayrangeovergoalsandgoalsmaybeargumentsofprediates.Inthislanguageweanwritelogiprogramswhihusegoalsasdata.Wegivepratialevidenethat,byexploitingthisapabilitywhentransformingprograms,weanimproveprogrameÆieny.Weproposeasetofprogramtransformationruleswhihextendthefamiliarunfoldingandfoldingrulesandallowustomanipulatelauseswithgoalswhihourasargu-mentsofprediates.Inordertoprovetheorretnessofthesetransformationrules,weformallydenetheoperationalsemantisofourextendedlogiprogramminglanguage.ThissemantisisasimplevariantofLD-resolution.WhensuitableonditionsaresatisedthissemantisagreeswithLD-resolutionand,thus,theprogramswritteninourextendedlanguageanberunbyordinaryPrologsystems.Ourtransformationrulesareshowntopreservetheoperationalsemantisandtermi-nation.KEYWORDS:programtransformation,unfold/foldtransformationrules,higherorderlogiprogramming,ontinuations1IntrodutionProgramtransformationisaverypowerfulandwidelyreognizedmethodologyforderivingprogramsfromspeiations.Therules+strategiesapproahtoprogramtransformationwasadvoatedinthe1970sbyBurstallandDarlington(1977)fordevelopingrstorderfuntionalprograms.SinethenBurstallandDarlington’sapproahhasbeenfollowedinavarietyoflanguageparadigms,inludinglogiallanguages(TamakiandSato1984)andhigherorderfuntionallanguages(Sands1996).Thedistintivefeatureoftherules+strategiesapproahisthatitallowsustoseparatetheonernofprovingtheorretnessofprogramswithrespettospeiationsfromtheonernofahievingomputationaleÆieny.Indeed,theorretnessofthederivedprogramsisensuredbytheuseofsemantispreservingtransformationrules,whereastheomputationaleÆienyisahievedthroughthe2A.PettorossiandM.Proiettiuseofsuitablestrategieswhihguidetheappliationoftherules.Thepreservationofthesemantisisprovedoneandforall,forsomegivensetsoftransformationrules,andifwerestritourselvestosuitablelassesofprograms,weanalsoguar-anteetheeetivenessofthestrategiesforimprovingeÆieny.Inthispaperwewillarguethroughsomeexamples,thatasimpleextensionoflogiprogrammingmaygiveextrapowertotheprogramtransformationmethod-ologybasedonrulesandstrategies.Thisextensiononsistsinallowingtheuseofvariableswhihrangeovergoals,alledgoalvariables,andtheuseofgoalswhihareargumentsofprediates,alledgoalarguments.Inthepratieoflogiprogrammingtheideaofhavinggoalvariablesandgoalargumentsisnotnovel.Thereadermaylook,forinstane,at(SterlingandShapiro1986;Warren1982).Goalvariablesandgoalargumentsanbeusedforexpress-ingthemeaningoflogialonnetivesandforwritingprogramsinaontinuationpassingstyle(TarauandBoyer1990;Wand1980)asthefollowingexampleshows.Example1ThefollowingprogramP1:F_GFF_GGexpressesthemeaningoftheoronnetive.ThefollowingprogramP2:p([℄;Cont)Contp([XjXs℄;Cont)p(Xs;q(X;Cont))q(0;Cont)ContusesthegoalvariableContwhihdenotesaontinuation.Thegoalp(l;true)su-eedsinP2ithelistlonsistsof0’sonly.Programswithgoalvariablesandgoalarguments,suhasP1andP2intheaboveexample,arenotallowedbytheusualrstordersyntaxofHornlauses,wherevariablesannotourasatomsandprediatesymbolsaredistintfromfuntionsymbols.Nevertheless,theseprogramsanberunbyordinaryPrologsystemswhoseoperationalsemantisisbasedonLD-resolution,thatis,SLD-resolutionwiththeleftmostseletionrule.FortheoneptsofLD-resolution,LD-derivation,andLD-treethereadermayreferto(Apt1997)Theextensionoflogiprogrammingweonsiderinthispaper,allowsustowriteprogramswhihusegoalsasdata.Thisextensionturnsouttobeusefulforper-formingprogrammanipulationswhiharerequiredduringprogramtransformationandareotherwiseimpossible.Forinstane,wewillseethatbyusinggoalvariablesandgoalarguments,weareabletoperformgoalrearrangements(alsoalledgoalreorderingsin(Bossietal.1996))whihareoftenrequiredforfolding,withoutaetingprogramterminationandwithoutinreasingnondeterminism.Goalrearrangementisalongstandingissueinlogiprogramtransformation.Indeed,althoughtheunfold/foldtransformationrulesbyTamakiandSato(1984)preservetheleastHerbrandmodel,theymayrequiregoalrearrangementsandthus,theymaynotpreservetheoperationalsemantisbasedonLD-resolution.Moreover,goalrearrangementsmayinreasenondeterminismbyrequiringthatprediateallsTransformationsofLogiProgramswithGoalsasArguments3havetobeevaluatedbeforetheirargumentsaresuÆientlyinstantiated,andinmanyPrologsystems,insuÆientlyinstantiatedallsofbuilt-inprediatesmayauseerrorsatrun-time.In(BossiandCoo1994)ithasbeenprovedthatbyrul-ingoutgoalrearrangements,ifsomesuitableonditionshold,thentheunfolding,folding,andgoalreplaementtransformationrulespreservetheoperationalseman-tisoflogiprogramsbasedonLD-resolutionand,inpartiular,theserulespreserveuniversaltermination,thatis,thenitenessofallLD-derivations(Apt1997;VasakandPotter1986).But,unfortunatel