structure Semantics.Montague.Interface.SyntaxInterface.TypeAssignment (SynCat : Type) : Type

Type assignment maps syntactic categories to semantic types

• typeOf : SynCat → Core.Logic.Intensional.Ty

class Semantics.Montague.Interface.SyntaxInterface.CompositionalSemantics (SynCat Deriv : Type) : Type 1

Compositional semantics maps derivations to meanings

• types : TypeAssignment SynCat
• frame : Core.Logic.Intensional.Frame
• interp : Deriv → (cat : SynCat) → (frame SynCat Deriv).Denot ((types Deriv).typeOf cat)

class Semantics.Montague.Interface.SyntaxInterface.MontagueSyntax (SynCat Deriv : Type) : Type 1

Requirements for a syntax to interface with Montague semantics

• catOf : Deriv → SynCat
• typeOf : SynCat → Core.Logic.Intensional.Ty
• wellFormed : Deriv → Prop
• interp (d : Deriv) (F : Core.Logic.Intensional.Frame) : F.Denot (typeOf Deriv (catOf d))

structure Semantics.Montague.Interface.SyntaxInterface.MontagueBenefits (SynCat Deriv : Type) [MontagueSyntax SynCat Deriv] : Type 1

Results that Montague provides to any compatible syntax

• trueIn : Deriv → Core.Logic.Intensional.Frame → Bool
• entails : Deriv → Deriv → Core.Logic.Intensional.Frame → Bool