I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach), yet there aren't many resources that provide an overview of this very technical field. I wish to be able to provide myself a general map to navigate this subject more clearly, so I will attempt explain my basic understanding of an overview of the fields that tackle with this subject, and I'd greatly appreciate any correction or addition to my limited insight.

From my understanding, (loosely speaking) there are two prominent mathematical-logical approaches in formalizing natural languages: Categorial Grammar and Montague Semantics. While Categorial Grammar uses methods borrowed from category theory to (mainly) study the syntax of natural languages, Montague Semantics, as the name might suggest, (mainly) focuses on the semantics of natural languages by implementing methods from Lambda Calculus. In terms of subareas of each of these two fields, I have not seen much discussed in terms of the subareas of Montague Semantics; however, Categorial Grammar seems ripe with subareas (although I have heard some of the fields mentioned below are only closely related to Categorial Grammar rather than being a strict subfield of it):

  1. Combinatory Categorial Grammar (CCG)
  2. Lambek Calculus
  3. Type-Logical Grammar
  4. Pre-Group Grammar
  5. Proof-Theoretic Semantics

In addition to any corrections or additions, I would greatly appreciate any suggestions for resources, references or books that deal with these subjects or their prerequisites.

4 Answers 4


Seconding the Kornai stuff mentioned above; it's all great.

Probably the seminal text here from the point of view of relatively modern linguistics would be Partee's 1993 book, which while somewhat old will definitly give a good overview:



There’s probably a good encyclopedia article or handbook on mathematical linguistics, Andras Kornai wrote some books on this.

You might like this blog post. https://blog.juliosong.com/linguistics/mathematics/a-new-application-of-category-theory-in-linguistics-part-1/

Or ncatlab: https://ncatlab.org/nlab/show/formal+grammar

or this blog post: https://golem.ph.utexas.edu/category/2018/02/linguistics_using_category_the.html

It’s a pretty big topic.

I’m trying to study topos theory which is a categorical treatment of logic, which I understand will take many years.

Here’s an entire bibliography on mathematical linguistics: https://www.oxfordbibliographies.com/display/document/obo-9780199772810/obo-9780199772810-0029.xml

This is a shorter overview by Andras Kornai and Geoffrey Pullum: https://www.kornai.com/MatLing/matling3.pdf


I’m a grad student in mathematics doing research in Formal Semantics.

Work in the Montague Semantics pulls upon a lot more than just Lambda Calculus. There’s a lot of work with non-standard logic (Kripke semantics for modal logic being a typical jumping off point into what is a very wide and exotic sea of logic).

In a nutshell the goal is to construct formal languages which act as reasonable facsimiles of a natural language, and then studying the models of those languages and the truth conditions therein. In many ways we actually start with the truth conditions and then work backwards.

If you’re interested, the text I used to teach myself the foundations was Introduction to Montague Semantics, by Dowty et Al. It assumes a fair amount of mathematical maturity so it should be of appropriate rigor for someone with a background in Mathematics.


Before pointing to some literature I want to clarify the interaction between Montague semantics and categorial grammar:

Montague semantics is intimately related to categorial grammar. Indeed, one the most widely used kinds of categorial grammar is the Lambek calculus, which is an implication fragment of intuitionistic logic that serves to assign categories to strings. The crucial thing is that via the Curry-Howard isomorphism formulas can be taken to be types of the simply typed lambda calculus and proofs can be considered as lambda terms. Roughly speaking, Montague semantics arises from the Lambek calculus in the form of its associated term calculus (for this terminology see Troelstra / Schwichtenberg: Basic Proof Theory)

That said here are some recommendations:

There is a nice SEP-entry on type logical grammar (to which the Lambek calculus belongs)


There are several textbooks on the Lambek calculus and type logical semantics aka Montague semantics:

Bob Carpenter: Type-Logical Semantics (linguistically oriented, but rigorous)

Glyn Morril: Categorial Grammar (linguistically oriented, but also including logical material on proof nets)

Moot / Retore: The Logic of Categorial Grammars (logically oriented)

Chatzikyriakidis / Luo: Formal Semantics in Modern Type Theories (linguistically oriented, using stronger type theories than the simply typed lambda calculus)

Combinatorial Categorial Grammar, which uses typed combinatory logic instead of the lambda calculus, is presented quite accessibly in Steedman: Surface Structure and Interpretation

Finally, there is the venerable Handbook of Logic and Language, where the articles by Partee / Hendriks, Moortgat and Buszkowski are of direct relevance to your interests.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.