D &243;&242; &243; &242; &236;&24

A graph-theoretic construction for representing the derivational side-conditions in the construction of axiomatic linkages for Lambek proof nets is presented, along with a naive algorithm that applies it to the sequent derivability problem for the Lambek C

AGraph-TheoreticApproachtoSequentDerivabilityintheLambekCalculus

GeraldPenn

DepartmentofComputerScience

UniversityofToronto

10King’sCollegeRd.

TorontoM5S3G4,Canada

1Introduction

ThispaperconsidersthequestionofwhetherastringofwordscanbeparsedrelativetoaLambekCategorialGrammar(LCG)inpolynomialtime.AlthoughLCGsareknowntobeweaklyequivalenttocontext-freegram-mars(CFG),themostrelevantformalconstrualofthisparsingquestionisstillopen,namely,”Isthesequent,derivableintheLambekCalculus?,”whereare(possiblycomplex)categories.GivenanLCG,,andastring,withuniquelexicalentries,,in,thisamountstostringrecognitionwhen,thedistinguishedcate-goryof.

Asimplegraph-theoreticconstructionforrepresentingthewell-form-ednessconstraintsofanLCGderivation,calledLC-graphs,ispresentedhere.AnalgorithmthatresemblesastandardCFGchart-parserisalsoprovidedforansweringtheabovesequentderivabilityquestion.Crucially,thisalgorithmisnotpolynomial-time,soitdoesnotsolvetheopenprob-lem,butitishopedthatitwillcontributetoaneventualsolutiontothe

A graph-theoretic construction for representing the derivational side-conditions in the construction of axiomatic linkages for Lambek proof nets is presented, along with a naive algorithm that applies it to the sequent derivability problem for the Lambek C

sequentderivabilityproblem.Afewrelatedparsingproblemsarealsodis-cussed.

Chart-parsingwithLCGsisnotanewapproach.Koenigproposedachartparseraugmentedwithmeta-rulesthatwouldspawnanewchartwheneveranintroductionrulewasapplied.Heppleproposedcombin-ingthesechartsintoasingle“multi-dimensional”chart.Inthischart,lex-icaledgesformatotallyorderedsequenceofprimitiveintervals,asusual,butwheneverahypotheticalcategoryisassumed,anewprimitiveintervalisaddedwithonefreeend.Introductionthenamountstoabstractingtheedgesthatusethisnewhypotheticalintervalbackontothetotallyorderedsequenceofintervalsthatitwasaddedto.Morrill[8]usedachart-likerep-resentationincombinationwithproofnetsfortheLambekCalculusPennusedasimilarrepresentationforrepresentingdeductionsintheLambekCalculusintheElfprogramminglanguageMorrillalsoprovidedanactualparsingalgorithm,againbasedonproofnets.

Proofnetshavetheadvantagethattheyabstractawayfromallofthespuriousambiguitiesthatarisefromproofsearchtechniquesbaseddi-rectlyonnaturaldeductionorsequentpresentationsoftheLambekCal-culus.Asaresult,theyexposetheessentialsourcesofnon-determinismthataworst-casecomplexityanalysisofLCGrecognitionmustface.MuchoftherecentworkonparsingwithLCGs,however,haschosentodwellonelegantimplementationsofLCGproofsearchinhigher-order(linear)logicprogramminglanguages.Whiletheseareindeedelegant,theyareperhapsnotthebestchoicefordiscoveringthecomplexityoftheproblemathand.

Itisforthisreasonthatthepresentarticlehasoptedfora“back-to-basics”approach,usingonlyafewsimplealgorithmsandbasicgraphthe-orytocharacterisetheproblem.LC-graphsrepresentinformationaboutsubstitutionsassociatedwithlinkagesofaxiomaticformulaeintheproofnetsofLCGderivations.Givenourextensiveknowledgeaboutalgorith-micef ciencyandNP-completenessinthedomainofgraphtheory,itishopedeitherthatthealgorithmgivenherecanbeenhancedandproventobepolynomial,orthatafailuretosoenhanceitwillrevealanembed-dingofaknownNP-hardproblemintoLCGrecognition.

Theuseofgraphtheoryinthecontextofproofsearchinsubstructurallogicsisalsonotanewone.LC-graphsandtheirwell-formednesscon-straintsarecertainlyreminiscentofGirard’soriginal“long-tripcondition”

[3],andlatercorrectnesscriteriaformultiplicativelinearlogicMootandPuite[7,13]proposeagraphrewritingsystemthatencompassesLCGandallofitsmultimodalextensions.LC-graphsaremuchsimpler,buttheirextensiontomultimodalLCGremainsatopicforfurtherresearch.ThetimecomplexityofvariousLCGparsingproblemsispartofabroad-ertheoreticalpicturethatisextremelyinterestinginitsownright.TheLambekCalculusisonlyoneofalargenumberofsubstructurallogicsthat

A graph-theoretic construction for representing the derivational side-conditions in the construction of axiomatic linkages for Lambek proof nets is presented, along with a naive algorithm that applies it to the sequent derivability problem for the Lambek C

havebeenstudiedtodate,allofwhichcanberelatedtoeachotherbytherelativepresenceorabsenceofmodaloperatorsalongwithstructuralrulesofinferencethatcontrolthebehaviouroftheseoperators[6].Whatisnotcompletelyunderstoodishowthepresenceorabsenceoftheseopera-torsandrulesaffectthecomplexityofproofsearch.Justaswitheachofthebetter-knownmembersoftheChomskyHierarchyofformallanguageswehaveacharacterisationofthatclassoflanguagesintermsoftheautomataandstacksrequiredtocomputestringmembership,anoperationalchar-acterisationofthisclassoflogicswouldalsobeextremelyuseful,bothasadualformofrepresentationandasaguidefortheconstructionofotherlogicswithcertainoperationalpropertiesforsomeapplication.

Withinthisbroaderpicture,theLambekCalculusstandsoutasonelogicofgreathistoricalinterestforwhichthetimecomplexityofsequentderivabilityisstillunknown.BecauseoftheknownweakequivalenceofLCGstothecontext-freelanguages,moreover,ithasanumberofveryin-terestingpotentialapplicationswithincomputationallinguisticsandcom-putationalbiology,whereCFGsarealreadybeingused.Inparticular,LCGscouldinprincipleserveasanunderlyingdiscretestructureforacontext-free-equivalentstatisticalmodelthatnaturallyexposesaverydifferentselectionofnumericalparametersfromthoseofastandardCFG,orforwhichcertainparameterscanmoreeasilybeestimatedfromdata.

Forsimplicity,thepresentationherewillconsidertheproduct-freefrag-mentoftheLambekcalculus,inwhichsequentswithemptypremisescannotbederived.Sectionbeginswithanintroductiontoproofnets,andhowtobuildthem.Sectionthenprovidesanin …… 此处隐藏：6123字，全部文档内容请下载后查看。喜欢就下载吧 ……