Construction-relative composition

Rules of semantic combination are construction-relative: a construction "specifies how the semantics of the daughters are combined to produce the semantics of the mother, and what additional semantics, if any, is contributed by the construction itself" ([KM19] §4). A composition rule is partial — it demands daughter denotations of the right shape — and mismatches are repaired by the override principle ([Mic04], (20)): the lexical item conforms to the meaning of the structure in which it is embedded.

Main definitions

• CompositionRule: from the daughters' denotations to the mother's
• CompositionRule.override: readings under the override principle, one per reconciliation operator
• Constructicon.interps: all readings of a token, through the licensing recognizer

@[reducible, inline]

abbrev ConstructionGrammar.CompositionRule (D : Type u_2) : Type u_2

A composition rule: from the daughters' denotations to the mother's, partial because a rule demands daughter denotations of the right shape ([KM19] §4).

Equations

• ConstructionGrammar.CompositionRule D = (List D → Option D)

def ConstructionGrammar.CompositionRule.override {D : Type u_1} [DecidableEq D] (r : CompositionRule D) (shifts : List (D → D)) (ds : List D) : List D

Readings under the override principle ([Mic04], (20)): the rule's own output where the daughters already conform, and otherwise one reading per reconciliation operator that makes them conform. Distinct operators yielding distinct repairs produce genuine ambiguity.

Equations

• r.override shifts ds = match r ds with | some d => [d] | none => (List.filterMap (fun (s : D → D) => r (List.map s ds)) shifts).dedup

theorem ConstructionGrammar.CompositionRule.override_eq_of_eq_some {D : Type u_1} [DecidableEq D] {r : CompositionRule D} {ds : List D} {d : D} (shifts : List (D → D)) (h : r ds = some d) : r.override shifts ds = [d]

Conforming daughters are composed directly: implicit type-shifting occurs only on mismatch ([Mic04], Table 3).

@[simp]

theorem ConstructionGrammar.CompositionRule.override_nil {D : Type u_1} [DecidableEq D] (r : CompositionRule D) (ds : List D) : r.override [] ds = (r ds).toList

With no reconciliation operators, a mismatch has no readings.

def ConstructionGrammar.Constructicon.interps {D : Type u_2} (cx : Constructicon (CompositionRule D)) (pos : String → Option UD.UPOS) (lex : String → Option D) : Token → List D

All readings of a token: each construction whose typed form the daughters instantiate contributes the readings its meaning pole — its composition rule — produces from the daughters' readings; words read from the lexicon.

Equations

• One or more equations did not get rendered due to their size.
• cx.interps pos lex (ConstructionGrammar.Token.word w) = (lex w).toList

def ConstructionGrammar.Constructicon.interpsList {D : Type u_2} (cx : Constructicon (CompositionRule D)) (pos : String → Option UD.UPOS) (lex : String → Option D) : List Token → List (List D)

All sequences of daughter readings.

Equations

• cx.interpsList pos lex [] = [[]]
• cx.interpsList pos lex (t :: ts) = List.flatMap (fun (d : D) => List.map (fun (x : List D) => d :: x) (cx.interpsList pos lex ts)) (cx.interps pos lex t)