def CCG.catToTy : Cat → Core.Logic.Intensional.Ty

Map CCG categories to semantic types

Equations

• CCG.catToTy (CCG.Cat.atom CCG.Atom.S) = Core.Logic.Intensional.Ty.t
• CCG.catToTy (CCG.Cat.atom CCG.Atom.NP) = Core.Logic.Intensional.Ty.e
• CCG.catToTy (CCG.Cat.atom CCG.Atom.N) = (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)
• CCG.catToTy (CCG.Cat.atom CCG.Atom.PP) = (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)
• CCG.catToTy (x_1.rslash y) = (CCG.catToTy y ⇒ CCG.catToTy x_1)
• CCG.catToTy (x_1.lslash y) = (CCG.catToTy y ⇒ CCG.catToTy x_1)

structure CCG.SemLexEntry (F : Core.Logic.Intensional.Frame) : Type

A CCG lexical entry with semantics

• form : String
• cat : Cat
• sem : F.Denot (catToTy self.cat)

def CCG.semLexicon : List (SemLexEntry Semantics.Montague.toyModel)

Semantic lexicon for the toy model

Equations

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

def CCG.john_sem' : Semantics.Montague.toyModel.Denot (catToTy NP)

Equations

• CCG.john_sem' = Semantics.Montague.ToyEntity.john

def CCG.sleeps_sem' : Semantics.Montague.toyModel.Denot (catToTy IV)

Equations

• CCG.sleeps_sem' = Semantics.Montague.ToyLexicon.sleeps_sem

def CCG.john_sleeps_sem : Semantics.Montague.toyModel.Denot (catToTy S)

Equations

• CCG.john_sleeps_sem = CCG.sleeps_sem' CCG.john_sem'

def CCG.sees_sem' : Semantics.Montague.toyModel.Denot (catToTy TV)

Equations

• CCG.sees_sem' = Semantics.Montague.ToyLexicon.sees_sem

def CCG.mary_sem' : Semantics.Montague.toyModel.Denot (catToTy NP)

Equations

• CCG.mary_sem' = Semantics.Montague.ToyEntity.mary

def CCG.sees_mary_sem : Semantics.Montague.toyModel.Denot (catToTy IV)

Equations

• CCG.sees_mary_sem = CCG.sees_sem' CCG.mary_sem'

def CCG.john_sees_mary_sem : Semantics.Montague.toyModel.Denot (catToTy S)

Equations

• CCG.john_sees_mary_sem = CCG.sees_mary_sem CCG.john_sem'

def CCG.mary_sees_john_sem : Semantics.Montague.toyModel.Denot (catToTy S)

Equations

• CCG.mary_sees_john_sem = CCG.sees_sem' CCG.john_sem' CCG.mary_sem'

def CCG.eats_sem' : Semantics.Montague.toyModel.Denot (catToTy TV)

Equations

• CCG.eats_sem' = Semantics.Montague.ToyLexicon.eats_sem

def CCG.pizza_sem' : Semantics.Montague.toyModel.Denot (catToTy NP)

Equations

• CCG.pizza_sem' = Semantics.Montague.ToyEntity.pizza

def CCG.john_eats_pizza_sem : Semantics.Montague.toyModel.Denot (catToTy S)

Equations

• CCG.john_eats_pizza_sem = CCG.eats_sem' CCG.pizza_sem' CCG.john_sem'

def CCG.sentenceTrue (meaning : Semantics.Montague.toyModel.Denot Core.Logic.Intensional.Ty.t) : Prop

A sentence is true if its meaning holds

Equations

• CCG.sentenceTrue meaning = meaning

theorem CCG.forward_app_type_preservation (x y : Cat) : catToTy (x.rslash y) = (catToTy y ⇒ catToTy x)

Forward application preserves semantic typing: If X/Y combines with Y to give X, then (σ→τ) applied to σ gives τ

theorem CCG.backward_app_type_preservation (x y : Cat) : catToTy (x.lslash y) = (catToTy y ⇒ catToTy x)

Backward application preserves semantic typing: If Y combines with X\Y to give X, then (σ→τ) applied to σ gives τ

