feat(English): write the chapter from CSwFP/6.1, 4.2, 6.2 and 6.3–6.4 - #29
Open
arademaker wants to merge 1 commit into
Open
arademaker wants to merge 1 commit into
arademaker wants to merge 1 commit into
Conversation
The chapter had been reduced to a skeleton of four headings. It now has the four sections, in the order the headings fix: linguistic form and translation into logic (6.1), the fragment of English (4.2), predicate logic as representation language (6.2), and the model together with evaluation in it (6.3 and 6.4). The order is forced, since 6.2 translates the 4.2 grammar category by category. The fragment is `Sent`, `NP`, `RCN` and `VP` in one `mutual` block over the lexical categories, with `ToString` for the surface string. The translation is `lfSent`, `lfNP`, `lfVP` and `lfRCN`, with `lfDET` building a fresh bound variable and Russell's analysis for the definite article. The model is the fairy-tale structure over `A`–`Z` and `Unspec`, and evaluation reuses `Interp`, `FInterp`, `Assign` and `Formula.eval` from `Logic/FOL.lean` rather than restating them. The chapter closes by spending `mem_entities` as the `hdom` of `Formula.eval_iff_denote`, so `checkSentence`'s `Bool` and the proposition the sentence states are shown to agree. Six exercises, all rated 2: `preposition-phrase`, `complex-relative- clauses`, `fragment-translations`, `check-sentence`, `help-defeat` and `reflexive-ditransitive`. Decisions that depart from the source, all recorded in `DEVIATIONS.md`: - A grammar is extended by declaring a category that contains the old one, not by redeclaring the `mutual` group. Adding a word still needs a new constructor, so the lexicon is complete from the declaration and CSwFP/4.6 is absorbed into the presentation. - `most` is out of `DET`, because it has no first-order translation and a Lean function has to be total. `AV`, `To`, `INF` and `TINF` are out for the same reason and because CSwFP/6 never translates them. - Constructors are named after the rules they implement — `npDet`, `rcnSubj`, `rcnObj`, `vpTrans` — not `NP1`, `RCN1`, `VP1`. - `adjective-types` and the categorial section it belonged to are gone; 6.1 makes the same point about type raising. `Bib.lean` gains Carroll and Russell. `PROVENANCE.md` gains the chapter's table and drops `feature-value`, withdrawn in the previous commit. `STYLE-CODE.md` records that the pattern-matching `fun` reaches ordinary code here. The generated `student` project builds. AI-usage disclosure: this chapter was drafted with the assistance of Claude Opus 5 (Anthropic, September 2026, via Claude Code). The assistant read the source material, chose the encoding of the grammar and its extensions, wrote the Lean definitions, exercises and proofs, drafted the Portuguese prose as a translation of the source, and updated the project's records. The author takes full responsibility for the final content.
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
The PR leaves a stale README reference and introduces spelling and code-comment language issues.
Get a fresh assessment by requesting another Copilot review.
Review effort: Lite
Findings: 3
Open (3)
What changed in this PR
Expands English.lean from a skeleton into the English-fragment chapter, including grammar, translations, model evaluation, and exercises.
Changes:
- Added grammar, FOL translation, fairy-tale model, evaluation, and six exercises.
- Updated provenance, deviations, and Lean style records.
- Added Carroll and Russell bibliography entries.
| File | Description |
|---|---|
CSwL/English.lean |
New chapter content and exercises |
DEVIATIONS.md |
Updated chapter placement and design decisions |
PROVENANCE.md |
Added exercise provenance and counts |
STYLE-CODE.md |
Recorded newly introduced Lean syntax |
Bib.lean |
Added bibliography entries |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| A regra `NPP ::= DET CN PP` exige um determinante e um substantivo comum. Como *Little Mook* é um nome próprio, sem determinante, não há como formar *Little Mook with a sword* como um único sintagma nominal, e resta apenas a leitura em que o sintagma preposicional se liga ao sintagma verbal. | ||
| ::: | ||
|
|
||
| A preposição *with* tem o nome de uma palavra reservada de Lean. Para usá-la assim mesmo como nome de construtor, basta cercá-la de guilhemets: `«with»`. Fora da declaração, `.with` já é lido como o construtor e dispensa os guilhemets. |
| ```lean | ||
| def withSword : PP := .pp .with (.npDet .a .sword) | ||
|
|
||
| -- O sintagma preposicional modifica o objeto. |
Comment on lines
+525
to
+529
| **There is no `ModelChecking.lean`.** The plan once called for one, and older | ||
| notes in this file use that name for CSwFP/6's content; they should be read as | ||
| naming the content, not a file. The reason it belongs with the English | ||
| fragment is that it is built on that fragment, so the two are one development | ||
| rather than two. |
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.
The chapter had been reduced to a skeleton of four headings. It now has the four sections, in the order the headings fix: linguistic form and translation into logic (6.1), the fragment of English (4.2), predicate logic as representation language (6.2), and the model together with evaluation in it (6.3 and 6.4). The order is forced, since 6.2 translates the 4.2 grammar category by category.
The fragment is
Sent,NP,RCNandVPin onemutualblock over the lexical categories, withToStringfor the surface string. The translation islfSent,lfNP,lfVPandlfRCN, withlfDETbuilding a fresh bound variable and Russell's analysis for the definite article. The model is the fairy-tale structure overA–ZandUnspec, and evaluation reusesInterp,FInterp,AssignandFormula.evalfromLogic/FOL.leanrather than restating them. The chapter closes by spendingmem_entitiesas thehdomofFormula.eval_iff_denote, socheckSentence'sBooland the proposition the sentence states are shown to agree.Six exercises, all rated 2:
preposition-phrase,complex-relative- clauses,fragment-translations,check-sentence,help-defeatandreflexive-ditransitive.Decisions that depart from the source, all recorded in
DEVIATIONS.md:mutualgroup. Adding a word still needs a new constructor, so the lexicon is complete from the declaration and CSwFP/4.6 is absorbed into the presentation.mostis out ofDET, because it has no first-order translation and a Lean function has to be total.AV,To,INFandTINFare out for the same reason and because CSwFP/6 never translates them.npDet,rcnSubj,rcnObj,vpTrans— notNP1,RCN1,VP1.adjective-typesand the categorial section it belonged to are gone; 6.1 makes the same point about type raising.Bib.leangains Carroll and Russell.PROVENANCE.mdgains the chapter's table and dropsfeature-value, withdrawn in the previous commit.STYLE-CODE.mdrecords that the pattern-matchingfunreaches ordinary code here.The generated
studentproject builds.AI-usage disclosure: this chapter was drafted with the assistance of Claude Opus 5 (Anthropic, September 2026, via Claude Code). The assistant read the source material, chose the encoding of the grammar and its extensions, wrote the Lean definitions, exercises and proofs, drafted the Portuguese prose as a translation of the source, and updated the project's records. The author takes full responsibility for the final content. To be manually revised yet.