Summary
This chapter, a large part of which is a translation of (Retoré, 1996), deals with the connection between Lambek categorial grammar and linear logic, the main objective being the presentation of proof nets which are excellent parse structures, because they identify linguistically equivalent analyses of a given sentence.
This graphical notation for proofs that are parse structures in categorial grammar is a not a mere variation for convenience. On a technical ground, it avoids the so-called spurious ambiguity problem of categorial grammars (the fact that we can find many different proofs/parse structures for what corresponds to a single analysis or lambda term). Conceptually, this proof syntax is a justification of the use of the expression parsing as deduction often associated with categorial grammar. Indeed proof nets only distinguish between proofs which correspond to different syntactic analyses.
We first give a rather complete presentation of the correspondence between the Lambek calculus and variants of multiplicative linear logic, since the Lambek calculus can be defined as non-commutative intuitionistic multiplicative linear logic without empty antecedents.
Next we define proof nets and establish their correspondence with the more traditional sequent calculus, present parsing as proof net construction and present some recent descriptions of non commutative proof nets.
As an evidence of their linguistic relevance, we explain how they provide a formal account of some performance questions, like the complexity of the processing of several intricate syntactic constructs, like center embedded relatives, garden path phenomena and preferred readings.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abrusci, V.M.: Phase semantics and sequent calculus for pure non-commutative classical linear logic. Journal of Symbolic Logic 56(4), 1403–1451 (1991)
Abrusci, V.M.: Non-commutative proof nets. In: Girard, et al., pp. 271–296 (1995)
Asperti, A.: A linguistic approach to dead-lock. Tech. Rep. LIENS 91-15, Dép. Maths et Info, Ecole Normale Supérieure, Paris (1991)
Asperti, A., Dore, G.: Yet Another Correctness Criterion for Multiplicative Linear Logic with Mix. In: Nerode, A., Matiyasevich, Y. (eds.) LFCS 1994. LNCS, vol. 813, pp. 34–46. Springer, Heidelberg (1994)
Bellin, G., Scott, P.J.: On the π-calculus and linear logic. Theoretical Computer Science 135, 11–65 (1994)
van Benthem, J.: Language in Action: Categories, Lambdas and Dynamic Logic. Studies in logic and the foundation of mathematics, vol. 130. North-Holland, Amsterdam (1991)
Bondy, J.A., Murty, U.S.R.: Graph Theory and Applications. Macmillan Press (1976)
Dalrymple, M., Lamping, J., Pereira, F., Saraswat, V.: Linear logic for meaning assembly. In: Morrill, G., Oehrle, R. (eds.) Formal Grammar, pp. 75–93. FoLLI, Barcelona (1995)
Danos, V.: La logique linéaire appliquée à l’étude de divers processus de normalisation et principalement du λ-calcul. Thèse de Doctorat, spécialité Mathématiques, Université Paris 7 (1990)
Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28, 181–203 (1989)
Diestel, R.: Graph Theory, 4th edn. Springer (2010)
Fleury, A.: La règle d’échange: logique linéaire multiplicative tréssée. Thèse de Doctorat, spécialité Mathématiques, Université Paris 7 (1996)
Fleury, A., Retoré, C.: The mix rule. Mathematical Structures in Computer Science 4(2), 273–285 (1994)
Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1–102 (1987)
Girard, J.Y.: Linear logic: its syntax and semantics. In: Girard, et al., pp. 1–42 (1995)
Girard, J.Y., Lafont, Y., Regnier, L. (eds.): Advances in Linear Logic. London Mathematical Society Lecture Notes, vol. 222. Cambridge University Press (1995)
de Groote, P.: Linear Logic with Isabelle: Pruning the Proof Search Tree. In: Baumgartner, P., Posegga, J., Hähnle, R. (eds.) TABLEAUX 1995. LNCS (LNAI), vol. 918, pp. 263–277. Springer, Heidelberg (1995)
de Groote, P.: A Dynamic Programming Approach to Categorial Deduction. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 1–15. Springer, Heidelberg (1999)
de Groote, P., Lamarche, F.: Classical non-associative Lambek calculus. Studia Logica 71(3), 355–388 (2002)
de Groote, P., Retoré, C.: Semantic readings of proof nets. In: Kruijff, G.J., Morrill, G., Oehrle, D. (eds.) Formal Grammar, pp. 57–70. FoLLI, Prague (1996)
Guerrini, S.: Correctness of multiplicative proof nets is linear. In: 14th Symposium on Logic in Computer Science (LICS 1999), pp. 454–463. IEEE (1999)
Guerrini, S.: A linear algorithm for MLL proof net correctness and sequentialization. Theoretical Computer Science 412(20), 1958–1978 (2011); Girard’s Festschrift
Johnson, M.E.: Proof nets and the complexity of processing center-embedded constructions. Journal of Logic Language and Information Special Issue on Recent Advances in Logical and Algebraic Approaches to Grammar 7(4), 433–447 (1998)
Lamarche, F.: Proof nets for intuitionistic linear logic: Essential nets. 35 page technical report available by FTP from the Imperial College archives (1994)
Lambek, J.: From categorial grammar to bilinear logic. In: Došen, K., Schröder-Heister, P. (eds.) Substructural Logics, pp. 207–237. Oxford University Press, Oxford (1993)
Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56(1-3), 239–311 (1992)
Melliès, P.A.: A topological correctness criterion for multiplicative non-commutative logic. In: Ehrhard, T., Girard, J.Y., Ruet, P., Scott, P. (eds.) Linear Logic in Computer Science. London Mathematical Society Lecture Note, vol. 316, ch. 8, pp. 283–321. Cambridge University Press (2004)
Merenciano, J.M., Morrill, G.: Generation as Deduction on Labelled Proof Nets. In: Retoré, C. (ed.) LACL 1996. LNCS (LNAI), vol. 1328, pp. 310–328. Springer, Heidelberg (1997)
Métayer, F.: Homology of proof-nets. Prépublication 39, Equipe de Logique, Université Paris 7 (1993)
Moot, R.: Filtering axiom links for proof nets. In: Kallmeyer, L., Monachesi, P., Penn, G., Satta, G. (eds.) Proceedings of the 12th Conference on Formal Grammar (FG 2007). CSLI Publications, Dublin (2007) (to appear) ISSN 1935-1569
Morrill, G.: Memoisation of categorial proof nets: parallelism in categorial processing. In: Abrusci, V.M., Casadio, C. (eds.) Third Roma Workshop: Proofs and Linguistics Categories – Applications of Logic to the Analysis and Implementation of Natural Language. CLUEB, Bologna (1996)
Morrill, G.: Incremental processing and acceptability. Computational Linguistics 26(3), 319–338 (2000); preliminary version: UPC Report de Recerca LSI-98-46-R (1998)
Morrill, G.: Categorial Grammar: Logical Syntax, Semantics, and Processing. Oxford University Press (2011)
Morrill, G., Fadda, M.: Proof nets for basic discontinuous Lambek calculus. Journal of Logic and Computation 18(2), 239–256 (2008)
Murawski, A., Ong, C.H.: Dominator trees and fast verification of proof nets. In: 15th Symposium on Logic in Computer Science (LICS 2000), pp. 181–191. IEEE (2000)
Pentus, M.: Lambek calculus is NP-complete. Theoretical Computer Science 357(1), 186–201 (2006)
Pogodalla, S.: Generation in the Lambek calculus framework: an approach with semantic proof nets. In: Proceedings of NAACL 2000 (2000a)
Pogodalla, S.: Generation, Lambek calculus, montague’s semantics and semantic proof nets. In: Proceedings of Coling 2000 (2000b)
Pogodalla, S.: Generation with semantic proof nets. Research Report 3878, INRIA (2000c), http://hal.inria.fr/docs/00/07/27/75/PDF/RR-3878.pdf
Pogodalla, S., Retoré, C.: Handsome non-commutative proof-nets: perfect matchings, series-parallel orders and hamiltonian circuits. Tech. Rep. RR-5409, INRIA, presented at Categorial Grammars (2004); to appear in the Journal of Applied Logic
Regnier, L.: Lambda calcul et réseaux. Thèse de doctorat, spécialité mathématiques, Université Paris 7 (1992)
Retoré, C.: Réseaux et séquents ordonnés. Thèse de Doctorat, spécialité Mathématiques, Université Paris 7 (1993)
Retoré, C.: Calcul de Lambek et logique linéaire. Traitement Automatique des Langues 37(2), 39–70 (1996)
Retoré, C.: Perfect matchings and series-parallel graphs: multiplicative proof nets as R&B-graphs. In: Girard, J.Y., Okada, M., Scedrov, A. (eds.) Linear 1996. Electronic Notes in Theoretical Science, vol. 3. Elsevier (1996)
Retoré, C.: A semantic characterisation of the correctness of a proof net. Mathematical Structures in Computer Science 7(5), 445–452 (1997)
Retoré, C.: Handsome proof-nets: perfect matchings and cographs. Theoretical Computer Science 294(3), 473–488 (2003), complete version RR-3652, http://hal.inria.fr/docs/00/07/30/20/PDF/RR-3652.pdf
Savateev, Y.: Product-Free Lambek Calculus Is NP-Complete. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 380–394. Springer, Heidelberg (2008)
Yetter, D.N.: Quantales and (non-commutative) linear logic. Journal of Symbolic Logic 55, 41–64 (1990)
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Moot, R., Retoré, C. (2012). Lambek Calculus and Linear Logic: Proof Nets as Parse Structures. In: The Logic of Categorial Grammars. Lecture Notes in Computer Science, vol 6850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31555-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-31555-8_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31554-1
Online ISBN: 978-3-642-31555-8
eBook Packages: Computer ScienceComputer Science (R0)