Booij (2010): Construction Morphology

This file formalizes the constructional schemas of Booij's programmatic article: a complex word is a construction licensed by a schema in a hierarchical lexicon, and a schema both motivates the words stored below it and coins new ones. The deadjectival -ness schema is the abstraction over the stored nouns of the opening word set, the meet of their descriptions (nessSchema_body_eq_inf), and coining is unification: unifying carless with the schema returns carlessness (carlessness_unifies), the novel coin the schema generates over the stored nouns while relating the listed awareness (carlessness_generates, awareness_related). The English compound schemas form a hierarchy ordered by generality, the right-headed schema over the nominal schema over its four subcases (nominal_covBy_general, covBy_nominal); right-headedness is the coindexation of head and whole, shared by every schema of the family without a Right-hand Head Rule (compound_right_headed), while the AN subschema overrides the recursive-modifier default that the NN subschema inherits (compound_inheritance). Dutch -baar is the paper's demand for default inheritance: the hierarchy of the schema and its words is derived from their descriptions, the regular leesbaar inherits the schema's transitive base (leesbaar_inherits), and werkbaar, whose base the Dutch verb fragment records as intransitive, overrides it (werkbaar_overrides). Schema unification composes on- prefixation with -baar suffixation into one schema whose instances are exactly their common instances (onbaar_unifies, onbaarSchema_instantiates_iff), so onbedwingbaar is generated over the empty lexicon, with no intermediate bedwingbaar listed (onbedwingbaar_generates).

Implementation notes

• The words are the CLDF forms of Data/Forms/Booij2010.json, read as slot-indexed segments on the flat carrier by Data.Forms.Form.slots. The -ness and -baar schemas are over the two slots base and affix, and the on-V-baar schema over prefix, base and suffix, so the embedding [on [V baar]] of the paper's display is the concatenation of three slots; the two-slot -baar schema is the three-slot one read at base and suffix (baarSchema_eq_comap).
• The compound schemas are over the category tier alone, valued in PhraseStructure.Cat; the phonological variables and the semantic relation of the paper's display are not modelled.
• A defeasible specification is an attribute beside the description: the description is matched monotonically by unification, the attribute inherited by default (DefaultInheritance.inherited). A regular word stores no value of its own, since the paper counts all its information as redundant, and the exceptional word stores the transitivity of its base as the Dutch verb fragment records it.
• The holistic constructions (Malay reduplication, Romance VN compounds, the intensifying compounds, Maale nayi), the phrasal constructional idioms and the inflectional schemas are not formalized.

References

• [Boo10b]
• [Boo10a]

The deadjectival -ness schema

def Booij2010.nessSchema : ConstructionMorphology.Schema (Fin 2) (Flat String)

The schema [[x]A ness]N of (3) over the slots base and affix: the base an open variable, the affix pinned to -ness.

Equations

• Booij2010.nessSchema = ConstructionMorphology.Schema.productive ![⊥, ↑"ness"]

def Booij2010.nessLexicon : Set (Fin 2 → Flat String)

The stored nouns in -ness: the opening word set (1b) and awareness (2).

Equations

• Booij2010.nessLexicon = {Booij2010.Forms.baldness.slots, Booij2010.Forms.bigness.slots, Booij2010.Forms.blackness.slots, Booij2010.Forms.britishness.slots, Booij2010.Forms.awareness.slots}

theorem Booij2010.nessSchema_body_eq_inf : nessSchema.body = Forms.baldness.slots ⊓ Forms.bigness.slots ⊓ Forms.blackness.slots ⊓ Forms.britishness.slots

The schema is the abstraction over the stored nouns of (1b): the meet of their descriptions keeps the shared affix and leaves a variable where the bases differ.

theorem Booij2010.ness_instantiates {w : Fin 2 → Flat String} (h : w 1 = ↑"ness") : nessSchema.Instantiates w

Any word whose affix is -ness instantiates the schema.

theorem Booij2010.carlessness_instantiates : nessSchema.Instantiates Forms.carlessness.slots

theorem Booij2010.carlessness_unifies : PartialUnify.unify nessSchema.body Forms.carlessness.slots = ↑Forms.carlessness.slots

Coining is unification: unifying the adjective carless with the schema returns the construct carlessness.

theorem Booij2010.nessSchema_isProductive : nessSchema.IsProductive

