[KM19]: Constructional Meaning and Compositionality

The survey chapter's two formal claims. First (§1, §4): 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". CompositionRule and Constructicon.interps give that architecture computational content over the licensing layer's local trees: a token's readings are whatever the syntactically matching constructions' rules produce from its daughters' readings. The chapter's opening contrast — purple plum composes by intersection, alleged thief by operator application, under one syntactic configuration — falls out as two constructions sharing a TypedForm whose rules accept disjoint daughter-denotation shapes, so each token gets exactly one reading.

Second (§3): the kinds of meaning constructions contribute — truth-conditional content, argument structure, conventional implicature, special illocutionary forces, metalinguistic comments, information flow (§9) — as MeaningKind, instantiated on the chapter's own cases already in the library (caused motion §5, let alone §6, the incredulity type §7).

Main declarations

• KayMichaelis2019.MeaningKind: §3's classification (+ §9)
• KayMichaelis2019.CompositionRule, Constructicon.interps: §4's daughters-to-mother composition, all readings of a token
• KayMichaelis2019.purple_plum_intersective, alleged_thief_operator, same_form: the §1 contrast
• KayMichaelis2019.chapterCases: §§5–7 instantiated

§3: kinds of constructional meaning

The chapter's classification, offered as "neither definitive nor exhaustive"; informationFlow is §9's strand.

inductive KayMichaelis2019.MeaningKind : Type

A kind of meaning contributed by a construction ([KM19] §3, §9).

• literal : MeaningKind
• argumentStructure : MeaningKind
• conventionalImplicature : MeaningKind
• illocutionaryForce : MeaningKind
• metalinguistic : MeaningKind
• informationFlow : MeaningKind

@[implicit_reducible]

instance KayMichaelis2019.instDecidableEqMeaningKind : DecidableEq MeaningKind

Equations

• KayMichaelis2019.instDecidableEqMeaningKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KayMichaelis2019.instReprMeaningKind : Repr MeaningKind

Equations

• KayMichaelis2019.instReprMeaningKind = { reprPrec := KayMichaelis2019.instReprMeaningKind.repr }

def KayMichaelis2019.instReprMeaningKind.repr : MeaningKind → ℕ → Std.Format

Equations

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

§4: construction-relative composition

"The construction also 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."

@[reducible, inline]

abbrev KayMichaelis2019.CompositionRule (D : Type u_1) : Type u_1

A composition rule: from the daughters' denotations to the mother's, partial because a rule demands daughter denotations of the right shape.

Equations

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

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

All readings of a token: each construction whose typed form the daughters instantiate contributes the readings 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 rules lex (ConstructionGrammar.Token.word w) = (lex w).toList

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

All sequences of daughter readings.

Equations

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

§1: purple plum vs. alleged thief

"A purple plum is a member of the set of purple things and a member of the set of plums. But an alleged thief is not a member of the intersection of the set of thieves and the set of alleged things." Two modification constructions share one syntactic form; their rules accept disjoint daughter shapes, so each token composes exactly one way.

inductive KayMichaelis2019.Den (E : Type u_1) : Type u_1

Demo denotations: first-order predicates and predicate operators.

• pred {E : Type u_1} : (E → Prop) → Den E
• op {E : Type u_1} : ((E → Prop) → E → Prop) → Den E

def KayMichaelis2019.intersectiveRule (E : Type u_1) : CompositionRule (Den E)

Intersective modification: both daughters denote predicates; the mother denotes their intersection (purple plum).

Equations

• KayMichaelis2019.intersectiveRule E [KayMichaelis2019.Den.pred a, KayMichaelis2019.Den.pred n] = some (KayMichaelis2019.Den.pred fun (x : E) => a x ∧ n x)
• KayMichaelis2019.intersectiveRule E x✝ = none

def KayMichaelis2019.operatorRule (E : Type u_1) : CompositionRule (Den E)

Operator modification: the adjective denotes a predicate operator applied to the head's predicate (alleged thief).

Equations

• KayMichaelis2019.operatorRule E [KayMichaelis2019.Den.op f, KayMichaelis2019.Den.pred n] = some (KayMichaelis2019.Den.pred (f n))
• KayMichaelis2019.operatorRule E x✝ = none

def KayMichaelis2019.modificationForm : ConstructionGrammar.TypedForm String

The shared prenominal-modification form.

Equations

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

def KayMichaelis2019.intersectiveModification : ConstructionGrammar.Construction

Intersective Adj+N modification.

Equations

