搜索
ISSN0249-6399apport derecherche INSTITUTNATIONALDERECHERCHEENINFORMATIQUEETAUTOMATIQUEOnComputationalInterpretationsoftheModalLogicS4IIIb.Con uence,Terminationofthe evQH-Calculus.JeanGoubault-LarrecqN 3164Mai1997TH EME2OnComputationalInterpretationsoftheModalLogicS4IIIb.Con uence,Terminationofthe evQH-Calculus.JeanGoubault-Larrecq Th eme2|G enielogicieletcalculsymboliqueProjetCoqRapportderecherchen 3164|Mai1997|48pagesAbstract:Alanguageofprooftermsforminimallogicisthe -calculus,wherecut-eliminationisencodedas -reduction.WeexaminecorrespondinglanguagesfortheminimalversionofthemodallogicS4,withnotionsofreductionthatencodescut-eliminationforthecorrespondingsequentsystem.Itturnsoutthatanaturalinterpretationofthelatterconstructionsisa -calculusextendedbyanidealizedversionofLisp’sevalandquoteconstructs.InthisPartIIIb,wecompletetheresultsofPartIIIa.Weshowthatthetyped evQH-calculusiscon uent.Itfollowsthatthetyped evQH-calculusisaconservativeextensionofthetyped S4H-calculus.Wealsoprovethatthetyped evQH-calculusisweaklyterminating.Someproblemsremainopen.Inparticular,westilldon’tknowwhetherthetyped evQ-calculusterminatesweakly,orwhethertheuntyped evQ-calculusiscon uent.Finally,wecorrectafewmistakesandinaccuraciesthatoccurredinpreviouspartsofthiswork.Key-words:modallogic,S4, -calculus,explicitsubstitutions,termination,con uence, -calculus,simpletypes(R esum e:tsvp) Jean.Goubault@inria.frUnit ederechercheINRIARocquencourtDomainedeVoluceau,Rocquencourt,BP105,78153LECHESNAYCedex(France)T el ephone:(331)39635511{T el ecopie:(331)39635330 Aproposdesinterpr etationscalculatoiresdelalogiquemodaleS4IIIb.Con uence,terminaisondu evQH-calcul.R esum e:Unlangagedetermesdepreuvepourlalogiqueminimaleestle -calcul,o ul’ eliminationdescoupuresestcod eeparla -reduction.Nousexaminonsdeslangagescor-respondantspourlaversionminimaledelalogiquemodaleS4,avecdesnotionsder eductionsquicodentl’ eliminationdescoupuresdanslesyst emedes equentscorrespondant.Ils’av erequ’uneinterpr etationnaturelledecesconstructionsestun -calcul etenduavecuneversionid ealis eedesconstructionsevaletquotedeLisp.DanscettepartieIIIb,nouscompl etonslesr esultatsdelapartieIIIa.Nousmontronsquele evQH-calcultyp eestcon uent.Ils’ensuitquele evQH-calcultyp eestuneextensionconservativedu S4H-calcultyp e.Nousprouvonsaussiquele evQH-calculestfaiblementterminant.Ilrestequelquesprobl emesouverts.Enparticulier,nousnesavonstoujourspassile evQ-calcultyp eterminefaiblement,ousile evQ-calculnontyp eestcon uent.Finalement,nouscorrigeonsquelqueserreursetinexactitudesdespartiespr ec edentesdecetravail.Mots-cl e:logiquemodale,S4, -calcul,substitutionsexplicites,terminaison,con uence, -calcul,typessimplesPlanWestartbycorrectingafewmistakesorinaccuraciesofpreviouspartsinSection1,thenestablishthatthetyped evQH-calculusiscon uentinSection2|andalthoughtheuntypedcalculusisnotcon uent,itiscon uentinthetypedcaseeveninthepreviousof xedpointoperators|,andthatthetyped evQH-calculusterminatesweaklyinSection3.Weexaminethecaseofthetyped evQ-calculus,andexplainwhythetechniqueswehaveusedarenotabletoshowthatitterminatesweakly:thedi cultyismainlyduetothecomplicatedformof(typed) -normalterms.Forde nitionsandpreviously-knownresults,seethereports[GL96a],hereafterdenotedasPartI,[GL96b](PartII)and[GL96c](PartIIIa).1Corrigendum1.1TerminationofTyped HTerminationofthetypedversion HwasprovedinPartIIIabyreducingittoavariantoftyped -calculuswith rst-orderoperatorsenjoyingspeci creductionrules,the -calculus.ThelatterwasthenprovedterminatingbyusingJouannaudandRubio’shigher-orderrecursivepathordering(horpo),asde nedinthepreliminarypaper[JR96a].Unfortunately,thisproposalwaswrong,inthesensethatitmanagestoproveterminatingevennon-terminatingrewritesystems.(Forinstance,theuntyped -calculus:de netheScotttranslationfromuntyped -termstosimply-typedonesby:( x u) =f( x:o u ),(uv) =g(u )v ,wherefmapstermsoftypeo!ototermsoftypeo,andgmapstermsoftypeototypeo!o,andobeythereductionruleg(f(u))!u.)Thecorrectedversionofthehorpoisinthe nalpaper[JR96b].Unfortunately,theresultpresentedthereistooweakforourpurposes,eventhoughweactuallyonlyneedreductionson -long -normalforms,notthefullreductionsofthetyped -calculus.Wethereforepresentadirectproofoftheterminationofthetyped -calculus,basedonreducibilityarguments alaTait-Girard[GLT89](calledstrongcomputabilityin[HS88]).Thede nitionofreducibilityandofneutralityisstandard,astheproperties(CR1),(CR2)and(CR3)andtheirproofs.Theonlydi cultyliesintheproofofthefactthatalltermsarereducible.Weadoptthepresentationof[GLT89],Chapter6.Sincethenotionsofnegativeandpositivetypesdoesnotmatter,wedropthe+and superscriptson -typesinmostcases.De nition1.1Wede nethesetsRED ofreducible -termsoftype byinductiononthe -type by: REDoisthesetofstronglynormalizing -termsoftypeo; RED 1 2=fs: 1 2j 1s2RED 1; 2s2RED 2g; RED 1! 2=fs: 1! 2j8t2RED 1 st2RED 2g.De nition1.2Wesaythata -termisneutralifandonlyifitisneitheralambda-abstraction x snorapairhs;ti.Theconditionsofreducibilityare:(CR1)Ifs2RED ,thensisstronglynormalizing.(