theorem Booij2010.carlessness_generates : nessSchema.Generates nessLexicon Forms.carlessness.slots

The schema's generative role: it coins the novel carlessness over the stored nouns, its open base taking an unlisted adjective.

theorem Booij2010.awareness_related : nessSchema.Relates nessLexicon Forms.awareness.slots

The schema's relational role: it motivates the listed awareness.

The compound hierarchy

The right-headed schema for all English compounds dominates the nominal schema (6), which dominates the NN, VN, AN and PN subcases (7). The hierarchy is derived from the schemas by generality, and each schema is read at the positions modifier, head and whole through one subscripting, which coindexes the head with the whole.

inductive Booij2010.CompoundVar : Type

The category variables of a compound schema: the modifier's X and the head's Y.

• x : CompoundVar
• y : CompoundVar

@[instance_reducible]

instance Booij2010.instDecidableEqCompoundVar : DecidableEq CompoundVar

Equations

• Booij2010.instDecidableEqCompoundVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Booij2010.instFintypeCompoundVar : Fintype CompoundVar

Equations

• Booij2010.instFintypeCompoundVar = { elems := { val := ↑Booij2010.CompoundVar.enumList, nodup := Booij2010.CompoundVar.enumList_nodup }, complete := Booij2010.instFintypeCompoundVar._proof_1 }

def Booij2010.compoundSub : Fin 3 → CompoundVar

The positions modifier, head and whole, subscripted as in (6): the whole shares the head's category.

Equations

• Booij2010.compoundSub = ![Booij2010.CompoundVar.x, Booij2010.CompoundVar.y, Booij2010.CompoundVar.y]

def Booij2010.compoundSchema (x y : Flat PhraseStructure.Cat) : ConstructionMorphology.Schema CompoundVar (Flat PhraseStructure.Cat)

The compound schema with the modifier's category x and the head's y, each a variable at ⊥.

Equations

• Booij2010.compoundSchema x y = ConstructionMorphology.Schema.productive fun (x_1 : Booij2010.CompoundVar) => match x_1 with | Booij2010.CompoundVar.x => x | Booij2010.CompoundVar.y => y

inductive Booij2010.CompoundNode : Type

The nodes of the hierarchy: the right-headed schema for all compounds, the nominal schema (6) and its four subcases (7).

• general : CompoundNode
• nominal : CompoundNode
• nn : CompoundNode
• vn : CompoundNode
• an : CompoundNode
• pn : CompoundNode

@[instance_reducible]

instance Booij2010.instDecidableEqCompoundNode : DecidableEq CompoundNode

Equations

• Booij2010.instDecidableEqCompoundNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Booij2010.instFintypeCompoundNode : Fintype CompoundNode

Equations

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

def Booij2010.compoundFamily : CompoundNode → ConstructionMorphology.Schema CompoundVar (Flat PhraseStructure.Cat)

The schema at each node: the general schema leaves both categories open, the nominal schema pins the head to N, and a subcase pins the modifier too.

Equations

• Booij2010.compoundFamily Booij2010.CompoundNode.general = Booij2010.compoundSchema ⊥ ⊥
• Booij2010.compoundFamily Booij2010.CompoundNode.nominal = Booij2010.compoundSchema ⊥ ↑PhraseStructure.Cat.N
• Booij2010.compoundFamily Booij2010.CompoundNode.nn = Booij2010.compoundSchema ↑PhraseStructure.Cat.N ↑PhraseStructure.Cat.N
• Booij2010.compoundFamily Booij2010.CompoundNode.vn = Booij2010.compoundSchema ↑PhraseStructure.Cat.V ↑PhraseStructure.Cat.N
• Booij2010.compoundFamily Booij2010.CompoundNode.an = Booij2010.compoundSchema ↑PhraseStructure.Cat.Adj ↑PhraseStructure.Cat.N
• Booij2010.compoundFamily Booij2010.CompoundNode.pn = Booij2010.compoundSchema ↑PhraseStructure.Cat.P ↑PhraseStructure.Cat.N

@[instance_reducible]

instance Booij2010.instPartialOrderCompoundNode : PartialOrder CompoundNode

The hierarchical lexicon of English compounds, ordered by the generality of the schemas.

Equations

