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

Well-typed CCG derivation with category and meaning.

• deriv : DerivStep
• cat : Cat
• catOk : self.deriv.cat = some self.cat
• meaning : F.Denot (catToTy self.cat)

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

Category paired with semantic denotation.

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

theorem CCG.Homomorphism.fapp_sem {F : Core.Logic.Intensional.Frame} {x y : Cat} (f_sem : F.Denot (catToTy (x.rslash y))) (a_sem : F.Denot (catToTy y)) : ∃ (result : F.Denot (catToTy x)), result = f_sem a_sem

Forward application is semantic function application.

def CCG.Homomorphism.fappSem {F : Core.Logic.Intensional.Frame} {x y : Cat} (f_sem : F.Denot (catToTy (x.rslash y))) (a_sem : F.Denot (catToTy y)) : F.Denot (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 {F : Core.Logic.Intensional.Frame} {x y : Cat} (a_sem : F.Denot (catToTy y)) (f_sem : F.Denot (catToTy (x.lslash y))) : ∃ (result : F.Denot (catToTy x)), result = f_sem a_sem

Backward application is semantic function application.

def CCG.Homomorphism.bappSem {F : Core.Logic.Intensional.Frame} {x y : Cat} (a_sem : F.Denot (catToTy y)) (f_sem : F.Denot (catToTy (x.lslash y))) : F.Denot (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 {F : Core.Logic.Intensional.Frame} {x y z : Cat} (f_sem : F.Denot (catToTy (x.rslash y))) (g_sem : F.Denot (catToTy (y.rslash z))) : ∃ (result : F.Denot (catToTy (x.rslash z))), result = Combinators.B f_sem g_sem

Forward composition is the B combinator.

def CCG.Homomorphism.fcompSem {F : Core.Logic.Intensional.Frame} {x y z : Cat} (f_sem : F.Denot (catToTy (x.rslash y))) (g_sem : F.Denot (catToTy (y.rslash z))) : F.Denot (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 {F : Core.Logic.Intensional.Frame} {x t : Cat} (a_sem : F.Denot (catToTy x)) : ∃ (result : F.Denot (catToTy (forwardTypeRaise x t))), ∀ (f : F.Denot (catToTy (t.lslash x))), result f = f a_sem

Forward type-raising is the T combinator.

def CCG.Homomorphism.ftrSem {F : Core.Logic.Intensional.Frame} {x t : Cat} (a_sem : F.Denot (catToTy x)) : F.Denot (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 {F : Core.Logic.Intensional.Frame} {x y : Cat} (f : F.Denot (catToTy (x.rslash y))) (a : F.Denot (catToTy y)) : fappSem f a = f a
• bapp {F : Core.Logic.Intensional.Frame} {x y : Cat} (a : F.Denot (catToTy y)) (f : F.Denot (catToTy (x.lslash y))) : bappSem a f = f a
• fcomp {F : Core.Logic.Intensional.Frame} {x y z : Cat} (f : F.Denot (catToTy (x.rslash y))) (g : F.Denot (catToTy (y.rslash z))) : fcompSem f g = Combinators.B f g
• ftr {F : Core.Logic.Intensional.Frame} {x t : Cat} (a : F.Denot (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 {F : Core.Logic.Intensional.Frame} {x y : Cat} (f : F.Denot (catToTy (x.rslash y))) (a : F.Denot (catToTy y)) : ∃! result : F.Denot (catToTy x), result = f a
• bapp_rule {F : Core.Logic.Intensional.Frame} {x y : Cat} (a : F.Denot (catToTy y)) (f : F.Denot (catToTy (x.lslash y))) : ∃! result : F.Denot (catToTy x), result = f a
• comp_rule {F : Core.Logic.Intensional.Frame} {x y z : Cat} (f : F.Denot (catToTy (x.rslash y))) (g : F.Denot (catToTy (y.rslash z))) : ∃! result : F.Denot (catToTy (x.rslash z)), ∀ (arg : F.Denot (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.Denot (catToTy NP) ⊕ Semantics.Montague.toyModel.Denot (catToTy IV) ⊕ Semantics.Montague.toyModel.Denot (catToTy TV))
• derivMeaning : DerivStep → Option (Interp Semantics.Montague.toyModel)
• directness (d : DerivStep) : self.derivMeaning d = d.interp toySemLexicon