D &243;&242; &243; &242; &236;&24(2)

Beginningwiththesequenceofterminalformulaeabove,weobtainthetransformations:

Thecategoriesintheseformulaebecomesimplerwitheachruleapplica-tion,sothistriviallyterminates,andnomatterinwhichordertheredexesofthetransformationsarechosen,thesame nalsequenceresults.Inthe nalsequence,allformulaeconsistofpolarisedatomic/basiccategories.Thisisthesequenceofaxiomaticformulae.

Ingeneral,eachpositiveformulawillbelabelledwithavariable,andeachnegativeformulawillbelabelledwithatermfromtheuntypedlamb-dacalculus.Weassignedvariablestoallformulae,positiveandnegative,whenwecreatedthesequenceofterminalformulae.Duringlexicalun-folding,wemustspecifywhatlabelstoassigntheformulaeresultingfromthetransformationrules.Thisinvolvesusingnewvariablesandformingnewtermsfromthesenewvariablesandtheoldtermslabellingtheun-foldedformulae.Wheneverweunfoldapositiveformula,wemustalsospecifyanadditionalvariablesubstitutionasasideconditionthatrelatesthevariablesusedbythatrule:

Theabovelabelledsequenceofterminalformulaethenunfoldslikethis:withthesubstitution,,arisingfromstep

.

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

2.3AxiomaticLinkage

Afterlexicalunfolding,welinkmatchingpairsofaxiomaticpolarformulaetogether(and,forabasiccategory).Asubsequenceofaxiomaticformulaeplusacompletematchingbytheselinksiscalledan(axiomatic)linkage.Ifthesubsequenceistheentiresequenceobtainedfromunfold-ingasequenceofterminalformulae,thenwedistinguishitasaspanninglinkage.Withinalinkage,wecanalsoidentifysublinkages,contiguoussubsequenceswhoseborderseverylinkcrosseseitherzeroortwotimes,i.e.,nolinkstraddlesthesubsequence’sboundaries.Herearetwospan-ninglinkagesfortheaboveexample:

Usually,wewritethelexicalunfoldingunderneaththeaxiomaticsequence,andthelinkageabove.The rstspanninglinkagecontainsasublinkagebetweenand.Thesecondonedoesnot,althoughthereisonebetweenand.

2.4VariableSubstitution

Eachaxiomaticlink:

canbeassociatedwithasubstitution,

spanninglinkagesaboveare:.Thesubstitutionsforthetwo

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

The rstsubstitutioncomesfromthesideconditionacquiredduringlex-icalunfolding.

The nalstepistoapplytheassociatedsubstitutionsiterativelytothevariablelabellingthepositiveterminalformulauntilnomoresubstitu-tionsareapplicable.Inourrunningexample,thislabelis:

2.5CorrectnessCriteriaforProofNets

A(Lambek)proofnetconsistsofalexicallyunfoldedsequenceoftermi-nalformulae,aspanninglinkageoftheresultingsequenceofaxiomaticformulaeandavariablesubstitutionyieldingatermforwhich:PN(1)thereispreciselyonepositiveterminalformula,

PN(2)variablesubstitutionterminates(isa niteterm),

PN(3)ifcontainssubterm

outside,,thenoccursinanddoesnotoccur

PN(4)everyvariableassignedtoanegativeterminalformulaoccursin,

PN(CT)hasnoclosedsubterms,and

PN(L)theaxiomaticlinkageisplanar,i.e.,theaxiomaticlinkscanbedrawnasin(1)and(2)abovesuchthatnotwolinkscross.

Roorda[14,pp.31–34]provedthatasequentisderivableintheLambekCalculusiffthereisaproofnetwhoseterminalformulaecorrespondtoit.3LC-Graphs

Successivelygeneratingspanninglinkagesandtestingthemagainstthecorrectnesscriteriaforproofnetsisclearlynotanef cientwaytoparsewithLCGs.Ideally,whatwewouldlikeisadynamicprogrammingmethodforincrementallyconstructingproofnets,withsomewayofrepresentingthestateofourknowledgeaboutcorrectnessandincrementallyandcom-pactlycombiningthatknowledgetoo.

Thissectionde nesagraphforrepresentingthestateofourknowl-edgeaboutcorrectness.Section5presentsadynamicprogrammingmeth-odthatusesthesegraphs.First,weneedsomemoreterminology.

Givenasequenceofterminalformulaeandalexicalunfolding,avari-able,,thatlabelsaformulaanywhereintheunfoldingiscalleda

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

plus-variable.Ifisabasiccategory,wedistinguishbysayingitisasimpleplus-variable.Ifisacomplexcategory,thenwedistinguishbysayingitisalambda-variable.Avariable,,thatlabelsaformulaisaminus-variable.Ingeneral,negativeformulaearelabelledbyterms,andingeneralthesetermscontainbothminus-variablesandplus-variables.Duringlexicalunfolding,asubstitutionisaddedforeverylambda-var-iable,,oftheform.Inthiscase,andarecalledthedaughtervariablesof.

Givenasequenceofaxiomaticformulae,,isthesetofvariablesoccurringassubtermsoflabelsoftheaxiomaticformulaein.

Givenalinkage,,overasequenceofaxiomaticformulae,,itsLC-graphisadirectedgraph,suchthatisthesmallestsetforwhich:

,

containseverylambda-variablewithatleastonedaughter-variablein,

andisthesmallestsetforwhich:

foreverypair,ifisalambda-variableand

daughtervariablesof,then,andisoneofthe

foreveryaxiomaticlinkin:

andforeveryvariablein,.

Whenthereisapathfromsometoin,wesay,or,whenitisclearwhichismeant.If,thentrivially.

InthecontextofLC-graphs,whenweseeaplus-variable(resp.minus-variable,lambda-variableetc.),wecallitaplus-node(resp.minus-node,lambda-nodeetc.).Inaddition,wecallanodeinaterminalnodeiffithasanout-degreeof.Note,however,thatplus-nodesoftenoccurintermsthatlabelnegativeaxiomaticformulae(anegativeoccurrenceofaplusnode),buttheyarestillplus-nodes.Thesearisefromthefollowingtwolexicalunfoldingrules:

wherelabelsapositiveformula,andisthusaplus-node,butalsooc-cursintheterm,,whichlabelsanegativeformula.Aminus-nod …… 此处隐藏：5946字，全部文档内容请下载后查看。喜欢就下载吧 ……