Localism versus globalism in morphology and phonology

[embick-2010]: contextual allomorphy holds only between concatenated nodes that are active in the same cycle of Spell-Out — the C₁-LIN theory. The category-defining heads are cyclic; merging one spells out the cyclic domains in its complement, so a cyclic head and the noncyclic heads attached to it are realized in the cycle of the next cyclic head, with the complement of the inner one inactive (the Domain and Activity Corollaries), and nodes with null exponents are pruned from the concatenation statements. Latin perfect agreement takes its special endings only when a null present tense is pruned between it and Asp[perf] (§3.1.1); a theme vowel reads the conjugation class of the node it is concatenated with — the root's across a null v, -ess's otherwise (§3.1.2); root-attached n has root-determined allomorphs and the gerund's n none, while -ity and -ation are potentiated by the -able and -ize they follow (§2.2, §3.3); past tense and plural see the root across pruned categorizers (§2.2–2.3); and Hindi Voice shows root-determined allomorphy in the transitive but only its default in the indirect causative, two cycles up (§3.2.2).

Main definitions

• Head, Morpheme, cyclic, phonNull: the heads of the case studies.
• Row, rows: each conditioning relation the book attests or excludes.

Main results

• root_rows, head_rows: attested conditioning is predicted and blocked conditioning excluded, by the root and by a head.
• perfect_one_cycle: the Latin perfects share one cycle, so only linear intervention separates the perfect indicative from the rest.

inductive Embick2010.Head : Type

The heads of the case studies: the categorizers, active and passive Voice, the theme position, and the inflectional heads.

• n : Head
• v : Head
• a : Head
• voice : Head
• voicePassive : Head
• theme : Head
• aspect : Head
• tense : Head
• agr : Head
• number : Head

@[instance_reducible]

instance Embick2010.instDecidableEqHead : DecidableEq Head

Equations

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

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

Equations

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

@[instance_reducible]

instance Embick2010.instReprHead : Repr Head

Equations

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

structure Embick2010.Morpheme : Type

A head occurrence with its exponent, empty when null.

• head : Head
• exponent : String

@[instance_reducible]

instance Embick2010.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• Embick2010.instDecidableEqMorpheme = Embick2010.instDecidableEqMorpheme.decEq

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

Equations

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

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

Equations

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

@[instance_reducible]

instance Embick2010.instReprMorpheme : Repr Morpheme

Equations

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

def Embick2010.cyclic (m : Morpheme) : Prop

The category-defining heads are the cyclic heads.

Equations

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

def Embick2010.phonNull (m : Morpheme) : Prop

A null exponent, pruned from concatenation.

Equations

• Embick2010.phonNull m = (m.exponent = "")

@[instance_reducible]

instance Embick2010.instDecidablePredMorphemeCyclic : DecidablePred cyclic

Equations

• Embick2010.instDecidablePredMorphemeCyclic x✝ = Embick2010.instDecidablePredMorphemeCyclic._aux_1 x✝

@[instance_reducible]

instance Embick2010.instDecidablePredMorphemePhonNull : DecidablePred phonNull

Equations

• Embick2010.instDecidablePredMorphemePhonNull x✝ = Embick2010.instDecidablePredMorphemePhonNull._aux_1 x✝

The case studies

inductive Embick2010.Claim : Type

Whether the book attests the conditioning or excludes it.

• attested : Claim
• blocked : Claim

@[instance_reducible]

instance Embick2010.instDecidableEqClaim : DecidableEq Claim

Equations

• Embick2010.instDecidableEqClaim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Embick2010.instReprClaim : Repr Claim

Equations

• Embick2010.instReprClaim = { reprPrec := Embick2010.instReprClaim.repr }

def Embick2010.instReprClaim.repr : Claim → ℕ → Std.Format

Equations

• Embick2010.instReprClaim.repr Embick2010.Claim.attested prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2010.Claim.attested")).group prec✝
• Embick2010.instReprClaim.repr Embick2010.Claim.blocked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Embick2010.Claim.blocked")).group prec✝

