Lambda Calculus for Natural Language Semantics

Why This Matters

Formal semantics — the project of assigning truth-conditional meanings to natural-language sentences — needs a precise combinatorial calculus for assembling the meaning of a sentence from the meanings of its parts. Frege's principle of compositionality says the meaning of a complex expression is a function of the meanings of its parts and the way they are combined; turning that principle into actual computation requires a formal language for parts (lexical meanings) and ways they are combined (composition rules).

The simply-typed lambda calculus (Church 1940) is the standard working substrate. Lexical meanings are typed lambda terms; syntactic combination is function application; the result is a truth-conditional representation of the whole sentence. This is the framework Montague used in his Proper Treatment of Quantification (1973) and that Heim and Kratzer (1998) codified into the textbook method that almost every contemporary graduate program in formal semantics teaches first.

The same machinery underwrites a surprising amount of contemporary ML and CS: dependent-type theory in proof assistants (Coq, Lean, Agda); the type systems of functional programming languages (ML, Haskell, OCaml); the semantics of programming languages generally; and the type-theoretic interpretations of transformer architectures and category-theoretic accounts of attention. Understanding the lambda calculus as it is used in semantics is the cleanest way to see the bridge between formal linguistics and formal computer science.

The Type System: e and t

Two basic types suffice to start.

Definition

Basic types in semantics

Type $e$ (for entity): the type of individuals. The denotations of names like Mary and Plato are objects of type $e$ .
Type $t$ (for truth value): the type of truth values $\{0, 1\}$ or equivalently $\{F, T\}$ . The denotation of a sentence is an object of type $t$ .

Definition

Function types

If $\alpha$ and $\beta$ are types, then $\langle \alpha, \beta \rangle$ is a type — the type of functions from $\alpha$ -objects to $\beta$ -objects.

The set of types is closed under this construction: starting from $e$ and $t$ , the function-type closure produces $\langle e, t \rangle$ , $\langle e, \langle e, t \rangle \rangle$ , $\langle \langle e, t \rangle, t \rangle$ , and so on indefinitely.

The two basic types and the function-type construction yield exactly the types needed to assemble standard syntactic categories into compositional meaning representations.

Syntactic category	Semantic type	Example denotations
Proper noun	$e$	$\textit{Mary}$ , $\textit{Plato}$
Sentence	$t$	$\textit{Mary smiles}$ has truth value 1 if and only if Mary smiles
Intransitive verb	$\langle e, t \rangle$	$\textit{smiles}$ takes an entity and returns a truth value
Common noun	$\langle e, t \rangle$	$\textit{dog}$ takes an entity and returns 1 iff that entity is a dog
Transitive verb	$\langle e, \langle e, t \rangle \rangle$	$\textit{loves}$ takes an entity (object) then an entity (subject) and returns a truth value
Determiner	$\langle \langle e, t \rangle, \langle \langle e, t \rangle, t \rangle \rangle$	$\textit{every}$ , $\textit{some}$ , $\textit{no}$
Generalized quantifier (NP)	$\langle \langle e, t \rangle, t \rangle$	$\textit{every dog}$ , $\textit{some cat}$
Adjective (intersective)	$\langle e, t \rangle$	$\textit{brown}$ takes an entity and returns 1 iff that entity is brown

The type assignment is partly empirical (we observe what kinds of arguments different categories take) and partly theoretical (generalized quantifiers must be high-typed because they bind into sentences). The types fall out of the syntactic structure under the standard composition rule below.

Lambda Notation and Function Application

Lambda terms are written $\lambda x . M$ where $x$ is a variable and $M$ is a term. The intended reading is "the function that takes $x$ and returns $M$ ."

Definition

Lambda abstraction

If $M$ is a term of type $\beta$ and $x$ is a variable of type $\alpha$ , then $\lambda x . M$ is a term of type $\langle \alpha, \beta \rangle$ .

Definition

Function application

If $f$ is a term of type $\langle \alpha, \beta \rangle$ and $a$ is a term of type $\alpha$ , then $f(a)$ is a term of type $\beta$ .

Beta-reduction: $(\lambda x . M)(a) \rightsquigarrow M[x := a]$ where $M[x := a]$ is the result of substituting $a$ for every free occurrence of $x$ in $M$ (with appropriate variable renaming to avoid capture).

The sole composition rule for sentence-meaning assembly in the basic Heim-Kratzer method is functional application: when one sister node has type $\langle \alpha, \beta \rangle$ and the other has type $\alpha$ , the parent has type $\beta$ and its denotation is the application of the first to the second.