• Booij2010.instPartialOrderCompoundNode = ConstructionMorphology.Schema.generalityOrder Booij2010.compoundFamily Booij2010.instPartialOrderCompoundNode._proof_1

@[instance_reducible]

instance Booij2010.instDecidableLECompoundNode : DecidableLE CompoundNode

Equations

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

@[instance_reducible]

instance Booij2010.instDecidableLTCompoundNode : DecidableLT CompoundNode

Equations

• Booij2010.instDecidableLTCompoundNode = decidableLTOfDecidableLE

theorem Booij2010.nominal_covBy_general : CompoundNode.nominal ⋖ CompoundNode.general

The nominal schema (6) lies immediately below the general right-headed schema.

theorem Booij2010.covBy_nominal (n : CompoundNode) : n ≠ CompoundNode.general → n ≠ CompoundNode.nominal → n ⋖ CompoundNode.nominal

Each subcase of (7) lies immediately below the nominal schema (6).

theorem Booij2010.compound_right_headed (n : CompoundNode) {w : Fin 3 → Flat PhraseStructure.Cat} (h : (compoundFamily n).InstantiatesAt compoundSub w) : w 2 = w 1

Right-headedness needs no rule: in any instance of any schema of the family read through the subscripting of (6), the whole's category is the head's.

theorem Booij2010.blackbird_instantiatesAt : (compoundFamily CompoundNode.an).InstantiatesAt compoundSub ![↑PhraseStructure.Cat.Adj, ↑PhraseStructure.Cat.N, ↑PhraseStructure.Cat.N] ∧ ¬(compoundFamily CompoundNode.nn).InstantiatesAt compoundSub ![↑PhraseStructure.Cat.Adj, ↑PhraseStructure.Cat.N, ↑PhraseStructure.Cat.N]

blackbird, an adjective and a noun making a noun, instantiates the AN subschema and not the NN subschema.

def Booij2010.recursiveModifier : CompoundNode → Option Bool

Whether the modifier may itself be a compound (8): allowed by the general schema, forbidden at the AN subschema.

Equations

• Booij2010.recursiveModifier Booij2010.CompoundNode.general = some true
• Booij2010.recursiveModifier Booij2010.CompoundNode.an = some false
• Booij2010.recursiveModifier x✝ = none

theorem Booij2010.compound_inheritance : DefaultInheritance.inherited recursiveModifier CompoundNode.nn = {true} ∧ DefaultInheritance.inherited recursiveModifier CompoundNode.an = {false}

The NN subschema inherits the recursive modifier through the nominal schema, and the AN subschema overrides it.

Default inheritance: -baar and werkbaar

The suffix -baar attaches to transitive verbs, leesbaar from lezen, yet werkbaar is formed on the intransitive werken. The words lie below the schema in the hierarchy because they instantiate it, and the transitivity of the base is a defeasible specification that the exceptional word overrides.

inductive Booij2010.BaarNode : Type

The nodes of the -baar hierarchy: the schema [V baar]A, the regular leesbaar and the exceptional werkbaar.

• schema : BaarNode
• leesbaar : BaarNode
• werkbaar : BaarNode

@[instance_reducible]

instance Booij2010.instDecidableEqBaarNode : DecidableEq BaarNode

Equations

• Booij2010.instDecidableEqBaarNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Booij2010.instFintypeBaarNode : Fintype BaarNode

Equations

• Booij2010.instFintypeBaarNode = { elems := { val := ↑Booij2010.BaarNode.enumList, nodup := Booij2010.BaarNode.enumList_nodup }, complete := Booij2010.instFintypeBaarNode._proof_1 }

def Booij2010.baarSchema : ConstructionMorphology.Schema (Fin 2) (Flat String)

The -baar schema over the slots base and affix, the base open.

Equations

• Booij2010.baarSchema = ConstructionMorphology.Schema.productive ![⊥, ↑"baar"]

def Booij2010.baarFamily : BaarNode → ConstructionMorphology.Schema (Fin 2) (Flat String)

The description at each node: the schema, or a word with no variable.

Equations

• Booij2010.baarFamily Booij2010.BaarNode.schema = Booij2010.baarSchema
• Booij2010.baarFamily Booij2010.BaarNode.leesbaar = { body := Booij2010.Forms.leesbaar.slots, opens := ∅ }
• Booij2010.baarFamily Booij2010.BaarNode.werkbaar = { body := Booij2010.Forms.werkbaar.slots, opens := ∅ }

