Construction Morphology: the constructional-schema engine [booij-2010-compass]

[booij-2010-compass] analyzes complex words as constructions — pairings of form and meaning — licensed by constructional schemas in a hierarchical lexicon. This file instantiates the Morphology/ConstructionMorphology/ substrate as that CxM engine over small Flat carriers: the deadjectival -ness schema and its unification-instantiation (carless unified with the schema is carlessness), generation of a novel -ness noun, the compound hierarchy with right-headed subschemas, the default-inheritance override (werkbaar), and schema unification (on- prefixation composed with V-baar).

Main results

• carlessness_unifies — instantiation is unification of an adjective with the -ness schema ([booij-2010-compass]'s worked example)
• carlessness_generates, awareness_related — the schema's two roles on one lexicon: coining the paper's novel noun, relating its stored one
• compoundHierarchy_parent, compound_right_headed, compound_inheritance — the compound hierarchy derived from its schemas: right-headedness is the shared coindexation, inherited without a Right-hand Head Rule, while the AN subschema overrides the recursive-modifier default
• werkbaar_overrides — the CxM default-inheritance demand site: werkbaar overrides the -baar schema's transitivity default
• onbaar_unifies, onbaarSchema_instantiates_iff — two word-formation schemas unify into on-V-baar, whose instances are exactly their common instances, no listed intermediate required

The deadjectival -ness schema

The schema [[x]A ness]N of [booij-2010-compass]: a two-slot construction whose affix slot is lexically fixed as -ness and whose base slot is an open (deadjectival) variable. A concrete adjective unified into the base slot yields a -ness noun.

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

The -ness schema over the two slots of a -ness noun, base and affix: the affix slot pinned to -ness, the base slot an open deadjectival variable (⊥).

Equations

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

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

Any filling whose affix slot is -ness instantiates the schema: the base slot is open, the affix slot's constraint is met.

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

carlessness, the paper's novel coin (Time, October 5, 2009), instantiates the -ness schema.

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

Instantiation as unification: unifying the schema description with carlessness returns carlessness — [booij-2010-compass]'s worked example.

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

The stored -ness nouns of the paper's opening word set, feeding the schema's two roles.

Equations

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

theorem Booij2010.nessSchema_isProductive : nessSchema.IsProductive

The -ness schema is productive: its one variable, the base slot, is open.

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

The schema licenses the novel coin carlessness over the stored nouns: the open base slot takes the unlisted adjective, and the affix slot is a constant. Being productive, the schema generates every instance whatever is stored.

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

The relational role over the same schema: awareness is listed and instantiates it — the paper's two functions of a schema, expressing the predictable properties of existing words and coining new ones, on one schema and one lexicon.

The compound hierarchy

The compound schema (6), [[a]X [b]Y]Y, dominates the NN/VN/AN/PN subcases (7). The hierarchy is derived from the schemas, each subschema's parent being the nearest more general schema of the family. Right-headedness is the schema's coindexation of the head with the whole, so every subschema inherits it and no Right-hand Head Rule is needed. A subschema still legislates locally: an NN modifier may itself be a compound, an AN modifier may not (8).

inductive Booij2010.CompoundVar : Type

The variables of the compound schema (6): the modifier's category 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 of a compound, modifier, head and whole, subscripted by (6): the whole shares the head's category, right-headedness.

Equations

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

def Booij2010.compoundSchema : ConstructionMorphology.Schema CompoundVar (Flat String)

The general compound schema (6): both categories open.

Equations

• Booij2010.compoundSchema = { body := fun (x : Booij2010.CompoundVar) => ⊥, opens := {Booij2010.CompoundVar.x, Booij2010.CompoundVar.y} }

def Booij2010.compoundSubschema (x : String) : ConstructionMorphology.Schema CompoundVar (Flat String)

A subschema of (7): the modifier's category pinned to x, the head's to N.

Equations

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

inductive Booij2010.CompoundNode : Type

The compound schema and its four subcases.

• compound : 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 String)

The family (6) and (7).

Equations

• Booij2010.compoundFamily Booij2010.CompoundNode.compound = Booij2010.compoundSchema
• Booij2010.compoundFamily Booij2010.CompoundNode.nn = Booij2010.compoundSubschema "N"
• Booij2010.compoundFamily Booij2010.CompoundNode.vn = Booij2010.compoundSubschema "V"
• Booij2010.compoundFamily Booij2010.CompoundNode.an = Booij2010.compoundSubschema "A"
• Booij2010.compoundFamily Booij2010.CompoundNode.pn = Booij2010.compoundSubschema "P"

def Booij2010.compoundHierarchy : ConstructionMorphology.Hierarchy CompoundNode

The hierarchical constructicon of English compounds, derived from the schemas.

Equations

• Booij2010.compoundHierarchy = ConstructionMorphology.Hierarchy.ofFamily Booij2010.compoundFamily Booij2010.compoundHierarchy._proof_1

theorem Booij2010.compoundHierarchy_parent (n : CompoundNode) (hn : n ≠ CompoundNode.compound) : compoundHierarchy.parent n = some CompoundNode.compound

Each subschema's parent is the general schema.

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

Right-headedness is inherited by every subschema without a rule: in any instance of any schema of the family through the subscripting of (6), the whole's category is the head's.