That single rule, plus the lexicon and the syntactic tree, produces the truth conditions of an entire class of sentences. The cases that resist this single rule (binding, scope ambiguity, donkey anaphora, presupposition projection) require additional composition rules and motivate the rest of the formal-semantics curriculum.

Worked Example 1: A Simple Sentence

Take Mary smiles. The lexicon assigns:

$\llbracket \textit{Mary} \rrbracket = m$ , of type $e$ (the individual Mary).
$\llbracket \textit{smiles} \rrbracket = \lambda x_e . \textit{smile}(x)$ , of type $\langle e, t \rangle$ (the function that maps an entity $x$ to 1 iff $x$ smiles).

The syntactic tree has Mary as the subject (NP) and smiles as the predicate (VP). Functional application gives:

\llbracket \textit{Mary smiles} \rrbracket = \llbracket \textit{smiles} \rrbracket (\llbracket \textit{Mary} \rrbracket) = (\lambda x . \textit{smile}(x))(m) \rightsquigarrow \textit{smile}(m).

The truth value is 1 iff Mary smiles, which is the intended result.

Worked Example 2: A Transitive Verb

Mary loves Plato. The lexicon adds:

$\llbracket \textit{Plato} \rrbracket = p$ , of type $e$ .
$\llbracket \textit{loves} \rrbracket = \lambda y_e . \lambda x_e . \textit{love}(x, y)$ , of type $\langle e, \langle e, t \rangle \rangle$ .

The transitive verb is Curried in the standard way: it takes the object first and then the subject. Composition:

\llbracket \textit{loves Plato} \rrbracket = \llbracket \textit{loves} \rrbracket(\llbracket \textit{Plato} \rrbracket) = (\lambda y . \lambda x . \textit{love}(x, y))(p) \rightsquigarrow \lambda x . \textit{love}(x, p).

The verb-phrase denotation is now of type $\langle e, t \rangle$ , the same type as an intransitive verb. The full sentence:

\llbracket \textit{Mary loves Plato} \rrbracket = \llbracket \textit{loves Plato} \rrbracket(\llbracket \textit{Mary} \rrbracket) = (\lambda x . \textit{love}(x, p))(m) \rightsquigarrow \textit{love}(m, p).

The Curried form lets the same composition rule (functional application) handle both arguments of the verb, one at a time. No new rule is needed. This is the cleanest exhibit of why types are load-bearing in the semantic enterprise: types tell us what combines with what.

Generalized Quantifiers

The hard cases for the type assignment above are noun phrases like every dog, some cat, and no senator. These cannot have type $e$ — there is no single individual that is "every dog." The standard solution (Barwise and Cooper 1981; codified in Heim- Kratzer) types determiners as functions that take a common noun (type $\langle e, t \rangle$ ) and return a generalized quantifier of type $\langle \langle e, t \rangle, t \rangle$ .

Determiner	Lambda denotation	Type
$\textit{every}$	$\lambda P_{\langle e,t \rangle} . \lambda Q_{\langle e,t \rangle} . \forall x . P(x) \to Q(x)$	$\langle \langle e, t \rangle, \langle \langle e, t \rangle, t \rangle \rangle$
$\textit{some}$	$\lambda P . \lambda Q . \exists x . P(x) \wedge Q(x)$	same
$\textit{no}$	$\lambda P . \lambda Q . \neg \exists x . P(x) \wedge Q(x)$	same
$\textit{most}$	$\lambda P . \lambda Q . \lvert P \cap Q \rvert > \lvert P \setminus Q \rvert$	same (essentially)

The composition for every dog smiles runs:

\llbracket \textit{every dog} \rrbracket = \llbracket \textit{every} \rrbracket(\llbracket \textit{dog} \rrbracket) \rightsquigarrow \lambda Q . \forall x . \textit{dog}(x) \to Q(x).

Then:

\llbracket \textit{every dog smiles} \rrbracket = \llbracket \textit{every dog} \rrbracket(\llbracket \textit{smiles} \rrbracket) \rightsquigarrow \forall x . \textit{dog}(x) \to \textit{smile}(x).

This is the desired truth condition.

The generalized-quantifier story neatly explains several linguistic phenomena that resisted earlier accounts:

