From ab26a1360f4bcc86335b2a561aaf4be50f5b3b20 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sun, 20 Sep 2026 23:27:56 -0300 Subject: [PATCH] =?UTF-8?q?feat(English):=20write=20the=20chapter=20from?= =?UTF-8?q?=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. `PROVENANCE.md` gains the chapter's table and drops `feature-value`, withdrawn in the previous commit. `STYLE-CODE.md` records that the pattern-matching `fun` reaches ordinary code here. The generated `student` project builds. AI-usage disclosure: this chapter was drafted with the assistance of Claude Opus 5 (Anthropic, September 2026, via Claude Code). The assistant read the source material, chose the encoding of the grammar and its extensions, wrote the Lean definitions, exercises and proofs, drafted the Portuguese prose as a translation of the source, and updated the project's records. The author takes full responsibility for the final content. --- Bib.lean | 18 + CSwL/English.lean | 1132 ++++++++++++++++++++++++++++++++++++++++++++- DEVIATIONS.md | 70 +-- PROVENANCE.md | 56 ++- STYLE-CODE.md | 11 +- 5 files changed, 1236 insertions(+), 51 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/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 882f119..0339faa 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -82,10 +82,9 @@ opens "We already talked about functions informally", so it needs 2.3; 2.5 build | 5 | `SeaBattle.lean` | 4.1, 5.1 | 2, 3 | 4 | | 6 | `Morphology.lean` | 3.11, 3.14 | 2 | 3 | | 7 | `InfEngine.lean` | 4.3, 5.7 | 2, 3 | 4 | -| 8 | `English.lean` | 4.2, 5.6; 2.5 | 2, 3, 4 | — | -| 9 | `ModelChecking.lean` | 6.1–6.5 | 2, 3, 8 | 4 | +| 8 | `English.lean` | 6.1, 4.2, 6.2, 6.3–6.4; 5.6 | 2, 3 | 4 | -`Sets.lean` requires `Logic.lean` because its exercises are proofs, and the tactics they need — quantifiers, `cases`, `by_contra` — arrive there. `SeaBattle.lean` requires `Logic.lean` for the same reason: it proves theorems about `WellFormed` by induction on an inductive predicate, which no earlier chapter has the machinery for. `English.lean` requires `Sets.lean` because its categorial section interprets a transitive verb over `Sets.Entity` and `Sets.likesR`, the domain and relation that chapter introduces. +`Sets.lean` requires `Logic.lean` because its exercises are proofs, and the tactics they need — quantifiers, `cases`, `by_contra` — arrive there. `SeaBattle.lean` requires `Logic.lean` for the same reason: it proves theorems about `WellFormed` by induction on an inductive predicate, which no earlier chapter has the machinery for. `English.lean` required `Sets.lean` while it carried a categorial section interpreting a transitive verb over `Sets.Entity` and `Sets.likesR`. That section is gone (see the chapter's entry below), the chapter declares its own domain, and the import with it: `Sets.lean` is now only *best after*, because the fairy-tale model is built from characteristic functions and that is the representation choice `Sets.lean` makes. `Morphology.lean` requires only `IntroL.lean` — its three sections are programs, and the proofs in them are `rfl` on concrete values. It is placed after `SeaBattle.lean` rather than at its old position right after `IntroL.lean` so that its exercises may use the tactics `Logic.lean` presents, rather than being confined to what `IntroL.lean` alone allows. @@ -437,7 +436,7 @@ Decision: `PL.lean` does not state unique readability as a theorem. What it stat What is left of CSwFP/2 after 2.3, 2.4 and 2.5 moved to `IntroL.lean` and `English.lean`: sets and relations. Renamed from `Foundation.lean`, which promised a foundations chapter that no longer exists. `Sets` covers both halves honestly, because CSwFP/2.2 *defines* a relation as a subset of A × B — a relation is a set — and because what the chapter adds in Lean is precisely the representation choice for `Set α`. -**What the chapter is.** Sets and relations are presupposed notation from CSwFP/1 onwards, as in any mathematical text — which is why 5.5 can speak of `I(R) ⊆ D²` before this chapter exists. This chapter is where they are *mechanised in Lean*, and its opening has to say so, or it promises the wrong thing. That is also what makes it worth having: Lean forces representation choices — `Set α` vs. the predicate `α → Bool` vs. `Finset`, `Rel` vs. a list of pairs, decidability — and those choices determine how the models of `ModelChecking.lean` are built. +**What the chapter is.** Sets and relations are presupposed notation from CSwFP/1 onwards, as in any mathematical text — which is why 5.5 can speak of `I(R) ⊆ D²` before this chapter exists. This chapter is where they are *mechanised in Lean*, and its opening has to say so, or it promises the wrong thing. That is also what makes it worth having: Lean forces representation choices — `Set α` vs. the predicate `α → Bool` vs. `Finset`, `Rel` vs. a list of pairs, decidability — and those choices determine how the fairy-tale model of `English.lean` is built. **Why after `Logic.lean`.** Nothing downstream requires this chapter — no later chapter fails to compile without it — but the chapter itself requires `Logic.lean`, and that is what fixes its position. Both reasons are about the exercises: @@ -490,42 +489,55 @@ This chapter is independent of the English fragment: `InfEngine.hs` imports noth Three divergences. The least fixed point is computed with a fuel bound rather than by iterating until the value stops changing, because the latter has no structural termination argument; the bound is the square of the domain size, which is beyond what the closure can need. Relations are `List (α × α)`, named `Relation` rather than `Rel`, so that Mathlib's `Rel` — which `Sets.lean` introduces and this chapter's closing section uses through `Set` — keeps its name. And CSwFP/5.7's natural-language *input* is not ported: the parser, the file I/O and the `chat` loop are the only place in the book that would need `IO`, and the chapter states its interface through `ToString` on `Statement`, which is the output half. -### 8. `English.lean` — CSwFP/4.2, 5.6 +### 8. `English.lean` — CSwFP/6.1, 4.2, 6.2, 6.3–6.4 -The fragment of English (4.2) and its semantics (5.6), plus the natural-language fragments that CSwFP scatters earlier and that `CSwL` deliberately does not present in place: the `likes` example of 2.4, the `Subject`/`Predicate` example of 3.13, and all of 2.5 — the `S → NP VP` this chapter always carried, and now the type BNF `τ ::= b | (τ → τ)` and the three typing rules as well. CSwFP introduces a slightly larger grammar in 4.2 and then, in 5.6, sketches the semantics of an initial vocabulary largely disconnected from it. Gathering these fragments in one place is the point of this chapter. +The chapter has four sections, in this order: 6.1 (linguistic form and translation into logic), 4.2 (the fragment of English), 6.2 (predicate logic as representation language), and 6.3 together with 6.4 (the model, and evaluation in it). The order is forced. CSwFP/6.2 translates the 4.2 grammar category by category — the text says so, and `MCWPL.hs` imports the syntax module and opens with `lfSent :: Sent -> LF` — so the grammar has to exist first. 6.1 is the argument that motivates the translation at all, so it opens the chapter. -**What this chapter must deliver to `ModelChecking.lean`.** Gathering the fragments is the editorial goal, but the chapter also has a hard obligation: CSwFP/6 translates the 4.2 grammar category by category, so every category it destructures has to exist by the end of this chapter. `MCWPL.hs` defines one translation function per category — `lfSent`, `lfNP`, `lfDET`, `lfCN`, `lfRCN`, `lfVP`, `lfTV`, `lfDV` — so the required inventory is: +**CSwFP/2.4, 2.5 and 3.13 are no longer here.** Earlier drafts carried the `likes` example of 2.4, the `Subject`/`Predicate` example of 3.13, and all of 2.5 — the type BNF `τ ::= b | (τ → τ)`, the three typing rules, and a categorial section that named the semantic types `e` and `t` (so as not to collide with the `inductive`s that *are* the syntactic categories) and interpreted a transitive verb over `Sets.Entity` and `Sets.likesR`. The rewrite of 2026-09-20 dropped all of it. CSwFP/6.1 makes the same point that section made — *Goldilocks* translates not as the constant `g` but as `λP ↦ P g`, "a function from properties to truth values", and *no one* has the same type — and making it twice, once as an informal argument and once over Lean types, is the fragmented presentation the writing guide rules out. `adjective-types` (CSwFP/2.17) went with that section; `PROVENANCE.md` records it. The chapter no longer imports `CSwL.Sets`. -`Sent`, `NP`, `DET`, `CN`, `RCN`, `VP`, `TV`, `DV`, plus the auxiliaries `ADJ` and `That` that `RCN` uses. +**Totality changes the inventory.** Haskell lets a translation function be partial, and `MCWPL.hs` uses that licence four times: `lfDET` has no clause for `Most`, `lfRCN` none for `RCN3` (the adjective rule), `lfTV` none for `Caught`, and `lfNP` none for `Everyone`/`Someone`. A Lean function has to be defined everywhere, so each gap is a decision: -**Semantic types are named `e` and `t`, and that is not cosmetic.** The categorial section that arrived from CSwFP/2.5 originally wrote the semantic types as `NP`, `S`, `VP` and `TV` — the category names. In this chapter those names are already taken, by the `inductive`s that *are* the fragment's syntactic categories: two meanings for one name in one namespace, which does not compile and would not be worth compiling. The types now carry Montague's letters, `e` for entities and `t` for truth values, which the prose was already naming as the conventional choice; the categories keep `NP`/`VP` where they belong, in the prose. So "the VP has type `e → t`" now says two different things with two different notations, which is exactly the distinction the section is about. +- **`most` is not in `DET`.** CSwFP's own 4.2 grammar does not have it either; it is in the Haskell data type and then goes untranslated, because — as 6.2 says — *most* has no first-order translation at all. Keeping it would mean either a false translation or making `lfDET` return `Option LF`, which turns every function in the family `Option`-valued and buries the linguistics in plumbing. The limitation is stated in the prose instead, where 6.2 states it. `a` goes the other way: CSwFP's `data DET` does not have it, but 6.2's prose lists it among the five determiners it treats, and the preposition-phrase exercise needs *a dwarf*, so `DET` carries it. +- **`AV`, `To`, `INF` and `TINF` are not in the grammar.** CSwFP throws them in "for purposes of illustrating intensionality" in a chapter this book does not plan, and 6.2 gives them no translation. They are also the one part of the 4.2 fragment that CSwFP/6 never needed. +- **`ADJ` stays, and is translated intersectively.** `RCN` uses it, and *happy* and *evil* — CSwFP/4.6, absorbed into the presentation — really are conjunctive: a *happy wizard* is happy and a wizard. *Fake* is not, and the prose says so: the translation exists because the function must be total, not because it is right. +- **`caught` gets an atom like every other transitive verb.** The model does not interpret it, so every sentence using it is false; the prose points at this, since `FOL.lean` already established that an uninterpreted symbol evaluates to `false`. -This is where the rest of 2.5 lands. The type BNF `τ ::= b | (τ → τ)` says that `e` and `t` are the two basic types and that everything else is built from them by `→`, and the three typing rules — a variable has the type it is declared with, `(λx ↦ E) : δ → τ` when `x : δ` and `E : τ`, `(E₁ E₂) : τ` when `E₁ : δ → τ` and `E₂ : δ` — are what licenses the composition the section then performs. They were in `IntroL.lean`, demonstrated over a `Day → Prop` predicate for want of anything better so early in the book; here they are demonstrated over the fragment's own types, which is what 2.5 was about in CSwFP. In Lean `t` is `Prop`. +**The grammar is extended by wrapping, not by redeclaring.** CSwFP/4.7 and 4.8 ask the reader to extend the fragment, and in Haskell the answer is to rewrite the whole `data` group. An `inductive` is closed in the same way, but a mutually recursive group does not have to be redeclared to be extended: a *new* category that contains the old one — `| base (np : NP)` — plus the constructors for the new rules does the job, and the functions already written over the old types keep working. The chapter presents the technique on sentence coordination (`SentAnd`, three lines) and both exercises apply it. Two consequences, neither hidden: the extension is not recursive, so a prepositional phrase cannot contain another one and a coordinated relative clause cannot contain a coordinated relative clause; and the new constructors are shaped so that they never overlap with the old ones, or the extended grammar would derive the *unextended* sentences twice, which would wreck an exercise about counting derivations. -`INF` is part of the 4.2 grammar but has no translation in CSwFP/6; it is not required by `ModelChecking.lean`. +The distinction the chapter draws is between adding a *word* and adding a *rule*. Adding a word is adding a constructor to a leaf category, and no wrapping reaches it, so the lexicon is complete from the declaration — which is why CSwFP/4.6 is absorbed rather than set as an exercise. -### 9. CSwFP/6 — in `English.lean` +**Naming.** The constructors are `npDet`, `npDetRel`, `rcnSubj`, `rcnObj`, `rcnAdj`, `vpTrans`, `vpDitrans`, not `NP1`, `NP2`, `RCN1`, `RCN2`, `RCN3`, `VP1`, `VP2`. The numbers are positions in a Haskell `data` declaration and say nothing; `rcnSubj` and `rcnObj` say which position the relative clause's gap is in, which is the distinction the coordination exercise turns on. -Sections 6.1–6.5; 6.6 (Further Reading) omitted. +**The model.** CSwFP/6.3's fairy-tale model arrives here, next to the grammar it interprets, rather than in `FOL.lean` — the reason is in the `Logic.lean` section above. Three differences from `Model.hs`. Predicates are `Entity → Bool` and built from lists, as in the source, but `admire` and `defeat` are written as the conditions they are (`person x && y == .G`, `dwarf x && giant y || …`) rather than as list comprehensions over `entities`, which in Lean would say the same thing at more length. `Unspec` is the default of the `FInterp`, which makes the function total in the one way that is linguistically meaningful — an unnamed constant denotes an unspecified entity. And the interpretation agrees with the translation on names and argument order: `MCWPL.hs` emits `Atom "love" [subj, obj]` while `int0` keys on `"Love"` and reverses the arguments, so the two halves of the source never actually meet. -**This material lands in `English.lean`, not in a chapter of its own.** The -plan once called for a separate `ModelChecking.lean`, and the table above and -the references below still use that name for the material; they should be read -as naming CSwFP/6's content, wherever it sits. The reason it belongs with the -English fragment is the one given immediately below: it is built on that -fragment, so the two are one development, not two. +**6.4 is absorbed rather than ported.** Everything it builds — the interpretation function, variable assignments, `change`, `eval` — is already in `FOL.lean` as `Interp`, `Assign`, `Assign.update` and `Formula.eval`. What is left for this chapter is the model itself and the two-step procedure, `checkSentence`, which is CSwFP/6.7. -What this means for `FOL.lean` is recorded in the `Logic.lean` section above: -the fairy-tale model of 6.3 is *not* pulled forward into it any more. It -arrives here, next to the grammar it interprets, and `FOL.lean` evaluates -against Enderton's four-vertex graph instead. Sections 6.5's structured-term -evaluation and its `[0..]` discussion, by contrast, *are* in `FOL.lean`: they -are about the evaluator rather than about the fragment, and the chapter that -defines `Term` is where they belong. +**CSwFP/5.6 is present only as an exercise.** Its content is a translation key from lexical items to predicate letters, which 6.2 supersedes by computing the translation. Its Exercise 5.27 — four sentences of the fragment to translate — survives as `fragment-translations`. + +### 9. CSwFP/6 — where it lands + +Sections 6.1–6.4 are in `English.lean`, as the section above describes. Section +6.5's structured-term evaluation and its `[0..]` discussion are in `FOL.lean`: +they are about the evaluator rather than about the fragment, and the chapter +that defines `Term` is where they belong. Section 6.6 (Further Reading) is +omitted. -**This material must come after the fragment of 4.2.** CSwFP/6 does not merely allude to the fragment of 4.2 — it is built on it. The text says so ("to translate the fragment from Section 4.2 into predicate logic, all we have to do is find appropriate translations for all the categories in the grammar"), and the code confirms it: `MCWPL.hs` imports the syntax module and its first definition is `lfSent :: Sent -> LF`, destructuring `Sent np vp`. Placing the English fragment after model checking would use the grammar before presenting it. +**There is no `ModelChecking.lean`.** The plan once called for one, and older +notes in this file use that name for CSwFP/6's content; they should be read as +naming the content, not a file. The reason it belongs with the English +fragment is that it is built on that fragment, so the two are one development +rather than two. + +What this means for `FOL.lean` is recorded in the `Logic.lean` section above: +the fairy-tale model of 6.3 is *not* pulled forward into it. It arrives with +the grammar it interprets, and `FOL.lean` evaluates against Enderton's +four-vertex graph instead. -This is also why `Sets.lean` reads best just before it, though it is not required: `Model.hs` builds the model with `OnePlacePred = Entity -> Bool` and `list2OnePlacePred xs = \x -> elem x xs` — the characteristic function of 2.3 and the set-as-predicate of 2.1, applied. The choice between `Set Entity` and `Entity → Bool` is exactly the one `Sets.lean` makes. +This is also why `Sets.lean` reads best just before `English.lean`, though it +is not required: `Model.hs` builds the model with `OnePlacePred = Entity -> +Bool` and `list2OnePlacePred xs = \x -> elem x xs` — the characteristic +function of 2.3 and the set-as-predicate of 2.1, applied. The choice between +`Set Entity` and `Entity → Bool` is exactly the one `Sets.lean` makes. ## Omitted throughout @@ -535,7 +547,7 @@ All "Further Reading" sections (1.8, 2.7, 3.15, 4.8, 5.8, 6.6), 1.7 (Overview of Everything above is settled and covers CSwFP/1 to CSwFP/6. The rest of the book is deferred, and the placements below are provisional, not decisions. -CSwFP/7 (The Composition of Meaning in Natural Language) goes after `ModelChecking.lean`. It continues `English.lean`'s fragment and, in CSwFP, builds on the same syntax module, so the same constraint that puts `English.lean` before `ModelChecking.lean` keeps 7 downstream of both. How much of `English.lean` it absorbs — CSwFP/7 is where a consolidated semantics of a natural-language fragment actually appears — is the question to settle when that chapter is taken up. +CSwFP/7 (The Composition of Meaning in Natural Language) goes after `English.lean`. It continues that chapter's fragment and, in CSwFP, builds on the same syntax module, so the constraint that puts the fragment before CSwFP/6 keeps 7 downstream of both. How much of `English.lean` it absorbs — CSwFP/7 is where a consolidated semantics of a natural-language fragment actually appears — is the question to settle when that chapter is taken up. A proof system as data — CSLib's `Cslib.Logic.PL.Theory.Derivation` — is deferred rather than rejected, for the reasons in the `Logic.lean` section. It becomes attractive exactly where `CSwL` would have something to give back: CSLib has the derivations but no propositional semantics, and this book builds the valuation. Soundness — every derivable sequent is true under every valuation satisfying its context — needs both halves, and neither project has both today. `Cslib/Logics/README.md` invites exactly this ("we are interested in expanding them or creating new ones that can cover your use cases"). Its natural place is after `Sets.lean`, once relations and quantifiers are available. It stays out of the plan until CSwFP/1–6 are in place. diff --git a/PROVENANCE.md b/PROVENANCE.md index 2b1483b..314eb5e 100644 --- a/PROVENANCE.md +++ b/PROVENANCE.md @@ -20,7 +20,7 @@ passage it comes from**. Keep it in step with any further rename. stated in Lean. In the source these carry a `✎` marker, which is otherwise undocumented. -The book has 76 exercises as of 2026-09-13, and all but one of them +The book has 79 exercises as of 2026-09-20, and all but one of them appear somewhere below — either in a table that names its source, or in the list of those with no counterpart. Two checks keep it that way: no `(name := …)` in `CSwL/` should be absent from this file, and no @@ -60,11 +60,13 @@ CSwFP Exercise 1.3 (infinitely many sentences, p. 8) is not ported. |---------------------|--------|-----------------------------------------|-------| | `yawelmani-harmony` | 3 | Exercise 3.19 (Yawelmani vowel harmony) | 61–62 | -`feature-value` (rating 2) and `append-suffix-text` (rating 3) have no counterpart: -CSwFP hands `feature-value`/`fMatch` to the reader as given code, and `CSwL` turns -them into exercises. +`append-suffix-text` (rating 3) has no counterpart: CSwFP hands `fMatch` to the +reader as given code, and `CSwL` turns it into an exercise. `feature-value` was +a second such exercise, over `fValue`; it was withdrawn on 2026-09-20, when +eliding it left the generated `student` project with a `sorry` behind an +`#eval`, and `fValue` is now presented code again, as in CSwFP. -### `Sets.lean` — CSwFP/2 (exercises `twice` and `adjective-types` moved on with CSwFP/2.4 and 2.5, to `IntroL.lean` and `English.lean`) +### `Sets.lean` — CSwFP/2 (exercise `twice` moved on with CSwFP/2.4, to `IntroL.lean`) | CSwL id | Rating | CSwFP | Page | Notes | |-----------------------------|--------|---------------|-------|--------------------------------------| @@ -84,13 +86,20 @@ them into exercises. | — | — | Exercise 2.14 | 26–27 | prose; not in an `:::exercise` block | | — | — | Exercise 2.15 | 28 | prose; not in an `:::exercise` block | | — | — | Exercise 2.16 | 28 | prose; not in an `:::exercise` block | -| `adjective-types` | 1 | Exercise 2.17 | 30 | | +| — | — | Exercise 2.17 | 30 | dropped 2026-09-20; see below | Note that 2.14, 2.15 and 2.16 sit in the prose without an exercise directive, so they get no rating, no solution elision and no autograding. +Exercise 2.17 was `adjective-types`, which travelled to `English.lean` +with the rest of CSwFP/2.5 and was dropped from it on 2026-09-20, when +that chapter was rewritten around CSwFP/6.1, 4.2, 6.2 and 6.3–6.4. The +categorial material it belonged to — the types `e` and `t`, the type +BNF and the three typing rules — has no section in the chapter any +more. `DEVIATIONS.md` records the decision. + Exercises 2.1, 2.2 and 2.3 (`empty-subset`–`double-complement` above) stay with this chapter when it moves after `Logic.lean`; 2.3 (`Ā̄ = A`) is the one that needs classical reasoning, and is the reason for the @@ -251,6 +260,38 @@ Exercise 5.25 logical consequences Delta |= b holds? dep: ex-fol-implies-from-list +### `English.lean` — CSwFP/4.2, 5.6, 6.1–6.4 + +| CSwL id | Rating | CSwFP | Page | +|----------------------------|--------|---------------|------| +| `preposition-phrase` | 2 | Exercise 4.7 | 69 | +| `complex-relative-clauses` | 2 | Exercise 4.8 | 69 | +| `fragment-translations` | 2 | Exercise 5.27 | 106 | +| `check-sentence` | 2 | Exercise 6.7 | 147 | +| `help-defeat` | 2 | Exercise 6.1 | 137 | +| `reflexive-ditransitive` | 2 | Exercise 6.4 | 139 | + +`help-defeat` is stated in terms of `checkSentence`, so `dep: check-sentence`. + +Exercise 4.6 (adjectives *happy* and *evil*, p. 69) is **absorbed into the +presentation**. Adding a word to a category means adding a constructor, and an +`inductive` is closed: the extension cannot be written without redeclaring the +category. `ADJ` therefore carries `fake`, `happy` and `evil` from its +declaration, and the chapter's two extension exercises add *rules* instead, +which the wrapping technique reaches without redeclaring anything. + +Exercise 5.26 (check by hand, against the truth definition, that the +translation of *Every boy loved a girl* is right) is not ported as an +exercise: `check-sentence` is the mechanised form of the same question, and +the chapter's point is that the machine does this checking. + +Exercises 6.2 and 6.3 (passivization) are not ported. `passivize` is presented +in the prose, because `Unspec` needs a motivation and the passive is the one +the source gives, but neither exercise is. + +Exercises 6.5 and 6.6 belong to CSwFP/6.4–6.5, which `Logic/FOL.lean` carries; +see `DEVIATIONS.md`. + ### `InfEngine.lean` — CSwFP/5.7 | CSwL id | Rating | CSwFP | Page | Notes | @@ -289,11 +330,8 @@ as an oversight. | File | CSwL id | Rating | |---------------------------------|----------------------------|--------| -| `Morphology/Phonemes.lean` | `feature-value` | 2 | | `Morphology/Phonemes.lean` | `append-suffix-text` | 3 | | `Morphology/SwedishPlural.lean` | `swedish-plural` | 2 | -| `English.lean` | `preposition-phrase` | 1 | -| `English.lean` | `complex-relative-clauses` | 1 | | `Sets.lean` | `five-in-above2` | 1 | | `Sets.lean` | `one-not-in-above2` | 1 | | `Sets.lean` | `above5-subset-above2` | 1 | diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 0d39192..a9ced0c 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -75,13 +75,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 @@ -134,7 +137,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