Embick (2021): The Motivation for Roots in Distributed Morphology

This file formalizes [Emb21]'s case for category-free roots. The Two Domains Intuition (1), that some form–meaning connections are fixed close to a lexical primitive and others are built compositionally, is explained not by the word, as lexicalism (5) has it, but by syntactic locality around roots. Following [Mar97]'s update of [Cho70], derived nominals combine the root directly with n and gerunds nominalize a verbal structure, (8) and (9); agents are licensed only by a Voice that selects v, the Agent-Licensing Assumption (10), so growth has no agentive reading while growing does, and destruction gets one only from its encyclopedically agentive root, (6) and (7). In the Roots-and-contexts theory of §5 the category-defining heads are cyclic: a head attached to the categorized root may show root-determined allomorphy and a special interpretation while an outer cyclic head may not, the generalizations (13) of [EM08] and structure (14), whereas an outer noncyclic head, the tense of ben-t or the aspect of brok-en, is still local to the root, structure (15). Since growth and growing are both words, the word cannot be the domain; the domains are the cycles.

Implementation notes

• Cycles and the root's domain are the substrate's ComplexHead API, the cyclic domains of [Emb10] that the paper adopts for (14) and (15); this file contributes the heads of the examples, the Agent-Licensing Assumption, the rows and the predictions checked over them.
• The gerund's verbal structure is taken as v with the agent-licensing Voice above it, the second option of (10).
• The examples are Data.Examples.Embick2021.

References

• [Emb21]
• [Cho70]
• [Mar97]
• [EM08]
• [Emb10]

inductive Embick2021.Head : Type

The heads of the examples are the categorizers, Voice, tense and aspect.

• n : Head
• v : Head
• a : Head
• voice : Head
• tense : Head
• aspect : Head

@[instance_reducible]

instance Embick2021.instDecidableEqHead : DecidableEq Head

Equations

• Embick2021.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Embick2021.instReprHead.repr : Head → ℕ → Std.Format

Equations

• Embick2021.instReprHead.repr Embick2021.Head.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2021.Head.n")).group prec✝
• Embick2021.instReprHead.repr Embick2021.Head.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2021.Head.v")).group prec✝
• Embick2021.instReprHead.repr Embick2021.Head.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2021.Head.a")).group prec✝
• Embick2021.instReprHead.repr Embick2021.Head.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2021.Head.voice")).group prec✝
• Embick2021.instReprHead.repr Embick2021.Head.tense prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2021.Head.tense")).group prec✝
• Embick2021.instReprHead.repr Embick2021.Head.aspect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2021.Head.aspect")).group prec✝

@[instance_reducible]

instance Embick2021.instReprHead : Repr Head

Equations

• Embick2021.instReprHead = { reprPrec := Embick2021.instReprHead.repr }

def Embick2021.cyclic (h : Head) : Prop

The category-defining heads are the cyclic heads (§5).

Equations

• Embick2021.cyclic h = (h = Embick2021.Head.n ∨ h = Embick2021.Head.v ∨ h = Embick2021.Head.a)

@[instance_reducible]

instance Embick2021.instDecidablePredHeadCyclic : DecidablePred cyclic

Equations

• Embick2021.instDecidablePredHeadCyclic x✝ = { decide := decide (x✝ = Embick2021.Head.n) || decide (x✝ = Embick2021.Head.v ∨ x✝ = Embick2021.Head.a), reflects_decide := ⋯ }

def Embick2021.AgentLicensed (s : DistributedMorphology.ComplexHead DistributedMorphology.Root Head) : Prop

The Agent-Licensing Assumption (10): an agent is introduced by a Voice that selects v, so only a structure with v below Voice licenses one.

Equations

• Embick2021.AgentLicensed s = ∃ (i : Fin s.heads.length), s.heads[i] = Embick2021.Head.voice ∧ ∃ j < i, s.heads[j] = Embick2021.Head.v

@[instance_reducible]

instance Embick2021.instDecidableAgentLicensed (s : DistributedMorphology.ComplexHead DistributedMorphology.Root Head) : Decidable (AgentLicensed s)

Equations

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

The words

inductive Embick2021.RootClass : Type

Whether the root is encyclopedically agentive, destroy, or not, grow (§4).