Conservativity: every natural-language determiner's truth value depends only on the intersection $P \cap Q$ , not on the rest of the domain. Conservativity is a typological universal with strong empirical support and falls out structurally from the lambda denotation.
Monotonicity: licensors of negative-polarity items (e.g., anyone) are precisely the downward-monotonic generalized quantifiers. The lattice-theoretic fact that no senator is downward monotonic predicts and explains the licensing asymmetry.
Scope ambiguity: Every senator voted for some bill has two readings (every-over-some vs some-over-every). The lambda calculus alone does not generate both readings; standard treatments add a quantifier raising movement rule or an alternative composition mechanism (continuations, type-shift).

Heim-Kratzer Composition Rules Beyond Functional Application

The single rule (functional application) handles a large fraction of sentences but not all. Standard extensions:

Predicate Modification: when two sisters both have type $\langle e, t \rangle$ , the parent has type $\langle e, t \rangle$ with denotation $\lambda x . \llbracket A \rrbracket(x) \wedge \llbracket B \rrbracket(x)$ . This handles intersective adjectives: brown dog combines brown and dog both of type $\langle e, t \rangle$ .
Predicate Abstraction: a movement trace creates a binder index that licenses lambda abstraction over the trace position. This handles relative clauses (the dog that Mary loves), wh-questions, and binding generally.
Intensional Functional Application: the type system extends to include a type $s$ for possible worlds; intensions are functions from worlds to extensions; intensional contexts (modals, attitude verbs, propositional attitudes) require composition relative to a world parameter.

