Under consideration for publication in Math. Struc

UnderconsiderationforpublicationinMath.Struct.inComp.ScienceCategory-basedConstraintLogicR˘azvanDiaconescu†JapanAdvancedInstituteforScienceandTechnologyReceived6September1999Thisresearchexploitstheviewofconstraintprogrammingascomputationinalogicalsystem,namelyconstraintlogic.Thebasicingredientsofconstraintlogicare:constraintmodelsforthesemantics(theyformacomma-categoryoverafixedmodelof“built-ins”),generalizedpolynomialsintherˆoleofbasicsyntacticingredient,andaconstraintsatisfactionrelationbetweensemanticsandsyntax.Category-basedconstraintlogicmeansthedevelopmentofthelogicisabstractcategoricalratherthanconcretesettheoretical.Weshowthat(category-based)constraintlogicisaninstitution,andweinternalizethestudyofconstraintlogictotheabstractframeworkofcategory-basedequationallogic,thusopeningthedoorforconsideringconstraintlogicprogrammingovernon-standardstructures(suchasCPO’s,topologies,graphs,categories,etc.).Byembeddingcategory-basedconstraintlogicintocategory-basedequationallogic,weintegratetheconstraintlogicprogrammingparadigminto(category-based)equationallogicprogramming.Resultsincludecompletenessofconstraintlogicdeduction,anovelHerbrandtheoremforconstraintlogicprogrammingcharacterizingHerbrandmodelsasinitialmodelsinconstraintlogic,andlogicalfoundationsformodularcombinationofconstraintsolversbasedonamalgamatedsumsofHerbrandmodelsintheconstraintlogicinstitution.1.Introduction1.1.ExtensibleConstraintLogicProgrammingConstraintlogicprogramminghasbeenrecentlyemergingasapowerfulprogrammingparadigmandithasattractedmuchresearchinterestoverthepastdecade.Constraintlogicprogrammingmergestwodeclarativeprogrammingparadigms:constraintsolvingandlogicprogramming.MathematicalProgramming,SymbolicComputation,ArtificialIntelligence,ProgramVerifica-tionandComputationalGeometryareexamplesofapplicationareasforconstraintsolving.Con-straintsolvingtechniqueshavebeenincorporatedinmanyprogrammingsystems;CLP(JaffarandLassez,1987),PrologIII(Colmerauer,),andMathematicaarethebestknownexamples.Thecomputationaldomainsincludelineararithmetic,booleanalgebra,lists,finitesets.Conventionallogicprogramming(i.e.,Prolog)canberegardedasconstraintsolvingovertermmodels(i.e.,Herbranduniverses).Inthisway,constraintlogicprogrammingcanberegardedasageneraliza-tionoflogicprogrammingthatreplacesunificationwithconstraintsolvingovercomputational†OnleavefromtheInstituteofMathematicsoftheRomanianAcademy,POBox1-764,Bucharest70700,ROMANIA.R˘azvanDiaconescu2domains.Ingeneral,theactualconstraintlogicprogrammingsystemsallowconstraintsolvingforafixedcollectionofdatatypesorcomputationaldomains.1Constraintlogicprogrammingallowingconstraintsoveranydatatype(possiblygivenwithloosesemantics)willbecalledex-tensible(abbreviatedECLP).Thispaperpresentsan(abstract)modeltheoreticsemanticsforECLP,withoutdirectlyad-dressingthecomputationalaspect.Thisisarathernovelapproachontheareaofconstraintswherealmostalleffortshavebeendevotedtocomputationalandoperationalissues;itisim-portantthereaderunderstandsthemodel-theoreticandfoundationalorientationofthispaper.However,weplantograduallydevelopthecomputationalsidebasedonthesefoundationsasfurtherresearch(Section7.2sketchessomeofthedirectionsofsuchfurtherresearch).Somecomputationalaspectsofthistheorycanalreadybefoundin(Diaconescu,1996c).Thissemanticsis—logical,—abstract,and—institution-independent.ThefirstaspectmeansthatthereisanunderlyinglogicinwhichallmainfeaturesofECLPcanberigorouslyexplained.Thesecondmeansthatwedevelopthemainconceptsandresultsatthe“highestappropriatelevelofabstraction”,leavingoutunnecessarydetailswhilststilladdressingthesubstanceofECLP.Finally,“institution-independent”addressesbothformeraspectswithinthetheoryofinstitutions(GoguenandBurstall,1992),whichrepresentsnowthemodernlevelofalgebraicspecification.ThismeansthatoursemanticstoECLPcanbeinternalizedtovariousin-stitutions(i.e.,logics),thusprovidinganuniformwayforintegratingECLPintovarioussystemswithrigorouslogicalsemantics,butalsodevelopingECLPovernovelstructures.Themainresultsreportedinthispaperare:—defineagenericlogicunderlyingECLP(calledconstraintlogic),—embeddingconstraintlogicintothecategory-basedequationallogicof(Diaconescu,1994;Diaconescu,1995;GoguenandDiaconescu,1995;Diaconescu,1996b),—agenericHerbrandTheoremforconstraintlogicsprovidingfoundationsfortheconceptofconstraintsolvinginECLP,—agenericinstitutionforECLPprovidingfoundationsformodularECLPandforconnectingconstraintlogictoothercomputinglogicsviainstitutionmappings(morphisms),and—logicalfoundationsformodularcombinationofconstraintsolversviaamalgamationofHer-brandmodelsinconstraintlogic.Theembeddingofconstraintlogicsintocategory-basedequationallogicconstitutetheengineformostofthemainresultsinthispaper,butalsoapotentialsourceforfurtherdevelopments.Duetothisembedding,theconstraintlogicinstitutionhaspropertiesclosetoalgebraicspec-ificationinstitutions;alsoweareabletoproveaHerbrandTheoremforECLPbyusingthe1Fromamodel-theoreticperspective,acomputationaldomainmaybeabstractedtoamodel(notnecessarilythestan-dardone)ofacertaindatatypesp