structure CCG.Homomorphism.TypedDeriv (m : Semantics.Montague.Model) : Type

Well-typed CCG derivation with category and meaning.

• deriv : DerivStep
• cat : Cat
• catOk : self.deriv.cat = some self.cat
• meaning : m.interpTy (catToTy self.cat)

structure CCG.Homomorphism.CatMeaning (m : Semantics.Montague.Model) : Type

Category paired with semantic denotation.

• cat : Cat
• meaning : m.interpTy (catToTy self.cat)

theorem CCG.Homomorphism.fapp_sem {m : Semantics.Montague.Model} {x y : Cat} (f_sem : m.interpTy (catToTy (x.rslash y))) (a_sem : m.interpTy (catToTy y)) : ∃ (result : m.interpTy (catToTy x)), result = f_sem a_sem

Forward application is semantic function application.

def CCG.Homomorphism.fappSem {m : Semantics.Montague.Model} {x y : Cat} (f_sem : m.interpTy (catToTy (x.rslash y))) (a_sem : m.interpTy (catToTy y)) : m.interpTy (catToTy x)

Semantic rule for forward application.

Equations

• CCG.Homomorphism.fappSem f_sem a_sem = f_sem a_sem

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

Forward application types align.

theorem CCG.Homomorphism.bapp_sem {m : Semantics.Montague.Model} {x y : Cat} (a_sem : m.interpTy (catToTy y)) (f_sem : m.interpTy (catToTy (x.lslash y))) : ∃ (result : m.interpTy (catToTy x)), result = f_sem a_sem

Backward application is semantic function application.

def CCG.Homomorphism.bappSem {m : Semantics.Montague.Model} {x y : Cat} (a_sem : m.interpTy (catToTy y)) (f_sem : m.interpTy (catToTy (x.lslash y))) : m.interpTy (catToTy x)

Semantic rule for backward application.

Equations

• CCG.Homomorphism.bappSem a_sem f_sem = f_sem a_sem

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

Backward application types align.

theorem CCG.Homomorphism.fcomp_sem {m : Semantics.Montague.Model} {x y z : Cat} (f_sem : m.interpTy (catToTy (x.rslash y))) (g_sem : m.interpTy (catToTy (y.rslash z))) : ∃ (result : m.interpTy (catToTy (x.rslash z))), result = Combinators.B f_sem g_sem

Forward composition is the B combinator.

def CCG.Homomorphism.fcompSem {m : Semantics.Montague.Model} {x y z : Cat} (f_sem : m.interpTy (catToTy (x.rslash y))) (g_sem : m.interpTy (catToTy (y.rslash z))) : m.interpTy (catToTy (x.rslash z))

Semantic rule for forward composition.

Equations

• CCG.Homomorphism.fcompSem f_sem g_sem = CCG.Combinators.B f_sem g_sem

theorem CCG.Homomorphism.ftr_sem {m : Semantics.Montague.Model} {x t : Cat} (a_sem : m.interpTy (catToTy x)) : ∃ (result : m.interpTy (catToTy (forwardTypeRaise x t))), ∀ (f : m.interpTy (catToTy (t.lslash x))), result f = f a_sem

Forward type-raising is the T combinator.

def CCG.Homomorphism.ftrSem {m : Semantics.Montague.Model} {x t : Cat} (a_sem : m.interpTy (catToTy x)) : m.interpTy (catToTy (forwardTypeRaise x t))

Semantic rule for forward type-raising.

Equations

• CCG.Homomorphism.ftrSem a_sem f = f a_sem

def CCG.Homomorphism.wellFormed (d : DerivStep) : Prop

Well-formed derivations have categories.

Equations

• CCG.Homomorphism.wellFormed d = (d.cat.isSome = true)

theorem CCG.Homomorphism.lex_wellFormed (e : LexEntry) : wellFormed (DerivStep.lex e)

Lexical entries are well-formed.

theorem CCG.Homomorphism.wellFormed_has_cat (d : DerivStep) (h : wellFormed d) : ∃ (c : Cat), d.cat = some c

Well-formed derivations have categories.

theorem CCG.Homomorphism.interp_deterministic (d : DerivStep) (lex : SemLexicon Semantics.Montague.toyModel) (i1 i2 : Interp Semantics.Montague.toyModel) (h1 : d.interp lex = some i1) (h2 : d.interp lex = some i2) : i1 = i2

Derivation meanings are unique.

structure CCG.Homomorphism.HomomorphismProperty : Prop

Homomorphism property: syntactic rules correspond to semantic operations.

• fapp {m : Semantics.Montague.Model} {x y : Cat} (f : m.interpTy (catToTy (x.rslash y))) (a : m.interpTy (catToTy y)) : fappSem f a = f a
• bapp {m : Semantics.Montague.Model} {x y : Cat} (a : m.interpTy (catToTy y)) (f : m.interpTy (catToTy (x.lslash y))) : bappSem a f = f a
• fcomp {m : Semantics.Montague.Model} {x y z : Cat} (f : m.interpTy (catToTy (x.rslash y))) (g : m.interpTy (catToTy (y.rslash z))) : fcompSem f g = Combinators.B f g
• ftr {m : Semantics.Montague.Model} {x t : Cat} (a : m.interpTy (catToTy x)) : ftrSem a = Combinators.T a

def CCG.Homomorphism.ccgHomomorphism : HomomorphismProperty

CCG-Montague homomorphism satisfies all structural properties.

Equations

• CCG.Homomorphism.ccgHomomorphism = ⋯

structure CCG.Homomorphism.RuleToRuleRelation : Prop

Rule-to-rule relation: each syntactic rule has unique semantic rule.

• fapp_rule {m : Semantics.Montague.Model} {x y : Cat} (f : m.interpTy (catToTy (x.rslash y))) (a : m.interpTy (catToTy y)) : ∃! result : m.interpTy (catToTy x), result = f a
• bapp_rule {m : Semantics.Montague.Model} {x y : Cat} (a : m.interpTy (catToTy y)) (f : m.interpTy (catToTy (x.lslash y))) : ∃! result : m.interpTy (catToTy x), result = f a
• comp_rule {m : Semantics.Montague.Model} {x y z : Cat} (f : m.interpTy (catToTy (x.rslash y))) (g : m.interpTy (catToTy (y.rslash z))) : ∃! result : m.interpTy (catToTy (x.rslash z)), ∀ (arg : m.interpTy (catToTy z)), result arg = f (g arg)

def CCG.Homomorphism.ccgRuleToRule : RuleToRuleRelation

CCG satisfies rule-to-rule.

Equations

• CCG.Homomorphism.ccgRuleToRule = ⋯

def CCG.Homomorphism.Monotonic (combine : DerivStep → DerivStep → Option DerivStep) : Prop

Monotonic grammars preserve well-formedness.

Equations

• CCG.Homomorphism.Monotonic combine = ∀ (d1 d2 d3 : CCG.DerivStep), combine d1 d2 = some d3 → d1.cat.isSome = true ∧ d2.cat.isSome = true → d3.cat.isSome = true

structure CCG.Homomorphism.DirectArchitecture : Type

CCG has direct lexicon-to-meaning architecture.

• lexMeaning : LexEntry → Option (Semantics.Montague.toyModel.interpTy (catToTy NP) ⊕ Semantics.Montague.toyModel.interpTy (catToTy IV) ⊕ Semantics.Montague.toyModel.interpTy (catToTy TV))
• derivMeaning : DerivStep → Option (Interp Semantics.Montague.toyModel)
• directness (d : DerivStep) : self.derivMeaning d = d.interp toySemLexicon