Syntax–Semantics Interface: Semantic Structure

Typeclasses defining what compositional semantics needs from syntax. Parameterized over an arbitrary type system T — Semantics.Montague instantiates with Ty, but other theories can supply their own.

class Core.Interfaces.HasTerminals (S : Type) : Type

Access to lexical/terminal content.

• getTerminal : S → Option String

  Get terminal content if this is a leaf node

class Core.Interfaces.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 Core.Interfaces.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 Core.Interfaces.HasBinding (S : Type) : Type

Binding sites for λ-abstraction.

• getBinder : S → Option (Nat × S)

  Get binding index and body if this is a binder

class Core.Interfaces.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 Core.Interfaces.SemanticStructure (S T : Type) extends Core.Interfaces.HasTerminals S, Core.Interfaces.HasBinaryComposition S, Core.Interfaces.HasUnaryProjection S, Core.Interfaces.HasBinding S, Core.Interfaces.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 (Nat × S)
• getType : S → Option T

def Core.Interfaces.isTerminal {S : Type} [HasTerminals S] (s : S) : Bool

Check if a node is a terminal.

Equations

• Core.Interfaces.isTerminal s = (Core.Interfaces.HasTerminals.getTerminal s).isSome

def Core.Interfaces.isBinary {S : Type} [HasBinaryComposition S] (s : S) : Bool

Check if a node is binary-branching.

Equations

• Core.Interfaces.isBinary s = (Core.Interfaces.HasBinaryComposition.getBinaryChildren s).isSome

def Core.Interfaces.isBinder {S : Type} [HasBinding S] (s : S) : Bool

Check if a node is a binder.

Equations

• Core.Interfaces.isBinder s = (Core.Interfaces.HasBinding.getBinder s).isSome