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

Type assignment maps syntactic categories to semantic types

• typeOf : SynCat → Ty

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

Compositional semantics maps derivations to meanings

• types : TypeAssignment SynCat
• model : Model
• interp : Deriv → (cat : SynCat) → (model SynCat Deriv).interpTy ((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 → Ty
• wellFormed : Deriv → Prop
• interp (d : Deriv) (m : Model) : m.interpTy (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 → Model → Bool
• entails : Deriv → Deriv → Model → Bool