Category-based modularisation for equational logic

Category-basedModularisationforEquationalLogicProgrammingRazvanDiaconescuProgrammingResearchGroup,UniversityofOxfordAbstract:Althoughmodularisationisbasictomoderncomputing,ithasbeenlittlestudiedforlogic-basedprogramming.Wetreatmodularisationforequationallogicprogrammingusingtheinstitutionofcategory-basedequationallogicinthreedierentways:(1)toprovideagenericsatisfactionconditionforequationallogics;(2)togiveacategory-basedsemanticsforqueriesandtheirsolutions;and(3)asanabstractdenitionofcompilationfromone(equational)logicprogramminglanguagetoanother.Regarding(2),westudysoundnessandcompletenessforequationallogicprogram-mingqueriesandtheirsolutions.Thiscanbeunderstoodasordinarysoundnessandcompletenessinasuitable\non-logicalinstitution.Soundnessholdsforallmoduleimports,butcompletenessonlyholdsforconservativemoduleimports.Category-basedequationalsignaturesareseenasmodules,andmorphismsofsuchsignaturesasmoduleimports.Regarding(3),completenesscorrespondstocompilercorrectness.Theresultsofthisresearchappliestolanguagesbasedonawideclassofequa-tionallogicsystems,includingHornclauselogic,withorwithoutequality;allvariantsoforderandmanysortedequationallogic,includingworkingmoduloasetofaxioms;constraintlogicprogrammingoverarbitraryuser-deneddatatypes;andanycom-binationoftheabove.Mostimportantly,duetotheabstractionlevel,thisresearchgivesthepossibilitytohavesemanticsandtostudymodularisationforequationallogicprogrammingdevelopedovernon-conventionalstructures.Contents1Introduction21.1Modularisation:::::::::::::::::::::::::::::::::21.1.1Somehistory::::::::::::::::::::::::::::::31.2EquationalLogicProgramming::::::::::::::::::::::::31.3Category-basedEquationalLogic:::::::::::::::::::::::41.3.1Beyondconventional\abstractmodeltheory::::::::::::51.4TheInstitutionofCategory-basedEquationalLogic:::::::::::::52Preliminaries62.1Limitsandcolimits:::::::::::::::::::::::::::::::62.22-categories:::::::::::::::::::::::::::::::::::72.3CategoricalRelations::::::::::::::::::::::::::::::8Currentaddress:InstituteofMathematicsoftheRomanianAcademy,POBox1-76470700Bucharest,Romania;[e-mail]13InstitutionsandModularisation83.1ParametricModulesandViews::::::::::::::::::::::::94Category-basedEquationalLogic114.1ModelsandDomains::::::::::::::::::::::::::::::124.2Examples::::::::::::::::::::::::::::::::::::124.2.1ManySortedAlgebra::::::::::::::::::::::::::124.2.2OrderSortedAlgebra::::::::::::::::::::::::::134.2.3HornClauseLogic:::::::::::::::::::::::::::134.2.4EquationalLogicModuloAxioms:::::::::::::::::::144.2.5ConstraintLogic::::::::::::::::::::::::::::144.2.6SummaryofExamples:::::::::::::::::::::::::154.3Equations,QueriesandSatisfaction::::::::::::::::::::::155TheInstitutionofCategory-basedEquationalLogic185.1Many-SortedInstitutions::::::::::::::::::::::::::::195.2SentenceTranslationsalongMorphismsofCategory-basedEquationalSig-natures::::::::::::::::::::::::::::::::::::::205.2.1Kleislitranslations:::::::::::::::::::::::::::215.3TheSatisfactionCondition:::::::::::::::::::::::::::256Queries,SolutionsandModularisation266.1TheInstitutionofQueriesandSubstitutions:::::::::::::::::266.2SoundnessandCompletenessforModuleImports::::::::::::::287CompilationbetweenELPlanguages308ConclusionsandFutureWork311IntroductionTheworkreportedinthispaperispartoftheresearchprojectoncategory-basedsemanticsforequationalandconstraintlogicprogrammingcarriedoutinOxfordinconnectiontothedevelopmentandimplementationofthelanguageEqlog(see[13]).1.1ModularisationApromisingapproachtodevelopinglargeandcomplexsystems(whichmaybesoftware,hardware,orboth)istostartfromadescriptionofthesystemasaninterconnectionofsomespecicationmodules.Thispermitsthevericationofmanypropertiestobecarriedoutatthelevelofdesignratherthancode,andthusshouldimprovereliability.Withsuitablemechanicalsupport,itmightalsoimprovetheeciencyofthedevelopmentprocess.Inaddition,itpromotesreuse,becausesomemodulesmaybetakendirectlyfromalibrary,orelsemaybemodicationsoflibrarymodules.Forthisreason,manymodernprogrammingandspecicationlanguagessupportsomeformofmodularisation,andmostmathematicalresultsaboutmoduleshaveappearedinthecontextofformalsoftwareengineering,particularlyspecicationlanguages.21.1.1SomehistoryTheearliestworkonsoftwaremoduleswithwhichwearefamiliarisbyParnas[36,37,38].Programmodulesdierfromearlierprogramstructuringmechanismssuchassubroutines,proceduresandblocks,inthattheymayincludeanumberofprocedureanddatadenitions,maybeparameterized,mayimportothermodules,andmayhidecertainelements.Amajormotivationformodulesinthissenseistofacilitatethemodicationofsoftware,bylocalizingtherepresentationofdataandtheoperationsthatdependuponit;thisiscalledinformationhiding.Suchmodulessupportsoftwarereusebecausetheycanbespecied,veried,andcompiledseparately.Notethatthisnotionofmoduleisessentiallysyntactic:itconcernstextsthatdescribesystems.TheearliestworkthatweknowonspecicationmodulesisbyGoguenandBurstall,fortheirspecicationlanguageClear[5,6],thesemanticsofwhichisbasedoninstitutions.Thisapproachtomoduleshasbeenappli