Semantics of constraint logic programs with bounde

UppsalaMaster’sThesisinComputingScience125ExamensarbeteDV31998-05-18ISSN1100-1836SemanticsofConstraintLogicProgramswithBoundedQuantiersMartinArgeniusComputingScienceDepartmentUppsalaUniversityBox311,S-75105Uppsala,[e-mail]:AndreiVoronkovExaminer:Sven-OlofNystromPassed:AbstractWesurveytheareasofConstraintprogramming,BoundedQuantiersandCollectionTypes,thenwedescribeanextensionofconstraintlogicprogrammingbyboundedquantiers.Boundedquan-tiersprovidethesupportfornitedomainconstraintprogramminginanaturalway.Wedeneseveralsemanticsforconstraintlogicprogramswithboundedquantiersandprovetheirequiva-lence.Ourresultscanbeusedtodenesemanticsforsomeexistingconstraintlogicprogramminglanguages,likecc(FD).Contents1Introduction21.1Constraintprogramming..................................21.2Boundedquantiers....................................41.3CollectiontypesinLogicProgrammingandDeductiveDatabases..........................................72Constraintlogicprogramswithboundedquantiers102.1Sortsandlists........................................102.2BoundedquantiersandCBQ-programs........................112.3Theorder-sortedpredicatecalculus............................123SemanticsofCBQ-programs133.1Model-theoreticsemantics.................................133.2Fixpointsemantics.....................................173.3Provabilitysemantics....................................193.4Thenaturalsemantics...................................204Operationalsemantics225Relatedwork271Section1IntroductionConstraintlogicprogrammingisadeclarativeextensionofHornclauselogicprogrammingwhereconstraintsandconstraintsolvingtechniquesareincorporatedinalogic-basedlanguage.AnotherdeclarativeextensionofHornclauselogicprogrammingbyboundedquantiersisdenedin[42,43].Boundedquantiersallowonetonaturallyexpressthesearchovernitedomains.Thisthesisextendstheresultsof[43]toconstraintlogicprogramming.Thatis,weshowhowtoincludeboundedquantiersintotheconstraintlogicprogrammingparadigm.Itallowsonetohandlebothniteandinnitedomainconstraints.Inaddition,boundedquantiersmakeitpossibletoconstructnitedomainswiththedesiredproperties.Weonlytreatsemanticsandaproceduralinterpretationhere,buttheresultsontheexpressivepowerandonnegationfrom[43]couldalsobestraightforwardlygeneralizedtoconstraintlogicprograms.Therestofthissectionwillserveasanintroductiontotheeldsofconstraintprogramming,boundedquantiersandcollectiontypes.Thefollowingsectionsarefromthetechnicalreport[2].InSection2wegivethebasicdenitionsofsorts,listsandCBQ-programs,i.e.constraintlogicprogramswithboundedquantiers.InSection3weintroduceseveralsemanticsoflogicprogramswithboundedquantiersandprovetheirequivalence.Section4describesCBQ-resolutionthatservesastheproceduralsemanticsofthelanguage.InSection5wediscussrelatedworks.1.1ConstraintprogrammingConstraintprogrammingisawayofincorporatingconstraintsolvingtechniquesintoaprogramminglanguage.Ithasbeendonebothforfunctionalandprocedurallanguagesaswellasforlogicpro-gramminglanguages.Theworkonconstraintprogramminglanguagesprecededlogicprogrammingwhichisshowninthefollowingsurveyofsomeearlylanguages,mainlyfrom[25].Constraintprogramminglanguageswasatrstusedintheareasofgraphicalsystems,electriccircuitengineeringandforsolvingcombinatorialproblems.TherstlanguageconsideredtobeaconstraintlanguagewasSKETCHPAD[37].Itwasaninteractivedrawingsystemwheretheusercouldbuildgeometricobjectsfromlanguageprimitivesandstaticconstraintsthatweresolvedbylocalpropagationandrelaxationtechniques.AnotherlanguagewasTHINGLAB[7]thatwasasomewhatobject-orientedgraphicalsystem,localpropagationandrelaxationwereusedtohandlethestaticconstraints.IntheareaofelectriccircuitingCONSTRAINTS[36]wasalanguagewherevariablesandconstraintswerestatic,i.e.couldnotbedynamicallygenerated,andtheconstraintsolvingwaslimitedtousinglocalpropagation,itwasusedinapplicationsforelectricalcircuitanalysisandsynthesis.EL/ARS2[35]andSYN[11]wasrelatedsystemsthatusedtheconstraintsolverMACSYMA[32]toavoidtherestrictionsoflocalpropagation.AnearlysystemdesignedforproblemsolvingwastheREF-ARF[15]system.REFisaprocedurallanguagewithnondeterminismbecauseofstaticconstraintsusedinconditionalstatements,ARFistheconstraintsolverusingbacktracking.DuringthistimealotofworkwasalsodoneinmodelingcombinatorialproblemsasConstraintSatisfactionProblems(CSP’s)anddevelopingtechniquesfortheirsolvingindependentofahostlanguage.TheseproblemscanbeclassiedasBooleanconstraintsatisfactionproblems,forexamplethemap-coloringproblem,andasconstraintoptimizationproblems.Constraintlogicprogramming(CLP)istheincorporationofconstraintsandconstraintsolvingmethodsinlogic-basedlanguages.Thelanguagescombinethedeclarativesemanticsandnondeter-minismoflogicprogrammingwithecientconstraint-solvingalgorithms.ThewellknownCLP-scheme[24]denestheclassoflanguagesCLP(X)obtainedbyinstanti-atingtheparameterX.Inthisschemealogic-basedprogramminglanguage,itsoperationalanddeclarativesemanticsandtherelationshipsbetweenthesesemanticsareallparameterizedbyachoiceofdomai