Under consideration for publication in Theory and

arXiv:cs/0601018v1[cs.LO]6Jan2006UnderconsiderationforpublicationinTheoryandPracticeofLogicProgramming1AcomparisonbetweentwologicalformalismsforrewritingMIGUELPALOMINO∗DepartamentodeSistemasInform´aticosyProgramaci´onFacultaddeInform´atica,UniversidadComplutensedeMadrid,Spain(e-mail:[e-mail])submitted12December2003;revised12April2005;accepted5January2006AbstractMeseguer’srewritinglogicandtherewritinglogicCRWLaretwowell-knownapproachestorewritingaslogicaldeductionthat,despitesomeclearsimilarities,weredesignedwithdifferentobjectives.Herewestudytherelationshipsbetweenthem,bothatasyntacticandatasemanticlevel.Eventhoughitisnotpossibletoestablishanentailmentsystemmapbetweenthem,bothcanbenaturallysimulatedineachother.Semantically,thereisnoembeddingbetweenthecorrespondinginstitutions.Alongtheway,thenotionsofentailmentandsatisfactioninMeseguer’srewritinglogicaregeneralized.WealsousethesyntacticresultstoprovereflectivepropertiesofCRWL.KEYWORDS:rewritinglogic,constructor-basedrewritinglogic,institutions1IntroductionTheaimofthispaperistostudyindetail,andtotrytoclarify,therelationshipsbetweentwowell-knownapproachestorewritingaslogicaldeduction,namely,Jos´eMeseguer’srewritinglogic(Meseguer1992),andtheconstructor-basedrewritinglogic(CRWL)developedbyMarioRodr´ıguez-Artalejo’sresearchgroupinMadrid(Gonz´alez-Morenoetal.1999).Thefirstofthesewasproposedasalogicalframeworkwhereintorepresentotherlogics,andalsoasasemanticframework,aunifiedmodelofconcurrencyforthespecificationoflanguagesandsystems.Theexperienceaccumulatedthroughoutthelastyearshascometosupportthatoriginalintention(Mart´ı-OlietandMeseguer2002b).Inparticular,ithasbeenshownthatrewritinglogicisaveryflexibleframeworkinwhichmanyotherlogics,includingfirst-orderlogic,intuitionisticlogic,linearlogic,Hornlogicwithequality,aswellasanyotherlogicwithasequentcalculus,canberepresented(Meseguer2000;Mart´ı-OlietandMeseguer2002a;VerdejoandMart´ı-Oliet2002;Thatietal.2002;Verdejo2003).Animportantfeatureoftheserepresentationsthat∗SupportedbyapostgraduatescholarshipfromtheSpanishMinistryforEducation,Culture,andSports,andbytheSpanishCICYTprojectAMEVATIC2000–0701–C02–01.ThisworkwascompletedduringastayoftheauthorattheDepartmentofComputerScienceintheUniversityofIllinoisatUrbana-Champaign.2M.Palominoshouldbestressedisthattheyareusuallyquitesimpleandnatural(inMeseguer’svocabulary,“therepresentationdistanceiszero”),sothatthemathematicalprop-ertiesofthesourcelogicsareoftenstraightforwardtoderiveintheirrewritinglogicrepresentation.Ontheotherhand,thegoaloftheconstructor-basedrewritinglogicistoserveasalogicalbasisfordeclarativeprogramminglanguagesinvolvinglazyevaluation,offeringsupport,inaddition,tonon-strictandpossiblynon-deterministicfunctions.Despitethesedifferences,thereisaclearresemblancebetweenbothlogics,namely,thefactthatlogicaldeductionisbasedonrewriting.Itseemsnatural,then,toaskabouttherelationshipsbetweendeductionintheselogicsandtoextendthequestionsoastoencompasswhetherthecorrespondingmodelsarealsorelated.AsuitableframeworkinwhichtocarryoutthisstudyisthetheoryofgenerallogicsdevelopedinMeseguer(1989).There,logicsaredescribedinaveryabstractmannerandtwoseparatedcomponentsaredistinguished:asyntacticpart,whichiscapturedbythenotionofentailmentsystem,andasemanticone,capturedbyGoguenandBurstall’sconceptofinstitution(GoguenandBurstall1992).Wewillbeginbystudyingderivabilityand,forthat,wewilltrytoassociateen-tailmentsystemstobothlogicsandtorelatethembymeansofamapofentailmentsystems.Unfortunately,itwillbeprovedthatthereisnonecorrespondingtodeduc-tioninCRWL,sowewillbeforcedtoleavethisformalframeworkandundertakemoreinformalsimulationsofthelogicsineachother.Althoughsuchsimulationsarealwayspossiblebymakinguseofsuitablelow-levelencodings,relyingontheanalogiesbetweenbothlogicsourinterestresidesinfindingnaturalandsimplesim-ulationsthatattheveryleastwouldshowthattheirexpressivepoweristhesame.Inaddition,theseresultswillbeusedtostudyreflectivepropertiesofCRWL.Afterthecomparisonatthesyntacticlevel,thenextstepisthestudyofthecorrespondingmodels.Nowwewillbeabletoassociateaninstitutiontoeachlogic,sothisstudywilltakeplacewithintheformalframeworkofthetheoryofinstitutions.Themainresultwewillobtainisthatmodelsintheselogicsbearnorelationatall.Alongtheway,wegeneralizethenotionsofderivabilityandsatisfactioninMeseguer’srewritinglogictoconditionalrewriterules,andclarifysomesubtlepointsregardingthedefinitionofmodelsinthislogic.Asimpliedbythepreviouspresentation,thispaperdoesnotconsidertheop-erationalsemanticsofthelogics,butfocusinsteadofcomparingthematamoreabstractlevelbyconsideringbothitsprovabilityandsatisfactionrelations.WerefertoworkslikeBoscoetal.(1988),wheresuchoperationalissuesrelatedtoresolutionornarrowingarepursuedinsimilarcontexts.Meseguer’srewritinglogicisparameterizedwithrespecttoanunderlyingequa-tionallogic;althoughthiscanbetypedandasgeneralasthemembershipequationallogicfromMeseguer(1998),inthispaperweconcentrateontheversionofrewrit-inglogicwhichusesunsortedandunconditionalequationallogicandwriteRLforit.Likewise