CCG Bridge: Agreement Phenomena

Connects string-based Agreement phenomena to CCG derivations.

This module demonstrates the Bridge pattern:

1. String data lives in Phenomena/Agreement/Basic.lean
2. Lexical entries live in Fragments/English/
3. This module connects them via CCG interpretation

Architecture

Phenomena.Agreement.data ← Pure strings: "he sleeps" ✓
       ↓ (parse via Lexicon)
Fragments.English.Lexicon ← Unified lookup
       ↓ (interpret via FromFragments)
CCG.FromFragments ← VerbEntry → CCG.Cat
       ↓ (derive)
CCG.DerivStep ← Syntactic derivation

def Phenomena.Agreement.Studies.CCGAgreement.parse (s : String) : Option (List CCG.LexEntry)

Parse a sentence string to CCG lexical entries.

Uses the unified lexicon from Fragments/English/Lexicon.lean and interprets results via CCG.FromFragments.

Equations

• Phenomena.Agreement.Studies.CCGAgreement.parse s = CCG.FromFragments.parseToLexEntries s

def Phenomena.Agreement.Studies.CCGAgreement.tryDerive (entries : List CCG.LexEntry) : Option CCG.DerivStep

Attempt to build a simple CCG derivation from a list of lexical entries.

This is a simplified version that handles basic subject-verb structures. A full implementation would use chart parsing or similar.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Agreement.Studies.CCGAgreement.tryDerive entries = none

def Phenomena.Agreement.Studies.CCGAgreement.canDerive (s : String) : Bool

Check if CCG can derive a sentence string.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Agreement.Studies.CCGAgreement.capturesPair (pair : SentencePair) : Bool

Check if CCG captures a sentence pair (derives good, blocks bad).

Equations

• One or more equations did not get rendered due to their size.

theorem Phenomena.Agreement.Studies.CCGAgreement.parse_he_sleeps : (parse "he sleeps").isSome = true

theorem Phenomena.Agreement.Studies.CCGAgreement.parse_they_sleep : (parse "they sleep").isSome = true

theorem Phenomena.Agreement.Studies.CCGAgreement.parse_John_sleeps : (parse "John sleeps").isSome = true

theorem Phenomena.Agreement.Studies.CCGAgreement.derive_he_sleeps : canDerive "he sleeps" = true

theorem Phenomena.Agreement.Studies.CCGAgreement.derive_they_sleep : canDerive "they sleep" = true

theorem Phenomena.Agreement.Studies.CCGAgreement.derive_John_sleeps : canDerive "John sleeps" = true