@[instance_reducible]

instance Embick2010.instFintypeClaim : Fintype Claim

Equations

• Embick2010.instFintypeClaim = { elems := { val := ↑Embick2010.Claim.enumList, nodup := Embick2010.Claim.enumList_nodup }, complete := Embick2010.instFintypeClaim._proof_1 }

structure Embick2010.Row : Type

A word, the head whose realization is at issue, what conditions it — the root, or another head — and the book's verdict.

• form : String
• spine : DistributedMorphology.Spine Morpheme
• target : Fin self.spine.heads.length
• conditioner : Option (Fin self.spine.heads.length)
• claim : Claim

@[instance_reducible]

instance Embick2010.instReprRow : Repr Row

Equations

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

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

Equations

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

def Embick2010.Morpheme.ofLabel (exp : String) : String → Option Morpheme

Equations

• Embick2010.Morpheme.ofLabel exp "n" = some { head := Embick2010.Head.n, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "v" = some { head := Embick2010.Head.v, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "a" = some { head := Embick2010.Head.a, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "voice" = some { head := Embick2010.Head.voice, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "voicePassive" = some { head := Embick2010.Head.voicePassive, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "theme" = some { head := Embick2010.Head.theme, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "aspect" = some { head := Embick2010.Head.aspect, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "tense" = some { head := Embick2010.Head.tense, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "agr" = some { head := Embick2010.Head.agr, exponent := exp }
• Embick2010.Morpheme.ofLabel exp "number" = some { head := Embick2010.Head.number, exponent := exp }
• Embick2010.Morpheme.ofLabel exp x✝ = none

def Embick2010.positionOfLabel : String → Option ℕ

A position among the heads, innermost first.

Equations

• Embick2010.positionOfLabel "1" = some 0
• Embick2010.positionOfLabel "2" = some 1
• Embick2010.positionOfLabel "3" = some 2
• Embick2010.positionOfLabel "4" = some 3
• Embick2010.positionOfLabel "5" = some 4
• Embick2010.positionOfLabel x✝ = none

def Embick2010.Claim.ofLabel : String → Option Claim

Equations

• Embick2010.Claim.ofLabel "attested" = some Embick2010.Claim.attested
• Embick2010.Claim.ofLabel "blocked" = some Embick2010.Claim.blocked
• Embick2010.Claim.ofLabel x✝ = none

def Embick2010.rootNames : List String

The roots of the pool, indexed by first occurrence.

Equations

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

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

Equations

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

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

def Embick2010.rows : List Row

The conditioning relations of §2.2–2.3, §3.1–3.3.

Equations

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

Predictions

theorem Embick2010.root_rows (r : Row) : r ∈ rows → r.conditioner = none → (r.spine.SeesRoot cyclic phonNull r.target ↔ r.claim = Claim.attested)

Root-determined allomorphy is attested exactly where the target sees the root: the first cycle, across pruned heads only.

theorem Embick2010.head_rows (r : Row) : r ∈ rows → ∀ (j : Fin r.spine.heads.length), r.conditioner = some j → (r.spine.Sees cyclic phonNull r.target j ↔ r.claim = Claim.attested)

Head-determined allomorphy is attested exactly where the target sees the conditioning head: present at its insertion and concatenated with it.

theorem Embick2010.perfect_one_cycle (r : Row) : r ∈ rows → r.spine.root = { index := List.idxOf "AM" rootNames } → ∀ (j : Fin r.spine.heads.length), r.conditioner = some j → r.spine.Coactive cyclic r.target j ∧ (r.spine.Sees cyclic phonNull r.target j ↔ ∀ (k : Fin r.spine.heads.length), j < k → k < r.target → phonNull r.spine.heads[k])

The Latin perfects share one cycle: agreement is coactive with Asp[perf] throughout, and only the overt tense of the non-indicative forms intervenes (§3.1.1).