Abstract
We will investigate proof-theoretic and linguistic aspects of first-order linear logic. We will show that adding partial order constraints in such a way that each sequent defines a unique linear order on the antecedent formulas of a sequent allows us to define many useful logical operators. In addition, the partial order constraints improve the efficiency of proof search.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
To show this in full detail would require us to do the simple but tedious job of proving that this definition satisfies the monotonicity and Application/Co-Application principles of Table 2.
- 2.
A more elegant solution for ensuring confluence would replace the right-hand side of the \( p \) and \( u \) contractions by the left-hand side of the \( c \) contraction.
- 3.
In the literature on finite state automata it is common to refer to sequences of symbols produced by such an automaton as “words”. However, we reserve “words” to refer to elements in the lexicon of a type-logical grammar and exclusively use “string” for a sequence of symbols produced by a finite state automaton.
- 4.
A closed form solution for this recurrence is the following [26].
$$ p[n] = \left\lceil \frac{2(2^n -1)}{3} \right\rceil $$.
- 5.
This analysis also makes an unexpected empirical claim: the treatment of parasitic gapping in type-logical grammars using the linear logic exponential ‘!’ would require the exponential to have scope over the quantified variable representing the empty string. We therefore need to claim that parasitic gapping can only happen with atomic formulas.
References
Areces, C., Bernardi, R., Moortgat, M.: Galois connections in categorial type logic. Electron. Notes Theor. Comput. Sci. 53, 3–20 (2004). https://doi.org/10.1016/S1571-0661(05)82570-8
Bellin, G., van de Wiele, J.: Empires and kingdoms in MLL. In: Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 249–270. Cambridge University Press, Cambridge (1995)
Bernardi, R., Moortgat, M.: Continuation semantics for the Lambek–Grishin calculus. Inf. Comput. 208(5), 397–416 (2010). https://doi.org/10.1016/j.ic.2009.11.005
Coecke, B., Grefenstette, E., Sadrzadeh, M.: Lambek vs. Lambek: functorial vector space semantics and string diagrams for Lambek calculus. Ann. Pure Appl. Log. 164(11), 1079–1100 (2013). https://doi.org/10.1016/j.apal.2013.05.009
Danos, V.: La logique linéaire appliquée à l’étude de divers processus de normalisation (principalement du \(\lambda \)-calcul). Ph.D. thesis, University of Paris VII (1990)
Danos, V., Regnier, L.: The structure of multiplicatives. Arch. Math. Log. 28, 181–203 (1989). https://doi.org/10.1007/BF01622878
Došen, K.: A brief survey of frames for the Lambek calculus. Z. Math. Log. Grundl. Math. 38, 179–187 (1992). https://doi.org/10.1002/malq.19920380113
Girard, J.Y.: Quantifiers in linear logic II. In: Corsi, G., Sambin, G. (eds.) Nuovi problemi della logica e della filosofia della scienza, CLUEB, Bologna, Italy, vol. II. (1991). Proceedings of the Conference with the Same Name, Viareggio, Italy (1990)
Girard, J.Y.: The Blind Spot: Lectures on Logic. European Mathematical Society, Zürich (2011)
Joshi, A., Schabes, Y.: Tree-adjoining grammars. In: Rosenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages 3: Beyond Words, pp. 69–123. Springer, New York (1997)
Kallmeyer, L.: Parsing Beyond Context-Free Grammars. Cognitive Technologies. Springer, Berlin (2010)
Kubota, Y., Levine, R.: Gapping as like-category coordination. In: Béchet, D., Dikovsky, A. (eds.) Logical Aspects of Computational Linguistics. Lecture Notes in Computer Science, vol. 7351, pp. 135–150. Springer, Nantes (2012). https://doi.org/10.1007/978-3-642-31262-5_9
Kubota, Y., Levine, R.: Type-Logical Syntax. MIT Press, Cambridge (2020)
Kurtonina, N., Moortgat, M.: Structural control. In: Blackburn, P., de Rijke, M. (eds.) Specifying Syntactic Structures, pp. 75–113. CSLI, Stanford (1997)
Lambek, J.: The mathematics of sentence structure. Am. Math. Mon. 65, 154–170 (1958). https://doi.org/10.1080/00029890.1958.11989160
Lambek, J.: Categorial and categorical grammars. In: Oehrle, R.T., Bach, E., Wheeler, D. (eds.) Categorial Grammars and Natural Language Structures. Studies in Linguistics and Philosophy, vol. 32, pp. 297–317. Reidel, Dordrecht (1988)
Lincoln, P.: Deciding provability of linear logic formulas. In: Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 109–122. Cambridge University Press, Cambridge (1995)
Lincoln, P., Shankar, N.: Proof search in first-order linear logic and other cut-free sequent calculi. In: Proceedings of Logic in Computer Science (LICS’94), pp. 282–291. IEEE Computer Society Press (1994)
Montague, R.: The proper treatment of quantification in ordinary English. In: Thomason, R. (ed.) Formal Philosophy. Selected Papers of Richard Montague. Yale University Press, New Haven (1974)
Moortgat, M.: Multimodal linguistic inference. J. Log. Lang. Inf. 5(3–4), 349–385 (1996). https://doi.org/10.1007/BF00159344
Moot, R.: Extended Lambek calculi and first-order linear logic. In: Casadio, C., Coecke, B., Moortgat, M., Scott, P. (eds.) Categories and Types in Logic, Language, and Physics: Essays dedicated to Jim Lambek on the Occasion of this 90th Birthday. Lecture Notes in Artificial Intelligence, vol. 8222, pp. 297–330. Springer, Berlin (2014). https://doi.org/10.1007/978-3-642-54789-8_17
Moot, R., Piazza, M.: Linguistic applications of first order multiplicative linear logic. J. Log. Lang. Inf. 10(2), 211–232 (2001). https://doi.org/10.1023/A:1008399708659
Morrill, G., Valentin, O., Fadda, M.: The displacement calculus. J. Log. Lang. Inf. 20(1), 1–48 (2011). https://doi.org/10.1007/s10849-010-9129-2
Oehrle, R.T.: Term-labeled categorial type systems. Linguist. Philos. 17(6), 633–678 (1994). https://doi.org/10.1007/BF00985321
Oehrle, R.T.: Multi-modal type-logical grammar. In: Borsley, R., Börjars, K. (eds.) Non-transformational Syntax: Formal and Explicit Models of Grammar, pp. 225–267. Wiley-Blackwell, Hoboken (2011)
OEIS Foundation: On-line encyclopedia of integer sequences (OEIS). http://oeis.org (1964). Accessed 23 Jul 2020
Seki, H., Matsumura, T., Fujii, M., Kasami, T.: On multiple context-free grammars. Theor. Comput. Sci. 88, 191–229 (1991). https://doi.org/10.1016/0304-3975(91)90374-B
Wijnholds, G.: Investigations into categorial grammar: symmetric pregroup grammar and displacement calculus. Master’s thesis, Utrecht University (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Moot, R. (2021). Partial Orders, Residuation, and First-Order Linear Logic. In: Loukanova, R. (eds) Natural Language Processing in Artificial Intelligence—NLPinAI 2020. Studies in Computational Intelligence, vol 939. Springer, Cham. https://doi.org/10.1007/978-3-030-63787-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-63787-3_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-63786-6
Online ISBN: 978-3-030-63787-3
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)