Kay and Michaelis (2019): Constructional Meaning and Compositionality

This file formalizes the two formal claims of Kay and Michaelis's survey chapter. First, rules of semantic combination are construction-relative: a construction specifies how the semantics of the daughters combine into the semantics of the mother and what the construction itself adds (Sections 1 and 4). CompositionRule and interps give that architecture content over the licensing layer's local trees, a token's readings being whatever the syntactically matching constructions' rules produce from its daughters' readings; the chapter's opening contrast, purple plum composed by intersection and alleged thief by operator application under one syntactic configuration, falls out as two constructions sharing a typed form whose rules accept disjoint daughter denotations, so that each token gets exactly one reading (purple_plum_intersective, alleged_thief_operator). Second, the kinds of meaning a construction contributes, truth-conditional content, argument structure, conventional implicature, illocutionary force, metalinguistic comment and information flow (Sections 3 and 9), are MeaningKind, instantiated on the chapter's own cases already in the library: caused motion, let alone and the incredulity response.

References

• [KM19]
• [FKOC88]

§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 MeaningKind is a kind of meaning a construction contributes ([KM19] §3, §9).

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

@[instance_reducible]

instance KayMichaelis2019.instDecidableEqMeaningKind : DecidableEq MeaningKind

Equations

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

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

Equations

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

@[instance_reducible]

instance KayMichaelis2019.instReprMeaningKind : Repr MeaningKind

Equations

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

§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" — the CompositionRule architecture of ConstructionGrammar.Composition, instantiated below.

§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

A Den E is a denotation, either a first-order predicate or a predicate operator.

• 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) : ConstructionGrammar.CompositionRule (Den E)

The intersective rule maps two predicate daughters to 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) : ConstructionGrammar.CompositionRule (Den E)

The operator rule applies the adjective's predicate operator 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

modificationForm is the prenominal-modification form the two constructions share.

Equations

• KayMichaelis2019.modificationForm = [{ filler := ConstructionGrammar.SlotFiller.open_ UD.UPOS.ADJ }, { filler := ConstructionGrammar.SlotFiller.open_ UD.UPOS.NOUN, isHead := true }]

def KayMichaelis2019.intersectiveModification (E : Type u_1) : ConstructionGrammar.Construction (ConstructionGrammar.CompositionRule (Den E))

Intersective Adj+N modification has the intersective rule as its meaning.

Equations

• KayMichaelis2019.intersectiveModification E = { form := KayMichaelis2019.modificationForm, meaning := KayMichaelis2019.intersectiveRule E }

def KayMichaelis2019.operatorModification (E : Type u_1) : ConstructionGrammar.Construction (ConstructionGrammar.CompositionRule (Den E))

Operator Adj+N modification has the operator rule as its meaning.

Equations

• KayMichaelis2019.operatorModification E = { form := KayMichaelis2019.modificationForm, meaning := KayMichaelis2019.operatorRule E }

theorem KayMichaelis2019.same_form (E : Type u_1) : (intersectiveModification E).form = (operatorModification E).form

The two constructions share their form, one rule of syntactic formation with two semantic specifications (§1).

def KayMichaelis2019.demoCx (E : Type u_1) : List (ConstructionGrammar.Construction (ConstructionGrammar.CompositionRule (Den E)))

demoCx is the inventory of the two modification constructions.

Equations

• KayMichaelis2019.demoCx E = [KayMichaelis2019.intersectiveModification E, KayMichaelis2019.operatorModification E]

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

demoLex gives purple, plum and thief predicates and alleged an operator.

Equations

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

def KayMichaelis2019.purplePlum : PhraseStructure.Tree Unit Morphology.Word

purplePlum is purple plum, two words tagged for part of speech.

Equations

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

def KayMichaelis2019.allegedThief : PhraseStructure.Tree Unit Morphology.Word

allegedThief is alleged thief, two words tagged for part of speech.

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) : ConstructionGrammar.interps (demoCx E) (demoLex purple plum thief alleged) purplePlum = [Den.pred fun (x : E) => purple x ∧ plum x]

Purple plum has exactly one reading, the intersection, since 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) : ConstructionGrammar.interps (demoCx E) (demoLex purple plum thief alleged) allegedThief = [Den.pred (alleged thief)]

Alleged thief has exactly one reading, the operator applied to the head predicate, and no intersective one.

theorem KayMichaelis2019.alleged_thief_needs_operator_construction {E : Type u_1} (purple plum thief : E → Prop) (alleged : (E → Prop) → E → Prop) : ConstructionGrammar.interps [intersectiveModification E] (demoLex purple plum thief alleged) allegedThief = []

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 Unit × MeaningKind)

chapterCases pairs the chapter's example constructions with their kinds of meaning: 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.