@[instance_reducible]

instance Booij2010.instPartialOrderBaarNode : PartialOrder BaarNode

The -baar hierarchy, ordered by the generality of the descriptions.

Equations

• Booij2010.instPartialOrderBaarNode = ConstructionMorphology.Schema.generalityOrder Booij2010.baarFamily Booij2010.instPartialOrderBaarNode._proof_1

@[instance_reducible]

instance Booij2010.instDecidableLEBaarNode : DecidableLE BaarNode

Equations

• Booij2010.instDecidableLEBaarNode a b = { decide := decide (∀ (i : Fin 2), (Booij2010.baarFamily b).body i ≤ (Booij2010.baarFamily a).body i), reflects_decide := ⋯ }

theorem Booij2010.le_schema (n : BaarNode) : n ≤ BaarNode.schema

Both words instantiate the schema, so the schema dominates them.

def Booij2010.baseTransitive : BaarNode → Option Bool

Whether the base verb is transitive: the schema's default is transitive, the regular leesbaar stores nothing, and werkbaar stores the transitivity of werken as the Dutch verb fragment records its basic frame.

Equations

• Booij2010.baseTransitive Booij2010.BaarNode.schema = some true
• Booij2010.baseTransitive Booij2010.BaarNode.leesbaar = none
• Booij2010.baseTransitive Booij2010.BaarNode.werkbaar = Option.map (fun (fr : ArgumentFrame) => decide fr.IsTransitive) Dutch.Verbs.werken.valency.frames.head?

theorem Booij2010.leesbaar_inherits : DefaultInheritance.inherited baseTransitive BaarNode.leesbaar = {true}

The regular word inherits the schema's transitive base.

theorem Booij2010.werkbaar_overrides : DefaultInheritance.inherited baseTransitive BaarNode.werkbaar = {false}

The exceptional word overrides the inherited transitivity of its base.

theorem Booij2010.lezen_isTransitive : ∃ fr ∈ Dutch.Verbs.lezen.valency.frames, fr.IsTransitive

The default fits the regular word: the fragment's lezen is transitive.

Schema unification: on- with -baar

Negative on- prefixation and deverbal -baar suffixation unify into one schema [on [V baar]A]A (16), so onbedwingbaar is coined directly from the verb without the intermediate bedwingbaar being listed. The unification is over the three slots prefix, base and suffix.

def Booij2010.onSchema : ConstructionMorphology.Schema (Fin 3) (Flat String)

The on- schema [on A]A over prefix, base and suffix: the prefix pinned, the rest open.

Equations

• Booij2010.onSchema = ConstructionMorphology.Schema.productive ![↑"on", ⊥, ⊥]

def Booij2010.baarSchema₃ : ConstructionMorphology.Schema (Fin 3) (Flat String)

The -baar schema over prefix, base and suffix: the suffix pinned, the rest open.

Equations

• Booij2010.baarSchema₃ = ConstructionMorphology.Schema.productive ![⊥, ⊥, ↑"baar"]

def Booij2010.onbaarSchema : ConstructionMorphology.Schema (Fin 3) (Flat String)

The unified schema [on [V baar]A]A: both affixes pinned, the base open.

Equations

• Booij2010.onbaarSchema = ConstructionMorphology.Schema.productive ![↑"on", ⊥, ↑"baar"]

theorem Booij2010.baarSchema_eq_comap : baarSchema₃.comap ![1, 2] = baarSchema

The two-slot -baar schema of the hierarchy is the three-slot one read at base and suffix.

theorem Booij2010.onbaar_unifies : PartialUnify.unify onSchema.body baarSchema₃.body = ↑onbaarSchema.body

The on- and -baar descriptions unify into the on-V-baar description (16).

theorem Booij2010.onbaarSchema_instantiates_iff {w : Fin 3 → Flat String} : onbaarSchema.Instantiates w ↔ onSchema.Instantiates w ∧ baarSchema₃.Instantiates w

The unified schema's instances are exactly the words at once on- prefixed and -baar suffixed.

theorem Booij2010.onbedwingbaar_generates : onbaarSchema.Generates ∅ Forms.onbedwingbaar.slots

The unified schema coins onbedwingbaar over the empty lexicon: no intermediate bedwingbaar need be listed.