Construction Morphology: the constructional-schema engine [Boo10a]

[Boo10a] analyzes complex words as constructions — pairings of form and meaning — licensed by constructional schemas in a hierarchical lexicon. This file instantiates the Morphology/Construction/ 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 ([Boo10a]'s worked example)
• awareness_generates — the -ness schema licenses a novel deadjectival noun
• compound_inheritance — subschemas inherit right-headedness (no Right-hand Head Rule) yet override locally (NN allows a recursive modifier, AN does not)
• werkbaar_overrides — the CxM default-inheritance demand site: werkbaar overrides the -baar schema's transitivity default
• onbaar_unifies — two word-formation schemas unify into on-V-baar, no listed intermediate required

The deadjectival -ness schema

The schema [[x]A ness]N of [Boo10a]: 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.

inductive Booij2010.Atom : Type

The morphs and (deadjectival) bases the -ness schema handles.

• ness : Atom
• aware : Atom
• carless : Atom
• bald : Atom

@[implicit_reducible]

instance Booij2010.instDecidableEqAtom : DecidableEq Atom

Equations

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

@[implicit_reducible]

instance Booij2010.instFintypeAtom : Fintype Atom

Equations

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

inductive Booij2010.NessSlot : Type

The two slots of the -ness construction.

• base : NessSlot
• affix : NessSlot

@[implicit_reducible]

instance Booij2010.instDecidableEqNessSlot : DecidableEq NessSlot

Equations

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

@[implicit_reducible]

instance Booij2010.instFintypeNessSlot : Fintype NessSlot

Equations

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

def Booij2010.nessSchema : Morphology.Construction.Schema NessSlot (Flat Atom)

The -ness schema: the affix slot pinned to -ness, the base slot an open deadjectival variable (⊥).

Equations

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

def Booij2010.carlessness : NessSlot → Flat Atom

carlessness: the adjective carless unified into the base slot.

Equations

• Booij2010.carlessness Booij2010.NessSlot.base = ↑Booij2010.Atom.carless
• Booij2010.carlessness Booij2010.NessSlot.affix = ↑Booij2010.Atom.ness

def Booij2010.baldness : NessSlot → Flat Atom

baldness: a stored -ness noun, the attested filler at the affix slot.

Equations

• Booij2010.baldness Booij2010.NessSlot.base = ↑Booij2010.Atom.bald
• Booij2010.baldness Booij2010.NessSlot.affix = ↑Booij2010.Atom.ness

def Booij2010.awareness : NessSlot → Flat Atom

awareness: a novel -ness noun the schema generates.

Equations

• Booij2010.awareness Booij2010.NessSlot.base = ↑Booij2010.Atom.aware
• Booij2010.awareness Booij2010.NessSlot.affix = ↑Booij2010.Atom.ness

theorem Booij2010.ness_instantiates {w : NessSlot → Flat Atom} (h : w NessSlot.affix = ↑Atom.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 carlessness

carlessness instantiates the -ness schema.

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

Instantiation as unification: unifying the schema description with carlessness returns carlessness — [Boo10a]'s worked example.

def Booij2010.nessLexicon : Set (NessSlot → Flat Atom)

The stored lexicon of -ness nouns feeding the generative role.

Equations

• Booij2010.nessLexicon = {Booij2010.baldness}

theorem Booij2010.awareness_generates : nessSchema.Generates nessLexicon awareness

The -ness schema generates the novel noun awareness: the open base slot is free, and the pinned affix slot takes only its attested filler -ness. The affix slot is not open, so this is Generates, not full productivity.

The compound hierarchy

The compound schema (6) dominates the NN/VN/AN/PN subcases (7). Headedness is read off the general schema — right-headed — so no Right-hand Head Rule is needed; subschemas inherit it. Subschemas still legislate locally: an NN modifier may itself be a compound, an AN modifier may not (8).

inductive Booij2010.CompoundNode : Type

The compound schema and its four subcases.

• compound : CompoundNode
• nn : CompoundNode
• vn : CompoundNode
• an : CompoundNode
• pn : CompoundNode

@[implicit_reducible]

instance Booij2010.instDecidableEqCompoundNode : DecidableEq CompoundNode

Equations

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

@[implicit_reducible]

instance Booij2010.instFintypeCompoundNode : Fintype CompoundNode

Equations

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

def Booij2010.compoundParent : CompoundNode → Option CompoundNode

The subschema-of relation: each subcase's parent is the general compound schema.

Equations

• Booij2010.compoundParent Booij2010.CompoundNode.compound = none
• Booij2010.compoundParent Booij2010.CompoundNode.nn = some Booij2010.CompoundNode.compound
• Booij2010.compoundParent Booij2010.CompoundNode.vn = some Booij2010.CompoundNode.compound
• Booij2010.compoundParent Booij2010.CompoundNode.an = some Booij2010.CompoundNode.compound
• Booij2010.compoundParent Booij2010.CompoundNode.pn = some Booij2010.CompoundNode.compound

def Booij2010.compoundHierarchy : Morphology.Construction.Hierarchy CompoundNode

The hierarchical constructicon of English compounds.

Equations

• Booij2010.compoundHierarchy = { parent := Booij2010.compoundParent, wf := Booij2010.compoundParent_wf✝ }

inductive Booij2010.Headed : Type

Headedness, specified once at the general schema.

• right : Headed
• left : Headed

@[implicit_reducible]

instance Booij2010.instDecidableEqHeaded : DecidableEq Headed

Equations

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

def Booij2010.headedness : CompoundNode → Option Headed

Right-headedness is a property of the general compound schema alone.

Equations

• Booij2010.headedness Booij2010.CompoundNode.compound = some Booij2010.Headed.right
• Booij2010.headedness x✝ = none

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 headedness CompoundNode.nn = some Headed.right ∧ compoundHierarchy.value recursiveModifier CompoundNode.nn = some true ∧ compoundHierarchy.value recursiveModifier CompoundNode.an = some false

Subschemas inherit right-headedness from the general schema (no Right-hand Head Rule), while the AN subschema overrides the default recursive-modifier option: an NN modifier may be a compound, an AN modifier may not.

Default inheritance and override: werkbaar

[Boo10a]'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

@[implicit_reducible]

instance Booij2010.instDecidableEqBaarNode : DecidableEq BaarNode

Equations

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

@[implicit_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 : Morphology.Construction.Hierarchy BaarNode

Equations

• Booij2010.baarHierarchy = { parent := Booij2010.baarParent, wf := Booij2010.baarParent_wf✝ }

inductive Booij2010.Transitivity : Type

Transitivity of the base verb.

• trans : Transitivity
• intrans : Transitivity

@[implicit_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

@[implicit_reducible]

instance Booij2010.instDecidableEqBaarAtom : DecidableEq BaarAtom

Equations

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

@[implicit_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

@[implicit_reducible]

instance Booij2010.instDecidableEqOnbaarSlot : DecidableEq OnbaarSlot

Equations

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

@[implicit_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.onBody : OnbaarSlot → Flat BaarAtom

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

Equations

• Booij2010.onBody Booij2010.OnbaarSlot.pre = ↑Booij2010.BaarAtom.on
• Booij2010.onBody Booij2010.OnbaarSlot.base = ⊥
• Booij2010.onBody Booij2010.OnbaarSlot.suf = ⊥

def Booij2010.baarBody : OnbaarSlot → Flat BaarAtom

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

Equations

• Booij2010.baarBody Booij2010.OnbaarSlot.pre = ⊥
• Booij2010.baarBody Booij2010.OnbaarSlot.base = ⊥
• Booij2010.baarBody Booij2010.OnbaarSlot.suf = ↑Booij2010.BaarAtom.baar

def Booij2010.onbaarBody : OnbaarSlot → Flat BaarAtom

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

Equations

• Booij2010.onbaarBody Booij2010.OnbaarSlot.pre = ↑Booij2010.BaarAtom.on
• Booij2010.onbaarBody Booij2010.OnbaarSlot.base = ⊥
• Booij2010.onbaarBody Booij2010.OnbaarSlot.suf = ↑Booij2010.BaarAtom.baar

theorem Booij2010.onbaar_unifies : PartialUnify.unify onBody baarBody = some onbaarBody

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

Further constructional phenomena (prose)

[Boo10a] 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 ([Aro94]). Periphrasis: have plus past participle is a constructional idiom whose perfect meaning is holistic — the natural home for a dedicated periphrasis carrier.