class Semantics.Montague.Composition.HasTerminals (S : Type) : Type

Access to lexical/terminal content.

• getTerminal : S → Option String

  Get terminal content if this is a leaf node

class Semantics.Montague.Composition.HasBinaryComposition (S : Type) : Type

Binary decomposition for Functional Application and Predicate Modification.

• getBinaryChildren : S → Option (S × S)

  Decompose into two children if this is a binary node

class Semantics.Montague.Composition.HasUnaryProjection (S : Type) : Type

Unary decomposition for H&K's Non-Branching Nodes rule.

• getUnaryChild : S → Option S

  Get single child if this is a unary node

class Semantics.Montague.Composition.HasBinding (S : Type) : Type

Binding sites for λ-abstraction.

• getBinder : S → Option (ℕ × S)

  Get binding index and body if this is a binder

class Semantics.Montague.Composition.HasSemanticType (S T : Type) : Type

Access to semantic types, parameterized over the type system T.

• getType : S → Option T

  Get the semantic type of this node

class Semantics.Montague.Composition.SemanticStructure (S T : Type) extends Semantics.Montague.Composition.HasTerminals S, Semantics.Montague.Composition.HasBinaryComposition S, Semantics.Montague.Composition.HasUnaryProjection S, Semantics.Montague.Composition.HasBinding S, Semantics.Montague.Composition.HasSemanticType S T : Type

Full semantic structure for H&K-style interpretation.

• getTerminal : S → Option String
• getBinaryChildren : S → Option (S × S)
• getUnaryChild : S → Option S
• getBinder : S → Option (ℕ × S)
• getType : S → Option T

structure Semantics.Montague.Composition.TypedDenot (m : Model) : Type

• ty : Ty
• val : m.interpTy self.ty

def Semantics.Montague.Composition.canApply (funTy argTy : Ty) : Option Ty

Equations

• Semantics.Montague.Composition.canApply (σ ⇒ τ) argTy = if σ = argTy then some τ else none
• Semantics.Montague.Composition.canApply funTy argTy = none

def Semantics.Montague.Composition.interpTerminal (m : Model) (lex : Lexicon m) (word : String) : Option (TypedDenot m)

TN: lexical lookup.

Equations

• Semantics.Montague.Composition.interpTerminal m lex word = Option.map (fun (entry : Semantics.Montague.LexEntry m) => { ty := entry.ty, val := entry.denot }) (lex word)

def Semantics.Montague.Composition.interpNonBranching {m : Model} (daughter : TypedDenot m) : TypedDenot m

NN: identity.

Equations

• Semantics.Montague.Composition.interpNonBranching daughter = daughter

def Semantics.Montague.Composition.interpFA {m : Model} {σ τ : Ty} (f : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) : m.interpTy τ

FA: ⟦β⟧(⟦γ⟧)

Equations

• Semantics.Montague.Composition.interpFA f x = f x

def Semantics.Montague.Composition.tryFA {m : Model} (d1 d2 : TypedDenot m) : Option (TypedDenot m)

Try FA in both orders.

Equations

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

def Semantics.Montague.Composition.tryPM {m : Model} (d1 d2 : TypedDenot m) : Option (TypedDenot m)

PM: combine two ⟨e,t⟩ predicates.

Equations

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

def Semantics.Montague.Composition.interpBinary {m : Model} (d1 d2 : TypedDenot m) : Option (TypedDenot m)

Binary node: try FA, then PM.

Equations

• Semantics.Montague.Composition.interpBinary d1 d2 = (Semantics.Montague.Composition.tryFA d1 d2 <|> Semantics.Montague.Composition.tryPM d1 d2)

def Semantics.Montague.Composition.interpret {S : Type} [HasTerminals S] [HasBinaryComposition S] [HasUnaryProjection S] (m : Model) (lex : Lexicon m) (interp : S → Option (TypedDenot m)) (s : S) : Option (TypedDenot m)

Generic recursive interpretation for any syntax via SemanticStructure.

Equations

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

inductive Semantics.Montague.Composition.SynTree : Type

