The formal and computational theory of constraint

TheFormalandComputationalTheoryofConstraintLogicGrammarsLuisDamasNelmaMoreiraUniversityofPortoGiovanniB.VarileCommissionoftheEuropeanCommunitiesTheframeworkpresentedinthischapterassumesthatanygrammarisaparticularfirstordertheorywithequality.Wewillturnourattentiontothosefirstordertheoriesadmittingcompletemodelsandextendthemtorecursivelydefinedrelations.Logicprogrammingisanidealparadigmforsuchaframeworkinthatitsupportsadirectmappingbetweengrammars,seenasfirstorderlogictheories,andthefirstordertheoryoftheirimplementationandatthesametimeprovideaformallysoundandefficientcomputationalscheme.Itisalsoparticularlywellsuitedtosimultaneouslysatisfythemainre-quirementsputoncomputationalgrammarformalisms,namelyexpressivity,formalsoundnessandcomputationaltractability.Aswewillsee,theframeworkpresentedinthischapterisnotonlycom-patiblewiththeunificationgrammartraditionbutitalsoconstitutesasim-pleframeworkforextendingthenotionofunificationtocomplexconstraintresolution.Atthesametimeahighdegreeofdeclarativenessisachievedbyavoidinganyreferencetoanoperationlikeunification.Themotivationsforthechoiceoftheparticularfamilyoffirstordertheorieswillbecomeapparentintherestofthischapter.Themainreasonsderivesfromthefactthatrestrictingtheformalanaly-sistothestaticpropertiesofformalismsdoesnotdojusticetothecomputa-tionalcomplexityofmodernlinguisticframeworks.Afinergrainedanalysisoftheformalandcomputationalpropertiesofformalismsthandecidability,formalcomplexityandmodeltheoreticproperties,shedsadifferentlighton1theproblemmotivatingchoiceswhichwouldotherwiseappeartobearbi-trary.Itisnotsufficienttodesignformalismswithasimpleandsounddenota-tionalsemanticsandappropriateformalcomplexitycharacteristics.Rather,itisnecessarytoprovidesoundandadequateformalprocessingschemesforsuchformalisms,lackingwhichthemainchallengesfacingmoderngram-maticalformalismdesignarenotaddressed.Takingthispointfurther,weclaimthatthetheoryofagrammarfor-malismanditsformalprocessingmodelconstituteahomogeneousandin-tegratedwholeandthatthepracticeofrelegatingprocessingissuestolowlevelimplementationdecisionshad,andhas,nefastconsequences,notleastpreventingtherightquestionstobeaddressed.Thedeductiveprocessbywhichafactisprovenoranobjectcomputedmustbethesubjectoftheoreticalinquiryjustas,andtogetherwith,thefactorobjectandtheirdescriptions.Theanalogywithlogicprogrammingisparadigmatic:definingthesyn-taxand(static)semanticsofalogicprogrammingschemeisanessentialfirststep.Butitalsoconstitutesarelativelytrivialtaskcomparedwithdefinitionofaformalprocessingschemewiththenecessarycomputationalcharacteristics.Ourgoalistoshowhowandunderwhatcircumstanceswecanensureasimpleandnaturalrelationbetweengrammarswithcomplexconstraintexpressionseenasfirstordertheoriesandthelogicprogrammingparadigm,inparticularaversionofConstraintLogicProgrammingoverthedomainofrationaltrees.Thischapterisorganizedasfollows:inSection1wewillpresentthefamilyoffirstordertheoriesuponwhichConstraintLogicGrammars,orCLGs,arebased,namelythosehavingthecompletealgebraRTofrationaltreesastheircanonicalmodel.Afterhavingjustifiedthischoice,wewillelaborateonthebasiccharac-teristicsofthesefirstordertheories,extendthemwithrecursiverelationsandrelatethemtoCLP(RT)1.InSection2wewillshowthatthesetheoriesrelateinanaturalwaytofeaturelogicsandinSection3howtoextendtermunificationtoconstraintresolutioninasimpleway.InSection4wewillpresentCLGscomplexconstraintsolveranditscompleteconstraintrewritingsystem.1ConstraintLogicProgrammingoverRT[JL88].2ThedescriptionoftheformalprocessingmodelofCLGswillbecom-pletedinSection5wherewedefinetheCLGmodelseenasaninstantiationoftheconstraintlogicprogrammingschemeforthesymbolicdomainofra-tionaltrees.1TheFirstOrderTheoryofCLGCLGgrammarsarefirstordertheories,i.e.objectoffirstorderlogicconsist-ingofalphabetsoflogicalandnonlogicalsymbolsincludingtheequality,theusuallogicalaxiomsandinferencerules,andanumberofnon-logicalaxioms2.Theroleofthenonlogicalaxiomsistwofold:forone,anumberoftheseaxiomswillrestrictthepossiblemodelsforourtheoriesinaconvenientwayasexplainedbelow.Thesecondroleoftheseaxiomsistorepresentgrammarrules,lexicalobjectsandlinguisticprinciples.Inotherwordstheycharacterizetheinter-pretationswhicharewellformedwithrespecttoagivengrammar.AllthetheoriesconsideredherewillbeextensionsoftheorieshavingascanonicalmodelsthecompletealgebraRTofrationaltrees.Theextensionareneededtoaccountforrecursivedefinitionswithinthetheory,asexplainedbelow.NogeneralityislostbymakingthischoiceaswewillseeinSection2.WewillfirstproceedtodefinethedenotingobjectsofaCLGtheory,i.e.theterms.Wewillthencharacterizetheconstraintlanguageandimposerestrictionsonthepossibleinterpretationsofthetheory.Lastlywewillextendthefirstordertheoryobtainedinthiswayinordertoaccountforrecursiverelationsneededtoexpressgrammarrulesandprinciples.1.1TermsGivencountablesetsFandVoffunctionsymbolsandvariablesrespectively,wedefinethetermsTofourtheoryintheusualwayasbeingtheleastsetsuchthat:1.elementsofVareinT2.forfninFandt1,...,tninT,fnt1,...,tnisinTFunctionsymbolscomeequippedwiththeiraritynwrittenasfn.2See[Sho67]