Towards efficient parsing with proof-nets

Towards efficient parsing with proof-nets Alain Lecomte GRIL Universit6 Blaise Pascal 63037-Clermont-Ferrand France email: lecomte@ shm.grenet.fr Abstract This paper presents a method for parsing associative Lambek grammars based on graph- theoretic properties. Connection graphs, which are a simplified version of proof-nets, are actually a mere conservative extension of the earlier method of syntactic connexion, discovered by Ajduckiewicz [1935]. The method amounts to find alternating spanning trees in graphs. A sketch of an algorithm for finding such a tree is provided. Interesting properties of time-complexity for this method are expected. It has some similarities with chart-parsing ([KOnig, 1991, 1992], [Hepple, 1992]) but is different at least in the fact that intervals are here edges and words are vertices (or trees) instead of the contrary in classical chart- parsing. 1 Introduction In this paper, we present a method for parsing Lambek grammars based on graph-theoretic properties. We expect that it may be done efficiently by an algorithm (time-polynomial even in the worst case) which aims at finding an alternating spanning tree in a graph. We do not give the explicit formulation of such an algorithm in this paper: we will only give an idea and an illustration of it. This paper is thus mostly devoted to the properties on which the method is based. We call connection graphs the special kind of proof-nets we explore, just in order to make explicit some difference with the usual method of proof-nets, as it can be found in [Roorda, 1991; 1992] and [Moortgat 1992], but the two concepts are very similar. In many respects, connection graphs are a mere conservative extension of the earlier method of syntactic connection, discovered by Ajduckiewicz [1935]. The method amounts to link the nodes of an ordered sequence of trees in such a way that properties of connexion, "non overlapping", acyclicity and "strong connectivity" are verified. Connection graphs are simpler than proof-nets in that they loose some information. As they are here formulated, they are only convenient for the associative version of the product-free Lambek calculus. One of their advantages lies in the geometrical viewpoint they provide on the proofs of a sequent. By means of this viewpoint, questions of provability may be reduced to graph- theoretical problems. For instance, every reading of a sentence is provided by an alternating spanning tree. In many aspects, the method resembles the well known method of chart-parsing. Ktnig [1991, 1992] was the first to apply chart-parsing to Lambek calculus. Hepple [1992] has recently improved this application. An obvious difference with the method proposed here lies in the fact that, in ours, words are points and intervals between them are edges instead of the contrary in chart-parsing. In both cases, computational advantages are found by keeping correct partial analyses after they have been obtained. A chart is actually used in both methods. 2 Connection Graphs 2.1 Links and Nodes Definition 1: Let S be a set of signed vertices (i-e: labelled with letters belonging to an alphabet A and with a + or - …

Content truncated to 500 words