Light types for polynomial time computation in lam

arXiv:cs/0402059v2[cs.LO]11May2004LightTypesforPolynomialTimeComputationinLambda-Calculus∗PatrickBaillotLaboratoired’InformatiquedeParis-Nord/CNRSUniversit´eParis-Nord,[e-mail]InstituteofInformaticsTokyo,[e-mail]ypesystemforlambda-calculusen-suringthatwell-typedprogramscanbeexecutedinpolyno-mialtime:Duallightaffinelogic(DLAL).DLALhasasim-pletypelanguagewithalinearandanintuitionistictypearrow,andonemodality.ItcorrespondstoafragmentofLightaffinelogic(LAL).WeshowthatcontrarilytoLAL,DLALensuresgoodpropertiesonlambda-terms:subjectreductionissatisfiedandawell-typedtermadmitsapoly-nomialboundonthereductionbyanystrategy.FinallyweestablishthatasLAL,DLALallowstorepresentallpoly-timefunctions.1IntroductionFunctionallanguageslikeMLassisttheprogrammerwithpreventionofsucherrorsasrun-timetypeerrors,thankstoautomatictypeinference.Onecouldwishtoex-tendthissettingtoverificationofquantitativeproperties,suchastimeorspacecomplexitybounds(seeforinstance[18]).Wethinkthatprogressesonsuchissuescanfol-lowfromadvancesinthetopicofImplicitComputationalComplexity,thefieldthatstudiescalculiandlanguageswithintrinsiccomplexityproperties.Inparticularsomelinesofresearchhaveexploredrecursion-basedapproaches([20,7,17,8,16])andapproachesbasedonlinearlogictocontrolthecomplexityofprograms([14,19]).HereweareinterestedinLightaffinelogic(LAL)([2,14]),alogicalsystemdesignedfromLinearlogicandwhichcharacterizespolynomialtimecomputation.BytheCurry-Howardcorrespondenceproofsinthislogiccanbeusedasprograms.Someniceaspectsofthissystemwithrespecttootherapproachesarethefactsthatitincludeshigher-ordertypesaswellaspolymorphism.Moreoveritnaturallyextendstoaconsistentnaivesettheory,inwhich∗WorkpartiallysupportedbyprojectGEOCALACINouvellesin-terfacesdesmath´ematiques,projectCRISSACIS´ecurit´einformatique(France)andGrant-in-AidforScientificResearch,MEXT,Japan.onecanreasonaboutpolynomialtimeconcepts.Inparticu-lartheprovablytotalfunctionsofthatsettheoryareexactlythepolynomialtimefunctions([14,26]).HoweverthesyntaxofLALisquitedelicate,inpartic-ularbecauseithastwomodalities.Sometermlanguageshavebeenproposed(inparticularin[25])butprogrammingisingeneraldifficult.Wethinkabettergraspwouldbegivenonthissystemifonecoulduseaslanguageplainlambda-calculusandtheninasecondphasehaveanauto-matic(orsemi-automatic)LALtypeinferenceperformed.Incaseofsuccessawell-typedprogramwouldhavetheguaranteethatitcanbeexecutedinpolynomialtime.Thisapproachhasbeenexaminedin[3,4].Inparticularithasbeenshownin[4]thattypeinferenceinpropositionalLALisdecidable.Howeversomeproblemsremain:•First,toexecutethewell-typedprogramwiththeex-pectedpolynomialboundthelambda-termisnotsuf-ficient.Onehastousethetypederivationandextractalightlambdaterm(introducedin[25])oraproof-net([2])thatcanbeexecutedwiththecorrectbound.Inparticularthismeansthatifweuseordinaryabstractmachinesfortheevaluationwedonothaveanyguar-anteeontheexecutiontime.•Second,eveniftypeinferenceisdecidablewedonothaveforthemomentanyefficientprocedure.Thediffi-cultyactuallycomesfromtwopoints:thetypederiva-tionmightneedtospecifysomesharingofsubterm;moreoverthelanguageoftypesislarge(becausetherearetwomodalities)andthisresultsinanimportantsearchspacetoexplore.Totrytoovercometheseproblemsweproposehereanewtypesystem,thatwecallDuallightaffinelogic(DLAL).ItcorrespondstoasimplefragmentofLAL.Itreliesontheideaofreplacingthe!modalitybytwonotionsofarrows:alinearoneandanintuitionisticone.ThisisinthelineoftheworksofBarberandPlotkin(Dualintuitionisticlinearlogic,[6])andBenton([9]).DLALthenoffersthefollow-ingadvantagesoverLALasatypesystem:1•Itslanguageoftypesis’smaller’,inthesensethatitcorrespondstoastrictsubsetofLALtypes.•DLALkeepsthesamepropertiesasLAL(P-completenessandpolynomialboundonexecution)butensuresthecomplexityboundonthelambda-termit-self:ifatermistypableonecanextracttheboundfromthederivation,thenforgetaboutthetypeandexe-cutethetermusinganystrategy(andanyabstractma-chine),withtheguaranteethatthereductionwillter-minatewithinthebound.ThismeansthatDLALof-fersasystemwheretheprogrampartandthecomplex-ityspecificationpartarereallyseparate.Theprogrampartcorrespondstothelambda-termandthecomplex-ityspecificationtothetype.•Wethinktypeinferenceshouldbecomeeasier,thoughthisquestionstillhastobeexplored.IndeedDLALof-fersthefollowingadvantages:firstthereisnosharinginDLALderivations;second,alargepartofthediffi-cultyofLALtypeinferencehastodowiththefactthatthetypescanuseanysequenceofthetwomodalities!,§,thatistosaywordsoverabinaryalphabet.Forthisreasonthetypeinferenceprocedureof[4]usedwordsconstraints,whicharehardtosolve.Bycon-trastElementaryaffinelogic(EAL)(correspondingtoelementarycomplexity)hasonlyonemodality!anditstypeinferencecanbeperformedusinglinearcon-straints,thatistosayintegerprogramming.Theprob-lemofEALtypeinferencehasbeenshowndecidableandstudiedindetailbyCoppolaetal.(see[11,12]),startingfrommotivationsinoptimalreduction.WebelieveDLALshouldbeeasiertounderstandthanLALandcouldmakethislightlogicapproachaccessibletoal