The lambda calculus, introduced by Alonzo Church in the 1930s as a foundation for mathematical logic, has become the indispensable tool for compositional semantics in both linguistics and computational linguistics. In semantic analysis, lambda expressions represent functions that take arguments and return values, enabling the systematic assembly of sentence meanings from word meanings through the operations of function application (beta-reduction) and lambda abstraction. Virtually every formal semantic framework uses lambda calculus as its compositional mechanism.
Lambda Abstraction and Application
Function application (beta-reduction):
(lambda x . love(x, j))(m) →_β love(m, j)
Example derivation for "Mary loves John":
⟦loves⟧ = lambda y . lambda x . love(x, y)
⟦loves John⟧ = lambda x . love(x, j)
⟦Mary loves John⟧ = love(m, j)
In a typed lambda calculus, every expression has a type. Basic types include e (entities) and t (truth values). Complex types are built with the arrow constructor: a transitive verb has type ⟨e, ⟨e, t⟩⟩, meaning it takes an entity argument and returns a function from entities to truth values. This type discipline ensures that only semantically well-formed combinations are permitted, mirroring the constraints of syntactic combination.
Compositionality via Lambda
Lambda calculus makes the Principle of Compositionality computationally explicit. Each lexical item is assigned a lambda expression as its meaning. Syntactic combination rules trigger semantic combination, typically function application: if node A has meaning f of type ⟨a, b⟩ and node B has meaning x of type a, then the combination AB has meaning f(x) of type b. This simple rule, augmented with a few additional operations like predicate modification and lambda abstraction for movement, suffices to derive the meanings of a remarkable range of English constructions.
In computational semantics, lambda calculus serves as the target meaning representation for semantic parsers. Systems like those of Zettlemoyer and Collins (2005) learn to map sentences to lambda-calculus expressions that can be evaluated against databases. The lambda DCS (Dependency-based Compositional Semantics) of Liang (2013) simplifies the lambda calculus interface for question answering. Even neural semantic parsers often produce lambda-calculus-like logical forms as their output, leveraging the compositionality of the formalism.
Extensions and Variants
Several extensions of the basic lambda calculus have been developed for linguistic semantics. The simply typed lambda calculus used in Montague Grammar has been augmented with polymorphic types, dependent types, and subtyping to handle more complex phenomena. Linear lambda calculus, which requires that every variable be used exactly once, underlies Glue Semantics and captures resource sensitivity in meaning composition. Continuation-passing transforms provide elegant treatments of quantifier scope, focus, and other phenomena involving non-local semantic dependencies.
The lambda calculus also connects formal semantics to computation theory. The Curry-Howard correspondence relates logical proofs to lambda terms, linking semantic derivations to computational processes. This correspondence has been exploited in type-logical grammar, where syntactic derivations are proofs in a substructural logic and semantic interpretations are the corresponding lambda terms, providing a deep unification of syntax, semantics, and computation.