theorem CCG.tv_type_is_relation : catToTy TV = (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Type correspondence for transitive verbs

theorem CCG.iv_type_is_property : catToTy IV = (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Type correspondence for intransitive verbs

structure CCG.SemDeriv (F : Core.Logic.Intensional.Frame) : Type

A semantic derivation: pairs a CCG category with its meaning. This represents a node in the derivation tree with its semantic interpretation.

• cat : Cat
• meaning : F.Denot (catToTy self.cat)

def CCG.applyMeaning {F : Core.Logic.Intensional.Frame} {σ τ : Core.Logic.Intensional.Ty} (f : F.Denot (σ ⇒ τ)) (x : F.Denot σ) : F.Denot τ

Apply a function meaning to an argument meaning

Equations

• CCG.applyMeaning f x = f x

theorem CCG.composition_is_application {F : Core.Logic.Intensional.Frame} {σ τ : Core.Logic.Intensional.Ty} (f : F.Denot (σ ⇒ τ)) (x : F.Denot σ) : applyMeaning f x = f x

Composition is function application

theorem CCG.lexical_has_meaning (entry : SemLexEntry Semantics.Montague.toyModel) : ∃ (meaning : Semantics.Montague.toyModel.Denot (catToTy entry.cat)), meaning = entry.sem

For a lexical entry, we can always extract its meaning.

theorem CCG.combination_has_meaning {F : Core.Logic.Intensional.Frame} {x y : Cat} (functor_meaning : F.Denot (catToTy (x.rslash y))) (arg_meaning : F.Denot (catToTy y)) : ∃ (result : F.Denot (catToTy x)), result = functor_meaning arg_meaning

If we have meanings for functor and argument with compatible types, we can compute the meaning of the result.

theorem CCG.john_sees_mary_typed_derivation : have sees_ty := Semantics.Montague.ToyLexicon.sees_sem; have mary_ty := Semantics.Montague.ToyEntity.mary; have sees_mary_ty := sees_ty mary_ty; have john_ty := Semantics.Montague.ToyEntity.john; have result := sees_mary_ty john_ty; result

The complete derivation of "John sees Mary" preserving types

theorem CCG.mary_sleeps_typed_derivation : have sleeps_ty := Semantics.Montague.ToyLexicon.sleeps_sem; have mary_ty := Semantics.Montague.ToyEntity.mary; have result := sleeps_ty mary_ty; ¬result

The derivation of "Mary sleeps" preserving types

theorem CCG.forward_app_homomorphism {F : Core.Logic.Intensional.Frame} {x y : Cat} (f_sem : F.Denot (catToTy (x.rslash y))) (a_sem : F.Denot (catToTy y)) : f_sem a_sem = f_sem a_sem

Forward application satisfies the homomorphism: ⟦fapp(f, a)⟧ = ⟦f⟧(⟦a⟧)

The semantic interpretation of syntactic combination is function application.

theorem CCG.backward_app_homomorphism {F : Core.Logic.Intensional.Frame} {x y : Cat} (a_sem : F.Denot (catToTy y)) (f_sem : F.Denot (catToTy (x.lslash y))) : f_sem a_sem = f_sem a_sem

Backward application satisfies the homomorphism: ⟦bapp(a, f)⟧ = ⟦f⟧(⟦a⟧)

The order of arguments in syntax doesn't affect semantic composition.

structure CCG.Interp (F : Core.Logic.Intensional.Frame) : Type

A semantic interpretation: category paired with its meaning

• cat : Cat
• meaning : F.Denot (catToTy self.cat)

def CCG.SemLexicon (F : Core.Logic.Intensional.Frame) : Type

Semantic lexicon: maps words to interpretations

Equations

• CCG.SemLexicon F = (String → CCG.Cat → Option (CCG.Interp F))

def CCG.toySemLexicon : SemLexicon Semantics.Montague.toyModel

The toy semantic lexicon

Equations

• One or more equations did not get rendered due to their size.
• CCG.toySemLexicon "John" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.john }
• CCG.toySemLexicon "Mary" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.mary }
• CCG.toySemLexicon "beans" (CCG.Cat.atom CCG.Atom.NP) = some { cat := CCG.NP, meaning := Semantics.Montague.ToyEntity.pizza }
• CCG.toySemLexicon "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.toySemLexicon "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.toySemLexicon word cat = none

def CCG.DerivStep.interp (d : DerivStep) (lex : SemLexicon Semantics.Montague.toyModel) : Option (Interp Semantics.Montague.toyModel)

Interpret a CCG derivation, computing its meaning from the lexicon.

Returns none if the derivation is ill-formed or uses unknown words.

Equations

• One or more equations did not get rendered due to their size.
• (CCG.DerivStep.lex entry).interp lex = lex entry.form entry.cat
• (d_2.ftr t).interp lex = do let __discr ← d_2.interp lex match __discr with | { cat := x, meaning := m } => some { cat := CCG.forwardTypeRaise x t, meaning := CCG.T✝ m }
• (d_2.btr t).interp lex = do let __discr ← d_2.interp lex match __discr with | { cat := x, meaning := m } => some { cat := CCG.backwardTypeRaise x t, meaning := CCG.T✝ m }

