Polarized Classical Non-associative Lambek Calculus and Formal Semantics

  • Arno Bastenhof
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6736)


While initially motivated for studying natural language syntax, the intuitionistic bias underlying traditional Lambek calculi renders them particularly suitable to a Montagovian formal semantics through the Curry-Howard correspondence. Several recent proposals, however, have departed from the intuitionistic tradition, seeking instead to formulate ‘classical’ Lambek calculi. We show that this classical turn need not come at the cost of the tight connection with formal semantics, concentrating on De Groote and Lamarche’s Classical Non-Associative Lambek calculus (CNL). Our work is founded in Girard’s and Andreoli’s research into polarities and focused proofs, suggesting the definition of polarized CNL, its connection to De Groote and Lamarche’s original proposal explicated through the use of phase spaces. We conclude with a discussion of related literature, particularly Moortgat’s Lambek-Grishin calculus.


Formal Semantic Linear Logic Double Negation Sequent Calculus Lexical Semantic 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297–347 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Belnap, N.: Display logic. Journal of Philosophical Logic 11(4), 375–417 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bernardi, R., Moortgat, M.: Continuation semantics for the Lambek-Grishin calculus. Information and Computation 208(5), 397–416 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Coquand, C.: From semantics to rules: a machine assisted analysis. In: Börger, E., Gurevich, Y., Meinke, K. (eds.) CSL 1993. LNCS, vol. 832, pp. 91–105. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  5. 5.
    Girard, J.Y.: A new constructive logic: classical logic. Mathematical Structures in Computer Science 1(3), 255–296 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Girard, J.Y.: On the meaning of logical rules II: multiplicatives and additives. In: Foundation of Secure Computation, pp. 183–212. IOS Press, Amsterdam (2000)Google Scholar
  7. 7.
    De Groote, P., Lamarche, F.: Classical non associative Lambek calculus. Studia Logica 71, 355–388 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Hendriks, H.: Studied flexibility. Categories and types in syntax and semantics. Ph.D. thesis, ILLC Amsterdam (1993)Google Scholar
  9. 9.
    Hepple, M.: Normal form theorem proving for the Lambek calculus. In: COLING, pp. 173–178 (1990)Google Scholar
  10. 10.
    Herbelin, H., Lee, G.: Forcing-based cut-elimination for gentzen-style intuitionistic sequent calculus. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds.) WoLLIC 2009. LNCS, vol. 5514, pp. 209–217. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Montague, R.: Universal grammar. Theoria 36(3), 373–398 (1970)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Moortgat, M.: Symmetric categorial grammar. Journal of Philosophical Logic 38(6), 681–710 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theoretical Computer Science 281(1-2), 471–498 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Prawitz, D.: Natural Deduction. Dover Publications, New York (2006)zbMATHGoogle Scholar
  15. 15.
    Wadler, P.: A taste of linear logic. In: Borzyszkowski, A., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 185–210. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  16. 16.
    Lafont, Y., Reus, B., Streichter, T.: Continuation semantics or expressing implication by negation. Technical Report 93-21, University of Munich (1993)Google Scholar
  17. 17.
    Yetter, D.: Quantales and (noncommutative) linear logic. Journal of Symbolic Logic 55(1), 41–64 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Zeilberger, N.: The logical basis of evaluation order and pattern-Matching. Ph.D. thesis, Carnegie Mellon University (2009)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Arno Bastenhof
    • 1
  1. 1.Utrecht UniversityThe Netherlands

Personalised recommendations