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

Thebasecasesarepreciselytheminus-nodeslabellingnegativetermi-nalformulaeandtheminus-daughtersoflambda-nodesalongthepathfromtheproperroottoitsaxiomaticre ection.Fortheformercategory,thelaststepmustbeanaxiomlinkbecausethenegativeterminalformu-laearenotdaughtersofalambda-node.Forthelattercategory,I(3)holdsbyPropositionsoeachoftheseminus-daughters,,hasaplus-daughtersister,,suchthatthereisapath.Thelaststepofthispathmustbeduetoanaxiomlink,sincethelambda-nodeparentofand

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

liesonthepathfromtheproperrootnodetoitsaxiomaticre ection,andnoneofthenodesonthispathhavenegativeoccurrences.

Supposethelastunfoldingstepisapositiveunfolding:

Bytheinductivehypothesis,thereisapathtothelowerlambda-node,andthusapathtotheplus-daughter,.ByI(3),thereisalsoapathfromto.ByProposition4.2,thein-degreeofis2,butifthelaststepofthepathwerevia,thentherewouldbeacycle.ByPropositionthisisacontradiction,sinceispath-accessiblefromtheproperrootnode.Sothelaststepofthepatharisesfromanaxiomlink.

Otherwise,thelastunfoldingstepisanegativeunfolding:

Bytheinductivehypothesis,thereisapathtotheminusnodeinwhoselaststeparisesfromanaxiomlink.Sincedoesnotlabelanaxiomaticformula,thelinkmustattachtoanegativeformulacontaining,andthusthereisapathtoaswell.

Proposition4.16Ifaspanninglinkagesatis esI(1)andPN(2),thenitsat-is esI(2).

Proof.ByPropositionnonodethatispath-accessiblefromthelabelpositiveterminalformulaiscontainedinacycle,andbyI(1),everynodeissoaccessible.

Proposition4.17Ifaspanninglinkagesatis esI(2)andI(3),thenitsatis- esI(CT)iffitsatis esPN(CT).

Proof.GivenI(CT),itisclaimedthatnolambda-nodeexpandsundervari-ablesubstitutiontoaclosedterm.Givenalambda-node,withminus-daughter,thereisapath,whereissometerminalnodeforwhichthereisnolambda-nodesuchthat.ByPropositionisaminus-node.

Ifisnottheminus-daughterofalambda-node,thencorrespondstothelabelofanegativeterminalformula,andsotriviallydoesnotex-pandtoaclosedterm.Otherwise,supposethateverysuchistheminus-daughterofalambda-node,i.e.,correspondstotheboundvariableofsomelambda-term.Letbeitslambda-node,andbetheplus-daughterof.,and,orelsetrivially.ByI(3),thereisapath,where,orelsethereisacycle,whichcontradictsI(2).

ByPropositionhasanin-degreeof2,soeither,which

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

contradictsourchoiceof,or.Inthelattercase,byProposi-tion.Thusexpandstoatermthatcontainsafreeinstanceof,andsoisnotclosed.

GivenPN(CT),nolambda-termisaclosedterm,sotheremustbeapathfromitscorrespondinglambda-nodetoaminus-nodeotherthanminus-daughtersofthelambda-nodesthatarereachablefrom.ThusI(3)holds.

PN(L)willbediscussedinSection5.

4.4Non-spanninglinkages

Whilemanyoftheaboveresultspertainonlytospanninglinkages,thereareafewremarkswecanmakeaboutlinkagesingeneral.Asmentionedabove,itcanhappenthataplus-nodeoccursinalinkage,butitsnegativeoccurrencefallsoutsidethelinkage’sboundaries.Theseareimproperrootnodes.Thereversecanalsohappen:anegativeoccurrenceofaplus-nodeoccursinalinkage,butthepositiveoccurrencefallsoutside.Theseareterminalplus-nodes.Aspanninglinkageisaspecialcaseinwhichthereisonlyonerootnode—aproperone—andtherearenoterminalplus-nodes.Inaddition,lambda-nodesinasublinkagecanhaveanout-degreeofeither1or2,dependingonhowmanyoftheirdaughtersfalloutside.Proposition4.18InanylinkagesatisfyingI(2),thereisatleastonerootnode,andeverynodeispath-accessiblefromatleastonerootnode.

Proof.AtrivialconsequenceofacyclicityandthefactthatLC-graphshave nitelymanynodes.

Proposition4.19Inanylinkage,everynodeispath-accessiblefromatmostonerootnode,exceptminus-daughtersoflambda-nodes.

Proof.AtrivialconsequenceofProposition4.8.

Wecallaterminalformula,,peripheralinasublinkageifftheright-mostorleftmostaxiomaticformulainthesublinkage’saxiomaticsequencederivesfromT’slexicalunfolding.Wecallanodeperipheralinasublink-ageiffitderivesfromthelexicalunfoldingofaperipheralterminalfor-mula.Thisobviouslyincludesthenodesthatappearinthetermlabellingtherightmostorleftmostaxiomaticformulaeinthesublinkage,butitmayincludemore.

Thefollowingisaninterestingcharacterisationofrootnodesandter-minalplus-nodesforthepurposesofsequentderivability:

Proposition4.20Ifasequenceofterminalformulaehasexactlyonepos-itiveterminalformula,anditistherightmostterminalformula,theninanyofthatsequence’ssublinkages,everyrootnodeandterminalplus-nodeisperipheral.

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

Proof.Terminalplus-nodesandimproperrootnodeshaveanegative(resp.positive)occurrenceinsideagivensublinkage,andapositive(resp.negative)occurrenceoutsidethesublinkage.Butthepositiveandnega-tiveoccurrencesofanode,whenbothexist,necessarilyderivefromthesamelexicalunfolding,i.e.,thelexicalunfoldingofthesameterminalfor-mula.Thatmeansthatthislexicalunfoldingmustbeperipheral,sinceoneoccurrence,andthuspartoftheunfolding,fallsoutsidethesublinkage.Properrootnodesaredifferent—theydonothavenegativeoccur-rencesanywhere.Byassumption,however,theproperrootnodelabelstherightmostterminalformula,sowhentheyoccurinasublinkage,theyarenecessarilypartoftherightmostunfolding.

5BuildingSpanningLinkages

Thede nitionofLC-graphsthemselvesdoesnotshedanylightonpars-ingcomplexityifwesimplyusethemtocheckvariablesubstitutionafterbuildingaspanningli …… 此处隐藏：5838字，全部文档内容请下载后查看。喜欢就下载吧 ……