• KayMichaelis2019.intersectiveModification = { name := "Intersective modification", form := KayMichaelis2019.modificationForm, meaning := "x is Adj and x is N" }

def KayMichaelis2019.operatorModification : ConstructionGrammar.Construction

Operator Adj+N modification.

Equations

• KayMichaelis2019.operatorModification = { name := "Operator modification", form := KayMichaelis2019.modificationForm, meaning := "x satisfies Adj applied to N" }

theorem KayMichaelis2019.same_form : intersectiveModification.form = operatorModification.form

§1's premise: one rule of syntactic formation, two semantic specifications — the constructions share their typed form.

def KayMichaelis2019.demoCx : ConstructionGrammar.Constructicon

The demo network: both modification constructions.

Equations

• KayMichaelis2019.demoCx = { constructions := [KayMichaelis2019.intersectiveModification, KayMichaelis2019.operatorModification], links := [] }

def KayMichaelis2019.demoPos : String → Option UD.UPOS

Toy POS lexicon.

Equations

• KayMichaelis2019.demoPos "purple" = some UD.UPOS.ADJ
• KayMichaelis2019.demoPos "alleged" = some UD.UPOS.ADJ
• KayMichaelis2019.demoPos "plum" = some UD.UPOS.NOUN
• KayMichaelis2019.demoPos "thief" = some UD.UPOS.NOUN
• KayMichaelis2019.demoPos x✝ = none

def KayMichaelis2019.demoLex {E : Type u_1} (purple plum thief : E → Prop) (alleged : (E → Prop) → E → Prop) : String → Option (Den E)

Toy denotation lexicon: purple is a predicate, alleged an operator.

Equations

• KayMichaelis2019.demoLex purple plum thief alleged "purple" = some (KayMichaelis2019.Den.pred purple)
• KayMichaelis2019.demoLex purple plum thief alleged "alleged" = some (KayMichaelis2019.Den.op alleged)
• KayMichaelis2019.demoLex purple plum thief alleged "plum" = some (KayMichaelis2019.Den.pred plum)
• KayMichaelis2019.demoLex purple plum thief alleged "thief" = some (KayMichaelis2019.Den.pred thief)
• KayMichaelis2019.demoLex purple plum thief alleged x✝ = none

def KayMichaelis2019.demoRules {E : Type u_1} : ConstructionGrammar.Construction → Option (CompositionRule (Den E))

Rule assignment for the demo network.

Equations

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

theorem KayMichaelis2019.purple_plum_intersective {E : Type u_1} (purple plum thief : E → Prop) (alleged : (E → Prop) → E → Prop) : demoCx.interps demoPos demoRules (demoLex purple plum thief alleged) (ConstructionGrammar.Token.node [ConstructionGrammar.Token.word "purple", ConstructionGrammar.Token.word "plum"]) = [Den.pred fun (x : E) => purple x ∧ plum x]

Purple plum has exactly one reading: the intersection. The operator construction matches the form but its rule rejects two predicate daughters.

theorem KayMichaelis2019.alleged_thief_operator {E : Type u_1} (purple plum thief : E → Prop) (alleged : (E → Prop) → E → Prop) : demoCx.interps demoPos demoRules (demoLex purple plum thief alleged) (ConstructionGrammar.Token.node [ConstructionGrammar.Token.word "alleged", ConstructionGrammar.Token.word "thief"]) = [Den.pred (alleged thief)]

Alleged thief has exactly one reading: the operator applied to the head predicate — not an intersection.

theorem KayMichaelis2019.alleged_thief_needs_operator_construction {E : Type u_1} (purple plum thief : E → Prop) (alleged : (E → Prop) → E → Prop) : { constructions := [intersectiveModification], links := [] }.interps demoPos demoRules (demoLex purple plum thief alleged) (ConstructionGrammar.Token.node [ConstructionGrammar.Token.word "alleged", ConstructionGrammar.Token.word "thief"]) = []

With only the intersective construction, alleged thief has no reading at all: the chapter's point that intersection cannot be the single rule of adjectival modification.

§§5–7 instantiated

The chapter's cases that the library already formalizes, with the kind of meaning each contributes.

def KayMichaelis2019.chapterCases : List (ConstructionGrammar.Construction × MeaningKind)

The chapter's example constructions by meaning kind: caused motion (§5, exx. 19–22, Frank sneezed the tissue off the table), let alone (§6, ex. 32), and the incredulity type (§7, ex. 14, Him get first prize?!).

Equations

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