A Lean 4 adaptation of Computational Semantics with Functional Programming, by Jan van Eijck and Christina Unger (Cambridge University Press, 2010) — inspired by the book's path through the material, not a translation of it. Definitions are rewritten from scratch in idiomatic Lean, exercises are code or proofs, and the presentation is reorganized wherever Lean's own resources (dependent types, tactics, formal proof) call for a different order or a different exercise than the original Haskell allowed.
It follows van Eijck & Unger but diverges whenever adapting to Lean or to this course asks for it — see Deviations from CSwFP below.
Exercises live inside each chapter, right where the corresponding book section is discussed — see Exercises below.
To run locally: install Lean, then
lake exe cache get(downloads prebuilt Mathlib — without it, lake build would compile
the whole library from scratch) and lake build.
Or, to build and browse the book locally:
make serve # serves at http://127.0.0.1:8000/In the order the book presents them, which is not the order of the source it adapts — see DEVIATIONS.md for why.
- The formal study of natural language — source
- Introduction to Lean — source
- [~] Morphology (Finnish vowel harmony, Swedish plural, phonemes) —
source (sections in
CSwL/Morphology/) - [~] Grammars for games (Sea Battle, Mastermind) —
source (sections in
CSwL/Games/) - [~] Logics (propositional and predicate) — source
(sections in
CSwL/Logic/) - [~] Sets and relations — source
- [~] An inference engine — source
- [~] A fragment of English — source
- Model checking with predicate logic —
CSwL/ModelChecking.lean - The composition of meaning
- Extension and intension
- Parsing
- Relations and scope
- Semantics in continuation passing style
- Discourse representation and context
- Communication as informative action
Exercises live inside the file for the section they correspond to (see
Chapters and Conventions), right after the book
section. Each sorry is an item left to complete (or example, for
exercises not reused later in the chapter itself).
Mnemonic file names. A short chapter is a single file (CSwL/Sets.lean,
namespace Sets); a chapter whose sections are long enough to deserve
their own file is a "glue" file (CSwL/Games.lean) that only gathers, via
{include 1 ...}, sections living in a same-named directory
(CSwL/Games/SeaBattle.lean, CSwL/Games/Mastermind.lean) — the same pattern
used by Functional Programming in Lean. Each content file has its own namespace,
mnemonic and necessary: the book redefines the same names in different chapters.
CSwL developments connect with those in CSLib where possible. We aim to reuse CSLib and contribute to CSLib.
CSwL is inspired by CSwFP, not a 1-to-1 port of it: chapters get
renumbered, sections and exercises get reordered, adapted or added,
whenever presenting the material well in Lean or in this course asks
for it. See DEVIATIONS.md for the detailed,
chapter-by-chapter log of where and why.
The book is © Jan van Eijck and Christina Unger, 2010, Cambridge University Press. This repository is an independent, adapted work: original code and prose, inspired by the book's themes and order but not a translation or reproduction of its text.