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/- The formal study of natural language — source
- Introduction to Lean — source
- [~] Applications (Finnish vowel harmony, Swedish plural, phonemes) —
source (sections in
CSwL/Applications/) - [~] Foundations — source
- [~] Grammars for games (Sea Battle, Mastermind) —
source (sections in
CSwL/Games/) - [~] A fragment of English — source
- [~] Logics (propositional and predicate) — source
(sections in
CSwL/Logic/) - Formal semantics of fragments
- Model checking with predicate logic
- 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/Foundation.lean,
namespace Foundation); 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 get reordered or added, exercises get reworded or replaced, 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.