The motivation for roots in Distributed Morphology

[Emb21]: the Two Domains Intuition — that some form–meaning connections are fixed close to a lexical primitive and others built compositionally — is explained not by the word but by syntactic locality around category-free roots. Derived nominals combine the root directly with n and gerunds nominalize a verbal structure ((8), (9)); agents are licensed only by a Voice that selects v ((10)), so growth has no agentive reading while growing does, and destruction gets one only from its encyclopedically agentive root ((6), (7)). Category-defining heads are cyclic: a head attached to the categorized root may show root-determined allomorphy and special interpretation, an outer cyclic head may not ((13), (14)), while an outer noncyclic head — the tense of bent, the aspect of broken — remains local ((15)). One cycle bounds both interfaces, each adding its own adjacency.

Main definitions

• Head, Morpheme, cyclic: the heads of the examples with the categorizers cyclic.
• AgentLicensed: the Agent-Licensing Assumption (10), Voice selecting v.
• Row, rows: the nominalizations of (6)–(7) and the inflected verbs of §5.

Main results

• agentive_possessor_rows: the possessor is agentive iff an agent is licensed or the root is encyclopedically agentive.
• derivedNominal_not_agentLicensed, gerund_n_not_rootLocal: a derived nominal licenses no agent, and the gerund's n is outer ((9), (14)).
• inflection_rootLocal: tense and aspect outside v are local ((15)).

inductive Embick2021.Head : Type

The heads of the examples.

• 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 }

structure Embick2021.Morpheme : Type

A head occurrence with its exponent.

• head : Head
• exponent : String

@[instance_reducible]

instance Embick2021.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• Embick2021.instDecidableEqMorpheme = Embick2021.instDecidableEqMorpheme.decEq

def Embick2021.instDecidableEqMorpheme.decEq (x✝ x✝¹ : Morpheme) : Decidable (x✝ = x✝¹)

Equations

• Embick2021.instDecidableEqMorpheme.decEq { head := a, exponent := a_1 } { head := b, exponent := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Embick2021.instReprMorpheme : Repr Morpheme

Equations

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

def Embick2021.instReprMorpheme.repr : Morpheme → ℕ → Std.Format

Equations

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

def Embick2021.cyclic (m : Morpheme) : Prop

The category heads are the cyclic heads.

Equations

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

@[instance_reducible]

instance Embick2021.instDecidablePredMorphemeCyclic : DecidablePred cyclic

Equations

• Embick2021.instDecidablePredMorphemeCyclic x✝ = Embick2021.instDecidablePredMorphemeCyclic._aux_1 x✝

def Embick2021.AgentLicensed (s : DistributedMorphology.Spine Morpheme) : 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].head = Embick2021.Head.voice ∧ ∃ j < i, s.heads[j].head = Embick2021.Head.v

@[instance_reducible]

instance Embick2021.instDecidableAgentLicensed (s : DistributedMorphology.Spine Morpheme) : Decidable (AgentLicensed s)

Equations

• Embick2021.instDecidableAgentLicensed s = Embick2021.instDecidableAgentLicensed._aux_1 s

The words

inductive Embick2021.RootClass : Type

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

• 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 ⋯

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

Equations

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

@[instance_reducible]

instance Embick2021.instReprConstruction : Repr Construction

Equations

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

structure Embick2021.Row : Type

• text : String
• spine : DistributedMorphology.Spine Morpheme
• rootClass : Option RootClass
• construction : Construction
• accepted : Bool

@[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.Morpheme.ofLabel (exp : String) : String → Option Morpheme

Equations

• Embick2021.Morpheme.ofLabel exp "n" = some { head := Embick2021.Head.n, exponent := exp }
• Embick2021.Morpheme.ofLabel exp "v" = some { head := Embick2021.Head.v, exponent := exp }
• Embick2021.Morpheme.ofLabel exp "a" = some { head := Embick2021.Head.a, exponent := exp }
• Embick2021.Morpheme.ofLabel exp "voice" = some { head := Embick2021.Head.voice, exponent := exp }
• Embick2021.Morpheme.ofLabel exp "T" = some { head := Embick2021.Head.tense, exponent := exp }
• Embick2021.Morpheme.ofLabel exp "aspect" = some { head := Embick2021.Head.aspect, exponent := exp }
• Embick2021.Morpheme.ofLabel exp x✝ = none

def Embick2021.RootClass.ofLabel : String → Option RootClass

Equations

• Embick2021.RootClass.ofLabel "agentive" = some Embick2021.RootClass.agentive
• Embick2021.RootClass.ofLabel "nonagentive" = some Embick2021.RootClass.nonagentive
• Embick2021.RootClass.ofLabel x✝ = none

def Embick2021.Construction.ofLabel : String → Option Construction

Equations

• Embick2021.Construction.ofLabel "derivedNominal" = some Embick2021.Construction.derivedNominal
• Embick2021.Construction.ofLabel "gerund" = some Embick2021.Construction.gerund
• Embick2021.Construction.ofLabel "inflected" = some Embick2021.Construction.inflected
• Embick2021.Construction.ofLabel x✝ = none

def Embick2021.rootNames : List String

The roots of the pool, indexed by first occurrence.

Equations

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

def Embick2021.Row.ofExample (ex : Data.Examples.LinguisticExample) : Option Row

Equations

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

theorem Embick2021.row_ofExample_isSome (ex : Data.Examples.LinguisticExample) : ex ∈ Examples.all → (Row.ofExample ex).isSome = true

def Embick2021.rows : List Row

Equations

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

Nominalizations ((6)–(10))

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

The possessor reads as an agent iff 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: 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 = 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), (14)), whereas the derived nominal's n is the first ((8), (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.