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 daughter and reconciliation operator
• interps: all readings of a tree, through the forms its constituents instantiate

References

• [KM19]
• [Mic04]

@[reducible, inline]

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

A composition rule maps the daughters' denotations to the mother's, partially, 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

The readings follow the override principle ([Mic04], (20)), "if a lexical item is semantically incompatible with its morphosyntactic context, the meaning of the lexical item conforms to the meaning of the structure in which it is embedded". They are the rule's own output where the daughters already conform, and otherwise one reading for each daughter and reconciliation operator that makes the daughters conform when applied to that daughter alone. Distinct repairs produce genuine ambiguity.

Equations

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

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, since implicit type-shifting occurs only on mismatch ([Mic04], (20)).

@[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.interps {D : Type u_1} (cxns : List (Construction (CompositionRule D))) (den : Morphology.Word → Option D) : PhraseStructure.Tree Unit Morphology.Word → List D

In the readings of a tree, each construction whose typed form the daughters instantiate contributes the readings its meaning pole, a composition rule, produces from the daughters' readings; words read their denotations den.

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.interps cxns den (RoseTree.node (PhraseStructure.Tree.Label.terminal a w) []) = (den w).toList
• ConstructionGrammar.interps cxns den x✝ = []

def ConstructionGrammar.interpsList {D : Type u_1} (cxns : List (Construction (CompositionRule D))) (den : Morphology.Word → Option D) : List (PhraseStructure.Tree Unit Morphology.Word) → List (List D)

All sequences of daughter readings.

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.interpsList cxns den [] = [[]]