Dialectica Categories for the Lambek Calculus

  • Valeria de PaivaEmail author
  • Harley EadesIII
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a \(\kappa \) modality, inspired by Yetter’s work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present the categorical semantics, proved sound and complete. Finally we show the traditional properties of type systems, like subject reduction, the Church-Rosser theorem and normalization for the calculi of extended modalities, which we did not have before.


Lambek calculus Dialectica models Categorical semantics Type theory Structural rules Non-commutative Linear logic 



The authors would like to thank the anonymous reviewers for their feedback which did make this a better paper. The second author was partially supported by the NSF grant #1565557.


  1. 1.
    Abramsky, S.: Proofs as processes. Theor. Comput. Sci. 135(1), 5–9 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Benton, N., Bierman, G., de Paiva, V., Hyland, M.: A term calculus for Intuitionistic Linear Logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 75–90. Springer, Heidelberg (1993). CrossRefGoogle Scholar
  3. 3.
    Benton, P.N.: Strong normalisation for the linear term calculus. J. Funct. Program. 5(1), 65–80 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bierman, G.M.: On Intuitionistic Linear Logic. PhD thesis, Wolfson College, Cambridge, December 1993Google Scholar
  5. 5.
    Bierman, G.M., de Paiva, V.C.V.: On an intuitionistic modal logic. Stud. Logica 65(3), 383–416 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda-a functional language with dependent types. TPHOLs 5674, 73–78 (2009)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Ciabattoni, A., Galatos, N., Terui, K.: Algebraic proof theory for substructural logics: Cut-elimination and completions. Ann. Pure Appl. Logic 163(3), 266–290 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Coecke, B., Grefenstette, E., Sadrzadeh, M.: Lambek vs. Lambek: Functorial vector space semantics and string diagrams for Lambek calculus. Ann. Pure Appl. Logic 164(11), 1079–1100 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    de Paiva, V.: The dialectica categories. PhD thesis, Computer Laboratory, University of Cambridge, PhD Thesis, 1990. Computer Laboratory, University of Cambridge, PhD Thesis (1990)Google Scholar
  10. 10.
    de Paiva, V.: A Dialectica model of the Lambek calculus. In: 8th Amsterdam Logic Colloquium (1991)Google Scholar
  11. 11.
    De Paiva, V.: Dialectica and chu constructions: Cousins? Theory Appl. Categories 17(7), 127–152 (2007)zbMATHGoogle Scholar
  12. 12.
    Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Greco, G., Palmigiano, A.: Linear Logic Properly Displayed. ArXiv e-prints, November 2016Google Scholar
  14. 14.
    Honda, K., Laurent, O.: An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Compu. Sci. 411(22), 2223–2238 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Hyland, M., de Paiva, V.: Full intuitionistic linear logic (extended abstract). Ann. Pure Appl. Logic 64(3), 273–291 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Barry Jay, C.: Coherence in category theory and the Church-Rosser property. Notre Dame J. Formal Logic 33(1), 140–143 (1991). 12Google Scholar
  17. 17.
    Lafont, Y., Streicher, T.: Games semantics for linear logic. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, 1991, LICS 1991, pp. 43–50. IEEE (1991)Google Scholar
  18. 18.
    Lamarche, F., Retoré, C.: Proof nets for the Lambek calculus - an overview. In: Proceedings of the Third Roma Workshop. Proofs and Linguistic Categories, pp. 241–262 (1996)Google Scholar
  19. 19.
    Lambek, J.: The mathematics of sentence structure. In: American Mathematical Monthly, pp. 154–170 (1958)Google Scholar
  20. 20.
    Moortgat, M.: Typelogical grammar. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Spring 2014 edition (2014)Google Scholar
  21. 21.
    Polakow, J.: Ordered linear logic and applications. PhD thesis, Carnegie Mellon University (2001)Google Scholar
  22. 22.
    Pratt, V.R.: Types as processes, via Chu spaces. Electr. Notes Theor. Comput. Sci. 7, 227–247 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Sewell, P., Nardelli, F., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: Effective tool support for the working semanticist. J. Funct. Program. 20, 71–122 (2010)CrossRefzbMATHGoogle Scholar
  24. 24.
    Szabo, M.E.: Algebra of Proofs. Studies in Logic and the Foundations of Mathematics, vol. 88, North-Holland (1978, 1979)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Nuance CommunicationsSunnyvaleUSA
  2. 2.Computer ScienceAugusta UniversityAugustaUSA

Personalised recommendations