Repository navigation
feat(Composition): add the chapter from CSwFP/7.1–7.6 - #44
Merged
Merged
Conversation
Add CSwL/Composition.lean with the headings of 7.1–7.7, wire it into Book.lean, and map chapter 7's sections and 28 exercises in CSwFP.yaml, flagging the overlaps with InfEngine, IntroL and ModelChecking. Record in the style guides the :::terse/:::full pattern from sf-in-lean, starting with this chapter, and that a :::terse cue may be drafted by AI and approved by a human. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author.
Translate the chapter summary as the opening, with Lean in place of Haskell as the lambda-calculus engine of ModelChecking, and 7.1, all in :::full blocks; 7.1 has no code, so its heading is dropped from the terse variant. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author.
Translate the opening of 7.2, cutting to a reminder the two paragraphs that ModelChecking's english-form already covers, and the subsection on the relational view of quantifiers, with `every` as the chapter's first Lean code. Add Mostowski (1957) and Barwise and Cooper (1981) to Bib, record "escopo" for both scope and body in the term list, and record the departures in DEVIATIONS.md. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author.
The example needs ToString (Formula Term), which Logic/FOL does not have yet; the build is broken until that lands from main.
# Conflicts: # CSwL/ModelChecking.lean
Sections are now written terse first: AI-drafted :::terse cues and the Lean code come first, and each :::full block holds only a pending translation note until its prose is translated under review. The chapter's translated prose is cleared for consistency; the draft remains in the history. STYLE-CODE.md and STYLE-WRITING.md record the workflow. The dev note at the top of the chapter now holds the plan for the whole of CSwFP/7. In 7.2, "Every mermaid hummed a song" becomes "Every dwarf defeated a giant", which the ModelChecking model can evaluate, with `a` and `defeated` defined to compute it. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues, the Lean code and the style-guide changes; all of it was reviewed by a human author.
…ical representations Continue CSwFP/7.2 in terse-first form: - Conditions on quantifier relations: namespace GQ with Det, all, some, no, only, the conditions Ext, Cons and Isom, and exercises no-cons, only-not-cons, many-not-ext, the-quant and poss-not-isom. Terse cues distinguish the syntactic category DET from GQ.Det and explain in which sense the articles a and the are quantifiers. - Numerical trees: row, showTree and Figure 7.6 computed, with exercises tree-of-numbers (7.1) and gen-tree (7.3). - Logical representations for quantifiers: NumQuant, allNum, atLeastNum, notNum, andNum, orNum, with exercise tree-patterns (7.2). CSwFP.yaml maps the new exercises, DEVIATIONS.md records the finite tree of numbers, the argument order of Quant and the computed Figure 7.6, and STYLE-CODE.md adds the Composition row to the ledger. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues, the Lean code and the exercises; all of it was reviewed by a human author.
…e quantifier forms Rework "Numerical Trees" and the start of "Logical Representations for Quantifiers" in CSwFP/7.2: - The tree of numbers is built from `tree k`, the list of rows 0 to k. `labelTree` and `drawTree` draw it; `numberTree` labels it with the pairs and `patternTree` (formerly `showTree`) with `+` and `-`. `treeOfNumbers` (exercise 7.1) flattens it. - Exercise gen-tree (7.3) is written over `tree`, so it no longer depends on the solution of tree-of-numbers. - CSwFP's `Quant` becomes `ListQuant`, in parallel with `NumQuant`. `toNum` turns one into the other, and two theorems compare the patterns of `List.all` and *no* with `allNum` and `noNum`. - Both subsections use one cast of example quantifiers, announced at the start; `atleast2butnotall` becomes `atLeast3ButNotAll`. - Terse cues no longer refer to Haskell, to CSwFP's figures, or to what the next exercise asks. - AI-drafted explanations are kept as dev notes next to the pending translation notes. CSwFP.yaml drops the gen-tree dependency, and DEVIATIONS.md records the shared `tree`, the computed figures, `ListQuant`/`toNum` and the single cast. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues, the Lean code and the dev notes; all of it was reviewed by a human author.
Add the subsection "Relational Properties" of CSwFP/7.2 in terse-first form. Each property is defined over sets and over the tree pattern: - Reflexivity: GQ.Refl and ReflNum, with exercise some-not-refl and a quiz on irreflexivity. *Some* is not reflexive: the empty set, at the top of the tree, fails it. - Symmetry: GQ.Symm, with exercise symm-pattern (7.4). - Monotonicity in the scope: GQ.MonUp, GQ.MonDown, MonUpNum and MonDownNum, with exercises no-mon-down and even-not-mon, and exercises 7.5 and 7.6 as quizzes. - Negation, conjunction and disjunction: exercises mon-not (7.7), mon-and (7.8), mon-or (7.9) and mon-up-down (7.10). - Monotonicity in the restriction: exercise left-mon-pattern. The comp-conditions cue no longer cites a CSwFP figure. CSwFP.yaml maps exercises 7.4 to 7.10 and the new original exercises, and DEVIATIONS.md records the reflexivity of *some*, the two versions of each property, and why 7.5 and 7.6 became quizzes. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues, the Lean code, the exercises and the quizzes; all of it was reviewed by a human author.
Evaluate reflexivity and symmetry in the model of ModelChecking with `every` and `a`: an intransitive verb in both positions, an empty restriction (`nobody`) that separates every from a, and the inversion of restriction and scope for a and every. The symmetry cue adds more There-are-Q examples, and a dev note keeps the intransitive-verb examples as material for the translation. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues, the Lean code and the dev note; all of it was reviewed by a human author.
Drop the model examples with `nobody`, which the section does not need, and explain step by step why `Q A A` is the right edge of the tree. The irreflexivity quiz answer now shows the patterns of not all and no. An `#eval` of `someNum` is dropped: `someNum` is defined by an exercise, so it is `sorry` in the student variant and cannot be evaluated there. Also small cleanups in two proofs. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues and the code changes; all of it was reviewed by a human author.
Composition.lean becomes the chapter's glue, with the opening and one include per section, as in Logic and Morphology. Section 7.2 stays whole in Composition/Quantification.lean. The sections set no `file :=`, so the HTML is still one page and the generated project still has a single Composition.lean. This commit was prepared with the assistance of an AI tool (Claude Code), which split the file and checked the builds; the structure was decided by a human author.
A quantifier becomes a language of words over Bool: `wordOf` reads the
restriction against the scope, `langOf q` is a Mathlib `Language Bool`,
and `langOf_perm` shows it is closed under permutation. Negation is
complement; exercises `lang-and-or` and `all-kstar` show conjunction
as intersection, disjunction as union, and all as `{[true]}∗`.
Automata and definability stay in the cues; exercises 7.11 and 7.12
are omitted.
This commit was prepared with the assistance of an AI tool (Claude
Code), which drafted the terse cues, the Lean code and the proofs;
all of it was reviewed by a human author.
The automata of 7.2 were recorded as omitted, but they are deferred: CSwFP.yaml and DEVIATIONS.md now point to issue 41, which lists what is left. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the issue and the corrections; all of it was reviewed by a human author.
Lean is the typed logic: its types, lambda terms and evaluation are what IntroL presents with the lambda calculus, and Lean reduces and substitutes for the reader. No later section handles terms as data, and CSLib's lambda calculi do not fit (the named one is untyped, the typed one is locally nameless). The opening of 7.5 will say that e is Entity and t is Bool. Exercises 7.13–7.22 go with the sections. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the changes and the recorded reasons; the decision was made by a human author.
Each grammar rule gets its semantic rule as a Lean function in namespace `Rule`, named after the constructor it interprets: `sent`, `npName`, `npDet`, `rcnSubj`, `rcnObj`, `vpTrans` and `vpDitrans`, with the determiners `no` and `the`. The opening says that e is Entity and t is Bool. The reduction of Alice admired Dorothy is a theorem proved by `rfl` for any relation, and exercise `snow-white-helped` (7.24) asks for the same. Both 7.5 and 7.6 take the subject first, as the model does. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues, the Lean code and the proofs; all of it was reviewed by a human author.
intSent, intNP, intVP and intRCN interpret ModelChecking's syntax trees by recursion, one line per constructor, applying the rules of `Rule` to the lexicon (intCN, intADJ, intTV, intDV, intDET). An #eval checks that the direct interpretation agrees with the translation into a formula on the 32 sentences of `help-defeat`. Most, and at least / at most in exercise `at-least-at-most` (7.25), are meanings used through the rules, with no change to the grammar (issue 42). This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cues, the Lean code and the proofs; all of it was reviewed by a human author.
The example of 7.5 is interpreted again from its syntax tree, and an `rfl` shows that `intSent` builds the same composition that 7.5 wrote by hand. This commit was prepared with the assistance of an AI tool (Claude Code), which drafted the terse cue and the code; all of it was reviewed by a human author.
Remove the empty section on handling ambiguity and record it, with exercises 7.26-7.28, as deferred (issue 43). The 7.2 cue no longer points to it. check-cswfp.py accepts `deferred` as a section target. Claude Code (Opus 5.5) drafted these changes and this message under the author's direction; the author reviewed them.
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
Existing Lean examples are no longer checked or extracted as usable definitions, and the glue chapter’s page settings prevent the required separate section pages.
6 open issues
What changed in this PR
Adds the unfinished Composition chapter to the Lean/Verso textbook, extending ModelChecking with direct, compositional semantics. Automata and ambiguity remain deferred, and much of the full prose is still pending.
Changes:
- Introduces generalized quantifiers, numerical trees, relational properties, and quantifier languages.
- Adds typed semantic rules and a direct interpreter for the existing grammar.
- Integrates the chapter into the book and updates source mappings, bibliography, and authoring guidance.
| File | Description |
|---|---|
STYLE-WRITING.md |
Documents terse-cue drafting and quantifier terminology. |
STYLE-CODE.md |
Updates the feature ledger and terse-first authoring guidance. |
scripts/check-cswfp.py |
Adds chapter 7 exercise counts and deferred section targets. |
README.md |
Marks Composition as partially implemented. |
DEVIATIONS.md |
Records chapter adaptations, omissions, and deferred work. |
CSwL/ModelChecking.lean |
Expands a translation example and links to Composition. |
CSwL/Logic/PL.lean |
Adds spacing between connective definitions. |
CSwL/Composition/TypedMeanings.lean |
Defines typed semantic composition rules. |
CSwL/Composition/Rules.lean |
Introduces the compositionality principle. |
CSwL/Composition/Quantification.lean |
Develops quantifier conditions, trees, properties, and languages. |
CSwL/Composition/Interpretation.lean |
Implements direct interpretation and additional determiner meanings. |
CSwL/Composition.lean |
Assembles the chapter and records its remaining work. |
CSwFP.yaml |
Maps chapter 7 sections and exercises. |
Book.lean |
Includes Composition in the textbook. |
Bib.lean |
Adds references on generalized quantifiers. |
Review effort: Balanced
The glue chapter no longer keeps itself on one page: each section has its own file, page and generated module. The AI-written draft explanations in Quantification move inside the dev notes that disclose them, so the student build no longer publishes them. Two exercise hints are corrected: the disjunction case of mon-up-down needs at least three and at most one, and in left-mon-pattern an element inside B increases n, not m. The cue on van Benthem's theorem allows self-loops. In ModelChecking, lf2 and lf3 are live Lean again. AI usage: Claude Code (Claude Opus 5.5) made these changes from a Copilot review, at the author's request; the author reviewed them.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the
Compositionchapter, ported from CSwFP/7, one file per section. The chapter is not finished, but it is merged so that what exists can be published.Language.terseonly; thefulltext is marked with:::dev BeforeNextReleaseTODOs.CSwFP.yaml,DEVIATIONS.md,STYLE-CODE.mdandSTYLE-WRITING.mdare updated, andcheck-cswfp.pyacceptsdeferredas a target.🤖 Generated with Claude Code
https://claude.ai/code/session_01UFZtiDzfskeJTJ2ntCt2vh