On computational interpretations of the modal logi

OnComputationalInterpretationsoftheModalLogicS4I.CutEliminationJeanGoubault-LarrecqInstitutfurLogik,KomplexitatundDeduktionssystemeUniversitatKarlsruhe,AmFasanengarten5,[e-mail],[e-mail]29,1996AbstractAlanguageofconstructionsforminimallogicisthe-calculus,wherecut-eliminationisencodedas-reduction.WeexaminecorrespondinglanguagesfortheminimalversionofthemodallogicS4,withnotionsofreductionthatencodescut-eliminationforthecorrespondingsequentsystem.Itturnsoutthatanaturalinterpretationofthelatterconstructionsisa-calculusextendedbyanidealizedversionofLisp’sevalandquoteconstructs.Inthisrstpart,weanalyzehowcut-eliminationworksinthestandardsequentsystemforminimalS4,andwhereproblemsarise.BiermanandDePaiva’sproposalisanaturallanguageofconstructionsforthislogic,buttheircalculuslacksafewrulesthatareessentialtoeliminateallcuts.TheS4-calculus,namelyBiermanandDePaiva’sproposalextendedwithallneededrules,isconuent.Thereisapolynomial-timealgorithmtocomputeprincipaltypingsofgiventerms,oranswerthatthegiventermsarenottypable.ThetypedS4-calculusterminates,andnormalformsareexactlyconstructionsforcut-freeproofs.Finally,modulosomenotionofequivalence,thereisanaturalCurry-HowardstyleisomorphismbetweentypedS4-termsandnaturaldeductionproofsinminimalS4.However,theS4-calculushasanon-operationalavor,inthattheextrarulesincludeexplicitgarbagecollection,contractionandexchangerules.WeshallproposeanotherlanguageofconstructionstorepairthisinPartII.1GeneralIntroductionThispaperpresentsananswertotwodualquestions.Therstis:whatlanguagedoweneedtogetaproofs-as-programs,formulas-as-typescorrespondencewiththemodallogicS4?AsalreadynotedbyDaviesandPfenning[DP95],theanswerisakindof-calculusaugmentedwithpolishedversionsofLisp’sevalandquoteprimitives.Ourinitialmotivationforansweringthisquestionwasintellectualcuriosity:ifintuitionisticandminimallogicshaveit[How80],andnowclassicallogic,too[Gri90],whynotsomemodallogics?Moreover,thecurrentinterestinlinearlogic,andthefactthattherulesofsequentsystemsforlinearlogiclooklikethoseforS4alot,haverecentlystimulatedsomeresearchers[BdP95]intoexploringfunctionalinterpretationsforS4,inthehopeofunderstandinglinearlogicbetter.Thesecondquestionis:whatkindoftypesystemcanweimposeonLisp’sevalandquoteprimitivesthatwouldmakethemusableinanML-like,stronglytypedandpolymorphicfunctionallanguage?Oralternatively,howcanwemaketype-safeversionsoftheseprimitivesinawaythatwouldbemostexpressive?WeshowthatagoodanswerisgivenbyaugmentingML’stypesystem,whichisbasicallyintuitionisticlogic,totheintuitionisticversionofthelogicS4.ResearchpartiallyfundedbytheHCMgrant7532.7-06fromtheEuropeanUnion.ThisworkstartedinJuly1994whileIwasatBull,andwasnishedwhileIwasattheuniversityofKarlsruhe.yOnleavefromBullCorporateResearchCenter,rueJeanJaures,F-78340LesClayessousBois.1Thepaperhasfourparts.PartIisagentleintroductiontothebasicnotionsthatweshallneedlateron:whatevalandquoteare,whatthemodallogicS4is,bothfromthesemanticandtheproof-theoreticpointofview,andwhatthenotionoffunctionalinterpretationofproofsalaCurryandHowardis.Wethenanalyzehowcutscanbeeliminatedfromsequentproofs,i.e.whatthereductionrulesforevalandquoteshouldbefrompurelylogicalprinciples.WeshowthataslightextensionofBiermanandDePaiva’sproposal[BdP95],theS4-calculus,istherightlanguagetorepresentproofsandprooftransformations.However,itisendowedwithverynon-operationalreductionrules,whichmakeitapoorchoiceforaprogramminglanguage.Infact,itdoesnotexplainmuchhowevaluationandquotingworks.PartIIpresentsanothersolution,theevQ-calculus.Weshowhowwearenaturallyledtothislanguage,whichismuchmorecomplicatedthanS4butalsomuchmoreoperational.Infact,itincludesaninnitetowerofinterpreters,muchasinLisp,encodedby-calculi.Thislanguagerevealshowevaluationandquotingreallywork.Interestinglyenough,suchimplementationdetailssuchasstacksarisenaturallyfrompurelylogicalprinciples.TheevQ-calculuscanalsobeseenasanextensionoftheS4-calculus,inthatthereisatranslationfromthelattertotheformerthatpreservesconvertibilityandreductibility.InPartIII,weprovethatthetypedevQ-calculusisconuent,andthatitisaconservativeextensionoftheS4-calculus:twotypedS4-termsareinterconvertibleifandonlyiftheirtranslationstoevQ-termsare,aswell.Thesamepropertiesholdwithbothcalculiextendedby-likerules.However,theuntypedevQ-calculuswith-likerulesisnotconuent;thestatusoftheuntypedevQ-calculuswithoutthe-likerulesisunknown,althoughweconjecturethatitisconuent.InPartIV,weexaminetheneededextensionstoS4andevQthatwouldmakethemsuitabletointerpretproofsintheclassicalversionofS4,wheredoublenegationeliminationisallowed.Asisnowwell-known,integratingclassicalfeaturesallowsonetorepresentcontroloperatorsinthelanguageofconstructions,i.e.exceptionhandling.BuildingonParigot’s-calculus,wedeneaclassicalversionofS4.However,thereseemstobenohopeofmakingitconuent.Ontheotherhand,theclassicalevQ-calculus,anextensionoftheevQ-calculuswith-likerulebasedonAudebaud’senv,seemstohavenosuchproblem.1.1P