Specialization of Functional Logic Programs Based

SpecializationofFunctionalLogicProgramsBasedonNeededNarrowing?PreliminaryversionMaraAlpuente1MichaelHanus2SalvadorLucas1GermanVidal11DSIC,UPV,CaminodeVeras/n,46020Valencia,Spain.falpuente,slucas,[e-mail]2InformatikII,RWTHAachen,D-52056,[e-mail]withacompleteoperationalsemanticsarebasedonnarrowing,aunication-basedgoal-solvingmechanismwhichsubsumesthereductionprincipleoffunctionallanguagesandtheresolutionprincipleoflogiclanguages.Needednarrowingisanoptimalnarrowingstrategyandthebasisofseveralrecentfunctionallogiclanguages.Inthispaper,wedeneapartialevaluatorforfunctionallogicprogramsbasedonneedednarrowing.Weprovestrongcorrectnessofthispartialevaluatorandshowthatthenicepropertiesofneedednarrowingcarryovertothespecializationprocessandthespecializedprograms.Inparticular,thestructureofthespecializedprogramsprovidesfortheapplicationofoptimalevaluationstrategies.Thisisincontrasttootherpartialevaluationmethodsforfunctionallogicprogramswhichcanchangetheoriginalprogramstructureinanegativeway.Finally,wepresentsomeexperimentswhichhighlightthepracticaladvantagesofourapproach.1IntroductionFunctionallogiclanguagescombinetheoperationalprinciplesofthemostimportantdeclarativeprogrammingparadigms,namelyfunctionalandlogicprogramming.Ecientdemand-drivenfunc-tionalcomputationsareamalgamatedwiththeexibleuseoflogicalvariablesprovidingforfunctioninversionandsearchforsolutions.Theoperationalsemanticsofsuchlanguagesisusuallybasedonnarrowing,ageneralizationoftermrewritingwhichcombinesreductionandvariableinstantiation.Anarrowingstepinstantiatesvariablesofanexpressionandappliesareductionsteptoaredexoftheinstantiatedexpression.Theinstantiationofvariablesisusuallycomputedbyunifyingasubtermoftheentireexpressionwiththeleft-handsideofsomerule.Example1.Considerthefollowingruleswhichdenetheless-or-equalpredicate\6onnaturalnumberswhicharerepresentedbytermsbuiltfrom0ands(notethatvariablenamesalwaysstartwithanuppercaseletter):06N!trues(M)60!falses(M)6s(N)!M6NThegoals(X)6Ycanbesolved(i.e.,reducedtotrue)byinstantiatingYtos(Y1)toapplythethirdrulefollowedbytheinstantiationofXto0toapplytherstrule:s(X)6Y;fY7!s(Y1)gX6Y1;fX7!0gtrueNarrowingprovidescompletenessinthesenseoflogicprogramming(computationofallsolutions)aswellasfunctionalprogramming(computationofvalues).Sincesimplenarrowingcanhaveahugesearchspace,greateorthasbeenmadetodevelopsophisticatednarrowingstrategieswithoutlosing?ThisworkhasbeenpartiallysupportedbyCICYTTIC98-0445-C03-01,byAccionIntegradahispano{alemanaHA1997-0073,andbytheGermanResearchCouncil(DFG)undergrantHa2457/1-1.completeness(see[25]forasurvey).Toavoidunnecessarycomputationsandtoprovidecomputationswithinnitedatastructuresaswellasademand-drivengenerationofthesearchspace,themostrecentworkhasadvocatedlazynarrowingstrategies(e.g.,[10,22,40,44]).Needednarrowing[10]isbasedontheideaofevaluatingonlysubtermswhichareneededinordertocomputearesult.Forinstance,inatermliket16t2,itisalwaysnecessarytoevaluatet1(tosomeheadnormalform)sinceallthreerulesinExample1haveanon-variablerstargument.Ontheotherhand,theevaluationoft2isonlyneededift1isoftheforms(2).Thus,ift1isafreevariable,needednarrowinginstantiatesittoaconstructor,here0ors(2).Dependingonthisinstantiation,eithertherstruleisappliedorthesecondargumentt2isevaluated.Needednarrowingiscurrentlythebestnarrowingstrategyforrst-orderfunctionallogicprogramsduetoitsoptimalitypropertiesw.r.t.thelengthofderivationsandthenumberofcomputedsolutions[10]anditcanbeecientlyimplementedbypatternmatchingandunication(e.g.,[26,40]).Moreover,ithasrecentlybeenextendedtohigher-orderfunctionsand-termsasdatastructuresandprovedoptimalw.r.t.independenceofcomputedsolutions[29].Partialevaluation(PE)isasemantics-preservingperformanceoptimizationtechniqueforcom-puterprogramswhichconsistsofthespecializationoftheprogramw.r.t.partsofitsinput.PEhasbeenwidelyappliedintheeldsoftermrewritingsystems[13{15,20,35,43],functionalpro-gramming[17,32],andlogicprogramming[21,39].Althoughtheobjectivesaresimilar,thegeneralmethodsareoftendierentduetothedistinctunderlyingmodelsandthedierentperspectives(see[5]foradetailedcomparison).Thisseparationhasthenegativeconsequenceofduplicatedworksincedevelopmentsarenotsharedandmanysimilaritiesareoverlooked.Aunied(narrowing-based)treatmentcanbringthedierentmethodologiescloserandlaysthegroundfornewinsightsinallthreeelds[5,6,23,46,48].Toperformreductionsatspecializationtime,apartialevaluatornormallyincludesaninterpreter[17,24].Thisimpliesthatthepowerofthetransformationishighlyinuencedbythepropertiesoftheevaluationstrategyfromtheunderlyinginterpreter.Narrowing-drivenPE[4,5]istherstgenericalgorithmforthespecializationoffunctionallogicprograms.Themethodisparametricw.r.t.thenarrowingstrategywhichisusedfortheautomaticconstructionofthesearchtrees.Themethodisformalizedwithinthetheoreticalframeworkestablishedin[39]forthepartialevaluationoflogicprograms(alsoknownaspartialdeduction),althoughanumberofconceptshavebeengeneralizedto