def CCG.Interpret.getWords : DerivStep → List String

Get all words (surface forms) from a derivation, left to right

Equations

• CCG.Interpret.getWords (CCG.DerivStep.lex entry) = [entry.form]
• CCG.Interpret.getWords (d1.fapp d2) = CCG.Interpret.getWords d1 ++ CCG.Interpret.getWords d2
• CCG.Interpret.getWords (d1.bapp d2) = CCG.Interpret.getWords d1 ++ CCG.Interpret.getWords d2
• CCG.Interpret.getWords (d1.fcomp d2) = CCG.Interpret.getWords d1 ++ CCG.Interpret.getWords d2
• CCG.Interpret.getWords (d1.bcomp d2) = CCG.Interpret.getWords d1 ++ CCG.Interpret.getWords d2
• CCG.Interpret.getWords (d.ftr a) = CCG.Interpret.getWords d
• CCG.Interpret.getWords (d.btr a) = CCG.Interpret.getWords d
• CCG.Interpret.getWords (d1.coord d2) = CCG.Interpret.getWords d1 ++ ["and"] ++ CCG.Interpret.getWords d2

def CCG.Interpret.getScalarEntry (form : String) : Option (Semantics.Montague.SemLexEntry Semantics.Montague.toyModel)

Check if a word form is a scalar item and return its lexical entry

Equations

• CCG.Interpret.getScalarEntry form = match Semantics.Montague.toyLexicon form with | some entry => if entry.isScalar = true then some entry else none | none => none

def CCG.Interpret.findScalarsHelper (words : List String) (pos : ℕ) : List (Semantics.Montague.Derivation.ScalarOccurrence Semantics.Montague.toyModel)

Helper to find scalar items with positions

Equations

• One or more equations did not get rendered due to their size.
• CCG.Interpret.findScalarsHelper [] pos = []

def CCG.Interpret.findScalarItems (d : DerivStep) : List (Semantics.Montague.Derivation.ScalarOccurrence Semantics.Montague.toyModel)

Find all scalar items in a derivation with their positions

Equations

• CCG.Interpret.findScalarItems d = CCG.Interpret.findScalarsHelper (CCG.Interpret.getWords d) 0

def CCG.Interpret.toDerivation (d : DerivStep) (ty : Semantics.Montague.Ty) (meaning : Semantics.Montague.toyModel.interpTy ty) : Semantics.Montague.Derivation.Derivation Semantics.Montague.toyModel

Convert a CCG derivation to a Montague semantic derivation.

Note: For a full implementation, we'd need to compositionally compute the meaning from the derivation tree. For now, we provide the structure and a placeholder for the meaning (requiring it to be provided separately).

Equations

• CCG.Interpret.toDerivation d ty meaning = { surface := CCG.Interpret.getWords d, ty := ty, meaning := meaning, scalarItems := CCG.Interpret.findScalarItems d }

def CCG.Interpret.ccg_john_sleeps : DerivStep

CCG derivation for "John sleeps"

Equations

• CCG.Interpret.ccg_john_sleeps = (CCG.DerivStep.lex { form := "John", cat := CCG.NP }).bapp (CCG.DerivStep.lex { form := "sleeps", cat := CCG.IV })

def CCG.Interpret.john_sleeps_sem : Semantics.Montague.Derivation.Derivation Semantics.Montague.toyModel

Convert to semantic derivation

Equations

• CCG.Interpret.john_sleeps_sem = CCG.Interpret.toDerivation CCG.Interpret.ccg_john_sleeps Semantics.Montague.Ty.t (Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyEntity.john)

def CCG.Interpret.ccg_some_student_sleeps : DerivStep

CCG derivation for "some student sleeps"

Equations

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

def CCG.Interpret.some_student_sleeps_sem : Semantics.Montague.Derivation.Derivation Semantics.Montague.toyModel

Convert to semantic derivation with scalar item

Equations

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