def CCG.TruthConditions.ccg_john_sleeps : DerivStep

"John sleeps" - backward application

Equations

• CCG.TruthConditions.ccg_john_sleeps = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.TruthConditions.ccg_mary_sleeps : DerivStep

"Mary sleeps" - backward application

Equations

• CCG.TruthConditions.ccg_mary_sleeps = (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.TruthConditions.ccg_john_laughs : DerivStep

"John laughs" - backward application

Equations

• CCG.TruthConditions.ccg_john_laughs = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "laughs", cat := CCG.IV })

def CCG.TruthConditions.ccg_mary_laughs : DerivStep

"Mary laughs" - backward application

Equations

• CCG.TruthConditions.ccg_mary_laughs = (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "laughs", cat := CCG.IV })

def CCG.TruthConditions.ccg_john_sees_mary : DerivStep

"John sees Mary" - forward then backward application

Equations

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

def CCG.TruthConditions.ccg_mary_sees_john : DerivStep

"Mary sees John" - forward then backward application

Equations

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

def CCG.TruthConditions.ccg_john_eats_pizza : DerivStep

"John eats pizza" - forward then backward application

Equations

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

def CCG.TruthConditions.extendedLexicon : SemLexicon Semantics.Montague.toyModel

Extended lexicon with all entities and predicates

Equations

• One or more equations did not get rendered due to their size.
• CCG.TruthConditions.extendedLexicon "John" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.john }
• CCG.TruthConditions.extendedLexicon "Mary" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.mary }
• CCG.TruthConditions.extendedLexicon "pizza" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.pizza }
• CCG.TruthConditions.extendedLexicon "book" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.book }
• CCG.TruthConditions.extendedLexicon "sleeps" ((CCG.Cat.atom CCG.Atom.S).lslash (CCG.Cat.atom CCG.Atom.NP)) = some { cat := CCG.IV, meaning := Semantics.Montague.ToyLexicon.sleeps_sem }
• CCG.TruthConditions.extendedLexicon "laughs" ((CCG.Cat.atom CCG.Atom.S).lslash (CCG.Cat.atom CCG.Atom.NP)) = some { cat := CCG.IV, meaning := Semantics.Montague.ToyLexicon.laughs_sem }
• CCG.TruthConditions.extendedLexicon word cat = none

def CCG.TruthConditions.ccgMeaning (d : DerivStep) : Option Prop

Get meaning (as Prop) from CCG derivation

Equations

• CCG.TruthConditions.ccgMeaning d = CCG.getMeaning (d.interp CCG.TruthConditions.extendedLexicon)

theorem CCG.TruthConditions.ccg_predicts_john_sleeps : ccgMeaning ccg_john_sleeps = some True

CCG correctly predicts "John sleeps" is true

theorem CCG.TruthConditions.ccg_predicts_mary_sleeps : ccgMeaning ccg_mary_sleeps = some False

CCG correctly predicts "Mary sleeps" is false

theorem CCG.TruthConditions.ccg_predicts_john_laughs : ccgMeaning ccg_john_laughs = some True

CCG correctly predicts "John laughs" is true

theorem CCG.TruthConditions.ccg_predicts_mary_laughs : ccgMeaning ccg_mary_laughs = some True

CCG correctly predicts "Mary laughs" is true

theorem CCG.TruthConditions.ccg_predicts_john_sees_mary : ccgMeaning ccg_john_sees_mary = some True

CCG correctly predicts "John sees Mary" is true

theorem CCG.TruthConditions.ccg_predicts_mary_sees_john : ccgMeaning ccg_mary_sees_john = some True

CCG correctly predicts "Mary sees John" is true

structure CCG.TruthConditions.TestCase : Type

A test case: derivation paired with expected Prop

• deriv : DerivStep
• expected : Prop

def CCG.TruthConditions.ccgPredictsCorrectly (tc : TestCase) : Prop

Check if CCG predicts a test case correctly

Equations

• CCG.TruthConditions.ccgPredictsCorrectly tc = (CCG.TruthConditions.ccgMeaning tc.deriv = some tc.expected)

theorem CCG.TruthConditions.ccg_predicts_all_intransitive : ccgMeaning ccg_john_sleeps = some True ∧ ccgMeaning ccg_mary_sleeps = some False ∧ ccgMeaning ccg_john_laughs = some True ∧ ccgMeaning ccg_mary_laughs = some True

CCG correctly predicts ALL intransitive test cases.

theorem CCG.TruthConditions.ccg_predicts_all_transitive : ccgMeaning ccg_john_sees_mary = some True ∧ ccgMeaning ccg_mary_sees_john = some True

CCG correctly predicts ALL transitive test cases.

theorem CCG.TruthConditions.ccg_predicts_all_cases : ccgMeaning ccg_john_sleeps = some True ∧ ccgMeaning ccg_mary_sleeps = some False ∧ ccgMeaning ccg_john_laughs = some True ∧ ccgMeaning ccg_mary_laughs = some True ∧ ccgMeaning ccg_john_sees_mary = some True ∧ ccgMeaning ccg_mary_sees_john = some True

CCG correctly predicts ALL test cases.

The syntax → semantics pipeline produces correct truth conditions for the entire test suite.