From b5b000eda0802e9e0fa850433dfe6d0247dfb9db Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sun, 20 Sep 2026 23:27:56 -0300 Subject: [PATCH 1/7] =?UTF-8?q?feat(English):=20write=20the=20chapter=20fr?= =?UTF-8?q?om=20CSwFP/6.1,=204.2,=206.2=20and=206.3=E2=80=936.4?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. `CSwFP.yaml` maps the chapter's exercises and sections, and `DEVIATIONS.md` gains the chapter's decisions. `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. --- Bib.lean | 18 + CSwFP.yaml | 54 ++- CSwL/English.lean | 1132 ++++++++++++++++++++++++++++++++++++++++++++- DEVIATIONS.md | 32 +- STYLE-CODE.md | 11 +- 5 files changed, 1204 insertions(+), 43 deletions(-) diff --git a/Bib.lean b/Bib.lean index af1ab53..501cbc7 100644 --- a/Bib.lean +++ b/Bib.lean @@ -97,6 +97,24 @@ def keller1902 : Article where volume := inlines!"" number := inlines!"" +def carroll1865 : Article where + title := inlines!"Alice in Wonderland" + authors := #[inlines!"Lewis Carroll"] + journal := inlines!"Macmillan, Londres" + year := 1865 + month := none + volume := inlines!"" + number := inlines!"" + +def russell1905 : Article where + title := inlines!"On Denoting" + authors := #[inlines!"Bertrand Russell"] + journal := inlines!"Mind" + year := 1905 + month := none + volume := inlines!"14" + number := inlines!"56" + def enderton2001 : Article where title := inlines!"A Mathematical Introduction to Logic" authors := #[inlines!"Herbert B. Enderton"] diff --git a/CSwFP.yaml b/CSwFP.yaml index a474c10..55389a8 100644 --- a/CSwFP.yaml +++ b/CSwFP.yaml @@ -35,9 +35,9 @@ exercises: 2.12 (p. 21): graph-is-functional 2.13 (p. 26): TODO, was `twice`, no longer in the book 2.14 (p. 26): in the prose of IntroL - 2.15 (p. 28): TODO, typing of lambda terms, goes with 2.5 to English + 2.15 (p. 28): dropped with the typing rules of 2.5 2.16 (p. 28): in the prose of IntroL - 2.17 (p. 30): TODO, was `adjective-types`, no longer in the book + 2.17 (p. 30): dropped with the categorial section of 2.5 CSwFP/3: 3.1 (p. 36): about Haskell itself @@ -66,9 +66,9 @@ exercises: 4.3 (p. 67): dropped with Mastermind 4.4 (p. 67): dropped with Mastermind 4.5 (p. 68): TODO - 4.6 (p. 69): TODO - 4.7 (p. 69): preposition-phrase # pending #29 - 4.8 (p. 69): complex-relative-clauses # pending #29 + 4.6 (p. 69): absorbed, since `ADJ` has happy and evil from its declaration + 4.7 (p. 69): preposition-phrase + 4.8 (p. 69): complex-relative-clauses 4.9 (p. 74): bangu-form 4.10 (p. 74): exclusive-or 4.11 (p. 74): needs Mathlib's ContextFreeGrammar @@ -112,8 +112,8 @@ exercises: 5.23 (p. 104): in the prose of Logic/FOL 5.24 (p. 104): ex-fol-consequence 5.25 (p. 105): ex-fol-entails - 5.26 (p. 106): TODO - 5.27 (p. 106): TODO + 5.26 (p. 106): check-sentence is the mechanised form of the same question + 5.27 (p. 106): fragment-translations 5.28 (p. 109): soundness is within reach, completeness needs a model construction 5.29 (p. 109): soundness is within reach, completeness needs a model construction 5.30 (p. 110): TODO @@ -121,13 +121,13 @@ exercises: 5.32 (p. 115): TODO CSwFP/6: - 6.1 (p. 137): help-defeat # pending #29 - 6.2 (p. 137): TODO - 6.3 (p. 138): TODO - 6.4 (p. 139): reflexive-ditransitive # pending #29 - 6.5 (p. 141): TODO - 6.6 (p. 146): TODO - 6.7 (p. 147): check-sentence # pending #29 + 6.1 (p. 137): help-defeat + 6.2 (p. 137): passivize is presented in the prose, as the motivation for Unspec + 6.3 (p. 138): passivize is presented in the prose, as the motivation for Unspec + 6.4 (p. 139): reflexive-ditransitive + 6.5 (p. 141): TODO, goes with 6.5 to Logic/FOL + 6.6 (p. 146): TODO, goes with 6.5 to Logic/FOL + 6.7 (p. 147): check-sentence original: IntroL.lean: [sum-of-squares, sum-to, sum-list, count-zeros] @@ -160,12 +160,12 @@ original: Morphology/Phonemes.lean: [append-suffix-text] Morphology/SwedishPlural.lean: [swedish-plural] InfEngine.lean: [inconsistent-kb, ferio] - English.lean: [fragment-translations] # pending #29 depends: bangu-proof: bangu-form pl-consequence: implies-from-list ex-fol-entails: ex-fol-implies-from-list + help-defeat: check-sentence sections: @@ -184,11 +184,11 @@ sections: 2.4 Lambda calculus: to: IntroL why: With Lean already on screen, lambda calculus is the theory of what - the reader has just written. Its linguistic example goes to English. + the reader has just written. Its linguistic example is dropped, with 2.5. 2.5 Types in Grammar and Computation: - to: English - why: The semantic types e and t and the typing rules are about the - fragment, and are shown over its own types. + to: dropped + why: 6.1 makes the same point in English, that a proper name translates + as λP ↦ P g. Making it twice would fragment the presentation. 2.6 Functional Programming: to: absorbed why: It bridges to a programming language the reader has already seen. @@ -211,8 +211,8 @@ sections: 3.12 Identifiers in Haskell: omitted 3.13 User-defined Data Types and Pattern Matching: to: IntroL - why: Its Subject/Predicate example goes to English, so that no fragment - of natural language appears before the one English builds. + why: Its Subject/Predicate example is dropped, so that no fragment of + natural language appears before the one English builds. 3.14 Application, Representing Phonemes: Morphology 3.15 Further Reading: omitted @@ -243,7 +243,10 @@ sections: to: Logic/FOL why: The model is the four-vertex graph of Enderton, since the model of 6.3 belongs with the fragment it interprets. - 5.6 Semantics of Natural Language Fragments: English + 5.6 Semantics of Natural Language Fragments: + to: English + why: Only its exercise 5.27 is kept. Its translation key is superseded by + 6.2, which computes the translation. 5.7 An Inference Engine with a Natural Language Interface: to: InfEngine why: The natural-language input, the only use of IO in the book, is not @@ -251,10 +254,13 @@ sections: 5.8 Further Reading: omitted CSwFP/6: - 6.1 Linguistic Form and Translation Into Logic: English + 6.1 Linguistic Form and Translation Into Logic: English, before 4.2 6.2 Predicate Logic as Representation Language: English 6.3 Representing a Model for Predicate Logic: English - 6.4 Evaluating Formulas in Models: English + 6.4 Evaluating Formulas in Models: + to: English + why: Absorbed. Its interpretation, assignments and eval are already in + Logic/FOL, so English adds only the model and checkSentence. 6.5 Evaluating Formulas with Structured Terms: to: Logic/FOL why: It is about the evaluator, not the fragment. The evaluation over diff --git a/CSwL/English.lean b/CSwL/English.lean index ac34671..d21c932 100644 --- a/CSwL/English.lean +++ b/CSwL/English.lean @@ -1,6 +1,6 @@ import CSwLMeta import Bib -import CSwL.Sets +import CSwL.Logic.FOL open Verso.Genre Manual open CSwLMeta @@ -17,29 +17,1141 @@ namespace English ``` # Formas Linguísticas e Traduções para Lógica +%%% +tag := "english-form" +%%% + +> — Não vejo ninguém na estrada — disse Alice. +> +> — Quem dera eu tivesse olhos assim — observou o Rei, em tom lamentoso. — Poder ver Ninguém! E a essa distância, ainda por cima! +> +> {citep Bib.carroll1865}[] + +Da sentença *Alice walked on the road* segue-se que alguém caminhou na estrada, mas de *No one walked on the road* não se segue que alguém caminhou na estrada. Por isso lógicos como Gottlob Frege (1848–1925), Bertrand Russell (1872–1970), Alfred Tarski (1902–1983) e Willard Van Orman Quine (1908–2000) sustentaram que a estrutura dessas duas sentenças tem de ser diferente, e que não basta dizer que ambas são composições de um sujeito e um predicado. + +Os lógicos que usaram a lógica de predicados de primeira ordem para analisar a estrutura lógica da língua natural se impressionaram com o fato de que as traduções lógicas de sentenças com expressões quantificadas não pareciam acompanhar a estrutura linguística. Nas traduções lógicas, as expressões quantificadas pareciam ter desaparecido. A tradução lógica de (1) não revela nenhum constituinte correspondente ao sintagma nominal quantificado que faz de sujeito. + +```display +(1) Every dwarf loved Goldilocks. + +(2) ∀x (Dwarf x → Love x g) +``` + +Na tradução (2) o constituinte *every dwarf* desapareceu; ele foi contextualmente eliminado. Frege observa que uma expressão quantificada como *every dwarf* não dá origem a um conceito por si só — *eine selbständige Vorstellung* —, e só pode ser interpretada no contexto da tradução da sentença inteira. Considerando este exemplo em particular, a paráfrase literal de (2) é: + +> Todos os objetos do domínio de discurso têm a propriedade de ou não ser anões, ou ser objetos que amaram Goldilocks. + +Nessa reformulação da sentença (1), o sintagma *every dwarf* não ocorre mais. + +As propriedades lógicas das sentenças que envolvem expressões quantificadas — e descrições, analisadas em termos de quantificadores — sugeriam, de fato, que o modo como um sintagma nominal simples, como um nome próprio, se combina com um predicado é logicamente diferente do modo como um sintagma nominal quantificado ou uma descrição definida se combina com um predicado. Isso levou à crença de que a forma linguística das expressões da língua natural era enganosa. -:::dev "Alexandre (arademaker)" -aqui entra seção CSwFP/6.1 +A aplicação das ferramentas lógicas de abstração e redução do cálculo lambda nos permite ver que essa conclusão era injustificada. Traduzindo a língua natural em expressões de uma lógica tipada, veremos que os constituintes da língua natural correspondem a expressões tipadas que se combinam umas com as outras como funções e argumentos. Depois da redução completa dos resultados, as expressões quantificadas e outros constituintes podem ter sido contextualmente eliminados, mas essa eliminação é resultado do processo de redução, e não da suposta forma enganosa da sentença original. Assim, embora as traduções lógicas completamente reduzidas de sentenças da língua natural possam ser enganosas em algum sentido, as expressões originais, não reduzidas, não são. + +Como exemplo do modo como as ferramentas do cálculo lambda aplainam as aparências lógicas, considere a lógica da combinação de sujeitos e predicados. Nos casos mais simples — como *Goldilocks laughed* — poderíamos dizer que o predicado toma o sujeito como argumento. Mas isso não funciona para sujeitos quantificados, como em *no one laughed*. Tudo se resolve, porém, se dissermos que o sujeito sempre toma o predicado como seu argumento, e fizermos isso valer também para os sujeitos simples, elevando logicamente seu estatuto de argumento a função. Com expressões lambda isso é bastante fácil: traduzimos *Goldilocks* não como a constante `g`, e sim como a expressão `λP ↦ P g`. Essa expressão denota uma função de propriedades em valores de verdade, e pode portanto tomar a tradução de um predicado como argumento. A tradução de *no one* é do mesmo tipo: + +```display +λP ↦ ¬∃x (Person x ∧ P x) +``` + +Antes da redução, as traduções de *Goldilocks laughed* e de *no one laughed* se parecem muito. As semelhanças só desaparecem depois que as duas traduções são reduzidas às suas formas mais simples. + +Em {ref "english-lf"}[FOL como linguagem de representação] demonstramos isso construindo fórmulas da lógica de predicados como traduções das sentenças da língua natural geradas pelo fragmento de {ref "english-fragment"}[Um fragmento do inglês]. Essa tradução é o primeiro passo para interpretar indiretamente as expressões da língua natural. O passo seguinte, em {ref "english-model"}[Uma estrutura de primeira ordem], é atribuir às fórmulas da lógica de predicados um objeto modelo-teórico como denotação. Desse modo, a expressão da língua natural representada recebe uma interpretação modelo-teórica. No caminho, veremos as limitações desse procedimento. + +:::dev "Claude Opus 5" (year := 2026) +Comentário gerado por IA. Duas observações sobre a tradução desta seção. + +A epígrafe é atribuída, na fonte, a *Alice in Wonderland*; o diálogo com o Rei é de *Through the Looking-Glass*. A tradução manteve a atribuição da fonte — corrigi-la é decisão humana. A entrada `Bib.carroll1865` registra o título que a fonte cita. + +Os exemplos em inglês foram mantidos em inglês, como em todo o capítulo: eles são o objeto de estudo, e traduzi-los destruiria o argumento (*No one walked on the road* e *ninguém caminhou na estrada* não têm a mesma sintaxe). As paráfrases *sobre* os exemplos estão em português. ::: # Um fragmento do Inglês +%%% +tag := "english-fragment" +%%% + +Suponha que queiramos escrever regras gramaticais para sentenças do inglês como as seguintes: + +1. The girl laughed. +2. No dwarf admired some princess that shuddered. +3. Every girl that some boy loved cheered. +4. The wizard that helped Snow White defeated the giant. + +O que precisamos é de uma regra para a estrutura sujeito–predicado das sentenças, uma regra para a estrutura interna dos sintagmas nominais, uma regra para os substantivos comuns com ou sem orações relativas, e é mais ou menos só isso. A gramática a seguir dá conta dos exemplos: + +```bnf +S ::= NP VP ; +NP ::= "Snow White" | "Alice" | "Dorothy" | "Goldilocks" | "Little Mook" | "Atreyu" + | "everyone" | "someone" | DET CN | DET RCN ; +DET ::= "a" | "the" | "every" | "some" | "no" ; +CN ::= "girl" | "boy" | "princess" | "dwarf" | "giant" | "wizard" | "sword" | "dagger" ; +ADJ ::= "fake" | "happy" | "evil" ; +RCN ::= CN "that" VP | CN "that" NP TV | ADJ CN ; +VP ::= "laughed" | "cheered" | "shuddered" | TV NP | DV NP NP ; +TV ::= "loved" | "admired" | "helped" | "defeated" | "caught" ; +DV ::= "gave" ; +``` + +Isto é muito básico e grosseiro, claro, mas dá uma idéia de como seria uma gramática para um fragmento do inglês. + +A tradução para Lean é direta: cada não-terminal da gramática vira um tipo indutivo, e cada alternativa de uma regra vira um construtor desse tipo. Um valor do tipo `Sent` não é uma sequência de palavras, é a árvore de análise de uma sentença — a estrutura que a gramática atribui a ela. + +Começamos pelos não-terminais cujas alternativas são todas palavras. Eles não dependem de nenhum outro não-terminal, e por isso podem ser declarados isoladamente. Junto de cada um declaramos a instância de `ToString` que devolve a palavra correspondente. + +```lean +inductive DET where + | a | the | every | some | no +deriving Repr + +instance : ToString DET := + ⟨fun | .a => "a" | .the => "the" | .every => "every" + | .some => "some" | .no => "no"⟩ + +inductive CN where + | girl | boy | princess | dwarf | giant | wizard + | sword | dagger +deriving Repr + +instance : ToString CN := + ⟨fun | .girl => "girl" | .boy => "boy" + | .princess => "princess" | .dwarf => "dwarf" + | .giant => "giant" | .wizard => "wizard" + | .sword => "sword" | .dagger => "dagger"⟩ + +inductive ADJ where + | fake | happy | evil +deriving Repr + +instance : ToString ADJ := + ⟨fun | .fake => "fake" | .happy => "happy" + | .evil => "evil"⟩ + +inductive TV where + | loved | admired | helped | defeated | caught +deriving Repr + +instance : ToString TV := + ⟨fun | .loved => "loved" | .admired => "admired" + | .helped => "helped" | .defeated => "defeated" + | .caught => "caught"⟩ + +inductive DV where + | gave +deriving Repr + +instance : ToString DV := ⟨fun | .gave => "gave"⟩ + +inductive That where + | that +deriving Repr + +instance : ToString That := ⟨fun | .that => "that"⟩ +``` + +O tipo `That` tem um único construtor e não carrega informação alguma. Ele está ali porque a palavra *that* ocupa uma posição na regra de `RCN`, e queremos que a árvore de análise registre essa posição como registra as outras. + +Os quatro não-terminais restantes se referem uns aos outros: `S` usa `NP` e `VP`, `NP` usa `RCN`, `RCN` usa `VP` e `NP`, e `VP` usa `NP`. Nenhum deles pode ser declarado antes dos outros, e por isso os quatro vão para um mesmo bloco `mutual`, como fizemos em {ref "FOL"}[FOL] para funções que se chamam mutuamente. + +```lean +mutual + inductive Sent where + | sent (np : NP) (vp : VP) + deriving Repr + + inductive NP where + | snowWhite | alice | dorothy | goldilocks + | littleMook | atreyu + | everyone | someone + | npDet (det : DET) (cn : CN) + | npDetRel (det : DET) (rcn : RCN) + deriving Repr + + inductive RCN where + | rcnSubj (cn : CN) (compl : That) (vp : VP) + | rcnObj (cn : CN) (compl : That) (np : NP) (tv : TV) + | rcnAdj (adj : ADJ) (cn : CN) + deriving Repr + + inductive VP where + | laughed | cheered | shuddered + | vpTrans (tv : TV) (np : NP) + | vpDitrans (dv : DV) (iobj dobj : NP) + deriving Repr +end +``` + +Os nomes dos construtores dizem qual alternativa da regra cada um implementa. Em `RCN`, `rcnSubj` é a oração relativa em que o substantivo modificado faz o papel de sujeito — *girl that laughed* —, e `rcnObj` aquela em que ele faz o papel de objeto — *girl that some boy loved*. Essa diferença vai reaparecer quando dermos a semântica do fragmento. + +Falta o caminho de volta: dada a árvore, recuperar a sentença de superfície. As funções que fazem isso se chamam umas às outras exatamente como os tipos, e por isso também vão para um bloco `mutual`. + +```lean +mutual + def Sent.toText : Sent → String + | .sent np vp => s!"{np.toText} {vp.toText}" + + def NP.toText : NP → String + | .snowWhite => "Snow White" + | .alice => "Alice" + | .dorothy => "Dorothy" + | .goldilocks => "Goldilocks" + | .littleMook => "Little Mook" + | .atreyu => "Atreyu" + | .everyone => "everyone" + | .someone => "someone" + | .npDet det cn => s!"{det} {cn}" + | .npDetRel det rcn => s!"{det} {rcn.toText}" + + def RCN.toText : RCN → String + | .rcnSubj cn compl vp => s!"{cn} {compl} {vp.toText}" + | .rcnObj cn compl np tv => + s!"{cn} {compl} {np.toText} {tv}" + | .rcnAdj adj cn => s!"{adj} {cn}" + + def VP.toText : VP → String + | .laughed => "laughed" + | .cheered => "cheered" + | .shuddered => "shuddered" + | .vpTrans tv np => s!"{tv} {np.toText}" + | .vpDitrans dv iobj dobj => + s!"{dv} {iobj.toText} {dobj.toText}" +end + +instance : ToString Sent := ⟨Sent.toText⟩ +instance : ToString NP := ⟨NP.toText⟩ +instance : ToString RCN := ⟨RCN.toText⟩ +instance : ToString VP := ⟨VP.toText⟩ +``` + +A árvore de análise de *The dwarf that Snow White helped admired every princess* é a seguinte. + +```display +S +├── NP +│ ├── DET — the +│ └── RCN +│ ├── CN — dwarf +│ ├── That — that +│ ├── NP — Snow White +│ └── TV — helped +└── VP + ├── TV — admired + └── NP + ├── DET — every + └── CN — princess +``` + +O termo Lean correspondente é este. + +```lean +def sent1 : Sent := + .sent (.npDetRel .the + (.rcnObj .dwarf .that .snowWhite .helped)) + (.vpTrans .admired (.npDet .every .princess)) +``` + +É por isso que cada tipo do fragmento deriva `Repr`: avaliar `sent1` no editor exibe o termo, isto é, a árvore, construtor por construtor. `ToString` faz o caminho oposto e devolve a sentença de superfície. + +```lean (name := sent1eval) +#eval toString sent1 +``` + +```leanOutput sent1eval +"the dwarf that Snow White helped admired every princess" +``` + +Ir da sentença de superfície para a árvore é o problema inverso, chamado de *análise sintática*. Não o trataremos aqui: neste capítulo as árvores são construídas à mão, e o que nos interessa é o que fazer com elas depois de construídas. + +## Estender uma gramática + +Um tipo indutivo em Lean é fechado: os construtores listados na declaração são todos os que existem, e não há como acrescentar um depois. É isso que torna as funções sobre `Sent` verificáveis — o compilador sabe que uma função que trata os cinco construtores de `VP` trata todos os casos. Mas é também o que impede que uma gramática seja estendida do jeito mais óbvio, acrescentando uma alternativa a uma regra que já existe. + +Há duas situações, e elas se comportam de maneiras diferentes. + +Acrescentar uma *palavra* a uma categoria — um adjetivo, um verbo transitivo — exige mesmo redeclarar o tipo daquela categoria, porque a palavra é um construtor novo. Por isso o léxico acima já está completo: `ADJ` traz *fake*, *happy* e *evil* desde a declaração. + +Acrescentar uma *regra*, por outro lado, pode ser feito sem tocar no que já existe. Em vez de acrescentar um construtor a `Sent`, declaramos uma categoria nova que contém a antiga: + +```lean +inductive Coord where + | and +deriving Repr + +instance : ToString Coord := ⟨fun | .and => "and"⟩ + +inductive SentAnd where + | base (s : Sent) + | coord (left : SentAnd) (c : Coord) (right : SentAnd) +deriving Repr + +def SentAnd.toText : SentAnd → String + | .base s => toString s + | .coord l c r => s!"{l.toText} {c} {r.toText}" + +instance : ToString SentAnd := ⟨SentAnd.toText⟩ +``` + +O construtor `base` diz que toda sentença do fragmento original é uma sentença do fragmento estendido, e `coord` acrescenta a regra nova, `S ::= S COORD S`. Nada de `Sent` foi redeclarado, e as funções já escritas sobre `Sent` continuam valendo — `SentAnd.toText` chama `toString` sobre o `Sent` de dentro. + +```lean (name := sentAndEval) +def sent2 : SentAnd := + .coord (.base (.sent .alice .laughed)) .and + (.base (.sent .dorothy .cheered)) + +#eval toString sent2 +``` + +```leanOutput sentAndEval +"Alice laughed and Dorothy cheered" +``` + +Os dois exercícios a seguir estendem o fragmento por esse caminho. + +::::exercise (rating := 2) (name := "preposition-phrase") + +Estenda o fragmento com sintagmas preposicionais, de modo que a sentença *A dwarf defeated a giant with a sword* seja gerada de duas maneiras estruturalmente diferentes, enquanto há apenas uma maneira de gerar *A dwarf defeated Little Mook with a sword*. -:::dev "Alexandre (arademaker)" -aqui entra seção CSwFP/4.2. os exercícios pedem expansoes de uma gramatica inicial, vamos tentar fazer evitando ao máximo redefinições de tipos indutivos. +:::solution +Primeiro acrescentamos duas regras para construir sintagmas preposicionais a partir de uma preposição e de um sintagma nominal. Em seguida estendemos a regra dos sintagmas nominais, para gerar sintagmas como *a giant with a sword*. Note que não acrescentamos simplesmente uma produção recursiva `NP ::= NP PP`: além de permitir um número arbitrário de sintagmas preposicionais modificando um mesmo sintagma nominal, ela geraria *Little Mook with a sword*, que é o que queremos excluir. Por fim, estendemos também a regra dos sintagmas verbais. + +```bnf +P ::= "with" ; +PP ::= P NP ; +NPP ::= DET CN PP ; +VPP ::= VP | TV NPP | TV NP PP ; +S' ::= NP VPP ; +``` + +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 +inductive Prep where + | «with» +deriving Repr + +instance : ToString Prep := ⟨fun | .with => "with"⟩ + +inductive PP where + | pp (p : Prep) (np : NP) +deriving Repr + +instance : ToString PP := + ⟨fun | .pp p np => s!"{p} {np}"⟩ + +inductive NPP where + | withPP (det : DET) (cn : CN) (pp : PP) +deriving Repr + +inductive VPP where + | base (vp : VP) + | objPP (tv : TV) (np : NPP) + | vpPP (tv : TV) (np : NP) (pp : PP) +deriving Repr + +inductive SentPP where + | sent (np : NP) (vp : VPP) +deriving Repr +``` + +Repare que `NPP` tem um único construtor, e que tanto `objPP` quanto `vpPP` exigem um sintagma preposicional. É isso que garante que a gramática estendida não gere duas vezes as sentenças que a original já gerava: uma sentença sem sintagma preposicional só pode passar por `base`. + +Complete as funções que devolvem a sentença de superfície. + +```lean +def NPP.toText : NPP → String := + solution!( + fun | .withPP det cn pp => s!"{det} {cn} {pp}") + +instance : ToString NPP := ⟨NPP.toText⟩ + +def VPP.toText : VPP → String := + solution!( + fun + | .base vp => toString vp + | .objPP tv np => s!"{tv} {np}" + | .vpPP tv np pp => s!"{tv} {np} {pp}") + +instance : ToString VPP := ⟨VPP.toText⟩ + +def SentPP.toText : SentPP → String := + solution!( + fun | .sent np vp => s!"{np} {vp}") + +instance : ToString SentPP := ⟨SentPP.toText⟩ +``` + +Agora construa as três árvores: as duas leituras de *A dwarf defeated a giant with a sword* e a única de *A dwarf defeated Little Mook with a sword*. + +```lean +def withSword : PP := .pp .with (.npDet .a .sword) + +-- O sintagma preposicional modifica o objeto. +def giantSword1 : SentPP := + solution!( + .sent (.npDet .a .dwarf) + (.objPP .defeated (.withPP .a .giant withSword))) + +-- O sintagma preposicional modifica o sintagma verbal. +def giantSword2 : SentPP := + solution!( + .sent (.npDet .a .dwarf) + (.vpPP .defeated (.npDet .a .giant) withSword)) + +-- Única leitura possível. +def mookSword : SentPP := + solution!( + .sent (.npDet .a .dwarf) + (.vpPP .defeated .littleMook withSword)) + +theorem giantSword_ambiguous : + toString giantSword1 = toString giantSword2 := + solution!(by rfl) + +theorem giantSword_surface : + toString giantSword1 = + "a dwarf defeated a giant with a sword" := + solution!(by rfl) + +theorem mookSword_surface : + toString mookSword = + "a dwarf defeated Little Mook with a sword" := + solution!(by rfl) +``` + +:::gradeTheorem "1" giantSword_ambiguous giantSword_surface mookSword_surface +::: + +As duas primeiras árvores são diferentes e imprimem a mesma sentença: é a ambiguidade pedida. +:::: + +::::exercise (rating := 2) (name := "complex-relative-clauses") + +Estenda o fragmento com orações relativas complexas, em que a oração relativa coordena dois sintagmas verbais ou dois pares sintagma nominal–verbo transitivo. O fragmento deve gerar, entre outras, a sentença *The dwarf that Snow White helped and Goldilocks admired cheered*. Que problemas você encontra? + +:::solution +As regras acrescentam duas alternativas para as orações relativas, cada uma coordenando duas ocorrências da mesma forma: + +```bnf +RCNC ::= CN "that" VP COORD VP | CN "that" NP TV COORD NP TV ; +NPC ::= NP | DET RCNC ; +S'' ::= NPC VP ; +``` + +O primeiro problema é que as duas regras não podem ser substituídas por uma só que coordenasse um sintagma verbal com um par sintagma nominal–verbo transitivo. Numa oração relativa há uma posição vazia, a *lacuna*, onde entraria o substantivo que ela modifica: em `CN "that" VP` a lacuna é o sujeito do sintagma verbal, e em `CN "that" NP TV` é o objeto do verbo transitivo. Cada uma das duas regras coordena duas lacunas do mesmo tipo. Misturá-las produziria *the dwarf that Goldilocks helped and admired Snow White*, em que a lacuna é o objeto no primeiro ramo e o sujeito no segundo, e que é agramatical. Coordenar sentenças inteiras, como em `SentAnd`, geraria exatamente essa mistura. + +O segundo problema é que nenhuma das duas regras é recursiva: cada uma coordena exatamente dois ramos. Para três ramos seria preciso mais uma regra, para quatro outra, e assim por diante. O fragmento não captura a generalização "coordenação de um número qualquer de sintagmas verbais paralelos". + +O terceiro é que os ramos coordenados usam os sintagmas nominais e verbais do fragmento original, e não os estendidos. Uma oração relativa coordenada não pode, portanto, conter outra oração relativa coordenada. +::: + +```lean +inductive RCNC where + | vpAnd (cn : CN) (compl : That) + (left : VP) (c : Coord) (right : VP) + | objAnd (cn : CN) (compl : That) + (np1 : NP) (tv1 : TV) (c : Coord) + (np2 : NP) (tv2 : TV) +deriving Repr + +inductive NPC where + | base (np : NP) + | npDetRel (det : DET) (rcn : RCNC) +deriving Repr + +inductive SentC where + | sent (np : NPC) (vp : VP) +deriving Repr +``` + +Complete as funções de superfície e construa a sentença do enunciado. + +```lean +def RCNC.toText : RCNC → String := + solution!( + fun + | .vpAnd cn compl l c r => + s!"{cn} {compl} {l} {c} {r}" + | .objAnd cn compl np1 tv1 c np2 tv2 => + s!"{cn} {compl} {np1} {tv1} {c} {np2} {tv2}") + +instance : ToString RCNC := ⟨RCNC.toText⟩ + +def NPC.toText : NPC → String := + solution!( + fun + | .base np => toString np + | .npDetRel det rcn => s!"{det} {rcn}") + +instance : ToString NPC := ⟨NPC.toText⟩ + +def SentC.toText : SentC → String := + solution!( + fun | .sent np vp => s!"{np} {vp}") + +instance : ToString SentC := ⟨SentC.toText⟩ + +def dwarfHelpedAdmired : SentC := + solution!( + .sent (.npDetRel .the + (.objAnd .dwarf .that .snowWhite .helped + .and .goldilocks .admired)) + .cheered) + +theorem dwarfHelpedAdmired_surface : + toString dwarfHelpedAdmired = + "the dwarf that Snow White helped and " ++ + "Goldilocks admired cheered" := + solution!(by rfl) +``` + +:::gradeTheorem "1" dwarfHelpedAdmired_surface ::: +:::: # FOL como Linguagem de representação +%%% +tag := "english-lf" +%%% + +A lógica de predicados nos dá representações para dois tipos: o tipo das entidades é representado pelos termos, e o tipo dos valores de verdade pelas fórmulas. Chamaremos de `LF` — *forma lógica* — o tipo das fórmulas de primeira ordem cujos termos são termos estruturados, o {name}`FOL.Formula` de {ref "FOL"}[FOL] com {name}`FOL.Term` no lugar do parâmetro. + +```lean +open FOL + +abbrev LF := Formula Term +``` + +Supondo que estejamos tratando de um fragmento que gera sentenças declarativas cujos significados podem ser representados na lógica de predicados, é razoável dar o tipo `LF` às representações das sentenças. -:::dev "Alexandre (arademaker)" -aqui entra seção CSwFP/6.2. Ela usa o fragmento definido na seção anterior que veio da CSwFP/4.2 +Para traduzir o fragmento de {ref "english-fragment"}[Um fragmento do inglês] para a lógica de predicados, tudo o que temos a fazer é achar traduções apropriadas para todas as categorias da gramática. Mas a primeira regra, `S ::= NP VP`, já nos apresenta uma dificuldade. Ao procurar traduções de `NP` e traduções de `VP`, devemos representar o `NP` como uma função que toma a representação do `VP` como argumento, ou o contrário? + +De todo modo, as representações de `VP` terão um tipo funcional, pois sintagmas verbais denotam propriedades. Um tipo razoável para a função que representa um `VP` é `Term → LF`: alimentada com um termo, ela devolve uma forma lógica. Os nomes próprios podem então receber o tipo dos termos. Tome o exemplo *Goldilocks laughed*. O verbo *laughed* é representado pela função que leva o termo `x` à fórmula `laugh[x]`. Obtemos assim uma forma lógica apropriada para a sentença, se `x` for um termo para *Goldilocks*. + +A dificuldade apontada em {ref "english-form"}[Formas linguísticas e traduções para lógica] é que sintagmas como *no boy* e *every girl* não se encaixam nesse padrão. Lá também dissemos que isso se resolve supondo que tais sintagmas se traduzem como funções que tomam representações de `VP` como argumento. Uma tradução apropriada para *everyone* seria uma função de tipo `(Term → LF) → LF`: alimentada com a representação de um `VP`, ela devolve uma forma lógica. O resultado da discussão é que, na representação de uma estrutura `S ::= NP VP`, a representação do `NP` deve ser a função e a do `VP` o argumento. Os tipos das quatro funções de tradução são, portanto, estes: + +```display +lfSent : Sent → LF +lfNP : NP → (Term → LF) → LF +lfVP : VP → Term → LF +lfRCN : RCN → Term → LF +``` + +Como `NP`, `VP` e `RCN` se referem uns aos outros, as quatro funções se chamam umas às outras, e vão para um bloco `mutual`. Antes dele, porém, vêm as funções de tradução que não dependem de nenhuma outra. + +As categorias lexicais são as mais simples. Um substantivo comum tem o mesmo tipo que um sintagma verbal, e um adjetivo também. + +```lean +def lfCN : CN → Term → LF + | .girl, t => .atom "girl" [t] + | .boy, t => .atom "boy" [t] + | .princess, t => .atom "princess" [t] + | .dwarf, t => .atom "dwarf" [t] + | .giant, t => .atom "giant" [t] + | .wizard, t => .atom "wizard" [t] + | .sword, t => .atom "sword" [t] + | .dagger, t => .atom "dagger" [t] + +def lfADJ : ADJ → Term → LF + | .fake, t => .atom "fake" [t] + | .happy, t => .atom "happy" [t] + | .evil, t => .atom "evil" [t] +``` + +Um verbo transitivo relaciona duas entidades, e um verbo bitransitivo, três. O primeiro argumento é sempre o do sujeito; no verbo bitransitivo, o segundo é o do objeto indireto e o terceiro o do objeto direto. + +```lean +def lfTV : TV → Term → Term → LF + | .loved, t1, t2 => .atom "love" [t1, t2] + | .admired, t1, t2 => .atom "admire" [t1, t2] + | .helped, t1, t2 => .atom "help" [t1, t2] + | .defeated, t1, t2 => .atom "defeat" [t1, t2] + | .caught, t1, t2 => .atom "catch" [t1, t2] + +def lfDV : DV → Term → Term → Term → LF + | .gave, t1, t2, t3 => .atom "give" [t1, t2, t3] +``` + +## Variáveis novas + +A tradução de um determinante toma dois argumentos de tipo `Term → LF` — formas lógicas com um buraco de termo dentro — e produz uma forma lógica. No caso dos quantificadores, o primeiro argumento é a *restrição* e o segundo o *escopo*. + +```display +lfDET : DET → (Term → LF) → (Term → LF) → LF +``` + +A tradução dos determinantes precisa ser feita com algum cuidado, porque envolve construir uma forma lógica em que uma variável fica ligada. Para garantir a ligação correta, temos de nos assegurar de que a variável recém-introduzida não seja capturada por um quantificador já presente na forma lógica. Mas, se refletirmos sobre como as variáveis são introduzidas, veremos que elas sempre aparecem junto de quem as liga, e que nenhuma ligação é vazia. Basta então colher os índices das ocorrências ligadas. + +```lean +def boundIndices : LF → List Nat + | .atom _ _ => [] + | .eq _ _ => [] + | .top => [] + | .bot => [] + | .neg f => boundIndices f + | .impl f1 f2 => boundIndices f1 ++ boundIndices f2 + | .equi f1 f2 => boundIndices f1 ++ boundIndices f2 + | .conj f1 f2 => boundIndices f1 ++ boundIndices f2 + | .disj f1 f2 => boundIndices f1 ++ boundIndices f2 + | .forall_ v f => v.index ++ boundIndices f + | .exists_ v f => v.index ++ boundIndices f +``` + +Para calcular um índice novo, basta escolher um índice fora dessa lista. Todas as variáveis são introduzidas pelo mesmo mecanismo: se começarmos com variáveis da forma `⟨"x", [0]⟩` e só introduzirmos variáveis novas da mesma forma, podemos supor que toda variável que ocorre na forma lógica tem esse feitio. O `0` inicial em `foldr max 0` garante que a lista sobre a qual tomamos o máximo não seja vazia. + +Os argumentos de `lfDET` não são formas lógicas, e sim funções à espera de um termo. Para ver que variáveis elas carregam, aplicamos cada uma a um termo qualquer que não contenha variável alguma. + +```lean +def dummy : Term := .struct "" [] + +def freshIndex (ps : List (Term → LF)) : Nat := + let used := + (ps.map (fun p => boundIndices (p dummy))).flatten + used.foldr max 0 + 1 + +def freshVar (ps : List (Term → LF)) : Variable := + ⟨"x", [freshIndex ps]⟩ +``` + +Podemos agora dar a tradução dos determinantes. Os indefinidos *a* e *some* recebem a mesma tradução. + +```lean +def lfDET : DET → (Term → LF) → (Term → LF) → LF + | .a, p, q => + let v := freshVar [p, q] + .exists_ v (.conj (p (.var v)) (q (.var v))) + | .some, p, q => + let v := freshVar [p, q] + .exists_ v (.conj (p (.var v)) (q (.var v))) + | .every, p, q => + let v := freshVar [p, q] + .forall_ v (.impl (p (.var v)) (q (.var v))) + | .no, p, q => + let v := freshVar [p, q] + .neg (.exists_ v (.conj (p (.var v)) (q (.var v)))) + | .the, p, q => + let i := freshIndex [p, q] + let v1 : Variable := ⟨"x", [i]⟩ + let v2 : Variable := ⟨"x", [i + 1]⟩ + .exists_ v1 + (.conj + (.forall_ v2 + (.equi (p (.var v2)) (.eq (.var v1) (.var v2)))) + (q (.var v1))) +``` + +Para o determinante definido usamos a teoria das descrições definidas proposta por Bertrand Russell {citep Bib.russell1905}[]. Russell propôs traduzir *The king of France is bald* como a conjunção de *existe exatamente uma pessoa que é rei da França* e *essa pessoa é careca*, o que se exprime assim na lógica de predicados: + +```display +∃x (∀y (King[y] <=> x = y) & Bald[x]) +``` + +Nem todo determinante do inglês admite uma tradução para a lógica de predicados. *Most* é o exemplo clássico: não há como dizer, com os quantificadores `∀` e `∃`, que a maioria dos anões riu. Determinantes como *at least n* e *at most n* têm tradução, mas as formas lógicas ficam muito pesadas. É por isso que `DET` traz apenas os cinco determinantes acima. + +## O bloco mutuamente recursivo + +Falta traduzir as quatro categorias que se referem umas às outras. Os nomes próprios são traduzidos como símbolos funcionais de aridade zero, isto é, como constantes: *Snow White* é o termo `SnowWhite`. + +Os sintagmas *everyone* e *someone* não têm um termo que lhes corresponda. Eles são traduzidos como quantificadores restritos à propriedade de ser uma pessoa, e é justamente essa a forma de que falamos na primeira seção: uma função que toma a representação do sintagma verbal como argumento. + +Usamos a conjunção para juntar a forma lógica de um substantivo comum e a de uma oração relativa numa forma lógica para o substantivo comum complexo. + +```lean +mutual + def lfSent : Sent → LF + | .sent np vp => lfNP np (lfVP vp) + + def lfNP : NP → (Term → LF) → LF + | .snowWhite, p => p (.struct "SnowWhite" []) + | .alice, p => p (.struct "Alice" []) + | .dorothy, p => p (.struct "Dorothy" []) + | .goldilocks, p => p (.struct "Goldilocks" []) + | .littleMook, p => p (.struct "LittleMook" []) + | .atreyu, p => p (.struct "Atreyu" []) + | .everyone, p => + let v := freshVar [p] + .forall_ v + (.impl (.atom "person" [.var v]) (p (.var v))) + | .someone, p => + let v := freshVar [p] + .exists_ v + (.conj (.atom "person" [.var v]) (p (.var v))) + | .npDet det cn, p => lfDET det (lfCN cn) p + | .npDetRel det rcn, p => lfDET det (lfRCN rcn) p + + def lfVP : VP → Term → LF + | .laughed, t => .atom "laugh" [t] + | .cheered, t => .atom "cheer" [t] + | .shuddered, t => .atom "shudder" [t] + | .vpTrans tv np, subj => + lfNP np (fun obj => lfTV tv subj obj) + | .vpDitrans dv np1 np2, subj => + lfNP np1 (fun iobj => + lfNP np2 (fun dobj => lfDV dv subj iobj dobj)) + + def lfRCN : RCN → Term → LF + | .rcnSubj cn _ vp, t => .conj (lfCN cn t) (lfVP vp t) + | .rcnObj cn _ np tv, t => + .conj (lfCN cn t) + (lfNP np (fun subj => lfTV tv subj t)) + | .rcnAdj adj cn, t => .conj (lfADJ adj t) (lfCN cn t) +end +``` + +A tradução do adjetivo em `rcnAdj` é a conjunção: um *happy wizard* é alguém que é feliz e é mago. Isso está certo para *happy* e para *evil*, e está errado para *fake*: um *fake wizard* justamente não é um mago. Adjetivos desse tipo pedem uma semântica que a lógica de predicados não alcança, e o fragmento os traduz assim porque em Lean uma função tem de estar definida em todos os casos — a tradução existe, mas não é uma boa tradução. + +Vejamos três exemplos. + +```lean +def lf1 : LF := + lfSent (.sent (.npDet .some .dwarf) + (.vpTrans .defeated (.npDet .some .giant))) + +def lf2 : LF := + lfSent (.sent (.npDetRel .the + (.rcnObj .wizard .that .dorothy .admired)) + .laughed) + +def lf3 : LF := + lfSent (.sent (.npDetRel .the + (.rcnSubj .princess .that + (.vpTrans .helped .alice))) + .shuddered) +``` + +```lean (name := lf1eval) +#eval lf1 +``` + +```leanOutput lf1eval +∃x2 (dwarf[x2] & ∃x1 (giant[x1] & defeat[x2, x1])) +``` + +```lean (name := lf2eval) +#eval lf2 +``` + +```leanOutput lf2eval +∃x1 (∀x2 ((wizard[x2] & admire[Dorothy, x2]) <=> x1 = x2) & laugh[x1]) +``` + +```lean (name := lf3eval) +#eval lf3 +``` + +```leanOutput lf3eval +∃x1 (∀x2 ((princess[x2] & help[x2, Alice]) <=> x1 = x2) & shudder[x1]) +``` + +::::exercise (rating := 2) (name := "fragment-translations") +Construa as árvores de análise das quatro sentenças a seguir, todas geradas pelo fragmento. + +1. Every girl that laughed helped a boy. +2. No giant that shuddered defeated every dwarf. +3. Every princess loved every dwarf that defeated a giant. +4. Every boy admired a girl that no wizard helped. + +Os teoremas conferem que cada árvore devolve a sentença certa. Depois disso, `#eval lfSent tr1` exibe a forma lógica da primeira. + +```lean +def tr1 : Sent := + solution!( + .sent (.npDetRel .every (.rcnSubj .girl .that .laughed)) + (.vpTrans .helped (.npDet .a .boy))) + +def tr2 : Sent := + solution!( + .sent (.npDetRel .no (.rcnSubj .giant .that .shuddered)) + (.vpTrans .defeated (.npDet .every .dwarf))) + +def tr3 : Sent := + solution!( + .sent (.npDet .every .princess) + (.vpTrans .loved + (.npDetRel .every + (.rcnSubj .dwarf .that + (.vpTrans .defeated (.npDet .a .giant)))))) + +def tr4 : Sent := + solution!( + .sent (.npDet .every .boy) + (.vpTrans .admired + (.npDetRel .a + (.rcnObj .girl .that (.npDet .no .wizard) + .helped)))) + +theorem tr1_surface : + toString tr1 = + "every girl that laughed helped a boy" := + solution!(by rfl) + +theorem tr2_surface : + toString tr2 = + "no giant that shuddered defeated every dwarf" := + solution!(by rfl) + +theorem tr3_surface : + toString tr3 = + "every princess loved every dwarf " ++ + "that defeated a giant" := + solution!(by rfl) + +theorem tr4_surface : + toString tr4 = + "every boy admired a girl that no wizard helped" := + solution!(by rfl) +``` + +:::gradeTheorem "1" tr1_surface tr2_surface +::: + +:::gradeTheorem "1" tr3_surface tr4_surface ::: +:::: + +Temos agora representações de sentenças declarativas da língua natural como fórmulas da lógica de predicados. Falta dizer quando essas fórmulas são verdadeiras. # Uma Estrutura de Primeira Ordem +%%% +tag := "english-model" +%%% + +Tudo o que precisamos para especificar uma estrutura de primeira ordem é um domínio de entidades e interpretações apropriadas para os nomes próprios e para os predicados. Começamos construindo um pequeno domínio de exemplo, formado pelos indivíduos `A`, …, `Z`, mais uma entidade especial. + +```lean +inductive Entity where + | A | B | C | D | E | F | G | H | I + | J | K | L | M | N | O | P | Q | R + | S | T | U | V | W | X | Y | Z + | Unspec +deriving Repr, DecidableEq +``` + +A entidade especial `Unspec` terá um papel importante no tratamento das relações subespecificadas: ela nos permitirá definir relações com algumas posições de argumento deixadas em aberto. + +Para avaliar uma fórmula quantificada é preciso percorrer o domínio, e percorrer exige uma coleção. Como em {ref "FOL"}[FOL], o tipo indutivo declara quais são os objetos e a lista os exibe na ordem em que serão percorridos. + +```lean +def entities : List Entity := + [.A, .B, .C, .D, .E, .F, .G, .H, .I, + .J, .K, .L, .M, .N, .O, .P, .Q, .R, + .S, .T, .U, .V, .W, .X, .Y, .Z, + .Unspec] + +theorem mem_entities (e : Entity) : e ∈ entities := by + cases e <;> decide +``` + +O teorema {name}`mem_entities` diz que na lista estão todos os elementos do tipo, e voltaremos a ele no fim da seção. + +Os nomes próprios são interpretados simplesmente como entidades. + +```lean +def snowWhite : Entity := .S +def alice : Entity := .A +def dorothy : Entity := .D +def goldilocks : Entity := .G +def littleMook : Entity := .M +def atreyu : Entity := .Y +``` + +Substantivos comuns como *girl* e *dwarf*, e verbos intransitivos como *laugh* e *shudder*, são interpretados como propriedades de entidades. Verbos transitivos como *love* são interpretados como relações entre entidades. + +Para propriedades e relações sobre `Entity`, poderíamos usar um tipo geral `List Entity → Bool`. Isso nos permitiria falar de relações de qualquer aridade de maneira uniforme, mas não seria conveniente para a composição do significado: na sintaxe, um verbo transitivo combina primeiro com o objeto direto e depois com o sujeito, e um verbo bitransitivo combina com um objeto indireto e um objeto direto, e então com o sujeito. Queremos, portanto, que os verbos denotem funções que tomam seus argumentos um a um. Definimos assim os tipos dos predicados de um, dois e três lugares. + +```lean +abbrev OnePlacePred := Entity → Bool +abbrev TwoPlacePred := Entity → Entity → Bool +abbrev ThreePlacePred := Entity → Entity → Entity → Bool +``` + +Como {ref "Sets"}[Conjuntos e Relações] mostrou, um predicado de um lugar é a função característica de um conjunto, e é natural pensá-lo como a lista das entidades para as quais ele vale. Definimos então funções de conversão que transformam listas em predicados. + +```lean +def list1 (xs : List Entity) : OnePlacePred := + fun x => xs.contains x + +def list2 (ps : List (Entity × Entity)) : TwoPlacePred := + fun x y => ps.contains (x, y) + +def list3 (ts : List (Entity × Entity × Entity)) : + ThreePlacePred := + fun x y z => ts.contains (x, y, z) +``` + +Com elas, o léxico se escreve como listas. + +```lean +def girl : OnePlacePred := list1 [.S, .A, .D, .G] +def boy : OnePlacePred := list1 [.M, .Y] +def princess : OnePlacePred := list1 [.E] +def dwarf : OnePlacePred := list1 [.B, .R] +def giant : OnePlacePred := list1 [.T] +def wizard : OnePlacePred := list1 [.W, .V] +def sword : OnePlacePred := list1 [.F] +def dagger : OnePlacePred := list1 [.X] +``` + +Com esses predicados podemos definir outros, como o de ser uma pessoa ou uma coisa: uma pessoa é um menino, uma menina, uma princesa, um anão, um gigante ou um mago, e uma coisa é tudo o que não é pessoa nem o objeto especial `Unspec`. É conveniente ter também homens e mulheres: supomos que as mulheres são as princesas e que os homens são os anões, os gigantes e os magos. -:::dev "Alexandre (arademaker)" -aqui entra seção CSwFP/6.3. Deve definir a estrutura para avaliação das fórmulas da seção anterior. +```lean +def child : OnePlacePred := fun x => girl x || boy x +def person : OnePlacePred := fun x => + child x || princess x || dwarf x || giant x || wizard x +def man : OnePlacePred := fun x => + dwarf x || giant x || wizard x +def woman : OnePlacePred := princess +def male : OnePlacePred := fun x => man x || boy x +def female : OnePlacePred := fun x => woman x || girl x +def thing : OnePlacePred := fun x => + !(person x || x == .Unspec) +``` + +Como os verbos intransitivos também denotam propriedades, seus significados são representados igualmente por predicados de um lugar. + +```lean +def laugh : OnePlacePred := list1 [.A, .G, .E] +def cheer : OnePlacePred := list1 [.M, .D] +def shudder : OnePlacePred := list1 [.S] +``` + +Os verbos transitivos denotam relações entre entidades, e é conveniente pensar um predicado de dois lugares como a lista dos pares para os quais ele vale. Dois deles não são dados por uma lista fixa: *admire* vale de toda pessoa para Goldilocks, e *defeat* vale de todo anão para todo gigante, além dos dois pares em que Alice derrota um mago. + +```lean +def love : TwoPlacePred := + list2 [(.Y, .E), (.B, .S), (.R, .S)] + +def help : TwoPlacePred := + list2 [(.W, .W), (.V, .V), (.S, .B), (.D, .M)] + +def admire : TwoPlacePred := fun x y => + person x && y == .G + +def defeat : TwoPlacePred := fun x y => + (dwarf x && giant y) || list2 [(.A, .W), (.A, .V)] x y +``` + +Os significados dos verbos bitransitivos são representados por predicados de três lugares, da mesma maneira. + +```lean +def give : ThreePlacePred := + list3 [(.T, .S, .X), (.A, .E, .S)] +``` + +:::details "Argumentos deixados em aberto" +A entidade `Unspec` serve para definir relações subespecificadas. Podemos, por exemplo, acrescentar um verbo *kill* e interpretá-lo como uma relação de três lugares em que o primeiro argumento dá o agente, o segundo a vítima e o terceiro o instrumento. Nos casos em que não há instrumento ou agente, deixamos o argumento em aberto. + +```lean +def kill : ThreePlacePred := + list3 [(.Y, .T, .F), (.Unspec, .D, .X), + (.Unspec, .M, .Unspec)] +``` + +O que essa entrada diz é que Atreyu matou o gigante com a espada, que Dorothy foi esfaqueada — deixando em aberto quem a esfaqueou — e que Little Mook simplesmente morreu. + +Usar `Unspec` para deixar argumentos implícitos pode ser explorado de maneira mais geral. Um exemplo são as passivas. A passivização é um processo de redução de argumentos: o agente da ação é suprimido. Sem entrar nas propriedades sutis das construções passivas, podemos especificar uma função de passivização semântica assim: + +```lean +def passivize (r : TwoPlacePred) : OnePlacePred := + fun x => r .Unspec x +``` + +A redução de argumentos não aparece só nas passivas. Outro caso é uma análise dos pronomes reflexivos segundo a qual *himself* e *herself* diferem semanticamente de *him* e *her* por não serem interpretados como variáveis individuais: eles denotam funções que reduzem argumentos. Considere a sentença *Snow White admired herself*. O reflexivo *herself* é interpretado como uma função que toma o predicado de dois lugares *admired* e o transforma num predicado de um lugar, que toma o sujeito como argumento e exprime que essa entidade admira a si mesma. + +```lean +def self {α β : Type} (p : α → α → β) : α → β := + fun x => p x x +``` + +Essa análise tem duas consequências desejáveis. A primeira é que a localidade dos reflexivos cai por terra sozinha: como `self` se aplica a um predicado e unifica argumentos desse predicado, não há como um argumento ser unificado com outro de fora da mesma oração. Em *Snow White thinks that Alice admired herself*, portanto, *herself* só pode se referir a Alice, e não a Snow White. A segunda é que reflexivos em posição de sujeito ficam excluídos: em *Herself admired Snow White*, a interpretação composicional aplica primeiro *admired* a Snow White, o que dá um predicado de um lugar, e aplicar `self` a ele falha, porque `self` espera um predicado de dois lugares. Não sobram duas posições de argumento a unificar. + +::: + +::::exercise (rating := 2) (name := "reflexive-ditransitive") +Nos verbos bitransitivos, um reflexivo pode ser tanto o objeto direto quanto o objeto indireto: + +1. Alice introduced herself to the rabbit. +2. Little Mook gave the figs to himself. + +Defina as funções `self3DO` e `self3IO`, de tipo `ThreePlacePred → TwoPlacePred`, que unificam o sujeito com o objeto direto e com o objeto indireto, respectivamente. Lembre que, num predicado de três lugares, o primeiro argumento é o do sujeito, o segundo o do objeto indireto e o terceiro o do objeto direto. + +Para testar as duas funções, `introduced x y z` diz que `x` apresentou `z` a `y`: Alice apresentou a si mesma ao anão `B`, e Snow White apresentou a princesa ao mesmo anão. + +```lean +def introduced : ThreePlacePred := + list3 [(.A, .B, .A), (.S, .B, .E)] + +def self3DO (p : ThreePlacePred) : TwoPlacePred := + solution!(fun x y => p x y x) + +def self3IO (p : ThreePlacePred) : TwoPlacePred := + solution!(fun x y => p x x y) + +theorem self3DO_introduced : + self3DO introduced .A .B = true := + solution!(by decide) + +theorem self3IO_introduced : + self3IO introduced .A .B = false := + solution!(by decide) +``` + +:::gradeTheorem "1" self3DO_introduced self3IO_introduced +::: +:::: + +## Interpretando os símbolos + +Já temos em {ref "fol-semantics"}[a semântica de FOL] tudo o que é preciso para avaliar fórmulas: {name}`FOL.Interp` interpreta os símbolos de predicado, {name}`FOL.FInterp` os símbolos funcionais, {name}`FOL.Assign` as variáveis, e {name}`FOL.Formula.eval` percorre a fórmula. Falta apenas ligar os nomes que a tradução produz às relações que acabamos de definir. + +```lean +def intFairy : Interp Entity + | "girl", [x] => girl x + | "boy", [x] => boy x + | "princess", [x] => princess x + | "dwarf", [x] => dwarf x + | "giant", [x] => giant x + | "wizard", [x] => wizard x + | "sword", [x] => sword x + | "dagger", [x] => dagger x + | "person", [x] => person x + | "laugh", [x] => laugh x + | "cheer", [x] => cheer x + | "shudder", [x] => shudder x + | "love", [x, y] => love x y + | "admire", [x, y] => admire x y + | "help", [x, y] => help x y + | "defeat", [x, y] => defeat x y + | "give", [x, y, z] => give x y z + | _, _ => false +``` + +Os nomes próprios foram traduzidos como constantes, isto é, como símbolos funcionais de aridade zero. É {name}`FOL.FInterp` que diz qual entidade cada um nomeia, e `Unspec` é o valor natural para os símbolos que a estrutura não nomeia. + +```lean +def fintFairy : FInterp Entity + | "SnowWhite", [] => snowWhite + | "Alice", [] => alice + | "Dorothy", [] => dorothy + | "Goldilocks", [] => goldilocks + | "LittleMook", [] => littleMook + | "Atreyu", [] => atreyu + | _, _ => .Unspec +``` + +Como vimos em {ref "fol-semantics"}[FOL], um símbolo que a interpretação não menciona é avaliado como {lean}`false`. No fragmento isso acontece com *catch* e com os adjetivos: a estrutura simplesmente não diz nada sobre eles, e toda sentença que os use será falsa. + +Falta a atribuição de valores às variáveis. As fórmulas que a tradução produz são sentenças, sem variáveis livres, e para elas a atribuição é irrelevante — mas {name}`FOL.Formula.eval` ainda exige alguma. + +```lean +def ass0 : Assign Entity := fun _ => .A +``` + +Agora podemos avaliar. A fórmula que diz que a relação de amor é reflexiva é falsa nesta estrutura, como seria de esperar. + +```lean (name := loveReflEval) +def loveReflexive : LF := + .forall_ x (.atom "love" [tx, tx]) + +#eval loveReflexive.eval entities intFairy ass0 + (liftAssign fintFairy) +``` + +```leanOutput loveReflEval +false +``` + +::::exercise (rating := 2) (name := "check-sentence") +Junte as duas metades. Defina a função que decide se uma sentença do fragmento é verdadeira nesta estrutura: ela deve traduzir a sentença para uma forma lógica e avaliar essa forma lógica no domínio {name}`entities`, com as interpretações {name}`intFairy` e {name}`fintFairy` e com a atribuição {name}`ass0`. + +```lean +def checkSentence (s : Sent) : Bool := + solution!( + (lfSent s).eval entities intFairy ass0 + (liftAssign fintFairy)) + +theorem goldilocksLaughed : + checkSentence (.sent .goldilocks .laughed) = true := + solution!(by native_decide) + +theorem dorothyLaughed : + checkSentence (.sent .dorothy .laughed) = false := + solution!(by native_decide) + +theorem someDwarfDefeatedSomeGiant : + checkSentence + (.sent (.npDet .some .dwarf) + (.vpTrans .defeated (.npDet .some .giant))) + = true := + solution!(by native_decide) + +theorem everyoneCheered : + checkSentence (.sent .everyone .cheered) = false := + solution!(by native_decide) +``` + +:::gradeTheorem "1" goldilocksLaughed dorothyLaughed +::: + +:::gradeTheorem "1" someDwarfDefeatedSomeGiant everyoneCheered +::: +:::: + +Temos assim um procedimento de interpretação indireta para o fragmento, em dois passos: primeiro construímos uma forma lógica a partir da expressão da língua natural, depois avaliamos essa forma lógica em relação a uma estrutura. + +Falta cobrar a promessa feita a {name}`mem_entities`. {name}`FOL.Formula.eval` decide um quantificador percorrendo uma lista, e só concorda com o `∀` de Lean se essa lista contiver todos os elementos do domínio — é o que a hipótese `hdom` de {name}`FOL.Formula.eval_iff_denote` exige, e é exatamente o que {name}`mem_entities` fornece. + +```lean +theorem eval_iff_denote_fairy (I : Interp Entity) + (g : Assign Entity) (f : Formula Term) : + f.eval entities I g (liftAssign fintFairy) = true ↔ + f.denote (fun n as => I n as = true) g + (liftAssign fintFairy) := + Formula.eval_iff_denote entities mem_entities I + (liftAssign fintFairy) g f +``` + +Nesta estrutura, portanto, as duas leituras de qualquer fórmula concordam: o {lean}`Bool` que {name}`checkSentence` calcula e a proposição que a sentença afirma são a mesma coisa. Isso vale porque o domínio é finito e está listado — em {ref "FOL"}[FOL] vimos que nenhuma lista consegue fazer o mesmo pelos naturais. + +::::exercise (rating := 2) (name := "help-defeat") +Considere os verbos *help* e *defeat* e os sintagmas nominais *Alice*, *Snow White*, *every wizard* e *a dwarf*. Determine, para cada sentença da forma `S ::= NP TV NP` construída com esses verbos e sintagmas, se ela é verdadeira ou falsa nesta estrutura. + +A lista `sentences` abaixo tem as trinta e duas sentenças, na ordem em que os laços as geram. Complete `values` com os trinta e dois valores de verdade. + +```lean +def someNPs : List NP := + [.alice, .snowWhite, + .npDet .every .wizard, .npDet .a .dwarf] + +def sentences : List Sent := + someNPs.flatMap fun subj => + [TV.helped, TV.defeated].flatMap fun v => + someNPs.map fun obj => + Sent.sent subj (.vpTrans v obj) + +def values : List Bool := + solution!( + [false, false, false, false, + false, false, true, false, + false, false, false, true, + false, false, false, false, + false, false, false, false, + false, false, false, false, + false, false, false, false, + false, false, false, false]) + +theorem values_correct : + sentences.map checkSentence = values := + solution!(by native_decide) +``` + +:::gradeTheorem "2" values_correct +::: +:::: -Como já implementamos a semantica de FOL no `FOL.lean`, nesta mesma seção podemos absorver CSwFP/6.4 usando o que já temos em `FOL.lean` +:::dev "Claude Opus 5" PotentialImprovement (year := 2026) +Comentário gerado por IA. Os trinta e dois valores em `values` foram calculados pela avaliação, não conferidos à mão; o `native_decide` garante que eles concordam com `checkSentence`, mas não que `checkSentence` seja a semântica pretendida. Vale conferir alguns casos no modelo antes de publicar. ::: diff --git a/DEVIATIONS.md b/DEVIATIONS.md index e099487..9569d1d 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -11,7 +11,7 @@ the decisions serve are in `STYLE-CODE.md` and `STYLE-WRITING.md`. CSwFP runs sets, lambda calculus and types (2) before Haskell (3). That works because its chapter 2 is prose. In Lean the same material is code, so the language has to come first, and chapter 2 is split: 2.3 and 2.4 into -`IntroL`, 2.1 and 2.2 into `Sets`, 2.5 into `English`. +`IntroL`, 2.1 and 2.2 into `Sets`; 2.5 is dropped. | Chapter | Requires | Why | |--------------|-----------|-----------------------------------------------------------------------------| @@ -22,7 +22,7 @@ language has to come first, and chapter 2 is split: 2.3 and 2.4 into | `SeaBattle` | `Logic` | its exercises prove theorems by induction on `WellFormed` | | `Morphology` | `IntroL` | placed here so that its exercises may use tactics | | `InfEngine` | `Sets` | the language of 4.3 is about sets, and the syllogisms are proved over `Set` | -| `English` | `Sets` | its categorial section interprets verbs over `Sets.Entity` | +| `English` | `Logic` | it translates into `FOL`'s `Formula` and evaluates with its `eval`; best after `Sets`, whose characteristic functions build the model | CSwFP/6 is in `English`: it is built on the fragment of 4.2, whose categories it translates one by one. @@ -104,10 +104,30 @@ decisions inside the chapters. ### `English` -Being written (#29). Planned: the semantic types are named `e` and `t`, since -`NP`, `VP` and the other category names are the fragment's `inductive`s, and -the typing rules of 2.5 are shown over the fragment's own types. `INF` is in -the 4.2 grammar but has no translation in CSwFP/6. +- The sections are 6.1, 4.2, 6.2, and 6.3 with 6.4. 6.2 translates the 4.2 + grammar category by category, so the grammar comes first; 6.1 motivates the + translation, so it opens the chapter. +- A Lean function is total, so the gaps `MCWPL.hs` leaves are decisions: + - `most` is not in `DET`: it has no first-order translation, as 6.2 says, + and the prose states the limitation. `a` is in `DET`, since 6.2 treats it. + - `AV`, `To`, `INF` and `TINF` are not in the grammar: they illustrate + intensionality, and 6.2 gives them no translation. + - `ADJ` is translated intersectively. That is right for *happy* and *evil*, + not for *fake*, and the prose says so. + - `caught` gets an atom like every transitive verb. The model does not + interpret it, so every sentence using it is false. +- The grammar is extended by wrapping, not by redeclaring: a new category + containing the old one (`| base (np : NP)`) plus the new rules. The chapter + shows it on sentence coordination, and the exercises of 4.7 and 4.8 use it. + The extension is not recursive, and the new constructors never overlap with + the old ones. +- Constructors are named for what they are (`npDet`, `rcnSubj`, `rcnObj`, + `vpTrans`), not numbered (`NP1`, `RCN2`). +- The fairy-tale model of 6.3 is here, next to the grammar it interprets. + Predicates are `Entity → Bool`; `admire` and `defeat` are written as + conditions rather than list comprehensions; `Unspec` is the default of the + `FInterp`; and names and argument order agree with the translation, which + in the Haskell source they do not. ## Beyond CSwFP/6 diff --git a/STYLE-CODE.md b/STYLE-CODE.md index a8b71a1..8b9b1aa 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -82,13 +82,16 @@ this way is usually a mistake; see "Known gaps." | `SeaBattle` | inductive predicate (`inductive WellFormed : Game → Prop where`) | structure fields that carry proofs, bounded `∀ x ∈ xs`, `by` as a structure-field value, `Fin.val`, dependent `if h : … then … else` **(solution only)**, `▸` **(solution only)** | *(none new)* | | `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, `ToString` and its instance, `s!` strings | — | -| `English` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`) | *(none new)* | +| `English` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`), pattern-matching `fun \| … => …` (first use outside a solution) | *(none new)* | `English` is where `abbrev` and `ToString` instances become the dominant idiom, but both arrive earlier; what is genuinely new there is the mutually recursive *grammar*, a `mutual` block over `inductive` declarations rather than over `def`s, and `«with»`, which quotes a Lean keyword so it can be used -as a constructor name. +as a constructor name. The pattern-matching `fun` — `fun | .a => "a" | …`, +with no `match` — first appears in `IntroL` and `Logic/PL`, both times inside +a `solution!`, so `English`'s `ToString` instances are where a student first +meets it in ordinary code. The table records features, not every piece of notation. Type ascription, list literals, projection dots, and the like are not tracked: they arrive with @@ -141,7 +144,9 @@ author decision, not a mechanical fix. ordinary code — `|>` at `FOL.lean:369` and `match e₁, e₂ with` at `Morphology/Phonemes.lean:227`. `mapM` is the same shape: first used inside a solution (`Phonemes.lean:309`) and visible only much later, at - `InfEngine.lean:439`. The rest never surface at all. + `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 `English`. 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 84f89bc52774636c0e9389c0a3ec8f03306b21d9 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sat, 26 Sep 2026 14:50:57 -0300 Subject: [PATCH 2/7] wip: English chapter --- CSwL/English.lean | 49 ++++++++++++++++------------------------------- 1 file changed, 17 insertions(+), 32 deletions(-) diff --git a/CSwL/English.lean b/CSwL/English.lean index d21c932..5214e0c 100644 --- a/CSwL/English.lean +++ b/CSwL/English.lean @@ -21,37 +21,25 @@ namespace English tag := "english-form" %%% -> — Não vejo ninguém na estrada — disse Alice. -> -> — Quem dera eu tivesse olhos assim — observou o Rei, em tom lamentoso. — Poder ver Ninguém! E a essa distância, ainda por cima! -> -> {citep Bib.carroll1865}[] - Da sentença *Alice walked on the road* segue-se que alguém caminhou na estrada, mas de *No one walked on the road* não se segue que alguém caminhou na estrada. Por isso lógicos como Gottlob Frege (1848–1925), Bertrand Russell (1872–1970), Alfred Tarski (1902–1983) e Willard Van Orman Quine (1908–2000) sustentaram que a estrutura dessas duas sentenças tem de ser diferente, e que não basta dizer que ambas são composições de um sujeito e um predicado. Os lógicos que usaram a lógica de predicados de primeira ordem para analisar a estrutura lógica da língua natural se impressionaram com o fato de que as traduções lógicas de sentenças com expressões quantificadas não pareciam acompanhar a estrutura linguística. Nas traduções lógicas, as expressões quantificadas pareciam ter desaparecido. A tradução lógica de (1) não revela nenhum constituinte correspondente ao sintagma nominal quantificado que faz de sujeito. -```display -(1) Every dwarf loved Goldilocks. - -(2) ∀x (Dwarf x → Love x g) -``` +1. Every dwarf loved Goldilocks. +2. `∀x (Dwarf x → Love x g)` -Na tradução (2) o constituinte *every dwarf* desapareceu; ele foi contextualmente eliminado. Frege observa que uma expressão quantificada como *every dwarf* não dá origem a um conceito por si só — *eine selbständige Vorstellung* —, e só pode ser interpretada no contexto da tradução da sentença inteira. Considerando este exemplo em particular, a paráfrase literal de (2) é: +Na tradução (2) o constituinte *every dwarf* desapareceu; ele foi contextualmente eliminado. Frege observa que uma expressão quantificada como *every dwarf* não dá origem a um conceito por si só, e só pode ser interpretada no contexto da tradução da sentença inteira. Considerando este exemplo em particular, a tradução literal de (2) seria: -> Todos os objetos do domínio de discurso têm a propriedade de ou não ser anões, ou ser objetos que amaram Goldilocks. +> All objects in the domain of discourse have the property of either not being dwarves or +being objects who loved Goldilocks. Nessa reformulação da sentença (1), o sintagma *every dwarf* não ocorre mais. -As propriedades lógicas das sentenças que envolvem expressões quantificadas — e descrições, analisadas em termos de quantificadores — sugeriam, de fato, que o modo como um sintagma nominal simples, como um nome próprio, se combina com um predicado é logicamente diferente do modo como um sintagma nominal quantificado ou uma descrição definida se combina com um predicado. Isso levou à crença de que a forma linguística das expressões da língua natural era enganosa. +As propriedades lógicas das sentenças que envolvem expressões quantificadas (e descrições, analisadas em termos de quantificadores) sugeriam, de fato, que o modo como um sintagma nominal simples, como um nome próprio, se combina com um predicado é logicamente diferente do modo como um sintagma nominal quantificado ou uma descrição definida se combina com um predicado. Isso levou à crença de que a forma linguística das expressões da língua natural era enganosa. A aplicação das ferramentas lógicas de abstração e redução do cálculo lambda nos permite ver que essa conclusão era injustificada. Traduzindo a língua natural em expressões de uma lógica tipada, veremos que os constituintes da língua natural correspondem a expressões tipadas que se combinam umas com as outras como funções e argumentos. Depois da redução completa dos resultados, as expressões quantificadas e outros constituintes podem ter sido contextualmente eliminados, mas essa eliminação é resultado do processo de redução, e não da suposta forma enganosa da sentença original. Assim, embora as traduções lógicas completamente reduzidas de sentenças da língua natural possam ser enganosas em algum sentido, as expressões originais, não reduzidas, não são. -Como exemplo do modo como as ferramentas do cálculo lambda aplainam as aparências lógicas, considere a lógica da combinação de sujeitos e predicados. Nos casos mais simples — como *Goldilocks laughed* — poderíamos dizer que o predicado toma o sujeito como argumento. Mas isso não funciona para sujeitos quantificados, como em *no one laughed*. Tudo se resolve, porém, se dissermos que o sujeito sempre toma o predicado como seu argumento, e fizermos isso valer também para os sujeitos simples, elevando logicamente seu estatuto de argumento a função. Com expressões lambda isso é bastante fácil: traduzimos *Goldilocks* não como a constante `g`, e sim como a expressão `λP ↦ P g`. Essa expressão denota uma função de propriedades em valores de verdade, e pode portanto tomar a tradução de um predicado como argumento. A tradução de *no one* é do mesmo tipo: - -```display -λP ↦ ¬∃x (Person x ∧ P x) -``` +Como exemplo do modo como as ferramentas do cálculo lambda aplainam as aparências lógicas, considere a lógica da combinação de sujeitos e predicados. Nos casos mais simples — como *Goldilocks laughed* — poderíamos dizer que o predicado toma o sujeito como argumento. Mas isso não funciona para sujeitos quantificados, como em *no one laughed*. Tudo se resolve, porém, se dissermos que o sujeito sempre toma o predicado como seu argumento, e fizermos isso valer também para os sujeitos simples, elevando logicamente seu estatuto de argumento a função. Com expressões lambda isso é bastante fácil: traduzimos *Goldilocks* não como a constante `g`, e sim como a expressão `λP ↦ P g`. Essa expressão denota uma função de propriedades em valores de verdade, e pode portanto tomar a tradução de um predicado como argumento. A tradução de *no one* é do mesmo tipo `λP ↦ ¬∃x (Person x ∧ P x)`. Antes da redução, as traduções de *Goldilocks laughed* e de *no one laughed* se parecem muito. As semelhanças só desaparecem depois que as duas traduções são reduzidas às suas formas mais simples. @@ -60,8 +48,6 @@ Em {ref "english-lf"}[FOL como linguagem de representação] demonstramos isso c :::dev "Claude Opus 5" (year := 2026) Comentário gerado por IA. Duas observações sobre a tradução desta seção. -A epígrafe é atribuída, na fonte, a *Alice in Wonderland*; o diálogo com o Rei é de *Through the Looking-Glass*. A tradução manteve a atribuição da fonte — corrigi-la é decisão humana. A entrada `Bib.carroll1865` registra o título que a fonte cita. - Os exemplos em inglês foram mantidos em inglês, como em todo o capítulo: eles são o objeto de estudo, e traduzi-los destruiria o argumento (*No one walked on the road* e *ninguém caminhou na estrada* não têm a mesma sintaxe). As paráfrases *sobre* os exemplos estão em português. ::: @@ -72,19 +58,20 @@ tag := "english-fragment" Suponha que queiramos escrever regras gramaticais para sentenças do inglês como as seguintes: -1. The girl laughed. -2. No dwarf admired some princess that shuddered. -3. Every girl that some boy loved cheered. -4. The wizard that helped Snow White defeated the giant. +1. The girl laughed. ("A menina riu.") +2. No dwarf admired some princess that shuddered. ("Nenhum anão admirou alguma princesa que estremeceu.") +3. Every girl that some boy loved cheered. ("Toda menina que algum menino amou torceu.") +4. The wizard that helped Snow White defeated the giant. ("O mago que ajudou Branca de Neve derrotou o gigante.") O que precisamos é de uma regra para a estrutura sujeito–predicado das sentenças, uma regra para a estrutura interna dos sintagmas nominais, uma regra para os substantivos comuns com ou sem orações relativas, e é mais ou menos só isso. A gramática a seguir dá conta dos exemplos: ```bnf S ::= NP VP ; -NP ::= "Snow White" | "Alice" | "Dorothy" | "Goldilocks" | "Little Mook" | "Atreyu" - | "everyone" | "someone" | DET CN | DET RCN ; +NP ::= "Snow White" | "Alice" | "Dorothy" | "Goldilocks" | "Little Mook" + | "Atreyu" | "everyone" | "someone" | DET CN | DET RCN ; DET ::= "a" | "the" | "every" | "some" | "no" ; -CN ::= "girl" | "boy" | "princess" | "dwarf" | "giant" | "wizard" | "sword" | "dagger" ; +CN ::= "girl" | "boy" | "princess" | "dwarf" | "giant" | "wizard" | "sword" + | "dagger" ; ADJ ::= "fake" | "happy" | "evil" ; RCN ::= CN "that" VP | CN "that" NP TV | ADJ CN ; VP ::= "laughed" | "cheered" | "shuddered" | TV NP | DV NP NP ; @@ -255,10 +242,6 @@ def sent1 : Sent := #eval toString sent1 ``` -```leanOutput sent1eval -"the dwarf that Snow White helped admired every princess" -``` - Ir da sentença de superfície para a árvore é o problema inverso, chamado de *análise sintática*. Não o trataremos aqui: neste capítulo as árvores são construídas à mão, e o que nos interessa é o que fazer com elas depois de construídas. ## Estender uma gramática @@ -596,6 +579,8 @@ def boundIndices : LF → List Nat | .disj f1 f2 => boundIndices f1 ++ boundIndices f2 | .forall_ v f => v.index ++ boundIndices f | .exists_ v f => v.index ++ boundIndices f + +-- #eval boundIndices (FOL.ExSchool.R FOL.tx FOL.ty) ~> [1] ``` Para calcular um índice novo, basta escolher um índice fora dessa lista. Todas as variáveis são introduzidas pelo mesmo mecanismo: se começarmos com variáveis da forma `⟨"x", [0]⟩` e só introduzirmos variáveis novas da mesma forma, podemos supor que toda variável que ocorre na forma lógica tem esse feitio. O `0` inicial em `foldr max 0` garante que a lista sobre a qual tomamos o máximo não seja vazia. From defb7e4d4535d3acdc381b10dc7626a2330d1814 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Wed, 14 Oct 2026 23:58:11 -0300 Subject: [PATCH 3/7] wip: english --- CSwL/English.lean | 33 +++++---------------------------- 1 file changed, 5 insertions(+), 28 deletions(-) diff --git a/CSwL/English.lean b/CSwL/English.lean index 5214e0c..0162430 100644 --- a/CSwL/English.lean +++ b/CSwL/English.lean @@ -21,7 +21,7 @@ namespace English tag := "english-form" %%% -Da sentença *Alice walked on the road* segue-se que alguém caminhou na estrada, mas de *No one walked on the road* não se segue que alguém caminhou na estrada. Por isso lógicos como Gottlob Frege (1848–1925), Bertrand Russell (1872–1970), Alfred Tarski (1902–1983) e Willard Van Orman Quine (1908–2000) sustentaram que a estrutura dessas duas sentenças tem de ser diferente, e que não basta dizer que ambas são composições de um sujeito e um predicado. +Da sentença *Alice walked on the road* segue-se que alguém caminhou na estrada, mas de *No one walked on the road* não se segue que alguém caminhou na estrada. Por isso lógicos como Gottlob Frege (1848–1925), Bertrand Russell (1872–1970), Alfred Tarski (1902–1983) e Willard Van Orman Quine (1908–2000) sustentaram que a estrutura dessas duas sentenças tem de ser diferente, e que não basta dizer que ambas são a composição de um sujeito e um predicado. Os lógicos que usaram a lógica de predicados de primeira ordem para analisar a estrutura lógica da língua natural se impressionaram com o fato de que as traduções lógicas de sentenças com expressões quantificadas não pareciam acompanhar a estrutura linguística. Nas traduções lógicas, as expressões quantificadas pareciam ter desaparecido. A tradução lógica de (1) não revela nenhum constituinte correspondente ao sintagma nominal quantificado que faz de sujeito. @@ -67,13 +67,16 @@ O que precisamos é de uma regra para a estrutura sujeito–predicado das senten ```bnf S ::= NP VP ; +S₁ ::= S | S "and" S; NP ::= "Snow White" | "Alice" | "Dorothy" | "Goldilocks" | "Little Mook" | "Atreyu" | "everyone" | "someone" | DET CN | DET RCN ; +NP₁ ::= NP | .... ; DET ::= "a" | "the" | "every" | "some" | "no" ; CN ::= "girl" | "boy" | "princess" | "dwarf" | "giant" | "wizard" | "sword" | "dagger" ; ADJ ::= "fake" | "happy" | "evil" ; RCN ::= CN "that" VP | CN "that" NP TV | ADJ CN ; +RCN₁ ::= RCN | CN "that" NP₁ TV ; VP ::= "laughed" | "cheered" | "shuddered" | TV NP | DV NP NP ; TV ::= "loved" | "admired" | "helped" | "defeated" | "caught" ; DV ::= "gave" ; @@ -283,10 +286,6 @@ def sent2 : SentAnd := #eval toString sent2 ``` -```leanOutput sentAndEval -"Alice laughed and Dorothy cheered" -``` - Os dois exercícios a seguir estendem o fragmento por esse caminho. ::::exercise (rating := 2) (name := "preposition-phrase") @@ -579,8 +578,6 @@ def boundIndices : LF → List Nat | .disj f1 f2 => boundIndices f1 ++ boundIndices f2 | .forall_ v f => v.index ++ boundIndices f | .exists_ v f => v.index ++ boundIndices f - --- #eval boundIndices (FOL.ExSchool.R FOL.tx FOL.ty) ~> [1] ``` Para calcular um índice novo, basta escolher um índice fora dessa lista. Todas as variáveis são introduzidas pelo mesmo mecanismo: se começarmos com variáveis da forma `⟨"x", [0]⟩` e só introduzirmos variáveis novas da mesma forma, podemos supor que toda variável que ocorre na forma lógica tem esse feitio. O `0` inicial em `foldr max 0` garante que a lista sobre a qual tomamos o máximo não seja vazia. @@ -703,31 +700,10 @@ def lf3 : LF := (.rcnSubj .princess .that (.vpTrans .helped .alice))) .shuddered) -``` -```lean (name := lf1eval) #eval lf1 ``` -```leanOutput lf1eval -∃x2 (dwarf[x2] & ∃x1 (giant[x1] & defeat[x2, x1])) -``` - -```lean (name := lf2eval) -#eval lf2 -``` - -```leanOutput lf2eval -∃x1 (∀x2 ((wizard[x2] & admire[Dorothy, x2]) <=> x1 = x2) & laugh[x1]) -``` - -```lean (name := lf3eval) -#eval lf3 -``` - -```leanOutput lf3eval -∃x1 (∀x2 ((princess[x2] & help[x2, Alice]) <=> x1 = x2) & shudder[x1]) -``` ::::exercise (rating := 2) (name := "fragment-translations") Construa as árvores de análise das quatro sentenças a seguir, todas geradas pelo fragmento. @@ -904,6 +880,7 @@ def shudder : OnePlacePred := list1 [.S] Os verbos transitivos denotam relações entre entidades, e é conveniente pensar um predicado de dois lugares como a lista dos pares para os quais ele vale. Dois deles não são dados por uma lista fixa: *admire* vale de toda pessoa para Goldilocks, e *defeat* vale de todo anão para todo gigante, além dos dois pares em que Alice derrota um mago. ```lean + def love : TwoPlacePred := list2 [(.Y, .E), (.B, .S), (.R, .S)] From 8f7e92adb3ac3a1d88b3dc1c659b7a778de2ee35 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sun, 18 Oct 2026 21:20:20 -0300 Subject: [PATCH 4/7] wip(English): trim the grammar and drop graded theorems MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove the S₁/NP₁/RCN₁ rules from the BNF block and the parse-tree display, turn the surface-string checks into plain examples (dropping their :::gradeTheorem blocks), and remove a stray #eval and comments. --- CSwL/English.lean | 59 +++++++++++------------------------------------ 1 file changed, 14 insertions(+), 45 deletions(-) diff --git a/CSwL/English.lean b/CSwL/English.lean index 0162430..33ba8fa 100644 --- a/CSwL/English.lean +++ b/CSwL/English.lean @@ -67,16 +67,13 @@ O que precisamos é de uma regra para a estrutura sujeito–predicado das senten ```bnf S ::= NP VP ; -S₁ ::= S | S "and" S; NP ::= "Snow White" | "Alice" | "Dorothy" | "Goldilocks" | "Little Mook" | "Atreyu" | "everyone" | "someone" | DET CN | DET RCN ; -NP₁ ::= NP | .... ; DET ::= "a" | "the" | "every" | "some" | "no" ; CN ::= "girl" | "boy" | "princess" | "dwarf" | "giant" | "wizard" | "sword" | "dagger" ; ADJ ::= "fake" | "happy" | "evil" ; RCN ::= CN "that" VP | CN "that" NP TV | ADJ CN ; -RCN₁ ::= RCN | CN "that" NP₁ TV ; VP ::= "laughed" | "cheered" | "shuddered" | TV NP | DV NP NP ; TV ::= "loved" | "admired" | "helped" | "defeated" | "caught" ; DV ::= "gave" ; @@ -212,25 +209,7 @@ instance : ToString RCN := ⟨RCN.toText⟩ instance : ToString VP := ⟨VP.toText⟩ ``` -A árvore de análise de *The dwarf that Snow White helped admired every princess* é a seguinte. - -```display -S -├── NP -│ ├── DET — the -│ └── RCN -│ ├── CN — dwarf -│ ├── That — that -│ ├── NP — Snow White -│ └── TV — helped -└── VP - ├── TV — admired - └── NP - ├── DET — every - └── CN — princess -``` - -O termo Lean correspondente é este. +A árvore de análise de *The dwarf that Snow White helped admired every princess* corresponde diretamente ao termo Lean. ```lean def sent1 : Sent := @@ -306,7 +285,7 @@ S' ::= NP VPP ; 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. +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 guillemets: `«with»`. Fora da declaração, `.with` já é lido como o construtor e dispensa os guilhemets. ```lean inductive Prep where @@ -369,42 +348,36 @@ Agora construa as três árvores: as duas leituras de *A dwarf defeated a giant ```lean def withSword : PP := .pp .with (.npDet .a .sword) --- O sintagma preposicional modifica o objeto. def giantSword1 : SentPP := solution!( .sent (.npDet .a .dwarf) (.objPP .defeated (.withPP .a .giant withSword))) --- O sintagma preposicional modifica o sintagma verbal. def giantSword2 : SentPP := solution!( .sent (.npDet .a .dwarf) (.vpPP .defeated (.npDet .a .giant) withSword)) --- Única leitura possível. def mookSword : SentPP := solution!( .sent (.npDet .a .dwarf) (.vpPP .defeated .littleMook withSword)) -theorem giantSword_ambiguous : - toString giantSword1 = toString giantSword2 := +example + : toString giantSword1 = toString giantSword2 := solution!(by rfl) -theorem giantSword_surface : - toString giantSword1 = - "a dwarf defeated a giant with a sword" := +example + : toString giantSword1 = + "a dwarf defeated a giant with a sword" := solution!(by rfl) -theorem mookSword_surface : - toString mookSword = - "a dwarf defeated Little Mook with a sword" := +example + : toString mookSword = + "a dwarf defeated Little Mook with a sword" := solution!(by rfl) ``` -:::gradeTheorem "1" giantSword_ambiguous giantSword_surface mookSword_surface -::: - As duas primeiras árvores são diferentes e imprimem a mesma sentença: é a ambiguidade pedida. :::: @@ -481,17 +454,15 @@ def dwarfHelpedAdmired : SentC := .and .goldilocks .admired)) .cheered) -theorem dwarfHelpedAdmired_surface : +example : toString dwarfHelpedAdmired = "the dwarf that Snow White helped and " ++ "Goldilocks admired cheered" := solution!(by rfl) ``` - -:::gradeTheorem "1" dwarfHelpedAdmired_surface -::: :::: + # FOL como Linguagem de representação %%% tag := "english-lf" @@ -700,8 +671,6 @@ def lf3 : LF := (.rcnSubj .princess .that (.vpTrans .helped .alice))) .shuddered) - -#eval lf1 ``` @@ -773,6 +742,7 @@ theorem tr4_surface : Temos agora representações de sentenças declarativas da língua natural como fórmulas da lógica de predicados. Falta dizer quando essas fórmulas são verdadeiras. + # Uma Estrutura de Primeira Ordem %%% tag := "english-model" @@ -963,6 +933,7 @@ theorem self3IO_introduced : ::: :::: + ## Interpretando os símbolos Já temos em {ref "fol-semantics"}[a semântica de FOL] tudo o que é preciso para avaliar fórmulas: {name}`FOL.Interp` interpreta os símbolos de predicado, {name}`FOL.FInterp` os símbolos funcionais, {name}`FOL.Assign` as variáveis, e {name}`FOL.Formula.eval` percorre a fórmula. Falta apenas ligar os nomes que a tradução produz às relações que acabamos de definir. @@ -1117,8 +1088,6 @@ Comentário gerado por IA. Os trinta e dois valores em `values` foram calculados ::: - - ```lean end English ``` From 70d3cadb926d86324013d713d53021b08153af21 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sun, 18 Oct 2026 23:08:25 -0300 Subject: [PATCH 5/7] refactor(ModelChecking): rename the English chapter The whole book is about English, so the old name did not tell this chapter apart. Follow CSwFP's title instead: the chapter translates the syntax trees into first-order logic and then checks the sentences against a model. Update the tag, namespace, Book, the ledger in STYLE-CODE.md, CSwFP.yaml, DEVIATIONS.md and README.md. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author. --- Book.lean | 4 ++-- CSwFP.yaml | 20 ++++++++++---------- CSwL/{English.lean => ModelChecking.lean} | 10 +++++----- DEVIATIONS.md | 10 +++++----- README.md | 3 +-- STYLE-CODE.md | 12 ++++++------ 6 files changed, 29 insertions(+), 30 deletions(-) rename CSwL/{English.lean => ModelChecking.lean} (99%) diff --git a/Book.lean b/Book.lean index 45aebdd..76f2ecf 100644 --- a/Book.lean +++ b/Book.lean @@ -8,7 +8,7 @@ import CSwL.Sets import CSwL.SeaBattle import CSwL.Morphology import CSwL.InfEngine -import CSwL.English +import CSwL.ModelChecking import VersoManual @@ -34,4 +34,4 @@ set_option verso.code.warnLineLength 80 {include CSwL.SeaBattle} {include CSwL.Morphology} {include CSwL.InfEngine} -{include CSwL.English} +{include CSwL.ModelChecking} diff --git a/CSwFP.yaml b/CSwFP.yaml index 55389a8..40d7f5a 100644 --- a/CSwFP.yaml +++ b/CSwFP.yaml @@ -187,8 +187,8 @@ sections: the reader has just written. Its linguistic example is dropped, with 2.5. 2.5 Types in Grammar and Computation: to: dropped - why: 6.1 makes the same point in English, that a proper name translates - as λP ↦ P g. Making it twice would fragment the presentation. + why: 6.1 makes the same point in ModelChecking, that a proper name + translates as λP ↦ P g. Making it twice would fragment the presentation. 2.6 Functional Programming: to: absorbed why: It bridges to a programming language the reader has already seen. @@ -212,7 +212,7 @@ sections: 3.13 User-defined Data Types and Pattern Matching: to: IntroL why: Its Subject/Predicate example is dropped, so that no fragment of - natural language appears before the one English builds. + natural language appears before the one ModelChecking builds. 3.14 Application, Representing Phonemes: Morphology 3.15 Further Reading: omitted @@ -221,7 +221,7 @@ sections: to: SeaBattle why: Together with 5.1, syntax and semantics in one chapter. The Mastermind grammar is dropped with 5.4. - 4.2 A Fragment of English: English + 4.2 A Fragment of English: ModelChecking 4.3 A Language for Talking about Classes: to: InfEngine why: Together with 5.7, and after Sets, since the language is about sets. @@ -244,7 +244,7 @@ sections: why: The model is the four-vertex graph of Enderton, since the model of 6.3 belongs with the fragment it interprets. 5.6 Semantics of Natural Language Fragments: - to: English + to: ModelChecking why: Only its exercise 5.27 is kept. Its translation key is superseded by 6.2, which computes the translation. 5.7 An Inference Engine with a Natural Language Interface: @@ -254,13 +254,13 @@ sections: 5.8 Further Reading: omitted CSwFP/6: - 6.1 Linguistic Form and Translation Into Logic: English, before 4.2 - 6.2 Predicate Logic as Representation Language: English - 6.3 Representing a Model for Predicate Logic: English + 6.1 Linguistic Form and Translation Into Logic: ModelChecking, before 4.2 + 6.2 Predicate Logic as Representation Language: ModelChecking + 6.3 Representing a Model for Predicate Logic: ModelChecking 6.4 Evaluating Formulas in Models: - to: English + to: ModelChecking why: Absorbed. Its interpretation, assignments and eval are already in - Logic/FOL, so English adds only the model and checkSentence. + Logic/FOL, so ModelChecking adds only the model and checkSentence. 6.5 Evaluating Formulas with Structured Terms: to: Logic/FOL why: It is about the evaluator, not the fragment. The evaluation over diff --git a/CSwL/English.lean b/CSwL/ModelChecking.lean similarity index 99% rename from CSwL/English.lean rename to CSwL/ModelChecking.lean index 33ba8fa..b6a15ec 100644 --- a/CSwL/English.lean +++ b/CSwL/ModelChecking.lean @@ -5,15 +5,15 @@ import CSwL.Logic.FOL open Verso.Genre Manual open CSwLMeta -#doc (Manual) "Um fragmento de inglês" => +#doc (Manual) "Verificação de modelos com lógica de primeira ordem" => %%% -tag := "English" +tag := "ModelChecking" htmlSplit := .never -file := "English" +file := "ModelChecking" %%% ```lean -namespace English +namespace ModelChecking ``` # Formas Linguísticas e Traduções para Lógica @@ -1089,5 +1089,5 @@ Comentário gerado por IA. Os trinta e dois valores em `values` foram calculados ```lean -end English +end ModelChecking ``` diff --git a/DEVIATIONS.md b/DEVIATIONS.md index 9569d1d..cb7822c 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -22,9 +22,9 @@ language has to come first, and chapter 2 is split: 2.3 and 2.4 into | `SeaBattle` | `Logic` | its exercises prove theorems by induction on `WellFormed` | | `Morphology` | `IntroL` | placed here so that its exercises may use tactics | | `InfEngine` | `Sets` | the language of 4.3 is about sets, and the syllogisms are proved over `Set` | -| `English` | `Logic` | it translates into `FOL`'s `Formula` and evaluates with its `eval`; best after `Sets`, whose characteristic functions build the model | +| `ModelChecking` | `Logic` | it translates into `FOL`'s `Formula` and evaluates with its `eval`; best after `Sets`, whose characteristic functions build the model | -CSwFP/6 is in `English`: it is built on the fragment of 4.2, whose +CSwFP/6 is in `ModelChecking`: it is built on the fragment of 4.2, whose categories it translates one by one. ## Reusing Mathlib and CSLib @@ -102,7 +102,7 @@ decisions inside the chapters. its name. - The closing section, which proves syllogisms valid over `Set`, has no source. -### `English` +### `ModelChecking` - The sections are 6.1, 4.2, 6.2, and 6.3 with 6.4. 6.2 translates the 4.2 grammar category by category, so the grammar comes first; 6.1 motivates the @@ -131,5 +131,5 @@ decisions inside the chapters. ## Beyond CSwFP/6 -Not planned yet. CSwFP/7 continues the fragment of `English` and builds on the -same syntax, so it comes after `English`. +Not planned yet. CSwFP/7 continues the fragment of `ModelChecking` and builds on the +same syntax, so it comes after `ModelChecking`. diff --git a/README.md b/README.md index 2701b6c..7b66a21 100644 --- a/README.md +++ b/README.md @@ -46,8 +46,7 @@ adapts — see [DEVIATIONS.md](DEVIATIONS.md) for why. [source](CSwL/Morphology.lean) (sections in [`CSwL/Morphology/`](CSwL/Morphology)) - [~] An inference engine — [source](CSwL/InfEngine.lean) -- [~] A fragment of English — [source](CSwL/English.lean) -- [ ] Model checking with predicate logic — in `CSwL/English.lean` +- [~] Model checking with first-order logic — [source](CSwL/ModelChecking.lean) - [ ] The composition of meaning - [ ] Extension and intension - [ ] Parsing diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 44515e7..9785565 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -82,16 +82,16 @@ this way is usually a mistake; see "Known gaps." | `SeaBattle` | inductive predicate (`inductive WellFormed : Game → Prop where`) | structure fields that carry proofs, bounded `∀ x ∈ xs`, `by` as a structure-field value, `Fin.val`, dependent `if h : … then … else` **(solution only)**, `▸` **(solution only)** | *(none new)* | | `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, `ToString` and its instance, `s!` strings | — | -| `English` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`), pattern-matching `fun \| … => …` (first use outside a solution) | *(none new)* | +| `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)* | -`English` is where `abbrev` and `ToString` instances become the dominant -idiom, but both arrive earlier; what is genuinely new there is the mutually +`ModelChecking` is where `abbrev` and `ToString` instances become the +dominant idiom, but both arrive earlier; what is genuinely new there is the mutually recursive *grammar*, a `mutual` block over `inductive` declarations rather than over `def`s, and `«with»`, which quotes a Lean keyword so it can be used as a constructor name. The pattern-matching `fun` — `fun | .a => "a" | …`, with no `match` — first appears in `IntroL` and `Logic/PL`, both times inside -a `solution!`, so `English`'s `ToString` instances are where a student first -meets it in ordinary code. +a `solution!`, so `ModelChecking`'s `ToString` instances are where a student +first meets it in ordinary code. The table records features, not every piece of notation. Type ascription, list literals, projection dots, and the like are not tracked: they arrive with @@ -146,7 +146,7 @@ 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 `English`. The rest never surface at all. + throughout `ModelChecking`. 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 e68985106fd469be077605b1438bd2e2c5234a0a Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sun, 18 Oct 2026 23:34:50 -0300 Subject: [PATCH 6/7] wip: remove extra blank line --- CSwL/ModelChecking.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/CSwL/ModelChecking.lean b/CSwL/ModelChecking.lean index b6a15ec..25275bc 100644 --- a/CSwL/ModelChecking.lean +++ b/CSwL/ModelChecking.lean @@ -850,7 +850,6 @@ def shudder : OnePlacePred := list1 [.S] Os verbos transitivos denotam relações entre entidades, e é conveniente pensar um predicado de dois lugares como a lista dos pares para os quais ele vale. Dois deles não são dados por uma lista fixa: *admire* vale de toda pessoa para Goldilocks, e *defeat* vale de todo anão para todo gigante, além dos dois pares em que Alice derrota um mago. ```lean - def love : TwoPlacePred := list2 [(.Y, .E), (.B, .S), (.R, .S)] From 90d4f70ad9582201fd2b820d941249e1f6be7bae Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sun, 18 Oct 2026 23:59:19 -0300 Subject: [PATCH 7/7] wip: review first section --- CSwL/ModelChecking.lean | 44 ++++++++++++++++++++++++++--------------- 1 file changed, 28 insertions(+), 16 deletions(-) diff --git a/CSwL/ModelChecking.lean b/CSwL/ModelChecking.lean index 25275bc..5ef8aa3 100644 --- a/CSwL/ModelChecking.lean +++ b/CSwL/ModelChecking.lean @@ -16,40 +16,52 @@ file := "ModelChecking" namespace ModelChecking ``` +Nas linguagens formais construídas artificialmente, como a lógica proposicional e a lógica de predicados, as regras de formação de fórmulas são perfeitamente estritas, unívocas e livres de ambiguidade. A língua natural humana, por outro lado, apresenta um desafio de outra ordem: ela é rica e expressiva, mas repleta de nuances estruturais. Para que um computador possa manipular e verificar a veracidade de sentenças em inglês, precisamos construir uma ponte rigorosa entre a gramática das línguas humanas e a precisão da lógica formal. + +Este capítulo constrói o pipeline clássico da semântica computacional para um fragmento do inglês. Primeiro, em {ref "english-fragment"}[Um fragmento do inglês], especificamos a sintaxe do fragmento por meio de uma gramática livre de contexto, implementada em Lean como tipos indutivos que representam diretamente árvores de análise sintática. Em seguida, em {ref "english-lf"}[FOL como linguagem de representação], traduzimos essas árvores sintáticas para fórmulas da lógica de primeira ordem, guiados pelo princípio da composicionalidade e por ferramentas do cálculo lambda. Por fim, em {ref "english-model"}[Uma estrutura de primeira ordem], avaliamos as fórmulas obtidas em um modelo concreto, conectando sentenças sobre um micromundo ficcional aos seus valores de verdade. + + # Formas Linguísticas e Traduções para Lógica %%% tag := "english-form" %%% -Da sentença *Alice walked on the road* segue-se que alguém caminhou na estrada, mas de *No one walked on the road* não se segue que alguém caminhou na estrada. Por isso lógicos como Gottlob Frege (1848–1925), Bertrand Russell (1872–1970), Alfred Tarski (1902–1983) e Willard Van Orman Quine (1908–2000) sustentaram que a estrutura dessas duas sentenças tem de ser diferente, e que não basta dizer que ambas são a composição de um sujeito e um predicado. +Da sentença *Alice walked on the road* segue-se que alguém caminhou na estrada, mas de *No one walked on the road* não se segue que alguém caminhou na estrada. Por isso lógicos como Gottlob Frege (1848–1925), Bertrand Russell (1872–1970), Alfred Tarski (1902–1983) e Willard Van Orman Quine (1908–2000) sustentaram que a estrutura dessas duas sentenças deveria ser diferente, e que não basta dizer que ambas são a composição de um sujeito e um predicado. + +Em linguística, chamamos de _sintagma nominal_ (_Noun Phrase_, ou `NP`) qualquer bloco de palavras centrado em um substantivo que funcione como uma unidade sintática (como um sujeito ou objeto). Quando esse bloco é encabeçado por palavras lógicas como _every_ ("todo"), _some_ ("algum") ou _no_ ("nenhum"), temos um *sintagma nominal quantificado*. -Os lógicos que usaram a lógica de predicados de primeira ordem para analisar a estrutura lógica da língua natural se impressionaram com o fato de que as traduções lógicas de sentenças com expressões quantificadas não pareciam acompanhar a estrutura linguística. Nas traduções lógicas, as expressões quantificadas pareciam ter desaparecido. A tradução lógica de (1) não revela nenhum constituinte correspondente ao sintagma nominal quantificado que faz de sujeito. +Ao tentar traduzir a língua natural para a lógica de predicados de primeira ordem, os lógicos notaram uma discrepância marcante: a fórmula lógica final não acompanhava a estrutura gramatical visível da oração. Considere o exemplo: -1. Every dwarf loved Goldilocks. +1. _Every dwarf loved Goldilocks._ ("Todo anão amava Cachinhos Dourados.") 2. `∀x (Dwarf x → Love x g)` -Na tradução (2) o constituinte *every dwarf* desapareceu; ele foi contextualmente eliminado. Frege observa que uma expressão quantificada como *every dwarf* não dá origem a um conceito por si só, e só pode ser interpretada no contexto da tradução da sentença inteira. Considerando este exemplo em particular, a tradução literal de (2) seria: +Na oração original em inglês, _Every dwarf_ é o sujeito da frase, formando um bloco sintático coeso. A discrepância decorre da perda de individualidade que o quantificador introduz. Se a sentença fosse _Alice loved Goldilocks_, o sujeito apontaria para uma pessoa específica no mundo, representada diretamente na lógica por uma constante individual `a` (resultando em `Love a g`). -> All objects in the domain of discourse have the property of either not being dwarves or -being objects who loved Goldilocks. +Contudo, ao dizermos _Every dwarf_, não estamos nos referindo a um anão em particular: não existe no mundo um indivíduo chamado "Todo anão". Em vez de apontar para uma entidade isolada, o quantificador estabelece uma condição geral sobre todos os objetos do universo: _para qualquer objeto x, se x for um anão, então x amou Cachinhos Dourados_ (o que equivale logicamente a dizer que ou esse objeto não é um anão, ou ele amou Cachinhos Dourados). -Nessa reformulação da sentença (1), o sintagma *every dwarf* não ocorre mais. +É a isso que lógicos como Gottlob Frege chamavam de *eliminação contextual*: expressões quantificadas não denotam indivíduos e, por isso, deixam de existir como termos isolados na lógica de predicados. Seu significado só se manifesta na forma como condicionam a oração inteira. -As propriedades lógicas das sentenças que envolvem expressões quantificadas (e descrições, analisadas em termos de quantificadores) sugeriam, de fato, que o modo como um sintagma nominal simples, como um nome próprio, se combina com um predicado é logicamente diferente do modo como um sintagma nominal quantificado ou uma descrição definida se combina com um predicado. Isso levou à crença de que a forma linguística das expressões da língua natural era enganosa. +Essa discrepância levou muitos lógicos do início do século XX a supor que a língua natural era inerentemente imperfeita ou enganosa. Contudo, o desenvolvimento da semântica formal por Richard Montague revelou que essa conclusão era precipitada. -A aplicação das ferramentas lógicas de abstração e redução do cálculo lambda nos permite ver que essa conclusão era injustificada. Traduzindo a língua natural em expressões de uma lógica tipada, veremos que os constituintes da língua natural correspondem a expressões tipadas que se combinam umas com as outras como funções e argumentos. Depois da redução completa dos resultados, as expressões quantificadas e outros constituintes podem ter sido contextualmente eliminados, mas essa eliminação é resultado do processo de redução, e não da suposta forma enganosa da sentença original. Assim, embora as traduções lógicas completamente reduzidas de sentenças da língua natural possam ser enganosas em algum sentido, as expressões originais, não reduzidas, não são. +A chave para resolver esse impasse está em retomar o princípio da composicionalidade (visto em {ref "IntroCS"}[IntroCS]) sob a ótica do cálculo lambda (apresentado em {ref "lambda"}[IntroL]). Quando traduzimos a língua natural para uma lógica tipada, cada constituinte da oração corresponde a uma expressão funcional bem tipada. A combinação gramatical das palavras passa a refletir diretamente a aplicação de _funções aos seus argumentos_. O desaparecimento contextual dos quantificadores é simplesmente o resultado da computação dessas funções (a β-redução), e não uma falha estrutural da sentença original. -Como exemplo do modo como as ferramentas do cálculo lambda aplainam as aparências lógicas, considere a lógica da combinação de sujeitos e predicados. Nos casos mais simples — como *Goldilocks laughed* — poderíamos dizer que o predicado toma o sujeito como argumento. Mas isso não funciona para sujeitos quantificados, como em *no one laughed*. Tudo se resolve, porém, se dissermos que o sujeito sempre toma o predicado como seu argumento, e fizermos isso valer também para os sujeitos simples, elevando logicamente seu estatuto de argumento a função. Com expressões lambda isso é bastante fácil: traduzimos *Goldilocks* não como a constante `g`, e sim como a expressão `λP ↦ P g`. Essa expressão denota uma função de propriedades em valores de verdade, e pode portanto tomar a tradução de um predicado como argumento. A tradução de *no one* é do mesmo tipo `λP ↦ ¬∃x (Person x ∧ P x)`. +Para ilustrar como o cálculo lambda harmoniza a análise lógica, considere a combinação de sujeitos e predicados: -Antes da redução, as traduções de *Goldilocks laughed* e de *no one laughed* se parecem muito. As semelhanças só desaparecem depois que as duas traduções são reduzidas às suas formas mais simples. +* Na sentença simples _Goldilocks laughed_, a intuição imediata da lógica de primeira ordem é tratar o predicado como a função que consome o sujeito: `Laughed(g)`. +* No entanto, essa estratégia falha para sujeitos quantificados como _No one laughed_: não existe um indivíduo "ninguém" que possamos passar como argumento para `Laughed`. -Em {ref "english-lf"}[FOL como linguagem de representação] demonstramos isso construindo fórmulas da lógica de predicados como traduções das sentenças da língua natural geradas pelo fragmento de {ref "english-fragment"}[Um fragmento do inglês]. Essa tradução é o primeiro passo para interpretar indiretamente as expressões da língua natural. O passo seguinte, em {ref "english-model"}[Uma estrutura de primeira ordem], é atribuir às fórmulas da lógica de predicados um objeto modelo-teórico como denotação. Desse modo, a expressão da língua natural representada recebe uma interpretação modelo-teórica. No caminho, veremos as limitações desse procedimento. +A solução elegante de Montague consiste em _inverter a relação funcional_ para todos os sujeitos (processo conhecido como *elevação de tipo*, ou _type raising_): em vez de o predicado consumir o sujeito, é o sujeito que consome o predicado como argumento! -:::dev "Claude Opus 5" (year := 2026) -Comentário gerado por IA. Duas observações sobre a tradução desta seção. +Com expressões lambda, isso se torna direto: + +1. O nome próprio _Goldilocks_ deixa de ser tratado como a constante individual `g` e passa a ser a função de ordem superior `λP ↦ P g`. Essa função recebe uma propriedade `P` e afirma que `g` tem essa propriedade. +2. O sintagma quantificado _no one_ recebe exatamente a mesma assinatura de tipo: `λP ↦ ¬∃x (Person x ∧ P x)`, consumindo igualmente uma propriedade `P`. +Assim, tanto _Goldilocks laughed_ quanto _no one laughed_ combinam-se sintática e semanticamente da mesma maneira: o sujeito aplica-se ao predicado. A aparente assimetria só ressurge quando efetuamos a β-redução para simplificar a fórmula lógica final. + +Esse método nos permite realizar a _interpretação indireta_ da língua natural: em vez de tentar avaliar sentenças em inglês diretamente em um modelo, nós as traduzimos primeiro para fórmulas da lógica de primeira ordem, cuja semântica formal já dominamos. + +Para que essa tradução composicional seja viável, porém, precisamos de um ponto de partida indispensável: delimitar a estrutura sintática das sentenças que queremos analisar. É a essa tarefa de modelagem gramatical que nos dedicamos a seguir em {ref "english-fragment"}[Um fragmento do inglês]. -Os exemplos em inglês foram mantidos em inglês, como em todo o capítulo: eles são o objeto de estudo, e traduzi-los destruiria o argumento (*No one walked on the road* e *ninguém caminhou na estrada* não têm a mesma sintaxe). As paráfrases *sobre* os exemplos estão em português. -::: # Um fragmento do Inglês %%%