• agentive : RootClass
• nonagentive : RootClass

@[instance_reducible]

instance Embick2021.instDecidableEqRootClass : DecidableEq RootClass

Equations

• Embick2021.instDecidableEqRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Embick2021.instReprRootClass : Repr RootClass

Equations

• Embick2021.instReprRootClass = { reprPrec := Embick2021.instReprRootClass.repr }

def Embick2021.instReprRootClass.repr : RootClass → ℕ → Std.Format

Equations

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

inductive Embick2021.Construction : Type

Derived nominal, gerund, or inflected verb.

• derivedNominal : Construction
• gerund : Construction
• inflected : Construction

@[instance_reducible]

instance Embick2021.instDecidableEqConstruction : DecidableEq Construction

Equations

• Embick2021.instDecidableEqConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Embick2021.instReprConstruction : Repr Construction

Equations

• Embick2021.instReprConstruction = { reprPrec := Embick2021.instReprConstruction.repr }

def Embick2021.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

structure Embick2021.Row : Type

A word of the examples records its heads above the root, the root's class where the paper gives one, its construction, and the paper's judgment of the agentive reading.

• spine : DistributedMorphology.ComplexHead DistributedMorphology.Root Head
• rootClass : Option RootClass
• construction : Construction
• judgment : Judgment

@[instance_reducible]

instance Embick2021.instReprRow : Repr Row

Equations

• Embick2021.instReprRow = { reprPrec := Embick2021.instReprRow.repr }

def Embick2021.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def Embick2021.headTable : List (String × Head)

The heads as named in the rows.

Equations

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

def Embick2021.rootClassTable : List (String × RootClass)

The root classes as named in the rows.

Equations

• Embick2021.rootClassTable = [("agentive", Embick2021.RootClass.agentive), ("nonagentive", Embick2021.RootClass.nonagentive)]

def Embick2021.constructionTable : List (String × Construction)

The constructions as named in the rows.

Equations

• Embick2021.constructionTable = [("derivedNominal", Embick2021.Construction.derivedNominal), ("gerund", Embick2021.Construction.gerund), ("inflected", Embick2021.Construction.inflected)]

def Embick2021.rootNames : List String

The roots of the pool, indexed by first occurrence.

Equations

• Embick2021.rootNames = (List.filterMap (fun (x : Datum) => x.feature? "root") Embick2021.Examples.all).eraseDups

def Embick2021.Row.ofDatum (ex : Datum) : Option Row

A row from an example, its heads innermost first.

Equations

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

theorem Embick2021.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def Embick2021.rows : List Row

The nominalizations of (6) and (7) and the inflected verbs of §5.

Equations

• Embick2021.rows = List.filterMap Embick2021.Row.ofDatum Embick2021.Examples.all

Nominalizations, (6)–(10)

theorem Embick2021.agentive_possessor_rows (r : Row) : r ∈ rows → ∀ (c : RootClass), r.rootClass = some c → (r.judgment = Judgment.acceptable ↔ AgentLicensed r.spine ∨ c = RootClass.agentive)

The possessor reads as an agent exactly when the structure licenses one or the root is encyclopedically agentive: destruction and both gerunds, not growth.

theorem Embick2021.derivedNominal_not_agentLicensed (r : Row) : r ∈ rows → r.construction = Construction.derivedNominal → ¬AgentLicensed r.spine

A derived nominal is a root noun, (8): no v, so no agent-licensing Voice.

Inner and outer heads, (13)–(15)

theorem Embick2021.gerund_n_not_rootLocal (r : Row) : r ∈ rows → ∀ (i : Fin r.spine.heads.length), r.spine.heads[i] = Head.n → (r.spine.RootLocal cyclic i ↔ r.construction = Construction.derivedNominal)

The gerund's n is an outer cyclic head, not local to the root, (9) and (14), whereas the derived nominal's n is attached to the root, (8) and (13).

theorem Embick2021.inflection_rootLocal (r : Row) : r ∈ rows → r.construction = Construction.inflected → ∀ (i : Fin r.spine.heads.length), r.spine.RootLocal cyclic i

Tense and aspect outside the verbalizer are local to the root, (15): ben-t, brok-en.