def CCG.getMeaning (result : Option (Interp Semantics.Montague.toyModel)) : Option Prop

Helper to extract meaning from interpretation result

Equations

• CCG.getMeaning (some { cat := CCG.Cat.atom CCG.Atom.S, meaning := m }) = some m
• CCG.getMeaning result = none

theorem CCG.john_sleeps_interp_correct : getMeaning (john_sleeps.interp toySemLexicon) = some True

Interpretation of "John sleeps" produces correct truth value

theorem CCG.john_sees_mary_interp_correct : getMeaning (john_sees_mary.interp toySemLexicon) = some True

Interpretation of "John sees Mary" produces correct truth value

def CCG.john_typeraised : DerivStep

Type-raised "John": John:NP → S/(S\NP) via forward type-raising

Equations

• CCG.john_typeraised = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).ftr CCG.S

def CCG.john_sees_mary_via_tr : DerivStep

"John sees Mary" via type-raising: John sees Mary NP (S\NP)/NP NP ↓T(S) S/(S\NP) (S\NP)/NP NP └────>────────┘ S\NP └──────>──────────────────────┘ S Note: Type-raised subject uses FORWARD application (it's S/(S\NP), seeking S\NP to its right)

Equations

• CCG.john_sees_mary_via_tr = CCG.john_typeraised.fapp ((CCG.DerivStep.lex { form := "sees", cat := CCG.TV }).fapp (CCG.DerivStep.lex { form := "Mary", cat := CCG.NP }))

theorem CCG.john_sees_mary_via_tr_correct : getMeaning (john_sees_mary_via_tr.interp toySemLexicon) = some True

Type-raised derivation produces correct truth value

def CCG.john_likes_composed : DerivStep

"John likes" as S/NP via type-raising + composition (for coordination): John likes NP (S\NP)/NP ↓T(S) S/(S\NP) └──────>B────┘ S/NP

This is the constituent that can coordinate with "Mary hates" in "John likes and Mary hates beans".

Equations

• CCG.john_likes_composed = CCG.john_typeraised.fcomp (CCG.DerivStep.lex { form := "likes", cat := CCG.TV })

theorem CCG.coordination_semantics_well_formed : (john_likes_and_mary_hates_beans.interp toySemLexicon).isSome = true

THE COORDINATION SEMANTICS THEOREM

The interpretation of non-constituent coordination "John likes and Mary hates beans" is semantically well-formed (produces a truth value).

This is non-trivial because it requires:

1. Type-raising (T combinator)
2. Forward composition (B combinator)
3. Generalized conjunction (pointwise ∧)
4. Forward application

All four operations must compose correctly for the derivation to succeed.

def CCG.getPredicateMeaning (result : Option (Interp Semantics.Montague.toyModel)) : Option (Semantics.Montague.ToyEntity → Prop)

Extract the meaning of a coordination derivation as a function.

For an S/NP derivation (like "John likes and Mary hates"), the meaning is a predicate on entities.

Equations

• CCG.getPredicateMeaning (some { cat := (CCG.Cat.atom CCG.Atom.S).rslash (CCG.Cat.atom CCG.Atom.NP), meaning := m }) = some m
• CCG.getPredicateMeaning result = none

def CCG.coordMeaningAt (e : Semantics.Montague.ToyEntity) : Option Prop

Helper to extract predicate from coordination result.

Equations

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

def CCG.pointwiseConjAt (e : Semantics.Montague.ToyEntity) : Option Prop

Helper to compute pointwise conjunction of two predicate meanings.

Equations

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

theorem CCG.coordination_is_pointwise_conjunction (e : Semantics.Montague.ToyEntity) : coordMeaningAt e = pointwiseConjAt e

THE POINTWISE CONJUNCTION THEOREM

The meaning of "John likes and Mary hates" (category S/NP) is the pointwise conjunction of "John likes" and "Mary hates".

That is: ⟦John likes and Mary hates⟧(x) = ⟦John likes⟧(x) ∧ ⟦Mary hates⟧(x)

This is the semantic counterpart to the syntactic coordination rule.

theorem CCG.coordination_truth_conditions_correct : getMeaning (john_likes_and_mary_hates_beans.interp toySemLexicon) = some (Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.john ∧ Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.mary)

THE TRUTH-CONDITIONAL CORRECTNESS THEOREM

The truth value of "John likes and Mary hates beans" is true iff both John likes beans AND Mary hates beans.

In our toy model (where likes = hates = sees), this computes to the conjunction of the two predications.