The Heim-Kratzer textbook (1998) codifies these rules. Most contemporary formal-semantics work uses some refinement of the HK system; alternative frameworks (categorial grammar with the Lambek calculus, dependent-type semantics, Montague's PTQ fragment) substitute different composition machinery but share the lambda-calculus substrate.

ML and CS Connections

The simply-typed lambda calculus is everywhere in computer science.

Functional programming. ML, Haskell, OCaml are simply-typed lambda calculi extended with sum types, recursion, and effect systems. The semantic-types-and-composition story translates: where formal semantics has $\langle e, t \rangle$ , Haskell has Entity -> Bool. Programmers writing parser combinators or type-driven semantic interpreters are directly using the linguistic-semantics formalism.

Dependent-type theory. Coq, Lean, Agda extend the simply- typed lambda calculus with dependent types (types that can depend on values). The Curry-Howard correspondence identifies propositions with types and proofs with lambda terms, making the lambda calculus simultaneously a programming language and a proof system. Recent dependent-type-theory accounts of natural- language semantics (Bekki's Dependent Type Semantics, Ranta's type-theoretical grammar) fuse the linguistic and CS uses.

Category-theoretic semantics. The lambda calculus is the internal language of cartesian closed categories. Compositional semantics in the Coecke-Sadrzadeh-Clark distributional- compositional framework reads exactly as a tensor-network analog of the lambda-calculus story.

Transformer interpretation. Some recent mechanistic- interpretability papers (Olsson et al. 2022 on induction heads; the broader copy-circuit / arithmetic-circuit literature) analyze transformer behavior using language that maps onto function-application chains. The mapping is more impressionistic than formal at present, but the conceptual link — transformers as performing repeated typed combination of contextually-supplied functions — is recognizable.

Probabilistic semantics. Probabilistic programming languages (Church, Anglican, Pyro) extend the lambda calculus with sampling and conditioning; the linguistic literature on probabilistic truth-conditional semantics (Goodman-Lassiter pragmatics, RSA models) uses these languages directly to model meaning.

Common Mistakes

Watch Out

Confusing semantic type with syntactic category

Syntactic categories (NP, VP, S) are theoretical constructs of generative syntax; semantic types are theoretical constructs of formal semantics. The two correspond systematically (NP -> e or generalized-quantifier; VP -> intransitive predicate; S -> t) but are not the same kind of object. A page that confuses them is making a category error in the most literal sense.

Watch Out

Treating functional application as 'the only rule'

Functional application handles a large but bounded fragment. Predicate Modification, Predicate Abstraction, intensional contexts, focus, anaphora, presupposition all require additional machinery. A semantics page that uses only functional application is staying inside the easy fragment.

Watch Out

Thinking the lambda calculus 'gives the meaning' of words

The lambda calculus gives a combinatorial representation. The lexical denotations $\textit{smile}(\cdot)$ , $\textit{love}(\cdot, \cdot)$ , $\textit{dog}(\cdot)$ are primitive — the framework does not explain what makes someone smile or what makes a dog a dog. Lexical semantics, conceptual structure, and grounding are separate projects; the lambda calculus is the glue that combines them, not the explanation of any individual lexical item.

Watch Out

Conflating Curry-style and Church-style typing

Curry-style (implicit) typing infers types from terms; Church- style (explicit) typing annotates each variable with its type. Linguistic semantics is overwhelmingly Church-style: types are written, lexical entries declare types, and composition rules are type-driven. CS literature uses both. The distinction matters in type-theoretic discussions but not in the semantics-textbook worked examples.

Exercises

ExerciseCore

Problem

Compute the type and the lambda-term denotation of every brown dog ran. Use the determiner denotation $\llbracket \textit{every} \rrbracket = \lambda P . \lambda Q . \forall x . P(x) \to Q(x)$ , the adjective denotation $\llbracket \textit{brown} \rrbracket = \lambda x . \textit{brown}(x)$ , and the noun-modification rule (Predicate Modification).

ExerciseCore

Problem

Show that every and no are conservative: their truth values depend only on the intersection of their two arguments. Specifically, prove that for any sets $A$ and $B$ ,

\llbracket \textit{every} \rrbracket(A)(B) = \llbracket \textit{every} \rrbracket(A)(A \cap B).

ExerciseAdvanced

Problem

Every senator voted for some bill is ambiguous between two readings: (a) every senator voted for some bill or other (the bills can differ across senators); (b) there is some specific bill that every senator voted for. Functional application alone does not generate both. Sketch the quantifier raising analysis that gives both readings.

ExerciseResearch

Problem

Compositional distributional semantics (Coecke-Sadrzadeh-Clark) maps the simply-typed lambda calculus into a tensor-network calculus where types correspond to vector-space dimensions and function application corresponds to tensor contraction. Sketch how a transitive verb $\langle e, \langle e, t \rangle \rangle$ becomes a 3-tensor, and discuss the empirical limitations of this approach.

Formalization Note

The simply-typed lambda calculus is implemented as the foundation of Lean, Coq, and Agda. Linguistic-semantics formalizations exist in all three:

Coq: the Grammatical Framework tradition (Ranta) and the Coq formalizations of generalized-quantifier theory (de Groote, Asudeh) provide working semantics fragments.
Agda: dependent-type semantics for natural language (Bekki's DTS) is implemented in Agda.
Lean: Mathlib4 has the lambda-calculus type theory at its core but does not yet have a dedicated linguistic-semantics library. The pieces needed (Heim-Kratzer composition rules, generalized-quantifier inventory, predicate-modification rule) would be a clean portfolio formalization project at the Lean 4 level.

For a working formalization of the kind of derivations in this page, Coppock and Champollion's draft Invitation to Formal Semantics (2024) provides Coq-companion code that works through the Heim-Kratzer fragment. The Grammatical Framework (Ranta) is the production-grade tool for typed-lambda-calculus semantics in a multilingual setting and is used in machine-translation research projects beyond the academic semantics community.

Cross-Network Links

TheoremPath (parallel content): the lambda calculus appears in several TheoremPath pages — the type-theory pages, the programming-languages-as-ML-foundations pages, and the category-theory pages. The semantic use described here is the linguistic application of the same formal object.
ProofsPath: type theory and the Curry-Howard correspondence are foundational logic content; ProofsPath's cauchy-functional-equation page exhibits the plainest functional-equation-meets-type-theory connection.
ComputationPath: formal grammars, computational- complexity classes for typed-lambda-calculus reduction, and the programming-language-semantics tradition all live there; LinguisticsPath's lambda-calculus page is the natural-language-meaning side of the same coin.

References

Canonical:

Heim, Irene, and Angelika Kratzer. Semantics in Generative Grammar (1998), Chapters 2-4.
Montague, Richard. "The Proper Treatment of Quantification in Ordinary English." Approaches to Natural Language (1973) 221-242.
Partee, Barbara H., Alice ter Meulen, and Robert E. Wall. Mathematical Methods in Linguistics (1990), Chapters 13-14.
Carpenter, Bob. Type-Logical Semantics (1997).
Coppock, Elizabeth, and Lucas Champollion. Invitation to Formal Semantics (2024 draft).

Logic and Type Theory:

Church, Alonzo. "A Formulation of the Simple Theory of Types." Journal of Symbolic Logic 5 (1940) 56-68.
Barendregt, Henk P. The Lambda Calculus: Its Syntax and Semantics (1984, revised ed.).
Pierce, Benjamin C. Types and Programming Languages (2002), Chapters 9-11.
Moot, Richard, and Christian Retore. The Logic of Categorial Grammars (2012).