def Booij2010.recursiveModifier : CompoundNode → Option Bool

Whether the modifier may itself be a compound: allowed by default, overridden at the AN subschema (8).

Equations

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

theorem Booij2010.compound_inheritance : compoundHierarchy.value recursiveModifier CompoundNode.nn = some true ∧ compoundHierarchy.value recursiveModifier CompoundNode.an = some false

The AN subschema overrides the default recursive-modifier option, which the NN subschema inherits: an NN modifier may be a compound, an AN modifier may not.

Default inheritance and override: werkbaar

[booij-2010-compass]'s own demand site for default inheritance: -baar attaches to transitive verbs, but werkbaar (from intransitive werk) overrides the inherited transitivity specification. "By default, complex words inherit the information specified in a schema, but a particular piece of information may be overruled by an individual lexical item." A minimal two-level hierarchy: the schema node and the werkbaar leaf.

inductive Booij2010.BaarNode : Type

The -baar schema node and the werkbaar lexical item.

• baarSchema : 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.baarParent : BaarNode → Option BaarNode

Equations

• Booij2010.baarParent Booij2010.BaarNode.baarSchema = none
• Booij2010.baarParent Booij2010.BaarNode.werkbaar = some Booij2010.BaarNode.baarSchema

def Booij2010.baarHierarchy : ConstructionMorphology.Hierarchy BaarNode

Equations

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

inductive Booij2010.Transitivity : Type

Transitivity of the base verb.

• trans : Transitivity
• intrans : Transitivity

@[instance_reducible]

instance Booij2010.instDecidableEqTransitivity : DecidableEq Transitivity

Equations

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

def Booij2010.baseTransitivity : BaarNode → Option Transitivity

The -baar schema requires a transitive base by default; werkbaar overrides to intransitive.

Equations

• Booij2010.baseTransitivity Booij2010.BaarNode.baarSchema = some Booij2010.Transitivity.trans
• Booij2010.baseTransitivity Booij2010.BaarNode.werkbaar = some Booij2010.Transitivity.intrans

theorem Booij2010.werkbaar_overrides : baarHierarchy.value baseTransitivity BaarNode.werkbaar = some Transitivity.intrans ∧ baarHierarchy.value baseTransitivity BaarNode.baarSchema = some Transitivity.trans

The default-override flagship: werkbaar overrides the inherited transitivity specification, while the schema keeps its default.

Schema unification: on- composed with V-baar

The two productive schemas — negative on- prefixation and deverbal -baar suffixation — unify into a single complex schema [on [V baar]A]A (16), so onbedwingbaar is coined directly from the verb without the intermediate bedwingbaar needing to be listed. The join is taken on the schema bodies over a shared slot space; the intermediate positive adjective is not required to exist, which is exactly the content the join without a listed intermediate expresses.

inductive Booij2010.BaarAtom : Type

The affixal morphs of the on-V-baar complex.

• on : BaarAtom
• baar : BaarAtom

@[instance_reducible]

instance Booij2010.instDecidableEqBaarAtom : DecidableEq BaarAtom

Equations

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

@[instance_reducible]

instance Booij2010.instFintypeBaarAtom : Fintype BaarAtom

Equations

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

inductive Booij2010.OnbaarSlot : Type

The three slots of the on-V-baar complex schema.

• pre : OnbaarSlot
• base : OnbaarSlot
• suf : OnbaarSlot

@[instance_reducible]

instance Booij2010.instDecidableEqOnbaarSlot : DecidableEq OnbaarSlot

Equations

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

@[instance_reducible]

instance Booij2010.instFintypeOnbaarSlot : Fintype OnbaarSlot

Equations

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

def Booij2010.onSchema : ConstructionMorphology.Schema OnbaarSlot (Flat BaarAtom)

The on-A schema: prefix pinned to on-, base open.

Equations

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

def Booij2010.baarSchema : ConstructionMorphology.Schema OnbaarSlot (Flat BaarAtom)

The V-baar schema: suffix pinned to -baar, base open.

Equations

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

def Booij2010.onbaarSchema : ConstructionMorphology.Schema OnbaarSlot (Flat BaarAtom)

The unified on-V-baar schema: both affixes pinned, base open.

Equations

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

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

The on- and V-baar descriptions unify into the on-V-baar description — the schema unification (16), with no intermediate V-baar word required.

theorem Booij2010.onbaarSchema_instantiates_iff {w : OnbaarSlot → Flat BaarAtom} : onbaarSchema.Instantiates w ↔ onSchema.Instantiates w ∧ baarSchema.Instantiates w

The unified schema's instances are exactly the words that are at once on- prefixed and -baar suffixed: the content of coining onbedwingbaar directly.

Further constructional phenomena (prose)

[booij-2010-compass] extends the constructional analysis in three directions this file records but does not formalize. Holistic VN exocentrics: Romance VN compounds (lava-piatti 'dishwasher') carry an agent/instrument meaning that is a property of the construction as a whole, with no head constituent and no zero-affix to bear it. Constructional inflection: the Russian declension paradigm treats each cell's morpho-syntactic value as a holistic property of the word form, with thematic material that is morphomic ([aronoff-1994]). Periphrasis: have plus past participle is a constructional idiom whose perfect meaning is holistic — the natural home for a dedicated periphrasis carrier.