A Compilation-Chart Method for Linear Categorial Deduction

A Compilation-Chart Method for Linear Categorial Deduction Mark Hepple l)epl;, of Compul;or Sole.He0. Universit;y of Sheffield Regent, Court;, 211 l%rl;obello St;reel; ShellMd $71 4DP, UK hepple@dcs, shef. ac. uk Abstract Recent, work in ca.t;eg(Mj gr;mmt;~r has seen proposals for a wide. r;Lltg(~ O[ sys-. t;(;i[IS, differing in their 'resomx:e sensi- tivil;y' and hence, implicitly, {;heir under.. lying nol;ion of qinguisl;ie SLlllet;ure'. a common frmnework for t)arsing such sys- t;elns is elll(;l'ging;, whereby some inel;hod of linear logi(: l;hcorent ])roving is used in COlnbinal;ion with ;~ sysl,em of l;t- 1)elling l;hat; ensures l;hat; only ([edtl(> Lions a,pl)rot)ri}tt;c Lo l;he r(~le.vanL (:at;ego- rM formalism are allowed. This l)al)(n' presenl, s a deduction reel;hod for impli- (-a.t, ional line~r logic I;ha|; brings with il, I;he benelil; thai; (:harl; parsing provides for CI,'G parsing, namely avoiding (;he need (;o recompu(;e intenne.dial;e resull;s wheal ,qcarching exhausi;ively for ;~ll possi- ble mmlyses. The mel;ho([ involves (:ore- piling possibly higher-or(l(;r linear formu- lae 1;o indexed firsl;-or(ler formulae, over whi(:h (tcdu(:l;ion is ina(le using jusL a, sin-. gle inference rule. 1 Introduction This t)al)er present;s a method applicalle to pars- ing a. range of cal;egorial gramm~u' formalisms, in pa.rl;ieulm ones Lhal; l';tll wil;hin l;he %yt>e-logieal' t;ra.dition, of which Lhe (associa.l;ive) l,mnbek cal- culus L is l;he most; familiar rcl)re.qenLal;iw; (l,am- bek, 1988). l{,e(;enl; work haos se.en proposals tier a range of such sysl;el[l.q, differing in their resource sensitivity (and hence, imt)licil;ly , (;heir underly- ing llo|;ion of 'linguisLi(: sl.rllei;llre'), in some eases combining differing resource sensiCivil;ies wi(;hin a, single sysl;e]n. I Some o17 l;hese propos;ds em- l)]oy a 'labelled de(luei;ion' me.l;hodology (G;d)b;~y, ]994), where|)y 1;he. I;yi)es in a pr()of are asso(:ial;(!d wil;h labels under a Sl)e.eiti(;d diseiI)litte , l;he la.bels iS(x;, for cxanLlile , the ['orma.lisnls devcqoped ill Moortg~t & Morrill (1991), Moortgat & ()ehrle (1.994), Morrill 11994), Ilct,1)le (1995). re.cording proof' inform;~l;ion a.s a basis for ensming; correcl; int'crelming. Alongside such developmenLs, vmiotts work ha.s addressed I;he ;tssoeial;e(t parsing 1)rol)lem. 2 ()[" l)~Lrt;iculm inl;eresl, here ~tre .qysl;ems t;ha,l; employ a 1;heorem proving reel;hod l;hat is (perhaps im- plicitly) appropriat;e for use with linear h)gi(:, and combine it wiLh ~ labelling system I;hat; restrict,s ;uhnil;t;cd deducl;ions 1;o be l,hose of some weaker logic. Moorl;gal; (]!)92) shows how a linear proof nel, mel;hod may 1)e combined wit;h a r;mge of la.- belling disciplines t;o provide dedu(:[;ion for a ran,g(! o1 ca,l;egori~l sys|;ems. Morrill (199,5) shows how 71, t;ypes nmy be t;ra.nsl;tl;ed Lo labelled inq)li(:ational linem' l;yl>es , wil;h deduct;ion implement;ed via. a version of SI,D resolution. The crucial ol)serva.I;ion is t;hat, linem' logic sl;;m(ls ~bove all of @e l;yl)(> logi(;a,l syst;ems prot)osed a,s (:at;cgorial formalisms in Lhe hierarchy of sul)st;ruel;m'a] logics, and he~tce linem' logi(: deduct, ion methods (:m] i)rovide ;t com- mon basis for parsing all of these systems. The prescnl, work contrilml;es to this pro.]ect by providing a met;hod of deduction for the impli- c;~l;ional fragment; of linear logic l;hal;, like charl; parsing for I'SG, avoids reeonipul;agion of result,,q, i.e. where any combination o[' 1;ypes c(mt;ril)ut;es {;o …

Content truncated to 500 words