Embick (2010): Localism versus Globalism in Morphology and Phonology

This file formalizes [Emb10]'s C₁-LIN theory of contextual allomorphy: a node conditions the Vocabulary Insertion ([HM93]) of another only when the two are concatenated and active in the same cycle of Spell-Out. 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, the Domain Corollary, while the complement of an inner cyclic head is inactive when an outer one is spelled out, the Activity Corollary; nodes with null exponents are pruned from the concatenation statements. The case studies follow. The Latin perfect indicative takes its special agreement endings only where a null present tense is pruned between Agr and Asp[perf], the overt tenses of the other perfects intervening (§3.1.1); a theme vowel reads the conjugation class of the node it is concatenated with, the root's across a null v and -ess's otherwise (§3.1.2); root-attached n has root-determined allomorphs while the gerund's n, an outer cyclic head, has none, and -ity and -ation are potentiated by the -able and -ize they follow (§2.2–2.3, §3.3); the noncyclic past tense and plural see the root across pruned categorizers (§2.3.3); and the Hindi agentive Voice ([Kra96]) shows root-determined allomorphy in the transitive but only its default in the indirect causative, where the root lies two cycles down (§3.2.2).

Implementation notes

• Cycles, coactivity, the root's domain and adjacency across pruned heads are the substrate's ComplexHead API; this file contributes the heads of the case studies, the rows, and the predictions checked over them. A row records a word's heads innermost first with their exponents, the head whose realization is at issue, its conditioner, the root or another head, and whether the book attests or excludes the conditioning.
• The examples are Data.Examples.Embick2010.

References

• [Emb10]
• [HM93]
• [Kra96]

inductive Embick2010.Head : Type

The heads of the case studies are 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 (§2.3.1).

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 the concatenation statements, (53) of ch. 2.

Equations

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

@[instance_reducible]

instance Embick2010.instDecidablePredMorphemeCyclic : DecidablePred cyclic

Equations

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

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

structure Embick2010.Row : Type

A conditioning relation records the word's heads, the head whose realization is at issue, its conditioner, none for the root, and the book's verdict.

• spine : DistributedMorphology.ComplexHead DistributedMorphology.Root Morpheme
• target : Fin self.spine.heads.length
• conditioner : Option (Fin self.spine.heads.length)
• claim : Claim

def Embick2010.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 Embick2010.claimTable : List (String × Claim)

The verdicts as named in the rows.

Equations

• Embick2010.claimTable = [("attested", Embick2010.Claim.attested), ("blocked", Embick2010.Claim.blocked)]

def Embick2010.rootNames : List String

The roots of the pool, indexed by first occurrence.

Equations

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

def Embick2010.heads (ex : Datum) : List Morpheme

The heads of a row innermost first, hᵢ with the exponent hᵢexp.

Equations

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

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

The row of an example, whose positions count from one, innermost first.

Equations

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

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

def Embick2010.rows : List Row

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

Equations

• Embick2010.rows = List.filterMap Embick2010.Row.ofDatum 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: in the first cycle, across pruned heads only. The gerund's n and the indirect causative's Voice are outside the root's domain, and -ess blocks the theme's view of the root.

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. Agr is coactive with Asp[perf] throughout, and only the overt tense of the non-indicative forms intervenes, so the effect is linear rather than cyclic (§3.1.1).