From ee096d17f620c568171e233cc97a20a72a804070 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Thu, 29 Oct 2026 21:39:10 -0300 Subject: [PATCH 1/6] feat(Parsing): add parse trees and context-free recognition Start the parsing chapter with CSwFP 9.1 and 9.2, skipping CSwFP 8. Parse trees carry positions and the tree relations of dominance, sisterhood, c-command and precedence, as lists of pairs. Recognition and parsing by splitting the input are shown on the palindrome grammar, with `partial def`, and checked against Mathlib's `List.Palindrome` up to length 6. Exercises 9.1-9.6 are ported; 9.7 goes into the cue on `partial def`. Claude Code (Opus 5.5) drafted these changes and this message under the author's direction; the author reviewed them. --- Book.lean | 2 + CSwFP.yaml | 30 ++- CSwL/Parsing.lean | 48 ++++ CSwL/Parsing/ParseTrees.lean | 427 ++++++++++++++++++++++++++++++++++ CSwL/Parsing/Recognition.lean | 221 ++++++++++++++++++ DEVIATIONS.md | 26 +++ README.md | 3 +- STYLE-CODE.md | 1 + scripts/check-cswfp.py | 3 +- 9 files changed, 758 insertions(+), 3 deletions(-) create mode 100644 CSwL/Parsing.lean create mode 100644 CSwL/Parsing/ParseTrees.lean create mode 100644 CSwL/Parsing/Recognition.lean diff --git a/Book.lean b/Book.lean index 76f2ecf..ccf7856 100644 --- a/Book.lean +++ b/Book.lean @@ -9,6 +9,7 @@ import CSwL.SeaBattle import CSwL.Morphology import CSwL.InfEngine import CSwL.ModelChecking +import CSwL.Parsing import VersoManual @@ -35,3 +36,4 @@ set_option verso.code.warnLineLength 80 {include CSwL.Morphology} {include CSwL.InfEngine} {include CSwL.ModelChecking} +{include CSwL.Parsing} diff --git a/CSwFP.yaml b/CSwFP.yaml index 40d7f5a..4d2214e 100644 --- a/CSwFP.yaml +++ b/CSwFP.yaml @@ -129,6 +129,25 @@ exercises: 6.6 (p. 146): TODO, goes with 6.5 to Logic/FOL 6.7 (p. 147): check-sentence + CSwFP/9: + 9.1 (p. 208): imm-dominance + 9.2 (p. 210): c-command-dominance + 9.3 (p. 210): mutual-c-command + 9.4 (p. 211): imm-precedence + 9.5 (p. 211): command + 9.6 (p. 214): split-nonempty + 9.7 (p. 214): absorbed into the cue on `partial def`, which says why left + recursion is no trouble for recognition by splitting + 9.8 (p. 217): TODO + 9.9 (p. 222): TODO + 9.10 (p. 237): TODO + 9.11 (p. 241): TODO + 9.12 (p. 244): TODO + 9.13 (p. 246): TODO + 9.14 (p. 248): TODO + 9.15 (p. 257): TODO + 9.16 (p. 259): TODO + original: IntroL.lean: [sum-of-squares, sum-to, sum-list, count-zeros] Logic/Proof.lean: @@ -269,7 +288,16 @@ sections: CSwFP/7 The Composition of Meaning in Natural Language: not yet taken up CSwFP/8 Extension and Intension: not yet taken up - CSwFP/9 Parsing: not yet taken up + CSwFP/9: + 9.1 Talking About Parse Trees: Parsing + 9.2 Recognizing and Parsing Context-Free Languages: Parsing + 9.3 Parsers and Parser Combinators: Parsing, not yet written + 9.4 Features and Categories: Parsing, not yet written + 9.5 Lexical Lookup and Scanning: Parsing, not yet written + 9.6 Parsing Categories: Parsing, not yet written + 9.7 Handling Extractions: Parsing, not yet written + 9.8 Adding Semantics: Parsing, not yet written + 9.9 Further Reading: omitted CSwFP/10 Handling Relations and Scoping: not yet taken up CSwFP/11 Continuation Passing Style Semantics: not yet taken up CSwFP/12 Discourse Representation and Context: not yet taken up diff --git a/CSwL/Parsing.lean b/CSwL/Parsing.lean new file mode 100644 index 0000000..3e28112 --- /dev/null +++ b/CSwL/Parsing.lean @@ -0,0 +1,48 @@ +import CSwLMeta +import Bib +import CSwL.Parsing.ParseTrees +import CSwL.Parsing.Recognition + +open Verso.Genre Manual +open CSwLMeta + +#doc (Manual) "Análise sintática" => +%%% +tag := "Parsing" +htmlSplit := .never +file := "Parsing" +%%% + +:::dev NOW +Plan. The headings follow CSwFP/9.1–9.8 (9.9, further reading, is +omitted). Sections are written `terse` first (see `STYLE-CODE.md`). + +- 9.1: `ParseTree α β`, positions, and the tree relations as lists of + pairs; dominance with Lean's `<+:`. +- 9.2: recognition and parsing by splitting, for the palindrome grammar, + with `partial def`; agreement with Mathlib's `List.Palindrome` checked + up to length 6 by `native_decide`. +- 9.3: list-of-successes parsers, still to decide: `StateT (List α) List` + with Mathlib's `Monad`/`Alternative List`, or plain functions. Lean's + `Std.Internal.Parsec` returns one result, not all parses; it can serve + the lexer of 9.5. +- 9.4–9.8: to plan. The representation of `Cat` is tied to issue 42. +::: + +:::terse +- Até aqui as árvores sintáticas eram construídas à mão. Agora o caminho + é o inverso: partir de uma sequência de palavras e encontrar as árvores + que a gramática lhe atribui. +- Primeiro, relações entre os nós de uma árvore. Depois, reconhecer e + analisar linguagens livres de contexto. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate the CSwFP/9 summary. +::: +:::: + +{include 1 CSwL.Parsing.ParseTrees} + +{include 1 CSwL.Parsing.Recognition} diff --git a/CSwL/Parsing/ParseTrees.lean b/CSwL/Parsing/ParseTrees.lean new file mode 100644 index 0000000..1aa0e78 --- /dev/null +++ b/CSwL/Parsing/ParseTrees.lean @@ -0,0 +1,427 @@ +import CSwLMeta +import Bib + +open Verso.Genre Manual +open CSwLMeta + +#doc (Manual) "Falando de árvores sintáticas" => +%%% +tag := "parse-trees" +%%% + +```lean +namespace Parsing +``` + +:::terse +- Uma árvore sintática tem informação lexical nas folhas e informação + sintática nos nós internos. +- O tipo deixa as duas em aberto: `α` para as folhas, `β` para os rótulos + dos nós. `ep` é a árvore vazia. +- Um `branch` guarda a *lista* das suas subárvores, por isso cada nó pode + ter quantas filhas quiser. +- A função `toText` escreve a árvore entre colchetes, com o rótulo depois + de `[.`. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.1, from the start to the example tree. +::: +:::: + +```lean +inductive ParseTree (α β : Type) where + | ep + | leaf (a : α) + | branch (b : β) (ts : List (ParseTree α β)) + deriving Repr, BEq + +def ParseTree.toText {α β : Type} + [ToString α] [ToString β] : ParseTree α β → String + | .ep => "[]" + | .leaf a => toString a + | .branch b ts => + "[." ++ toString b ++ " " ++ + toString (ts.map toText) ++ "]" + +instance {α β : Type} [ToString α] [ToString β] : + ToString (ParseTree α β) := + ⟨ParseTree.toText⟩ + +def snowWhite : ParseTree String String := + .branch "S" + [.branch "NP" [.leaf "Snow White"], + .branch "VP" [.branch "TV" [.leaf "loved"], + .branch "NP" [.leaf "the dwarfs"]]] + +#eval IO.println snowWhite +``` + +:::terse +- Uma mesma subárvore pode ocorrer mais de uma vez numa árvore: em + *Snow White loved Snow White*, `[NP Snow White]` ocorre duas vezes. +- Para apontar uma ocorrência usamos uma *posição*: a lista dos índices + das filhas no caminho desde a raiz, contando a partir de 0. A raiz é a + posição `[]`. +- `pos` lista todas as posições. Como a recursão desce por uma lista de + subárvores, ela é escrita junto com `posFrom`, num bloco `mutual`: + `posFrom i ts` dá as posições das árvores de `ts`, a primeira com + índice `i`. +- `subtree t p` é a subárvore de `t` na posição `p`. Numa posição que + não existe em `t`, devolve `ep`. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.1, from "In this first section, we will develop…" +to the definition of `subtrees`. +::: +:::: + +```lean +abbrev Pos := List Nat + +mutual + def pos {α β : Type} : ParseTree α β → List Pos + | .ep => [[]] + | .leaf _ => [[]] + | .branch _ ts => [] :: posFrom 0 ts + + def posFrom {α β : Type} : + Nat → List (ParseTree α β) → List Pos + | _, [] => [] + | i, t :: ts => + (pos t).map (i :: ·) ++ posFrom (i + 1) ts +end + +#eval pos snowWhite + +def subtree {α β : Type} : + ParseTree α β → Pos → ParseTree α β + | t, [] => t + | .branch _ ts, i :: is => + match ts[i]? with + | some t => subtree t is + | none => .ep + | _, _ :: _ => .ep + +def subtrees {α β : Type} (t : ParseTree α β) : + List (ParseTree α β) := + (pos t).map (subtree t) + +#eval IO.println (subtree snowWhite [1, 1]) +``` + +:::terse +- Uma posição `p` *domina* `q` quando `p` é prefixo de `q`: a subárvore + em `q` está dentro da subárvore em `p`. Toda posição domina a si mesma; + a dominância *própria* exclui esse caso. +- Em Lean, `p <+: q` diz que `p` é prefixo de `q`. É uma proposição + decidível, então pode ser usada como `Bool` num `filter`. +- As relações sobre as posições de uma árvore são listas de pares. + `posPairs` lista todos os pares de posições; cada relação filtra os + que lhe interessam. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.1, from "If p, q are tree positions…" to the +definition of `dominance`. +::: +:::: + +```lean +def posPairs {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + (pos t).flatMap fun p => (pos t).map fun q => (p, q) + +def properDominance {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + (posPairs t).filter fun (p, q) => p != q && p <+: q + +def dominance {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + (posPairs t).filter fun (p, q) => p <+: q + +#eval properDominance snowWhite +``` + +::::exercise (rating := 2) (name := "imm-dominance") +A posição `p` *domina imediatamente* `q` quando `p` domina propriamente +`q` e não há posição `r`, diferente das duas, tal que `p` domina `r` e +`r` domina `q`. Defina `immDominance` e confira o resultado na árvore +`snowWhite`. + +```lean +def immDominance {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + solution!( + (properDominance t).filter fun (p, q) => + !(pos t).any fun r => + r != p && r != q && p <+: r && r <+: q) + +theorem immDominance_snowWhite : + immDominance snowWhite = + [([], [0]), ([], [1]), ([0], [0, 0]), ([1], [1, 0]), + ([1], [1, 1]), ([1, 0], [1, 0, 0]), + ([1, 1], [1, 1, 0])] := by + solution! + decide +``` +:::: + +:::terse +- Duas posições são *irmãs* quando são filhas diferentes da mesma mãe: + coincidem em tudo, menos no último índice. +- O *c-comando* é a composição de duas relações: `p` c-comanda `q` quando + uma irmã de `p` domina `q`. +- `relComp r s` liga `x` a `z` quando `r` liga `x` a algum `y` e `s` liga + esse `y` a `z`. `eraseDups` tira os pares repetidos. +- Na árvore `snowWhite`, o sujeito `[0]` c-comanda tudo o que está dentro + do VP; o objeto `[1, 1]` c-comanda o verbo `[1, 0]`, mas não o sujeito. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.1, from "Two positions p, q are sister positions…" +to the c-command relation of the example tree. +::: +:::: + +```lean +def sisters : Pos → Pos → Bool + | [i], [j] => i != j + | i :: is, j :: js => i == j && sisters is js + | _, _ => false + +def sisterhood {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + (posPairs t).filter fun (p, q) => sisters p q + +#eval sisterhood snowWhite + +def relComp {γ : Type} [BEq γ] (r s : List (γ × γ)) : + List (γ × γ) := + (r.flatMap fun (x, y) => + (s.filter fun (w, _) => y == w).map fun (_, z) => + (x, z)).eraseDups + +def cCommand {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + relComp (sisterhood t) (dominance t) + +#eval cCommand snowWhite +``` + +:::terse +- Uma posição *ramifica* quando tem pelo menos duas filhas. Na árvore + `snowWhite`, só a raiz e o VP ramificam. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.1, the branching positions. +::: +:::: + +```lean +def branchingPos {α β : Type} (t : ParseTree α β) : + List Pos := + let ps := pos t + ps.filter fun p => + ps.contains (p ++ [0]) && ps.contains (p ++ [1]) + +#eval branchingPos snowWhite +``` + +:::terse +- Os fatos sobre o c-comando valem para quaisquer posições, não só para + as de uma árvore. Por isso os teoremas abaixo falam de posições. +- Dois lemas sobre irmãs: elas têm o mesmo comprimento, e nenhuma é + prefixo da outra. +::: + +:::details "Dois lemas sobre posições irmãs" +```lean +theorem sisters_length (p r : Pos) + (h : sisters p r = true) : p.length = r.length := by + induction p generalizing r with + | nil => simp [sisters] at h + | cons i is ih => + cases r with + | nil => simp [sisters] at h + | cons j js => + cases is with + | nil => + cases js with + | nil => rfl + | cons k ks => simp [sisters] at h + | cons i' is' => + cases js with + | nil => simp [sisters] at h + | cons k ks => + simp only [sisters, Bool.and_eq_true] at h + simp [ih _ h.2] + +theorem sisters_not_prefix (p r : Pos) + (h : sisters p r = true) : ¬ p <+: r := by + induction p generalizing r with + | nil => simp [sisters] at h + | cons i is ih => + cases r with + | nil => simp [sisters] at h + | cons j js => + cases is with + | nil => + cases js with + | nil => simp_all [sisters] + | cons k ks => simp_all [sisters] + | cons i' is' => + cases js with + | nil => simp [sisters] at h + | cons k ks => + simp only [sisters, Bool.and_eq_true, + beq_iff_eq] at h + obtain ⟨rfl, h⟩ := h + rw [List.cons_prefix_cons] + intro ⟨_, hp⟩ + exact ih _ h hp +``` +::: + +::::exercise (rating := 3) (name := "c-command-dominance") +Suponha que `p` c-comanda `q`: uma irmã `r` de `p` domina `q`. Prove que +`p` não domina `q` e que `q` não domina `p`. + +Dica: um prefixo de `q` que não é mais longo do que outro prefixo de `q` +é prefixo dele (`List.prefix_of_prefix_length_le`), e um prefixo do mesmo +comprimento é a própria lista (`List.IsPrefix.eq_of_length`). + +```lean +theorem cCommand_not_dominates (p r q : Pos) + (hs : sisters p r = true) (hd : r <+: q) : + ¬ p <+: q := by + solution! + intro hp + have hl := sisters_length p r hs + have h : p <+: r := + List.prefix_of_prefix_length_le hp hd (by omega) + exact sisters_not_prefix p r hs h + +theorem cCommand_not_dominated (p r q : Pos) + (hs : sisters p r = true) (hd : r <+: q) : + ¬ q <+: p := by + solution! + intro hq + have hl := sisters_length p r hs + have h1 := hd.length_le + have h2 := hq.length_le + have hqp : q = p := hq.eq_of_length (by omega) + have hrq : r = q := hd.eq_of_length (by omega) + rw [hrq, hqp] at hs + exact sisters_not_prefix p p hs (List.prefix_refl p) +``` +:::: + +::::exercise (rating := 2) (name := "mutual-c-command") +O c-comando não é simétrico, mas o *c-comando mútuo* é: `p` e `q` se +c-comandam mutuamente quando `p` c-comanda `q` e `q` c-comanda `p`. +Defina `mutualCCommand` e confira, na árvore `snowWhite`, que ele coincide +com a relação de irmãs. + +```lean +def mutualCCommand {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + solution!( + (cCommand t).filter fun (p, q) => + (cCommand t).contains (q, p)) + +theorem mutualCCommand_snowWhite : + mutualCCommand snowWhite = sisterhood snowWhite := by + solution! + decide +``` +:::: + +:::terse +- `p` *precede* `q` quando, no primeiro índice em que diferem, o de `p` é + menor. Uma posição não precede as que ela domina. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.1, from "A position p in a syntax tree precedes…" +to the precedence relation of the example tree. +::: +:::: + +```lean +def precede : Pos → Pos → Bool + | i :: is, j :: js => i < j || (i == j && precede is js) + | _, _ => false + +def precedence {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + (posPairs t).filter fun (p, q) => precede p q + +#eval precedence snowWhite +``` + +::::exercise (rating := 2) (name := "imm-precedence") +Defina a *precedência imediata*, a partir da precedência, do mesmo modo +que a dominância imediata foi definida a partir da dominância. Confira o +resultado na árvore `snowWhite`. + +```lean +def immPrecedence {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + solution!( + (precedence t).filter fun (p, q) => + !(pos t).any fun r => precede p r && precede r q) + +theorem immPrecedence_snowWhite : + immPrecedence snowWhite = + [([0], [1]), ([0], [1, 0]), ([0], [1, 0, 0]), + ([0, 0], [1]), ([0, 0], [1, 0]), + ([0, 0], [1, 0, 0]), ([1, 0], [1, 1]), + ([1, 0], [1, 1, 0]), ([1, 0, 0], [1, 1]), + ([1, 0, 0], [1, 1, 0])] := by + solution! + decide +``` +:::: + +:::terse +- O *comando* é uma noção anterior ao c-comando: `p` comanda `q` quando + nenhuma das duas domina a outra e o S mais próximo acima de `p` também + domina `q`. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.1, the paragraph on command. +::: +:::: + +::::exercise (rating := 2) (name := "command") +Defina `command` supondo que o S mais próximo é sempre a raiz da árvore. +Confira o resultado na árvore `snowWhite`. + +```lean +def command {α β : Type} (t : ParseTree α β) : + List (Pos × Pos) := + solution!( + (posPairs t).filter fun (p, q) => + !(p <+: q) && !(q <+: p)) + +theorem command_snowWhite : + (command snowWhite).length = 28 := by + solution! + decide +``` +:::: + +```lean +end Parsing +``` diff --git a/CSwL/Parsing/Recognition.lean b/CSwL/Parsing/Recognition.lean new file mode 100644 index 0000000..327853b --- /dev/null +++ b/CSwL/Parsing/Recognition.lean @@ -0,0 +1,221 @@ +import CSwLMeta +import Bib +import CSwL.Parsing.ParseTrees +import Mathlib.Data.List.Palindrome + +open Verso.Genre Manual +open CSwLMeta + +#doc (Manual) "Reconhecendo e analisando linguagens livres de contexto" => +%%% +tag := "cf-recognition" +%%% + +```lean +namespace Parsing +``` + +:::terse +- *Reconhecer*: dizer se a gramática gera ou não uma sequência. + *Analisar* (*parsing*): dizer também como ela é gerada, isto é, dar as + suas árvores sintáticas. +- O exemplo é a gramática dos palíndromos sobre `{a, b, c}`, as palavras + iguais à sua inversa: + A → ε | a | b | c | aAa | bAb | cAc. +- A ideia para qualquer gramática livre de contexto: uma regra com `n` + símbolos à direita divide a entrada em `n` pedaços, de todos os modos + possíveis, e testa cada pedaço contra o seu símbolo. +- `split2` dá todas as divisões de uma lista em duas; `splitN n`, em `n`. +- Em Lean, uma `String` não é uma lista. `"Jan".toList` dá a lista de + caracteres, e `String.ofList` faz o caminho de volta. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.2, from the start to the definition of `splitN`. +::: +:::: + +```lean +def split2 {α : Type} : List α → List (List α × List α) + | [] => [([], [])] + | x :: xs => + ([], x :: xs) :: + (split2 xs).map fun (ys, zs) => (x :: ys, zs) + +#eval split2 "Jan".toList + +def splitN {α : Type} : Nat → List α → List (List (List α)) + | 0, _ | 1, _ => [] + | 2, xs => (split2 xs).map fun (ys, zs) => [ys, zs] + | n + 3, xs => + (split2 xs).flatMap fun (ys, zs) => + (splitN (n + 2) zs).map fun rs => ys :: rs + +#eval splitN 3 "Jan".toList +``` + +:::terse +- O reconhecedor segue a gramática: uma linha por regra. Para A → aAa, + ele procura uma divisão em três pedaços `[a]`, `ys`, `[a]` e reconhece + `ys`. +- `recognize` chama a si mesma em `ys`. Lean exige que toda função + termine, e aqui ele não consegue ver sozinho que `ys` é menor do que + `xs`. +- `partial def` aceita a definição sem essa verificação. O preço: Lean + roda a função, mas não sabe nada sobre o que ela calcula, e nenhuma + prova pode olhar dentro dela. +- Ela termina: `ys` tem dois elementos a menos. Uma regra recursiva à + esquerda, V → V T, também não seria problema, porque V recebe um pedaço + menor da entrada, desde que o pedaço de T não seja vazio. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.2, from "Now the function for recognizing…" to +"…for splitting the input into n substrings." +::: +:::: + +```lean +partial def recognize (xs : List Char) : Bool := + xs == [] || xs == ['a'] || xs == ['b'] || xs == ['c'] || + (splitN 3 xs).any fun + | [['a'], ys, ['a']] => recognize ys + | [['b'], ys, ['b']] => recognize ys + | [['c'], ys, ['c']] => recognize ys + | _ => false + +#eval recognize "aabcbbcbaa".toList +#eval recognize "aabcbbcba".toList +``` + +:::terse +- Do reconhecimento à geração: gerar todas as palavras sobre o alfabeto e + ficar com as reconhecidas. +- `gener n` dá as palavras de comprimento `n`; `generUpTo n`, as de + comprimento até `n`. As palavras são infinitas, mas uma lista em Lean é + finita, por isso a geração para num comprimento dado. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.2, from "From recognition to generation…" to the +first fifteen palindromes. +::: +:::: + +```lean +def gener {α : Type} : Nat → List α → List (List α) + | 0, _ => [[]] + | n + 1, alphabet => + alphabet.flatMap fun x => + (gener n alphabet).map (x :: ·) + +def generUpTo {α : Type} (n : Nat) (alphabet : List α) : + List (List α) := + (List.range (n + 1)).flatMap fun k => gener k alphabet + +#eval ((generUpTo 3 "abc".toList).filter recognize).map + String.ofList +``` + +:::terse +- O Mathlib define palíndromo como um predicado indutivo, + `List.Palindrome`. Os seus três construtores são as regras da + gramática: a lista vazia, uma lista de um elemento, e `x :: (l ++ [x])` + para `l` palíndromo. +- O teorema confere que `recognize` concorda com essa definição em todas + as palavras sobre `{a, b, c}` de comprimento até 6. +- `decide` não serve, porque o Lean não olha dentro de um `partial def`. + `native_decide` roda o código compilado e aceita o resultado. +::: + +:::details "O reconhecedor e a definição de palíndromo" +```lean +theorem recognize_upTo6 : + ∀ w ∈ generUpTo 6 "abc".toList, + recognize w = true ↔ w.Palindrome := by + native_decide +``` +::: + +:::terse +- Analisar é construir as árvores. A entrada é uma `List Char`, e as + árvores são do tipo `ParseTree Char Char`: caracteres nas folhas e o + rótulo `A` nos nós. +- Mesma receita do reconhecedor, uma linha por regra; agora cada linha + devolve a lista das suas árvores, vazia quando a regra não se aplica. +- A palavra vazia vira a árvore vazia `ep`. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.2, from "Parsing with a context-free grammar…" +to the end of the section. +::: +:::: + +```lean +partial def parse (xs : List Char) : + List (ParseTree Char Char) := + (if xs == [] then [.ep] else []) ++ + (if xs == ['a'] then [.leaf 'a'] else []) ++ + (if xs == ['b'] then [.leaf 'b'] else []) ++ + (if xs == ['c'] then [.leaf 'c'] else []) ++ + (splitN 3 xs).flatMap fun + | [['a'], ys, ['a']] => + (parse ys).map fun t => + .branch 'A' [.leaf 'a', t, .leaf 'a'] + | [['b'], ys, ['b']] => + (parse ys).map fun t => + .branch 'A' [.leaf 'b', t, .leaf 'b'] + | [['c'], ys, ['c']] => + (parse ys).map fun t => + .branch 'A' [.leaf 'c', t, .leaf 'c'] + | _ => [] + +#eval IO.println (parse "aabaa".toList) +#eval IO.println (parse "aabbaa".toList) +#eval IO.println (parse "aabcbbcba".toList) +``` + +::::exercise (rating := 2) (name := "split-nonempty") +Numa gramática sem regras ε, nenhum pedaço da divisão pode ser vazio. +Defina `split2'` e `splitN'`, que dão só as divisões sem pedaços vazios. +Confira o resultado em `"Jan"`. + +```lean +def split2' {α : Type} : List α → List (List α × List α) + | [] | [_] => [] + | x :: y :: ys => + solution!( + ([x], y :: ys) :: + (split2' (y :: ys)).map fun (us, vs) => + (x :: us, vs)) + +def splitN' {α : Type} : Nat → List α → List (List (List α)) + | 0, _ | 1, _ => [] + | 2, xs => + solution!((split2' xs).map fun (ys, zs) => [ys, zs]) + | n + 3, xs => + solution!( + (split2' xs).flatMap fun (ys, zs) => + (splitN' (n + 2) zs).map fun rs => ys :: rs) + +theorem split2'_jan : + split2' "Jan".toList = + [(['J'], ['a', 'n']), (['J', 'a'], ['n'])] := by + solution! + decide + +theorem splitN'_jan : + splitN' 3 "Jan".toList = [[['J'], ['a'], ['n']]] := by + solution! + decide +``` +:::: + +```lean +end Parsing +``` diff --git a/DEVIATIONS.md b/DEVIATIONS.md index cb7822c..065cfdb 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -129,6 +129,32 @@ decisions inside the chapters. `FInterp`; and names and argument order agree with the translation, which in the Haskell source they do not. +### `Parsing` + +CSwFP/8 is skipped for now, and the chapter follows `ModelChecking`. + +- 9.1: the tree relations are lists of pairs, as in CSwFP, because the + section shows them with `#eval`; Mathlib's `Rel` of `Sets` is a `Prop` + and cannot be printed. Dominance uses Lean's `<+:` (`List.IsPrefix`) in + place of a helper `prefix`. `pos` is written with a helper `posFrom` in a + `mutual` block, so that Lean sees the recursion over the list of + subtrees as structural. `subtree` returns `ep` at a position the tree + does not have, where CSwFP's is undefined. +- Exercise 9.2 becomes two theorems about positions, parts (1) and (2): + the relation of c-command is a sister followed by dominance, and neither + part depends on the tree. Part (3), on the lowest branching position, is + not ported. Exercises 9.1, 9.3, 9.4 and 9.5 ask for a definition checked + on the example tree; 9.6 asks for the splitting functions without empty + parts. +- 9.2: `recognize` and `parse` are `partial def`, since Lean cannot see + that the middle piece of a split is shorter than the input. The cue on + `partial def` says why left recursion is no trouble here, which is + exercise 9.7. Generation stops at a given length, since Lean lists are + finite. A theorem checks, with `native_decide`, that `recognize` agrees + with Mathlib's `List.Palindrome` on all words up to length 6; a proof + for all words would need `recognize` to be total. `parse` gives the + empty word the empty tree `ep`, where CSwFP uses a leaf `"[]"`. + ## Beyond CSwFP/6 Not planned yet. CSwFP/7 continues the fragment of `ModelChecking` and builds on the diff --git a/README.md b/README.md index 7b66a21..6034b30 100644 --- a/README.md +++ b/README.md @@ -49,7 +49,8 @@ adapts — see [DEVIATIONS.md](DEVIATIONS.md) for why. - [~] Model checking with first-order logic — [source](CSwL/ModelChecking.lean) - [ ] The composition of meaning - [ ] Extension and intension -- [ ] Parsing +- [~] Parsing — [source](CSwL/Parsing.lean) (sections in + [`CSwL/Parsing/`](CSwL/Parsing)) - [ ] Relations and scope - [ ] Semantics in continuation passing style - [ ] Discourse representation and context diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 54c961a..3bbd773 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -83,6 +83,7 @@ this way is usually a mistake; see "Known gaps." | `Morphology` | `open` of constructor namespaces (`open Attr Value`) | `match e₁, e₂ with` (first use outside a solution), `mapM` over `Option` **(solution only)** | *(none new)* | | `InfEngine` | `let rec` | `do`-notation | — | | `ModelChecking` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`), pattern-matching `fun \| … => …` (first use outside a solution) | *(none new)* | +| `Parsing` | `partial def` | `<+:` (`List.IsPrefix`), Mathlib's `List.Palindrome` | *(none new)* | `ModelChecking` is where `abbrev` and `ToString` instances become the dominant idiom, but both arrive earlier; what is genuinely new there is the mutually diff --git a/scripts/check-cswfp.py b/scripts/check-cswfp.py index f3fe56d..db44263 100755 --- a/scripts/check-cswfp.py +++ b/scripts/check-cswfp.py @@ -30,7 +30,8 @@ # How many exercises each CSwFP chapter has. COUNTS = {"CSwFP/1": 3, "CSwFP/2": 17, "CSwFP/3": 19, - "CSwFP/4": 24, "CSwFP/5": 32, "CSwFP/6": 7} + "CSwFP/4": 24, "CSwFP/5": 32, "CSwFP/6": 7, + "CSwFP/9": 16} EXERCISE = re.compile(r'^:+exercise\b.*\(name := "([^"]+)"\)') CITATION = re.compile(r"CSwFP|página \d+|\(p\. \d+|§\s*\d|exemplo \(\d+\.\d+\)" From c7cab12753fe241c92e75dfa29a59da33e08f941 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Tue, 3 Nov 2026 22:03:39 -0300 Subject: [PATCH 2/6] refactor(Parsing): make recognize and parse total recognize and parse no longer need partial def. They recurse over (splitN 3 xs).attach, which pairs each split with a proof that it belongs to splitN 3 xs, and decreasing_by uses flatten_of_mem_splitN, the fact that the pieces of a split concatenate to the input, to show that the middle piece is shorter. Its converse, mem_splitN_flatten, states that every split is produced; both hold for any n. With recognize total, the bounded check by native_decide on words up to length 6 gives way to a proof, in a details block, that recognize agrees with Mathlib's List.Palindrome on every word over {a, b, c}. The cues follow: the one on termination keeps exercise 9.7, and the one before parse says why the trees of all rules are concatenated. STYLE-CODE.md records the features the chapter now uses for the first time: termination_by, decreasing_by, List.attach, and rcases and Or.inr outside a solution. DEVIATIONS.md, CSwFP.yaml and the chapter overview no longer mention partial def. AI-usage disclosure: these changes were drafted with the assistance of Claude Opus 5.5 (Anthropic, via Claude Code), under the author's direction. The assistant wrote the termination argument and the proofs, drafted the Portuguese cues, and updated the project's records; the author reviewed them and takes full responsibility for the final content. --- CSwFP.yaml | 2 +- CSwL/Parsing.lean | 4 +- CSwL/Parsing/ParseTrees.lean | 36 +++--- CSwL/Parsing/Recognition.lean | 227 +++++++++++++++++++++++++++++----- DEVIATIONS.md | 16 +-- STYLE-CODE.md | 6 +- 6 files changed, 229 insertions(+), 62 deletions(-) diff --git a/CSwFP.yaml b/CSwFP.yaml index 4d2214e..e97ea37 100644 --- a/CSwFP.yaml +++ b/CSwFP.yaml @@ -136,7 +136,7 @@ exercises: 9.4 (p. 211): imm-precedence 9.5 (p. 211): command 9.6 (p. 214): split-nonempty - 9.7 (p. 214): absorbed into the cue on `partial def`, which says why left + 9.7 (p. 214): absorbed into the cue on termination, which says why left recursion is no trouble for recognition by splitting 9.8 (p. 217): TODO 9.9 (p. 222): TODO diff --git a/CSwL/Parsing.lean b/CSwL/Parsing.lean index 3e28112..951eddd 100644 --- a/CSwL/Parsing.lean +++ b/CSwL/Parsing.lean @@ -20,8 +20,8 @@ omitted). Sections are written `terse` first (see `STYLE-CODE.md`). - 9.1: `ParseTree α β`, positions, and the tree relations as lists of pairs; dominance with Lean's `<+:`. - 9.2: recognition and parsing by splitting, for the palindrome grammar, - with `partial def`; agreement with Mathlib's `List.Palindrome` checked - up to length 6 by `native_decide`. + total by `termination_by`; agreement with Mathlib's `List.Palindrome` + proved for every word over `{a, b, c}`. - 9.3: list-of-successes parsers, still to decide: `StateT (List α) List` with Mathlib's `Monad`/`Alternative List`, or plain functions. Lean's `Std.Internal.Parsec` returns one result, not all parses; it can serve diff --git a/CSwL/Parsing/ParseTrees.lean b/CSwL/Parsing/ParseTrees.lean index 1aa0e78..d14f4f5 100644 --- a/CSwL/Parsing/ParseTrees.lean +++ b/CSwL/Parsing/ParseTrees.lean @@ -69,7 +69,8 @@ def snowWhite : ParseTree String String := `posFrom i ts` dá as posições das árvores de `ts`, a primeira com índice `i`. - `subtree t p` é a subárvore de `t` na posição `p`. Numa posição que - não existe em `t`, devolve `ep`. + não existe em `t`, devolve `ep`; isso nunca acontece com as posições + de `pos t`. ::: ::::full @@ -82,23 +83,21 @@ to the definition of `subtrees`. ```lean abbrev Pos := List Nat -mutual - def pos {α β : Type} : ParseTree α β → List Pos - | .ep => [[]] - | .leaf _ => [[]] - | .branch _ ts => [] :: posFrom 0 ts - - def posFrom {α β : Type} : - Nat → List (ParseTree α β) → List Pos - | _, [] => [] - | i, t :: ts => - (pos t).map (i :: ·) ++ posFrom (i + 1) ts -end +def pos {α β : Type} (p : ParseTree α β) : List Pos := + let rec posFrom {α β : Type} : + Nat → List (ParseTree α β) → List Pos + | _, [] => [] + | i, t :: ts => + (pos t).map (i :: ·) ++ posFrom (i + 1) ts + match p with + | .ep => [[]] + | .leaf _ => [[]] + | .branch _ ts => [] :: posFrom 0 ts #eval pos snowWhite def subtree {α β : Type} : - ParseTree α β → Pos → ParseTree α β + ParseTree α β → Pos → ParseTree α β | t, [] => t | .branch _ ts, i :: is => match ts[i]? with @@ -106,11 +105,11 @@ def subtree {α β : Type} : | none => .ep | _, _ :: _ => .ep -def subtrees {α β : Type} (t : ParseTree α β) : - List (ParseTree α β) := +def subtrees {α β : Type} (t : ParseTree α β) + : List (ParseTree α β) := (pos t).map (subtree t) -#eval IO.println (subtree snowWhite [1, 1]) +#eval IO.println (subtree snowWhite [1]) ``` :::terse @@ -138,7 +137,7 @@ def posPairs {α β : Type} (t : ParseTree α β) : def properDominance {α β : Type} (t : ParseTree α β) : List (Pos × Pos) := - (posPairs t).filter fun (p, q) => p != q && p <+: q + (posPairs t).filter fun (p, q) => p ≠ q && p <+: q def dominance {α β : Type} (t : ParseTree α β) : List (Pos × Pos) := @@ -211,6 +210,7 @@ def cCommand {α β : Type} (t : ParseTree α β) : List (Pos × Pos) := relComp (sisterhood t) (dominance t) +#eval dominance snowWhite #eval cCommand snowWhite ``` diff --git a/CSwL/Parsing/Recognition.lean b/CSwL/Parsing/Recognition.lean index 327853b..0d0f5dd 100644 --- a/CSwL/Parsing/Recognition.lean +++ b/CSwL/Parsing/Recognition.lean @@ -26,8 +26,7 @@ namespace Parsing símbolos à direita divide a entrada em `n` pedaços, de todos os modos possíveis, e testa cada pedaço contra o seu símbolo. - `split2` dá todas as divisões de uma lista em duas; `splitN n`, em `n`. -- Em Lean, uma `String` não é uma lista. `"Jan".toList` dá a lista de - caracteres, e `String.ofList` faz o caminho de volta. +- Em Lean. `"Jan".toList` dá a lista de caracteres, e `String.ofList` faz o caminho de volta. ::: ::::full @@ -43,7 +42,8 @@ def split2 {α : Type} : List α → List (List α × List α) ([], x :: xs) :: (split2 xs).map fun (ys, zs) => (x :: ys, zs) -#eval split2 "Jan".toList +#eval split2 "Jan".toList |>.map + λ (a, b) ↦ (String.ofList a, String.ofList b) def splitN {α : Type} : Nat → List α → List (List (List α)) | 0, _ | 1, _ => [] @@ -52,7 +52,8 @@ def splitN {α : Type} : Nat → List α → List (List (List α)) (split2 xs).flatMap fun (ys, zs) => (splitN (n + 2) zs).map fun rs => ys :: rs -#eval splitN 3 "Jan".toList +#eval splitN 3 "Jan".toList |>.map + (·.map String.ofList) ``` :::terse @@ -60,14 +61,15 @@ def splitN {α : Type} : Nat → List α → List (List (List α)) ele procura uma divisão em três pedaços `[a]`, `ys`, `[a]` e reconhece `ys`. - `recognize` chama a si mesma em `ys`. Lean exige que toda função - termine, e aqui ele não consegue ver sozinho que `ys` é menor do que - `xs`. -- `partial def` aceita a definição sem essa verificação. O preço: Lean - roda a função, mas não sabe nada sobre o que ela calcula, e nenhuma - prova pode olhar dentro dela. -- Ela termina: `ys` tem dois elementos a menos. Uma regra recursiva à - esquerda, V → V T, também não seria problema, porque V recebe um pedaço - menor da entrada, desde que o pedaço de T não seja vazio. + termine, e sozinho ele não vê que `ys` é menor do que `xs`: o padrão + `[['a'], ys, ['a']]` não diz de onde a lista veio. +- `attach` junta a cada divisão a prova de que ela está em + `splitN 3 xs`. `termination_by xs.length` diz o que diminui; + `decreasing_by` prova que diminui, com o lema do bloco acima: os + pedaços juntos dão `xs`, então `ys` tem dois elementos a menos. +- Uma regra recursiva à esquerda, V → V T, também não seria problema, + porque V recebe um pedaço menor da entrada, desde que o pedaço de T + não seja vazio. ::: ::::full @@ -77,22 +79,55 @@ TODO: translate CSwFP/9.2, from "Now the function for recognizing…" to ::: :::: +:::details "As divisões juntam-se de volta na entrada" ```lean -partial def recognize (xs : List Char) : Bool := +theorem append_of_mem_split2 {α : Type} : + ∀ {xs : List α} {p : List α × List α}, + p ∈ split2 xs → p.1 ++ p.2 = xs + | [], p, h => by + simp [split2] at h + simp [h] + | x :: xs, p, h => by + simp only [split2, List.mem_cons, List.mem_map] at h + rcases h with rfl | ⟨⟨ys, zs⟩, h, rfl⟩ + · rfl + · simp [← append_of_mem_split2 h] + +theorem flatten_of_mem_splitN {α : Type} : + ∀ {n : Nat} {xs : List α} {l : List (List α)}, + l ∈ splitN n xs → l.flatten = xs + | 0, _, _, h | 1, _, _, h => by simp [splitN] at h + | 2, xs, l, h => by + simp only [splitN, List.mem_map] at h + obtain ⟨⟨ys, zs⟩, h, rfl⟩ := h + simpa using append_of_mem_split2 h + | n + 3, xs, l, h => by + simp only [splitN, List.mem_flatMap, List.mem_map] at h + obtain ⟨⟨ys, zs⟩, h1, rs, h2, rfl⟩ := h + simp [flatten_of_mem_splitN h2, append_of_mem_split2 h1] +``` +::: + +```lean +def recognize (xs : List Char) : Bool := xs == [] || xs == ['a'] || xs == ['b'] || xs == ['c'] || - (splitN 3 xs).any fun - | [['a'], ys, ['a']] => recognize ys - | [['b'], ys, ['b']] => recognize ys - | [['c'], ys, ['c']] => recognize ys + (splitN 3 xs).attach.any fun + | ⟨[['a'], ys, ['a']], h⟩ => recognize ys + | ⟨[['b'], ys, ['b']], h⟩ => recognize ys + | ⟨[['c'], ys, ['c']], h⟩ => recognize ys | _ => false +termination_by xs.length +decreasing_by + all_goals + have := congrArg List.length (flatten_of_mem_splitN h) + simp at this + omega #eval recognize "aabcbbcbaa".toList #eval recognize "aabcbbcba".toList ``` :::terse -- Do reconhecimento à geração: gerar todas as palavras sobre o alfabeto e - ficar com as reconhecidas. - `gener n` dá as palavras de comprimento `n`; `generUpTo n`, as de comprimento até `n`. As palavras são infinitas, mas uma lista em Lean é finita, por isso a geração para num comprimento dado. @@ -125,18 +160,138 @@ def generUpTo {α : Type} (n : Nat) (alphabet : List α) : `List.Palindrome`. Os seus três construtores são as regras da gramática: a lista vazia, uma lista de um elemento, e `x :: (l ++ [x])` para `l` palíndromo. -- O teorema confere que `recognize` concorda com essa definição em todas - as palavras sobre `{a, b, c}` de comprimento até 6. -- `decide` não serve, porque o Lean não olha dentro de um `partial def`. - `native_decide` roda o código compilado e aceita o resultado. +- `recognize_iff_palindrome`: `recognize` concorda com essa definição + em toda palavra sobre `{a, b, c}`, de qualquer comprimento. +- A prova é por indução no comprimento da palavra, uma direção de cada + vez. Ela só é possível porque `recognize` não é `partial`: o Lean + conhece a equação que a define. +- `recognize_generUpTo` é o caso das palavras geradas por + `generUpTo n`, para todo `n`. ::: :::details "O reconhecedor e a definição de palíndromo" ```lean -theorem recognize_upTo6 : - ∀ w ∈ generUpTo 6 "abc".toList, +theorem mem_split2_append {α : Type} : + ∀ ys zs : List α, (ys, zs) ∈ split2 (ys ++ zs) + | [], [] => by simp [split2] + | [], z :: zs => by simp [split2] + | y :: ys, zs => by + simp only [List.cons_append, split2, List.mem_cons, + List.mem_map] + exact Or.inr ⟨(ys, zs), mem_split2_append ys zs, rfl⟩ + +theorem mem_splitN_flatten {α : Type} : + ∀ l : List (List α), 2 ≤ l.length → + l ∈ splitN l.length l.flatten + | [ys, zs], _ => by + simp only [List.length, splitN, List.mem_map] + exact ⟨(ys, zs), by simpa using mem_split2_append ys zs, + rfl⟩ + | ys :: zs :: ws :: rs, _ => by + simp only [List.length_cons, List.flatten_cons] + simp only [splitN, List.mem_flatMap, List.mem_map] + refine ⟨(ys, (zs :: ws :: rs).flatten), + by simpa using mem_split2_append ys _, + zs :: ws :: rs, ?_, rfl⟩ + simpa using + mem_splitN_flatten (zs :: ws :: rs) (by simp) + | [], h | [_], h => by simp at h + +theorem recognize_sound (n : Nat) : + ∀ w : List Char, w.length ≤ n → + recognize w → w.Palindrome := by + induction n with + | zero => + intro w hw hr + simp at hw + rw [hw] + exact .nil + | succ n ih => + intro w hw h + rw [recognize] at h + simp only [Bool.or_eq_true, beq_iff_eq, + List.any_eq_true] at h + rcases h with (((rfl | rfl) | rfl) | rfl) + | ⟨⟨l, hl⟩, _, hm⟩ + · exact .nil + · exact .singleton _ + · exact .singleton _ + · exact .singleton _ + · split at hm <;> (try contradiction) <;> + · rename_i ys hys _ + have he := flatten_of_mem_splitN hys + simp at he + subst he + apply List.Palindrome.cons_concat + exact ih ys (by simp at hw; omega) hm + +theorem recognize_complete (n : Nat) : + ∀ w : List Char, w.length ≤ n → w ⊆ "abc".toList → + w.Palindrome → recognize w = true := by + induction n with + | zero => + intro w hw _ _ + simp at hw + subst hw + rw [recognize] + simp + | succ n ih => + intro w hw ha hp + cases hp with + | nil => + rw [recognize] + simp + | singleton x => + have hx : x ∈ "abc".toList := ha (by simp) + simp at hx + rcases hx with rfl | rfl | rfl <;> + (rw [recognize]; simp) + | cons_concat x hl => + rename_i l + have hx : x ∈ "abc".toList := ha (by simp) + have hl' : l ⊆ "abc".toList := + fun c hc => ha (by simp [hc]) + have ih' := ih l (by simp at hw; omega) hl' hl + rw [recognize] + simp only [Bool.or_eq_true, beq_iff_eq, + List.any_eq_true] + right + have hmem : + [[x], l, [x]] ∈ splitN 3 (x :: (l ++ [x])) := by + simpa using + mem_splitN_flatten [[x], l, [x]] (by simp) + refine ⟨⟨_, hmem⟩, List.mem_attach _ _, ?_⟩ + simp at hx + rcases hx with rfl | rfl | rfl <;> simpa using ih' + +theorem recognize_iff_palindrome (w : List Char) + (hw : w ⊆ "abc".toList) : + recognize w ↔ w.Palindrome := + ⟨recognize_sound _ w (Nat.le_refl _), + recognize_complete _ w (Nat.le_refl _) hw⟩ + +theorem subset_of_mem_gener {α : Type} (alphabet : List α) : + ∀ n w, w ∈ gener n alphabet → w ⊆ alphabet + | 0, w, h => by + simp [gener] at h + simp [h] + | n + 1, w, h => by + simp only [gener, List.mem_flatMap, List.mem_map] at h + obtain ⟨x, hx, v, hv, rfl⟩ := h + intro c hc + simp at hc + rcases hc with rfl | hc + · exact hx + · exact subset_of_mem_gener alphabet n v hv hc + +theorem recognize_generUpTo (n : Nat) : + ∀ w ∈ generUpTo n "abc".toList, recognize w = true ↔ w.Palindrome := by - native_decide + intro w hw + simp only [generUpTo, List.mem_flatMap] at hw + obtain ⟨k, _, hk⟩ := hw + exact recognize_iff_palindrome w + (subset_of_mem_gener _ k w hk) ``` ::: @@ -146,6 +301,9 @@ theorem recognize_upTo6 : rótulo `A` nos nós. - Mesma receita do reconhecedor, uma linha por regra; agora cada linha devolve a lista das suas árvores, vazia quando a regra não se aplica. +- As regras de uma gramática podem valer ao mesmo tempo, por isso as + listas de todas as linhas são concatenadas com `++`. Numa gramática + ambígua, uma palavra recebe assim mais de uma árvore. - A palavra vazia vira a árvore vazia `ep`. ::: @@ -157,23 +315,28 @@ to the end of the section. :::: ```lean -partial def parse (xs : List Char) : - List (ParseTree Char Char) := +def parse (xs : List Char) : List (ParseTree Char Char) := (if xs == [] then [.ep] else []) ++ (if xs == ['a'] then [.leaf 'a'] else []) ++ (if xs == ['b'] then [.leaf 'b'] else []) ++ (if xs == ['c'] then [.leaf 'c'] else []) ++ - (splitN 3 xs).flatMap fun - | [['a'], ys, ['a']] => + (splitN 3 xs).attach.flatMap fun + | ⟨[['a'], ys, ['a']], _h⟩ => (parse ys).map fun t => .branch 'A' [.leaf 'a', t, .leaf 'a'] - | [['b'], ys, ['b']] => + | ⟨[['b'], ys, ['b']], _h⟩ => (parse ys).map fun t => .branch 'A' [.leaf 'b', t, .leaf 'b'] - | [['c'], ys, ['c']] => + | ⟨[['c'], ys, ['c']], _h⟩ => (parse ys).map fun t => .branch 'A' [.leaf 'c', t, .leaf 'c'] | _ => [] +termination_by xs.length +decreasing_by + all_goals + have := congrArg List.length (flatten_of_mem_splitN _h) + simp at this + omega #eval IO.println (parse "aabaa".toList) #eval IO.println (parse "aabbaa".toList) diff --git a/DEVIATIONS.md b/DEVIATIONS.md index 065cfdb..cccefa0 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -146,13 +146,15 @@ CSwFP/8 is skipped for now, and the chapter follows `ModelChecking`. not ported. Exercises 9.1, 9.3, 9.4 and 9.5 ask for a definition checked on the example tree; 9.6 asks for the splitting functions without empty parts. -- 9.2: `recognize` and `parse` are `partial def`, since Lean cannot see - that the middle piece of a split is shorter than the input. The cue on - `partial def` says why left recursion is no trouble here, which is - exercise 9.7. Generation stops at a given length, since Lean lists are - finite. A theorem checks, with `native_decide`, that `recognize` agrees - with Mathlib's `List.Palindrome` on all words up to length 6; a proof - for all words would need `recognize` to be total. `parse` gives the +- 9.2: `recognize` and `parse` are total. They recurse over + `(splitN 3 xs).attach`, which pairs each split with a proof of + membership, and `decreasing_by` uses the lemma `flatten_of_mem_splitN` + (the pieces of a split concatenate to the input) to show that the + middle piece is shorter. The cue on termination says why left + recursion is no trouble here, which is exercise 9.7. Generation stops + at a given length, since Lean lists are finite. A theorem, in a + `:::details` block, proves that `recognize` agrees with Mathlib's + `List.Palindrome` on every word over `{a, b, c}`. `parse` gives the empty word the empty tree `ep`, where CSwFP uses a leaf `"[]"`. ## Beyond CSwFP/6 diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 3bbd773..16e8b43 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -83,7 +83,7 @@ this way is usually a mistake; see "Known gaps." | `Morphology` | `open` of constructor namespaces (`open Attr Value`) | `match e₁, e₂ with` (first use outside a solution), `mapM` over `Option` **(solution only)** | *(none new)* | | `InfEngine` | `let rec` | `do`-notation | — | | `ModelChecking` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`), pattern-matching `fun \| … => …` (first use outside a solution) | *(none new)* | -| `Parsing` | `partial def` | `<+:` (`List.IsPrefix`), Mathlib's `List.Palindrome` | *(none new)* | +| `Parsing` | `termination_by`, `decreasing_by` | `<+:` (`List.IsPrefix`), Mathlib's `List.Palindrome`, `List.attach` and subtype patterns (`\| ⟨l, h⟩`), `congrArg` | `subst`, `split at`, `try`, `rename_i`, `contradiction`; `rcases` and `Or.inr` (first use outside a solution) | `ModelChecking` is where `abbrev` and `ToString` instances become the dominant idiom, but both arrive earlier; what is genuinely new there is the mutually @@ -147,7 +147,9 @@ author decision, not a mechanical fix. a solution (`Phonemes.lean:309`) and visible only much later, at `InfEngine.lean:439`. The pattern-matching `fun` is the same shape again — `IntroL.lean:364` and `PL.lean:245`, both in solutions, then ordinary code - throughout `ModelChecking`. The rest never surface at all. + throughout `ModelChecking`. `rcases` and `Or.inr` surface in the + `:::details` proofs of `Parsing/Recognition.lean` (lines 92 and 181). + The rest never surface at all. `IntroCS` is the constraint's one accepted exception: it uses Lean that `IntroL` only presents later, deliberately, and the chapter says so where its From 69c88b6c251f892469eda3216d5e72c6bc35c839 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Tue, 3 Nov 2026 22:26:37 -0300 Subject: [PATCH 3/6] fix(Parsing): address review of the parsing chapter splitN now covers every number of pieces: one piece is the input itself, and the empty input has the split into zero pieces. CSwFP's version stops with an error below two. The recursion becomes uniform, splitN serves unary rules, and mem_splitN_flatten holds for every list of pieces. The base cases of splitN' in exercise 9.6 sit outside the solution, so they follow suit there. ParseTree.toText separates the daughters of a node by spaces, as in the bracket notation of qtree, instead of printing them as a list. Nothing reads the text back. Parsing is a glue chapter, so it drops htmlSplit := .never and each section gets its file key, as STYLE-CODE.md asks: each section is now its own page and its own generated module. The cue on left recursion says what goes wrong when the piece of T may be empty, and that Lean would then refuse the definition. AI-usage disclosure: these changes were drafted with the assistance of Claude Opus 5.5 (Anthropic, via Claude Code), under the author's direction, in response to an automated review of the pull request. The author reviewed them and takes full responsibility for the final content. --- CSwL/Parsing.lean | 1 - CSwL/Parsing/ParseTrees.lean | 5 +-- CSwL/Parsing/Recognition.lean | 58 +++++++++++++++++------------------ DEVIATIONS.md | 18 ++++++++--- 4 files changed, 46 insertions(+), 36 deletions(-) diff --git a/CSwL/Parsing.lean b/CSwL/Parsing.lean index 951eddd..0b93355 100644 --- a/CSwL/Parsing.lean +++ b/CSwL/Parsing.lean @@ -9,7 +9,6 @@ open CSwLMeta #doc (Manual) "Análise sintática" => %%% tag := "Parsing" -htmlSplit := .never file := "Parsing" %%% diff --git a/CSwL/Parsing/ParseTrees.lean b/CSwL/Parsing/ParseTrees.lean index d14f4f5..849c70e 100644 --- a/CSwL/Parsing/ParseTrees.lean +++ b/CSwL/Parsing/ParseTrees.lean @@ -7,6 +7,7 @@ open CSwLMeta #doc (Manual) "Falando de árvores sintáticas" => %%% tag := "parse-trees" +file := "ParseTrees" %%% ```lean @@ -21,7 +22,7 @@ namespace Parsing - Um `branch` guarda a *lista* das suas subárvores, por isso cada nó pode ter quantas filhas quiser. - A função `toText` escreve a árvore entre colchetes, com o rótulo depois - de `[.`. + de `[.` e as filhas separadas por espaços. ::: ::::full @@ -43,7 +44,7 @@ def ParseTree.toText {α β : Type} | .leaf a => toString a | .branch b ts => "[." ++ toString b ++ " " ++ - toString (ts.map toText) ++ "]" + " ".intercalate (ts.map toText) ++ "]" instance {α β : Type} [ToString α] [ToString β] : ToString (ParseTree α β) := diff --git a/CSwL/Parsing/Recognition.lean b/CSwL/Parsing/Recognition.lean index 0d0f5dd..507e8b9 100644 --- a/CSwL/Parsing/Recognition.lean +++ b/CSwL/Parsing/Recognition.lean @@ -9,6 +9,7 @@ open CSwLMeta #doc (Manual) "Reconhecendo e analisando linguagens livres de contexto" => %%% tag := "cf-recognition" +file := "Recognition" %%% ```lean @@ -46,11 +47,12 @@ def split2 {α : Type} : List α → List (List α × List α) λ (a, b) ↦ (String.ofList a, String.ofList b) def splitN {α : Type} : Nat → List α → List (List (List α)) - | 0, _ | 1, _ => [] - | 2, xs => (split2 xs).map fun (ys, zs) => [ys, zs] - | n + 3, xs => + | 0, [] => [[]] + | 0, _ :: _ => [] + | 1, xs => [[xs]] + | n + 2, xs => (split2 xs).flatMap fun (ys, zs) => - (splitN (n + 2) zs).map fun rs => ys :: rs + (splitN (n + 1) zs).map fun rs => ys :: rs #eval splitN 3 "Jan".toList |>.map (·.map String.ofList) @@ -70,6 +72,10 @@ def splitN {α : Type} : Nat → List α → List (List (List α)) - Uma regra recursiva à esquerda, V → V T, também não seria problema, porque V recebe um pedaço menor da entrada, desde que o pedaço de T não seja vazio. +- Se o pedaço de T puder ser vazio, V recebe a entrada inteira e chama + a si mesma sem fim. As divisões com pedaço vazio têm de ser + descartadas antes da chamada; sem isso, `decreasing_by` não prova + nada e o Lean recusa a definição. ::: ::::full @@ -96,12 +102,11 @@ theorem append_of_mem_split2 {α : Type} : theorem flatten_of_mem_splitN {α : Type} : ∀ {n : Nat} {xs : List α} {l : List (List α)}, l ∈ splitN n xs → l.flatten = xs - | 0, _, _, h | 1, _, _, h => by simp [splitN] at h - | 2, xs, l, h => by - simp only [splitN, List.mem_map] at h - obtain ⟨⟨ys, zs⟩, h, rfl⟩ := h - simpa using append_of_mem_split2 h - | n + 3, xs, l, h => by + | 0, [], l, h | 1, _, l, h => by + simp [splitN] at h + simp [h] + | 0, _ :: _, _, h => by simp [splitN] at h + | n + 2, xs, l, h => by simp only [splitN, List.mem_flatMap, List.mem_map] at h obtain ⟨⟨ys, zs⟩, h1, rs, h2, rfl⟩ := h simp [flatten_of_mem_splitN h2, append_of_mem_split2 h1] @@ -181,21 +186,16 @@ theorem mem_split2_append {α : Type} : exact Or.inr ⟨(ys, zs), mem_split2_append ys zs, rfl⟩ theorem mem_splitN_flatten {α : Type} : - ∀ l : List (List α), 2 ≤ l.length → - l ∈ splitN l.length l.flatten - | [ys, zs], _ => by - simp only [List.length, splitN, List.mem_map] - exact ⟨(ys, zs), by simpa using mem_split2_append ys zs, - rfl⟩ - | ys :: zs :: ws :: rs, _ => by + ∀ l : List (List α), l ∈ splitN l.length l.flatten + | [] => by simp [splitN] + | [ys] => by simp [splitN] + | ys :: zs :: rs => by simp only [List.length_cons, List.flatten_cons] simp only [splitN, List.mem_flatMap, List.mem_map] - refine ⟨(ys, (zs :: ws :: rs).flatten), + refine ⟨(ys, (zs :: rs).flatten), by simpa using mem_split2_append ys _, - zs :: ws :: rs, ?_, rfl⟩ - simpa using - mem_splitN_flatten (zs :: ws :: rs) (by simp) - | [], h | [_], h => by simp at h + zs :: rs, ?_, rfl⟩ + simpa using mem_splitN_flatten (zs :: rs) theorem recognize_sound (n : Nat) : ∀ w : List Char, w.length ≤ n → @@ -258,8 +258,7 @@ theorem recognize_complete (n : Nat) : right have hmem : [[x], l, [x]] ∈ splitN 3 (x :: (l ++ [x])) := by - simpa using - mem_splitN_flatten [[x], l, [x]] (by simp) + simpa using mem_splitN_flatten [[x], l, [x]] refine ⟨⟨_, hmem⟩, List.mem_attach _ _, ?_⟩ simp at hx rcases hx with rfl | rfl | rfl <;> simpa using ih' @@ -358,13 +357,14 @@ def split2' {α : Type} : List α → List (List α × List α) (x :: us, vs)) def splitN' {α : Type} : Nat → List α → List (List (List α)) - | 0, _ | 1, _ => [] - | 2, xs => - solution!((split2' xs).map fun (ys, zs) => [ys, zs]) - | n + 3, xs => + | 0, [] => [[]] + | 0, _ :: _ => [] + | 1, [] => [] + | 1, xs => [[xs]] + | n + 2, xs => solution!( (split2' xs).flatMap fun (ys, zs) => - (splitN' (n + 2) zs).map fun rs => ys :: rs) + (splitN' (n + 1) zs).map fun rs => ys :: rs) theorem split2'_jan : split2' "Jan".toList = diff --git a/DEVIATIONS.md b/DEVIATIONS.md index cccefa0..97a77b1 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -136,16 +136,26 @@ CSwFP/8 is skipped for now, and the chapter follows `ModelChecking`. - 9.1: the tree relations are lists of pairs, as in CSwFP, because the section shows them with `#eval`; Mathlib's `Rel` of `Sets` is a `Prop` and cannot be printed. Dominance uses Lean's `<+:` (`List.IsPrefix`) in - place of a helper `prefix`. `pos` is written with a helper `posFrom` in a - `mutual` block, so that Lean sees the recursion over the list of - subtrees as structural. `subtree` returns `ep` at a position the tree - does not have, where CSwFP's is undefined. + place of a helper `prefix`. `pos` is written with a local helper + `posFrom` (`let rec`), so that Lean sees the recursion over the list + of subtrees as structural. `subtree` returns `ep` at a position the + tree does not have, where CSwFP's is undefined. `toText` separates the + daughters of a node by spaces, as in the bracket notation of LaTeX's + `qtree` (`[.NP Snow White]`); CSwFP's `show` prints them as a list, + with a further pair of brackets and commas. Nothing reads the text + back: later chapters walk the trees, not their text. - Exercise 9.2 becomes two theorems about positions, parts (1) and (2): the relation of c-command is a sister followed by dominance, and neither part depends on the tree. Part (3), on the lowest branching position, is not ported. Exercises 9.1, 9.3, 9.4 and 9.5 ask for a definition checked on the example tree; 9.6 asks for the splitting functions without empty parts. +- 9.2: `splitN` is defined for every number of pieces, where CSwFP's + stops with an error below two: one piece is the input itself, and the + empty input has the split into zero pieces. This makes `splitN` serve + unary rules too, and lets `mem_splitN_flatten`, the converse of + `flatten_of_mem_splitN`, hold for every list of pieces. `splitN'` in + exercise 9.6 follows suit. - 9.2: `recognize` and `parse` are total. They recurse over `(splitN 3 xs).attach`, which pairs each split with a proof of membership, and `decreasing_by` uses the lemma `flatten_of_mem_splitN` From a5ccc5879789a7661db5d1ae5f9a32cb674bac11 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Wed, 4 Nov 2026 00:23:02 -0300 Subject: [PATCH 4/6] feat(Parsing): add parsers and parser combinators MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Section from CSwFP/9.3. A parser is StateT (List α) List β, which unfolds by definition to a function from the input to the list of (result, remainder) pairs; Mathlib's Monad and Alternative instances for List give pure, failure, <|>, <$> and do-notation with the meaning the section needs. Recursive parsers are partial def. Exercise 9.8 becomes symbol-satisfy; 9.9 is answered in the closing cue, with a left-recursive parser that is defined but never run. The Mastermind parser is dropped with Mastermind; parseManyAs, which only it used, becomes the exercise parse-many-as. AI usage: Claude Code (Claude Opus 5.5) drafted the Lean code, the terse cues and the documentation updates under the author's direction; the author reviewed and approved the changes. --- Bib.lean | 6 + CSwFP.yaml | 9 +- CSwL/Parsing.lean | 11 +- CSwL/Parsing/Combinators.lean | 420 ++++++++++++++++++++++++++++++++++ DEVIATIONS.md | 23 ++ STYLE-CODE.md | 2 +- 6 files changed, 463 insertions(+), 8 deletions(-) create mode 100644 CSwL/Parsing/Combinators.lean diff --git a/Bib.lean b/Bib.lean index 501cbc7..4856a47 100644 --- a/Bib.lean +++ b/Bib.lean @@ -50,6 +50,12 @@ def love2026 : Article where number := inlines!"" url := "https://github.com/lean-forward/logical_verification_2026" +def danielsson2010 : InProceedings where + title := inlines!"Total Parser Combinators" + authors := #[inlines!"Nils Anders Danielsson"] + year := 2010 + booktitle := inlines!"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010)" + def FPiL : Article where title := inlines!"Functional Programming in Lean" authors := #[inlines!"David Thrane Christiansen"] diff --git a/CSwFP.yaml b/CSwFP.yaml index e97ea37..49d88c7 100644 --- a/CSwFP.yaml +++ b/CSwFP.yaml @@ -138,8 +138,9 @@ exercises: 9.6 (p. 214): split-nonempty 9.7 (p. 214): absorbed into the cue on termination, which says why left recursion is no trouble for recognition by splitting - 9.8 (p. 217): TODO - 9.9 (p. 222): TODO + 9.8 (p. 217): symbol-satisfy + 9.9 (p. 222): absorbed into the closing cue of parser-combinators, which + says why left recursion makes a parser loop 9.10 (p. 237): TODO 9.11 (p. 241): TODO 9.12 (p. 244): TODO @@ -179,6 +180,7 @@ original: Morphology/Phonemes.lean: [append-suffix-text] Morphology/SwedishPlural.lean: [swedish-plural] InfEngine.lean: [inconsistent-kb, ferio] + Parsing/Combinators.lean: [parse-many-as] depends: bangu-proof: bangu-form @@ -291,7 +293,8 @@ sections: CSwFP/9: 9.1 Talking About Parse Trees: Parsing 9.2 Recognizing and Parsing Context-Free Languages: Parsing - 9.3 Parsers and Parser Combinators: Parsing, not yet written + 9.3 Parsers and Parser Combinators: Parsing, without the Mastermind + parser, since Mastermind is dropped with 5.4 9.4 Features and Categories: Parsing, not yet written 9.5 Lexical Lookup and Scanning: Parsing, not yet written 9.6 Parsing Categories: Parsing, not yet written diff --git a/CSwL/Parsing.lean b/CSwL/Parsing.lean index 0b93355..f17cd99 100644 --- a/CSwL/Parsing.lean +++ b/CSwL/Parsing.lean @@ -2,6 +2,7 @@ import CSwLMeta import Bib import CSwL.Parsing.ParseTrees import CSwL.Parsing.Recognition +import CSwL.Parsing.Combinators open Verso.Genre Manual open CSwLMeta @@ -21,10 +22,10 @@ omitted). Sections are written `terse` first (see `STYLE-CODE.md`). - 9.2: recognition and parsing by splitting, for the palindrome grammar, total by `termination_by`; agreement with Mathlib's `List.Palindrome` proved for every word over `{a, b, c}`. -- 9.3: list-of-successes parsers, still to decide: `StateT (List α) List` - with Mathlib's `Monad`/`Alternative List`, or plain functions. Lean's - `Std.Internal.Parsec` returns one result, not all parses; it can serve - the lexer of 9.5. +- 9.3: list-of-successes parsers as `StateT (List α) List`, with + Mathlib's `Monad`/`Alternative List`; recursive parsers are + `partial def`. Lean's `Std.Internal.Parsec` returns one result, not + all parses; it can serve the lexer of 9.5. - 9.4–9.8: to plan. The representation of `Cat` is tied to issue 42. ::: @@ -45,3 +46,5 @@ TODO: translate the CSwFP/9 summary. {include 1 CSwL.Parsing.ParseTrees} {include 1 CSwL.Parsing.Recognition} + +{include 1 CSwL.Parsing.Combinators} diff --git a/CSwL/Parsing/Combinators.lean b/CSwL/Parsing/Combinators.lean new file mode 100644 index 0000000..d5c9434 --- /dev/null +++ b/CSwL/Parsing/Combinators.lean @@ -0,0 +1,420 @@ +import CSwLMeta +import Bib +import CSwL.Parsing.ParseTrees +import Mathlib.Data.List.Monad + +open Verso.Genre Manual +open CSwLMeta + +#doc (Manual) "Parsers e combinadores de parsers" => +%%% +tag := "parser-combinators" +file := "Combinators" +%%% + +```lean +namespace Parsing +``` + +:::terse +- Objetivo: um método geral para analisar com qualquer gramática livre + de contexto, em que o código do parser tem a forma das regras da + gramática. +- Basta tratar três coisas: os símbolos terminais, a escolha `|` entre + regras, e a sequência B₁ ⋯ Bₙ do lado direito de uma regra. +- Um parser lê um *prefixo* da entrada e devolve todos os pares + (resultado, resto da entrada) que consegue construir. A lista vazia é + a falha; mais de um par é ambiguidade. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from the start to the type of a parser. +::: +:::: + +:::terse +- Em Lean, esse tipo já existe: `StateT (List α) List β`. O estado é o + resto da entrada, e `List` dá as várias respostas. +- O `example` mostra que os dois tipos são o mesmo, por definição: um + `Parser` é uma função, e pode ser escrito como tal. +- Usar `StateT` dá de graça as operações de que vamos precisar, com a + notação que o Lean já tem para elas: `pure`, `failure`, `<|>`, `<$>` e + `do`. +::: + +```lean +abbrev Parser (α β : Type) := StateT (List α) List β + +example {α β : Type} : + Parser α β = (List α → List (β × List α)) := rfl +``` + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from "The parser uses the grammar rules…" to +Figure 9.1 and the paragraph after it. +::: +:::: + +:::terse +- Os dois parsers mais simples não leem nada. O parser `pure r` sempre + dá certo, com o resultado `r`. O parser `failure` sempre falha. +- A expressão `p.run xs` aplica o parser `p` à entrada `xs`. +::: + +```lean +#eval (pure 1 : Parser Char Nat).run "ab".toList +#eval (failure : Parser Char Nat).run "ab".toList +``` + +:::terse +- O parser `symbol c` reconhece o símbolo `c` no início da entrada; + `token cs`, a lista de símbolos `cs`; `satisfy p`, um símbolo + qualquer que tenha a propriedade `p`. +- Os três são escritos diretamente como funções sobre a entrada. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from "Two very elementary parsers…" to the +definition of `digit`. +::: +:::: + +```lean +def symbol {α : Type} [BEq α] (c : α) : Parser α α + | x :: xs => if x == c then [(x, xs)] else [] + | [] => [] + +def token {α : Type} [BEq α] (cs : List α) + : Parser α (List α) + | xs => + if cs == xs.take cs.length then + [(cs, xs.drop cs.length)] + else [] + +def satisfy {α : Type} (p : α → Bool) : Parser α α + | x :: xs => if p x then [(x, xs)] else [] + | [] => [] + +def digit : Parser Char Char := satisfy Char.isDigit + +#eval (symbol 'a').run "ab".toList +#eval (token "ab".toList).run "abc".toList +#eval digit.run "42".toList +``` + +::::exercise (rating := 1) (name := "symbol-satisfy") +Defina `symbol'`, que faz o mesmo que `symbol`, usando `satisfy`. + +```lean +def symbol' {α : Type} [BEq α] (c : α) : Parser α α := + solution!(satisfy (· == c)) + +theorem symbol'_eq_symbol {α : Type} [BEq α] (c : α) + (xs : List α) : symbol' c xs = symbol c xs := by + solution! + cases xs <;> rfl +``` +:::: + +:::terse +- Os parsers elementares servem para os terminais. Com terminais + `String`, a palavra *Alice* é `symbol "Alice"`; com terminais `Char`, + é `token "Alice".toList`. +- Combinadores de parsers são funções que constroem parsers a partir de + outros parsers. +- O combinador `just` filtra as análises: `just p` só aceita as de `p` + que consomem a entrada toda. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from "Now, these elementary parsers…" to the +definition of `just`. +::: +:::: + +```lean +def just {α β : Type} (p : Parser α β) : Parser α β + | xs => (p xs).filter fun (_, ys) => ys.isEmpty +``` + +:::terse +- A escolha é `p <|> q`: todas as análises de `p`, seguidas de todas as + de `q`. O `example` mostra que isso é a concatenação das listas. +- VP → smiled | laughed vira `symbol "smiled" <|> symbol "laughed"`. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from "For parsing one of our grammars…" to +the parser for VP. +::: +:::: + +```lean +example {α β : Type} (p q : Parser α β) (xs : List α) : + (p <|> q) xs = p xs ++ q xs := rfl +``` + +:::terse +- A sequência é um bloco `do`. Em `let r₁ ← p`, o parser `p` lê o início + da entrada e dá o resultado `r₁`; o parser da linha seguinte começa no + resto que `p` deixou. +- Cada análise de `p` continua separadamente. O `example` mostra a + operação por trás do `do`, `>>=`: um `flatMap` sobre as análises de + `p`. +- Com isso, a gramática da figura vira uma definição por regra; aqui, o + resultado é só a lista das palavras lidas. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from "Next, what to do with rules like +S → NP VP?" to the definitions of `pS`, …, `pN` and the paragraph +after them. +::: +:::: + +```lean +example {α β γ : Type} (p : Parser α β) (q : β → Parser α γ) + (xs : List α) : + (p >>= q) xs = + (p xs).flatMap fun (r, ys) => q r ys := rfl + +def pD : Parser String String := + symbol "every" <|> symbol "some" <|> symbol "no" + +def pN : Parser String String := + symbol "dwarf" <|> symbol "wizard" + +def pVP : Parser String String := + symbol "smiled" <|> symbol "laughed" + +def pNP : Parser String (List String) := + (do + let w ← symbol "Alice" <|> symbol "Dorothy" + return [w]) <|> + (do + let d ← pD + let n ← pN + return [d, n]) + +def pS : Parser String (List String) := do + let np ← pNP + let vp ← pVP + return np ++ [vp] + +#eval pS.run ["every", "wizard", "smiled"] +#eval pS.run ["Alice", "laughed", "loudly"] +``` + +:::terse +- O parser `f <$> p` aplica `f` ao resultado de cada análise de `p`, + sem mexer no resto da entrada. +- O parser `digitize` lê um dígito e devolve o número que ele + representa. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from "However, we are not quite there +yet…" to the definition of `digitize`. +::: +:::: + +```lean +example {α β γ : Type} (f : β → γ) (p : Parser α β) + (xs : List α) : + (f <$> p) xs = + (p xs).flatMap fun (r, ys) => [(f r, ys)] := rfl + +def digitize : Parser Char Nat := + (fun c => c.toNat - '0'.toNat) <$> digit + +#eval digitize.run "42".toList +``` + +:::terse +- Agora, parsers que constroem árvores: `Parser α (ParseTree α β)`, + com terminais `α` nas folhas e não terminais `β` nos nós. +- O parser `epsilonT` não lê nada e dá a árvore vazia. O parser + `symbolT s` lê o terminal `s` e dá uma folha. +- A função `collect` aplica uma lista de parsers um depois do outro e + junta os resultados numa lista. A função `parseAs` faz disso um nó: + `parseAs A ps` é a regra A → B₁ ⋯ Bₙ, com `ps` os parsers de B₁, …, + Bₙ, e o nó tem rótulo `A`. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, from "We will use <$> for constructing parse +trees." to the definition of `parseAs` and the paragraph after it. +::: +:::: + +```lean +def epsilonT {α β : Type} : Parser α (ParseTree α β) := + pure .ep + +def symbolT {α β : Type} [BEq α] (s : α) : + Parser α (ParseTree α β) := + .leaf <$> symbol s + +def collect {α β : Type} : + List (Parser α β) → Parser α (List β) + | [] => pure [] + | p :: ps => do + let r ← p + let rs ← collect ps + return r :: rs + +def parseAs {α β : Type} (label : β) + (ps : List (Parser α (ParseTree α β))) : + Parser α (ParseTree α β) := + .branch label <$> collect ps +``` + +:::terse +- A gramática de novo, agora com árvores: um parser por categoria, uma + linha por regra. +::: + +```lean +def det : Parser String (ParseTree String Char) := + symbolT "every" <|> symbolT "some" <|> symbolT "no" + +def cn : Parser String (ParseTree String Char) := + symbolT "man" <|> symbolT "woman" + +def vp : Parser String (ParseTree String Char) := + symbolT "smiled" <|> symbolT "laughed" + +def np : Parser String (ParseTree String Char) := + symbolT "Alice" <|> symbolT "Dorothy" + <|> parseAs 'N' [det, cn] + +def sent : Parser String (ParseTree String Char) := + parseAs 'S' [np, vp] + +#eval (just sent).run ["every", "man", "laughed"] |>.map + (toString ·.1) +``` + +:::terse +- Os palíndromos outra vez, agora uma linha por regra da gramática. Não + há mais divisão da entrada: cada parser lê o que precisa e deixa o + resto para o seguinte. +- O parser `palindrome` chama a si mesmo, mas sobre um resto da entrada + que o Lean não vê: ele está escondido dentro do `StateT`. Por isso a + definição é `partial def`. O Lean aceita a definição sem provar que + ela termina, mas em troca não conhece a equação que a define: nada + que dependa do que `palindrome` faz pode ser provado. +- Sem `just`, o parser também devolve as análises de prefixos da + entrada, com o seu resto. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, the sentences introducing the two parsers +above and the palindrome parser. +::: +:::: + +```lean +partial def palindrome : + Parser Char (ParseTree Char Char) := + epsilonT <|> symbolT 'a' <|> symbolT 'b' <|> symbolT 'c' + <|> parseAs 'A' [symbolT 'a', palindrome, symbolT 'a'] + <|> parseAs 'A' [symbolT 'b', palindrome, symbolT 'b'] + <|> parseAs 'A' [symbolT 'c', palindrome, symbolT 'c'] + +#eval (just palindrome).run "abcba".toList |>.map + (toString ·.1) +#eval palindrome.run "aba".toList |>.map fun (t, ys) => + (toString t, String.ofList ys) +``` + +:::terse +- O combinador `many` faz a repetição `{A}` das gramáticas em EBNF: + `many p` aplica `p` quantas vezes for possível, inclusive nenhuma. A análise mais longa vem + primeiro. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, the sentences introducing `many`. +::: +:::: + +```lean +partial def many {α β : Type} (p : Parser α β) : + Parser α (List β) := + (do + let r ← p + let rs ← many p + return r :: rs) <|> pure [] + +#eval (many (symbol 'a')).run "aab".toList +``` + +::::exercise (rating := 1) (name := "parse-many-as") +Para ter uma árvore, a repetição precisa ficar sob um rótulo. Defina +`parseManyAs l p`, que aplica `p` quantas vezes for possível e põe as +árvores obtidas sob um nó com rótulo `l`. Confira o resultado com +`adjectives`, uma sequência de adjetivos sob o rótulo `J`. + +```lean +def parseManyAs {α β : Type} (l : β) + (p : Parser α (ParseTree α β)) : + Parser α (ParseTree α β) := + solution!(.branch l <$> many p) + +def adjectives : Parser String (ParseTree String Char) := + parseManyAs 'J' (symbolT "happy" <|> symbolT "evil") + +theorem adjectives_happy_evil : + ((adjectives.run ["happy", "evil", "dwarf"]).map + fun (t, ys) => (toString t, ys)) = + [("[.J happy evil]", ["dwarf"]), + ("[.J happy]", ["evil", "dwarf"]), + ("[.J ]", ["happy", "evil", "dwarf"])] := by + solution! + native_decide +``` +:::: + +:::terse +- Em resumo: um terminal t vira `symbolT t`, um não terminal A vira + `parseAs A`, a escolha vira `<|>`, e o lado direito de uma regra vira a + lista de parsers passada a `parseAs`. +- O método não serve para toda gramática livre de contexto. Numa regra + recursiva à esquerda, A → A T, o parser de A chama a si mesmo antes de + ler qualquer símbolo, sobre a mesma entrada, e nunca para. +- O parser `leftRec` abaixo é aceito, por ser `partial def`, mas não + deve ser rodado: cada chamada abre outra, até esgotar a pilha, e o Lean para + com um erro de recursão profunda. +- O reconhecedor por divisão não tinha esse problema, desde que as + divisões com pedaço vazio fossem descartadas: aí cada chamada recebia + um pedaço menor da entrada, e o Lean exigia uma prova disso. +- Há combinadores de parsers que garantem a terminação e aceitam + recursão à esquerda; ver {citep Bib.danielsson2010}[]. +::: + +::::full +:::dev BeforeNextRelease +TODO: translate CSwFP/9.3, the closing summary ("To sum up, …"), +without the sentence on `parseManyAs`. +::: +:::: + +```lean +partial def leftRec : Parser Char (ParseTree Char Char) := + parseAs 'A' [leftRec, symbolT 'a'] <|> symbolT 'b' +``` + +```lean +end Parsing +``` diff --git a/DEVIATIONS.md b/DEVIATIONS.md index 97a77b1..0d43940 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -166,6 +166,29 @@ CSwFP/8 is skipped for now, and the chapter follows `ModelChecking`. `:::details` block, proves that `recognize` agrees with Mathlib's `List.Palindrome` on every word over `{a, b, c}`. `parse` gives the empty word the empty tree `ep`, where CSwFP uses a leaf `"[]"`. +- 9.3: `Parser α β` is `StateT (List α) List β`, which unfolds by + definition to CSwFP's `[a] -> [(b,[a])]` (an `example … := rfl` says + so). Mathlib's `Monad` and `Alternative` instances for `List` then give + `pure`, `failure`, `<|>` and `<$>` with CSwFP's meaning, so `succeed` + and `failp` are not defined: they are `pure` and `failure`. CSwFP's + sequencing `<*>` and `<:>` become `do` blocks (Lean's `<*>` is the + applicative one, with another type), and `collect` is written with + `do`. The synonym `PARSER a b` is not ported: as an `abbrev` over + `Parser α (ParseTree α β)` it hides the type constructor that `<$>` + and `<|>` need to find their instances. Lean's `Std.Internal.Parsec` + was considered and rejected: it returns one result, and its `<|>` + commits to the first alternative that succeeds. +- 9.3: `palindrome`, `many` and the left-recursive example are + `partial def`. The input they recurse on is the remainder left inside + the `StateT`, and proving it shorter would need parsers that carry a + proof that their remainder is a suffix of the input. Later sections + only run parsers. A cue cites Danielsson's total parser combinators. + The left-recursive example is defined but never run: it overflows the + stack. +- 9.3: the Mastermind parser is dropped with Mastermind (see 5.4). + `many` stays: 9.6 uses it. `parseManyAs`, which only the Mastermind + parser used, becomes the new exercise `parse-many-as`, checked on a + sequence of adjectives. ## Beyond CSwFP/6 diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 16e8b43..044d019 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -83,7 +83,7 @@ this way is usually a mistake; see "Known gaps." | `Morphology` | `open` of constructor namespaces (`open Attr Value`) | `match e₁, e₂ with` (first use outside a solution), `mapM` over `Option` **(solution only)** | *(none new)* | | `InfEngine` | `let rec` | `do`-notation | — | | `ModelChecking` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`), pattern-matching `fun \| … => …` (first use outside a solution) | *(none new)* | -| `Parsing` | `termination_by`, `decreasing_by` | `<+:` (`List.IsPrefix`), Mathlib's `List.Palindrome`, `List.attach` and subtype patterns (`\| ⟨l, h⟩`), `congrArg` | `subst`, `split at`, `try`, `rename_i`, `contradiction`; `rcases` and `Or.inr` (first use outside a solution) | +| `Parsing` | `termination_by`, `decreasing_by`, `partial def` | `<+:` (`List.IsPrefix`), Mathlib's `List.Palindrome`, `List.attach` and subtype patterns (`\| ⟨l, h⟩`), `congrArg`, `StateT` with Mathlib's `Monad`/`Alternative List`, `pure`, `failure`, `<\|>`, `<$>`, `>>=`, `.run` | `subst`, `split at`, `try`, `rename_i`, `contradiction`; `rcases` and `Or.inr` (first use outside a solution) | `ModelChecking` is where `abbrev` and `ToString` instances become the dominant idiom, but both arrive earlier; what is genuinely new there is the mutually From 03af59fbb3549e97fef2fc1315aee3a15752dd55 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Wed, 4 Nov 2026 00:23:02 -0300 Subject: [PATCH 5/6] docs(Parsing): name the identifier that opens a cue sentence Terse cues in ParseTrees and Recognition no longer open a sentence with a lowercase Lean identifier, as STYLE-WRITING.md asks. The cue on pos now says it uses a local let rec helper, not a mutual block. AI usage: Claude Code (Claude Opus 5.5) rewrote the sentences at the author's request; the author reviewed the changes. --- CSwL/Parsing/ParseTrees.lean | 26 ++++++++++++++------------ CSwL/Parsing/Recognition.lean | 27 +++++++++++++++------------ 2 files changed, 29 insertions(+), 24 deletions(-) diff --git a/CSwL/Parsing/ParseTrees.lean b/CSwL/Parsing/ParseTrees.lean index 849c70e..fb2d4f7 100644 --- a/CSwL/Parsing/ParseTrees.lean +++ b/CSwL/Parsing/ParseTrees.lean @@ -18,7 +18,7 @@ namespace Parsing - Uma árvore sintática tem informação lexical nas folhas e informação sintática nos nós internos. - O tipo deixa as duas em aberto: `α` para as folhas, `β` para os rótulos - dos nós. `ep` é a árvore vazia. + dos nós. O construtor `ep` é a árvore vazia. - Um `branch` guarda a *lista* das suas subárvores, por isso cada nó pode ter quantas filhas quiser. - A função `toText` escreve a árvore entre colchetes, com o rótulo depois @@ -65,11 +65,12 @@ def snowWhite : ParseTree String String := - Para apontar uma ocorrência usamos uma *posição*: a lista dos índices das filhas no caminho desde a raiz, contando a partir de 0. A raiz é a posição `[]`. -- `pos` lista todas as posições. Como a recursão desce por uma lista de - subárvores, ela é escrita junto com `posFrom`, num bloco `mutual`: - `posFrom i ts` dá as posições das árvores de `ts`, a primeira com - índice `i`. -- `subtree t p` é a subárvore de `t` na posição `p`. Numa posição que +- A função `pos` lista todas as posições. Como a recursão desce por uma + lista de subárvores, ela usa uma função auxiliar local, definida com + `let rec`: `posFrom i ts` dá as posições das árvores de `ts`, a + primeira com índice `i`. +- A função `subtree` dá subárvores: `subtree t p` é a de `t` na posição + `p`. Numa posição que não existe em `t`, devolve `ep`; isso nunca acontece com as posições de `pos t`. ::: @@ -120,8 +121,8 @@ def subtrees {α β : Type} (t : ParseTree α β) - Em Lean, `p <+: q` diz que `p` é prefixo de `q`. É uma proposição decidível, então pode ser usada como `Bool` num `filter`. - As relações sobre as posições de uma árvore são listas de pares. - `posPairs` lista todos os pares de posições; cada relação filtra os - que lhe interessam. + A função `posPairs` lista todos os pares de posições; cada relação + filtra os que lhe interessam. ::: ::::full @@ -176,8 +177,9 @@ theorem immDominance_snowWhite : coincidem em tudo, menos no último índice. - O *c-comando* é a composição de duas relações: `p` c-comanda `q` quando uma irmã de `p` domina `q`. -- `relComp r s` liga `x` a `z` quando `r` liga `x` a algum `y` e `s` liga - esse `y` a `z`. `eraseDups` tira os pares repetidos. +- A composição é `relComp`: `relComp r s` liga `x` a `z` quando `r` + liga `x` a algum `y` e `s` liga esse `y` a `z`. A função `eraseDups` + tira os pares repetidos. - Na árvore `snowWhite`, o sujeito `[0]` c-comanda tudo o que está dentro do VP; o objeto `[1, 1]` c-comanda o verbo `[1, 0]`, mas não o sujeito. ::: @@ -346,8 +348,8 @@ theorem mutualCCommand_snowWhite : :::: :::terse -- `p` *precede* `q` quando, no primeiro índice em que diferem, o de `p` é - menor. Uma posição não precede as que ela domina. +- Uma posição `p` *precede* `q` quando, no primeiro índice em que + diferem, o de `p` é menor. Uma posição não precede as que ela domina. ::: ::::full diff --git a/CSwL/Parsing/Recognition.lean b/CSwL/Parsing/Recognition.lean index 507e8b9..04ab307 100644 --- a/CSwL/Parsing/Recognition.lean +++ b/CSwL/Parsing/Recognition.lean @@ -26,7 +26,8 @@ namespace Parsing - A ideia para qualquer gramática livre de contexto: uma regra com `n` símbolos à direita divide a entrada em `n` pedaços, de todos os modos possíveis, e testa cada pedaço contra o seu símbolo. -- `split2` dá todas as divisões de uma lista em duas; `splitN n`, em `n`. +- A função `split2` dá todas as divisões de uma lista em duas; + `splitN n`, em `n`. - Em Lean. `"Jan".toList` dá a lista de caracteres, e `String.ofList` faz o caminho de volta. ::: @@ -62,13 +63,14 @@ def splitN {α : Type} : Nat → List α → List (List (List α)) - O reconhecedor segue a gramática: uma linha por regra. Para A → aAa, ele procura uma divisão em três pedaços `[a]`, `ys`, `[a]` e reconhece `ys`. -- `recognize` chama a si mesma em `ys`. Lean exige que toda função +- A função `recognize` chama a si mesma em `ys`. Lean exige que toda função termine, e sozinho ele não vê que `ys` é menor do que `xs`: o padrão `[['a'], ys, ['a']]` não diz de onde a lista veio. -- `attach` junta a cada divisão a prova de que ela está em - `splitN 3 xs`. `termination_by xs.length` diz o que diminui; - `decreasing_by` prova que diminui, com o lema do bloco acima: os - pedaços juntos dão `xs`, então `ys` tem dois elementos a menos. +- A função `attach` junta a cada divisão a prova de que ela está em + `splitN 3 xs`. A cláusula `termination_by xs.length` diz o que + diminui, e `decreasing_by` prova que diminui, com o lema do bloco + acima: os pedaços juntos dão `xs`, então `ys` tem dois elementos a + menos. - Uma regra recursiva à esquerda, V → V T, também não seria problema, porque V recebe um pedaço menor da entrada, desde que o pedaço de T não seja vazio. @@ -133,9 +135,9 @@ decreasing_by ``` :::terse -- `gener n` dá as palavras de comprimento `n`; `generUpTo n`, as de - comprimento até `n`. As palavras são infinitas, mas uma lista em Lean é - finita, por isso a geração para num comprimento dado. +- A função `gener n` dá as palavras de comprimento `n`; `generUpTo n`, + as de comprimento até `n`. As palavras são infinitas, mas uma lista + em Lean é finita, por isso a geração para num comprimento dado. ::: ::::full @@ -165,12 +167,13 @@ def generUpTo {α : Type} (n : Nat) (alphabet : List α) : `List.Palindrome`. Os seus três construtores são as regras da gramática: a lista vazia, uma lista de um elemento, e `x :: (l ++ [x])` para `l` palíndromo. -- `recognize_iff_palindrome`: `recognize` concorda com essa definição - em toda palavra sobre `{a, b, c}`, de qualquer comprimento. +- O teorema `recognize_iff_palindrome` diz que `recognize` concorda + com essa definição em toda palavra sobre `{a, b, c}`, de qualquer + comprimento. - A prova é por indução no comprimento da palavra, uma direção de cada vez. Ela só é possível porque `recognize` não é `partial`: o Lean conhece a equação que a define. -- `recognize_generUpTo` é o caso das palavras geradas por +- O teorema `recognize_generUpTo` é o caso das palavras geradas por `generUpTo n`, para todo `n`. ::: From 88c84c01af45a14ab4148dd16c90bd7213c24188 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Wed, 4 Nov 2026 01:04:41 -0300 Subject: [PATCH 6/6] docs(style): update line references to Recognition in the ledger AI usage: Claude Code (Claude Opus 5.5) found and fixed the stale references; the author reviewed the change. --- STYLE-CODE.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 06f05e5..5d327f6 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -149,7 +149,7 @@ author decision, not a mechanical fix. `InfEngine.lean:439`. The pattern-matching `fun` is the same shape again — `IntroL.lean:364` and `PL.lean:245`, both in solutions, then ordinary code throughout `ModelChecking`. `rcases` and `Or.inr` surface in the - `:::details` proofs of `Parsing/Recognition.lean` (lines 92 and 181). + `:::details` proofs of `Parsing/Recognition.lean` (lines 100 and 189). The rest never surface at all. `IntroCS` is the constraint's one accepted exception: it uses Lean that