Pure type systems in rewriting logic Specifying ty

PureTypeSystemsinRewritingLogic:SpecifyingTypedHigher-OrderLanguagesinaFirst-OrderLogicalFrameworkMark-OliverStehr?Jos´eMeseguerUniversit¨atHamburgFachbereichInformatik-TGI22527Hamburg,[e-mail]Urbana-ChampaignComputerScienceDepartmentUrbana,IL61801,[e-mail]aspectsofrewritinglogicasalogi-calframeworkaretestedandillustratedindetailbyrepresentingpuretypesystemsasobjectlogics.Moreprecisely,weapplymembershipequationallogic,theequationalsublogicofrewritinglogic,tospecifypuretypesys-temsastheycanbefoundintheliteratureandalsoanewvariantofpuretypesystemswithexplicitnamesthatsolvestheproblemswithclosureun-derα-conversioninaverysatisfactoryway.Furthermore,weuserewritinglogicitselftogiveaformaloperationaldescriptionoftypechecking,thatdirectlyservesasanefficienttypecheckingalgorithm.Theworkreportedhereispartofamoreambitiousprojectconcernedwiththedevelopmentoftheopencalculusofconstructions,anequationalextensionofthecal-culusofconstructionsthatincorporatesrewritinglogicasacomputationalsublanguage.Thispaperisadetailedstudyontheeaseandnaturalnesswithwhichafamilyofhigher-orderformalsystems,namelypuretypesystems(PTSs)[6,50],canberep-resentedinthefirst-orderlogicalframeworkofrewritinglogic[36].PTSsgeneralizetheλ-cube[1],whichalreadycontainsimportantcalculilikeλ→[12],thesystemsF[23,43]andFω[23],asystemλPclosetothelogicalframeworkLF[24],andtheircombination,thecalculusofconstructionsCC[16].PTSsareconsideredtobeofkeyimportance,sincetheirgeneralityandsimplicitymakesthemanidealbasisforrepresentinghigher-orderlogics,eitherviathepropositions-as-typesinterpretation[21],orviatheiruseasahigher-orderlogicalframeworkinthespiritofLF[24,20]orIsabelle[39].Exploitingthefactthatrewritinglogic(RWL)anditsmembershipequationalsublogic(MEL)[10]haveinitialandfreemodels,wecandefinetherepresentationofPTSsasaparameterizedtheoryintheframeworklogic;thatis,wedefineinasinglepara-metricwayalltherepresentationsfortheinfinitefamilyofPTSs.Furthermore,therepresentationalversatilityofRWL,andofMEL,arealsoexercisedbyconsideringfourdifferentrepresentationsofPTSsatdifferentlevelsofabstraction,fromamoreabstracttextbookversioninwhichtermsareidentifieduptoα-conversion,toamoreconcreteversionwithacalculusofnamesandexplicitsubstitutions,andwithatypecheckinginferencesystemthatcaninfactbeusedasareasonablyefficient?CurrentlyvisitingUniversityofIllinoisatUrbana-Champaign,ComputerScienceDe-partmentUrbana,IL61801,USA,e-mail:[e-mail]yexecutingtherepresentationintheMaudelanguage[13,14].Thiscasestudycomplementsearlierwork[31,32],showingthatrewritinglogichasgoodpropertiesasalogicalframeworktorepresentawiderangeoflogics,includinglinearlogic,Hornlogicwithequality,first-orderlogic,modallogics,sequent-basedpresentationsoflogics,andsoon.Inparticular,representationsfortheλ-calculus,andforbindersandquantifiershavealreadybeenstudiedin[32],butthisisthefirstsystematicstudyontherepresentationoftypedhigher-ordersystems.Onepropertysharedbyalltheaboverepresentations,includingallthosediscussedinthispaper,isthatwhatmightbecalledtherepresentationaldistancebetweenthelogicbeingformalizedanditsrewritinglogicrepresentationisvirtuallyzero.Thatis,boththesyntaxandtheinferencesystemoftheobjectlogicaredirectlyandfaithfullymirroredbytherepresentation.Thisisanimportantadvantagebothintermsofunderstandabilityoftherepresentations,andinmakingtheuseofencodinganddecodingfunctionsunnecessaryinaso-calledadequacyproof.Besidesthedirectnessandnaturalnesswithwhichlogicscanberepresentedinaframeworklogic,anotherimportantqualityofalogicalframeworkisthescopeofitsapplicability;thatis,theclassoflogicsforwhichfaithfulrepresentationspre-servingrelevantstructurecanbedefined.Typically,wewantrepresentationsthatbothpreserveandreflectprovability;thatis,somethingisatheoremintheoriginallogicifandonlyifitstranslationcanbeprovedintheframework’srepresentationofthelogic.Suchmappingsgounderdifferentnamesanddifferintheirgeneral-ity;inhigher-orderlogicalframeworksrepresentationsaretypicallyrequiredtobeadequatemappings[20],andinthetheoryofgenerallogicsmoreliberal,namelyconservativemappingsofentailmentsystems[35],arestudied.Inthispaper,wewefurthergeneralizeconservativemappingstothenotionofasoundandcompletefullcorrespondenceofsentencesbetweentwoentailmentsystems.Infact,alltherepresentationsofPTSsthatweconsiderarecorrespondencesofthiskind.SoundandcompletefullcorrespondencesaresystematicallyusednotonlytostatethecorrectnessoftherepresentationsofPTSsatdifferentlevelsofabstraction,butalsotorelatethosedifferentlevelsofabstraction,showingthatthemoreconcreterepresentationscorrectlyimplementtheirmoreabstractcounterparts.AsystematicwayofcomparingthescopesoftwologicalframeworksFandGistoexhibitasoundandcompletefullcorrespondenceF;G,representingFinG.Inviewofthisquitegeneralconcept,itisimportanttoaddthattherepresentationaldistance,whichweinformallydefineasthecomplexityofthiscorrespondence,isanimportantmeasureofthequali