• terminal : String → SynTree
• unary : SynTree → SynTree
• binary : SynTree → SynTree → SynTree

def Semantics.Montague.Composition.instReprSynTree.repr : SynTree → ℕ → Std.Format

Equations

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

instance Semantics.Montague.Composition.instReprSynTree : Repr SynTree

Equations

• Semantics.Montague.Composition.instReprSynTree = { reprPrec := Semantics.Montague.Composition.instReprSynTree.repr }

instance Semantics.Montague.Composition.instHasTerminalsSynTree : HasTerminals SynTree

Equations

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

instance Semantics.Montague.Composition.instHasBinaryCompositionSynTree : HasBinaryComposition SynTree

Equations

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

instance Semantics.Montague.Composition.instHasUnaryProjectionSynTree : HasUnaryProjection SynTree

Equations

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

instance Semantics.Montague.Composition.instHasBindingSynTree : HasBinding SynTree

Equations

• Semantics.Montague.Composition.instHasBindingSynTree = { getBinder := fun (x : Semantics.Montague.Composition.SynTree) => none }

instance Semantics.Montague.Composition.instHasSemanticTypeSynTreeTy : HasSemanticType SynTree Ty

Equations

• Semantics.Montague.Composition.instHasSemanticTypeSynTreeTy = { getType := fun (x : Semantics.Montague.Composition.SynTree) => none }

instance Semantics.Montague.Composition.instSemanticStructureSynTreeTy : SemanticStructure SynTree Ty

Equations

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

def Semantics.Montague.Composition.interpTree (m : Model) (lex : Lexicon m) : SynTree → Option (TypedDenot m)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Montague.Composition.interpTree m lex (Semantics.Montague.Composition.SynTree.terminal a) = Semantics.Montague.Composition.interpTerminal m lex a
• Semantics.Montague.Composition.interpTree m lex a.unary = Option.map Semantics.Montague.Composition.interpNonBranching (Semantics.Montague.Composition.interpTree m lex a)

def Semantics.Montague.Composition.isInterpretableWith {S : Type} {m : Model} (interp : S → Option (TypedDenot m)) (s : S) : Bool

Equations

• Semantics.Montague.Composition.isInterpretableWith interp s = (interp s).isSome

def Semantics.Montague.Composition.satisfiesInterpretabilityWith {S : Type} {m : Model} (interp : S → Option (TypedDenot m)) (s : S) : Prop

Equations

• Semantics.Montague.Composition.satisfiesInterpretabilityWith interp s = (Semantics.Montague.Composition.isInterpretableWith interp s = true)

def Semantics.Montague.Composition.isInterpretable (m : Model) (lex : Lexicon m) (t : SynTree) : Bool

Equations

• Semantics.Montague.Composition.isInterpretable m lex t = (Semantics.Montague.Composition.interpTree m lex t).isSome

def Semantics.Montague.Composition.satisfiesInterpretability (m : Model) (lex : Lexicon m) (t : SynTree) : Prop

Equations

• Semantics.Montague.Composition.satisfiesInterpretability m lex t = (Semantics.Montague.Composition.isInterpretable m lex t = true)

theorem Semantics.Montague.Composition.interpNonBranching_id {m : Model} (d : TypedDenot m) : interpNonBranching d = d

theorem Semantics.Montague.Composition.interpFA_type {m : Model} {σ τ : Ty} (f : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) : interpFA f x = f x

theorem Semantics.Montague.Composition.tryPM_preserves_type {m : Model} (d1 d2 : TypedDenot m) (h1 : d1.ty = (Ty.e ⇒ Ty.t)) (h2 : d2.ty = (Ty.e ⇒ Ty.t)) : ∃ (d : TypedDenot m), tryPM d1 d2 = some d ∧ d.ty = (Ty.e ⇒ Ty.t)

theorem Semantics.Montague.Composition.interpBinary_eq {m : Model} (d1 d2 : TypedDenot m) : interpBinary d1 d2 = (tryFA d1 d2).orElse fun (x : Unit) => tryPM d1 d2