Locality domains for contextual allomorphy and allosemy

A word is its root with the heads merged above it, innermost first — the complex head that successive Merger builds, whose first k heads form the word after k steps. Its surface follows from the side on which each head's exponent attaches: prefixes outermost first, the root, suffixes innermost first, so the affixes of each side mirror the order of merger. The category-defining heads are cyclic: merging one sends the cyclic domains in its complement to the interfaces, so the heads of a word fall into cycles — a head's cycle is the number of cyclic heads at or below it — and a head undergoes Vocabulary Insertion in its own cycle, the material below the first cyclic head in the first. When a head is spelled out, the heads of its cycle and of the cycle before are present, the latter already realized, while earlier material is inactive and later cycles are not yet merged; the root, in the complement of the first cyclic head, is active in the first cycle only. Within a cycle each interface adds its own adjacency: a head conditions another only across heads null at that interface — pruned phonological zeros for allomorphy, semantically null heads for allosemy — so the two domains coincide exactly where the two kinds of nullness do. The idiom domain is a different bound, the heads below an agentive Voice, and neither contains the other.

Main definitions

• Spine, Spine.toWordStructure, Spine.toTree: the word as root and head sequence, its word-structure tree, and its word tree by affix side.
• Spine.word: the complex head after k steps of Merger.
• Spine.cycle, Spine.insertionCycle: a head's cycle and the cycle of its insertion.
• Spine.Coactive, Spine.RootLocal: presence of one head at another's insertion, and of the root.
• Spine.Sees, Spine.SeesRoot: presence plus adjacency across heads null at an interface.
• Spine.IdiomLocal: the heads below an agentive Voice.

Main results

• surface_eq: the Mirror Principle — the surface reads each side's heads outward from the root in order of merger.
• heads_word_isPrefix, mem_word_of_le: the merged word is an initial segment of the spine.
• cycle_mono, RootLocal.of_le: cycles grow outward and the root's domain is an initial segment.
• not_rootLocal_of_cyclic_of_cyclic, RootLocal.cyclic_first: an outer cyclic head is not local to the root, and a local cyclic head is the first.
• not_coactive_of_lt_of_cyclic, not_coactive_of_cyclic_of_cyclic: nothing sees an outer cyclic head — no outward sensitivity to, and no fusion with, a later category head.
• not_coactive_of_add_two_le: material two cycles down is inactive.
• not_sees_of_not_null, sees_congr: an intervening non-null head blocks conditioning, and the interface domains agree where nullness agrees.

References

• M. Baker, The Mirror Principle and morphosyntactic explanation
• [D. Embick, Localism versus globalism in morphology and phonology][embick-2010]
• [A. Marantz, Locality domains for contextual allomorphy across the interfaces][marantz-2013]
• D. Embick, The motivation for roots in Distributed Morphology

structure DistributedMorphology.Spine (H : Type u_1) : Type u_1

A word as its root and the heads merged above it, innermost first.

• root : Root

  The root.

• heads : List H

  The heads above the root, innermost first.

def DistributedMorphology.instDecidableEqSpine.decEq {H✝ : Type u_1} [DecidableEq H✝] (x✝ x✝¹ : Spine H✝) : Decidable (x✝ = x✝¹)

Equations

• DistributedMorphology.instDecidableEqSpine.decEq { root := a, heads := a_1 } { root := b, heads := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.instDecidableEqSpine {H✝ : Type u_1} [DecidableEq H✝] : DecidableEq (Spine H✝)

Equations

• DistributedMorphology.instDecidableEqSpine = DistributedMorphology.instDecidableEqSpine.decEq

def DistributedMorphology.instReprSpine.repr {H✝ : Type u_1} [Repr H✝] : Spine H✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprSpine {H✝ : Type u_1} [Repr H✝] : Repr (Spine H✝)

Equations

• DistributedMorphology.instReprSpine = { reprPrec := DistributedMorphology.instReprSpine.repr }

The word-structure tree

noncomputable def DistributedMorphology.Spine.toWordStructure {H : Type u_1} (s : Spine H) : WordStructure H

The word structure the spine builds: each head categorizes what lies below it.

Equations

• s.toWordStructure = List.foldl (fun (T : DistributedMorphology.WordStructure H) (h : H) => DistributedMorphology.categorize h T) (DistributedMorphology.ofRoot s.root) s.heads

theorem DistributedMorphology.Spine.heads_foldl_categorize {H : Type u_1} (T : WordStructure H) (hs : List H) : DistributedMorphology.heads (List.foldl (fun (T : WordStructure H) (h : H) => categorize h T) T hs) = ↑hs + DistributedMorphology.heads T

theorem DistributedMorphology.Spine.roots_foldl_categorize {H : Type u_1} (T : WordStructure H) (hs : List H) : roots (List.foldl (fun (T : WordStructure H) (h : H) => categorize h T) T hs) = roots T

@[simp]

theorem DistributedMorphology.Spine.roots_toWordStructure {H : Type u_1} (s : Spine H) : roots s.toWordStructure = {s.root}

@[simp]

theorem DistributedMorphology.Spine.heads_toWordStructure {H : Type u_1} (s : Spine H) : DistributedMorphology.heads s.toWordStructure = ↑s.heads

Merger and the surface

def DistributedMorphology.Spine.word {H : Type u_1} (s : Spine H) (k : ℕ) : Spine H

The complex head after k steps of Merger: the root with the first k heads. The remaining heads are realized periphrastically.

Equations

• s.word k = { root := s.root, heads := List.take k s.heads }

theorem DistributedMorphology.Spine.heads_word_isPrefix {H : Type u_1} (s : Spine H) (k : ℕ) : (s.word k).heads <+: s.heads

theorem DistributedMorphology.Spine.mem_word_of_le {H : Type u_1} (s : Spine H) {k : ℕ} {i j : Fin s.heads.length} (hji : j ≤ i) (hi : ↑i < k) : ↑j < k

Merger skips no head: a head in the word brings every head below it.

def DistributedMorphology.Spine.toTree {H : Type u_1} (s : Spine H) (side : H → Morphology.Morph.Side) : Morphology.Word.Tree (Root ⊕ H)

The word tree: each head attached on the side its exponent takes, innermost first.

Equations

• s.toTree side = Morphology.Word.Tree.attachAll (Sum.inl s.root) (List.map (fun (h : H) => (side h, Sum.inr h)) s.heads)

def DistributedMorphology.Spine.surface {H : Type u_1} (s : Spine H) (side : H → Morphology.Morph.Side) : List (Root ⊕ H)

The surface order of root and heads.

Equations

• s.surface side = (s.toTree side).toList

theorem DistributedMorphology.Spine.surface_eq {H : Type u_1} (s : Spine H) (side : H → Morphology.Morph.Side) : s.surface side = (List.map Sum.inr (List.filter (fun (h : H) => decide (side h = Morphology.Morph.Side.before)) s.heads)).reverse ++ Sum.inl s.root :: List.map Sum.inr (List.filter (fun (h : H) => decide (side h = Morphology.Morph.Side.after)) s.heads)

The Mirror Principle: the surface is the prefixal heads outermost first, the root, and the suffixal heads innermost first — on each side, surface order outward from the root is the order of merger.

Cycles

def DistributedMorphology.Spine.cycle {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (i : Fin s.heads.length) : ℕ

The cycle of a head: the number of cyclic heads at or below it. The root counts as cycle zero.

Equations

• s.cycle cyclic i = {j : Fin s.heads.length | j ≤ i ∧ cyclic s.heads[j]}.card

def DistributedMorphology.Spine.insertionCycle {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (i : Fin s.heads.length) : ℕ

The cycle in which a head undergoes Vocabulary Insertion: its own, or the first for the material below the first cyclic head.

Equations

• s.insertionCycle cyclic i = max 1 (s.cycle cyclic i)

def DistributedMorphology.Spine.Coactive {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (i j : Fin s.heads.length) : Prop

Head j is present when head i is spelled out: it belongs to that cycle or to the one before, whose heads remain present though already realized.

Equations

• s.Coactive cyclic i j = (s.cycle cyclic j ≤ s.insertionCycle cyclic i ∧ s.insertionCycle cyclic i ≤ s.cycle cyclic j + 1)

def DistributedMorphology.Spine.RootLocal {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (i : Fin s.heads.length) : Prop

The root is present for the heads of the first cycle only: the first category head and the noncyclic heads up to the next.

Equations

• s.RootLocal cyclic i = (s.cycle cyclic i ≤ 1)

@[instance_reducible]

instance DistributedMorphology.Spine.instDecidableCoactive {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (i j : Fin s.heads.length) : Decidable (s.Coactive cyclic i j)

Equations

• s.instDecidableCoactive cyclic i j = DistributedMorphology.Spine.instDecidableCoactive._aux_1 s cyclic i j

@[instance_reducible]

instance DistributedMorphology.Spine.instDecidableRootLocal {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (i : Fin s.heads.length) : Decidable (s.RootLocal cyclic i)

Equations

• s.instDecidableRootLocal cyclic i = DistributedMorphology.Spine.instDecidableRootLocal._aux_1 s cyclic i

theorem DistributedMorphology.Spine.cycle_mono {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (hij : i ≤ j) : s.cycle cyclic i ≤ s.cycle cyclic j

theorem DistributedMorphology.Spine.one_le_cycle_of_cyclic {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i : Fin s.heads.length} (hi : cyclic s.heads[i]) : 1 ≤ s.cycle cyclic i

theorem DistributedMorphology.Spine.cycle_add_one_le_of_lt_of_cyclic {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (hij : i < j) (hj : cyclic s.heads[j]) : s.cycle cyclic i + 1 ≤ s.cycle cyclic j

theorem DistributedMorphology.Spine.two_le_cycle_of_cyclic_of_cyclic {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j k : Fin s.heads.length} (hjk : j < k) (hki : k ≤ i) (hj : cyclic s.heads[j]) (hk : cyclic s.heads[k]) : 2 ≤ s.cycle cyclic i

The root's domain

theorem DistributedMorphology.Spine.RootLocal.of_le {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (h : s.RootLocal cyclic i) (hji : j ≤ i) : s.RootLocal cyclic j

The root's domain is an initial segment.

theorem DistributedMorphology.Spine.not_rootLocal_of_cyclic_of_cyclic {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (hji : j < i) (hj : cyclic s.heads[j]) (hi : cyclic s.heads[i]) : ¬s.RootLocal cyclic i

A cyclic head above a cyclic head is not local to the root: category change closes the root's domain.

theorem DistributedMorphology.Spine.RootLocal.cyclic_first {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i : Fin s.heads.length} (h : s.RootLocal cyclic i) (hi : cyclic s.heads[i]) (j : Fin s.heads.length) : j < i → ¬cyclic s.heads[j]

A local cyclic head is the first one.

Presence between heads

theorem DistributedMorphology.Spine.coactive_self {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] (i : Fin s.heads.length) : s.Coactive cyclic i i

theorem DistributedMorphology.Spine.coactive_of_cycle_eq {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (h : s.cycle cyclic i = s.cycle cyclic j) : s.Coactive cyclic i j

Heads of one cycle are present for one another.

theorem DistributedMorphology.Spine.not_coactive_of_lt_of_cyclic {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (hij : i < j) (hi : 1 ≤ s.cycle cyclic i) (hj : cyclic s.heads[j]) : ¬s.Coactive cyclic i j

Nothing already in a cycle sees a later cyclic head: no outward sensitivity to a further category head.

theorem DistributedMorphology.Spine.not_coactive_of_cyclic_of_cyclic {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (hij : i < j) (hi : cyclic s.heads[i]) (hj : cyclic s.heads[j]) : ¬s.Coactive cyclic i j

Two cyclic heads are never realized in one cycle: no fusion of category-defining heads.

theorem DistributedMorphology.Spine.not_coactive_of_add_two_le {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} (h : s.cycle cyclic j + 2 ≤ s.cycle cyclic i) : ¬s.Coactive cyclic i j

Material two cycles down is inactive: the complement of an inner cyclic head is closed off once the next cyclic head is spelled out.

Interface adjacency

def DistributedMorphology.Spine.Sees {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (null : H → Prop) (i j : Fin s.heads.length) : Prop

Head i sees head j at an interface: j is present at i's insertion and every head between them is null there — pruned for allomorphy, semantically null for allosemy.

Equations

• s.Sees cyclic null i j = (s.Coactive cyclic i j ∧ ∀ (k : Fin s.heads.length), min i j < k → k < max i j → null s.heads[k])

def DistributedMorphology.Spine.SeesRoot {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (null : H → Prop) (i : Fin s.heads.length) : Prop

Head i sees the root: it is in the first cycle and every head below it is null at the interface.

Equations

• s.SeesRoot cyclic null i = (s.RootLocal cyclic i ∧ ∀ k < i, null s.heads[k])

@[instance_reducible]

instance DistributedMorphology.Spine.instDecidableSeesOfDecidablePred {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (null : H → Prop) [DecidablePred null] (i j : Fin s.heads.length) : Decidable (s.Sees cyclic null i j)

Equations

• s.instDecidableSeesOfDecidablePred cyclic null i j = DistributedMorphology.Spine.instDecidableSeesOfDecidablePred._aux_1 s cyclic null i j

@[instance_reducible]

instance DistributedMorphology.Spine.instDecidableSeesRootOfDecidablePred {H : Type u_1} (s : Spine H) (cyclic : H → Prop) [DecidablePred cyclic] (null : H → Prop) [DecidablePred null] (i : Fin s.heads.length) : Decidable (s.SeesRoot cyclic null i)

Equations

• s.instDecidableSeesRootOfDecidablePred cyclic null i = DistributedMorphology.Spine.instDecidableSeesRootOfDecidablePred._aux_1 s cyclic null i

theorem DistributedMorphology.Spine.Sees.coactive {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} {null : H → Prop} (h : s.Sees cyclic null i j) : s.Coactive cyclic i j

theorem DistributedMorphology.Spine.SeesRoot.rootLocal {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i : Fin s.heads.length} {null : H → Prop} (h : s.SeesRoot cyclic null i) : s.RootLocal cyclic i

theorem DistributedMorphology.Spine.not_sees_of_not_null {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j k : Fin s.heads.length} {null : H → Prop} (hik : min i j < k) (hkj : k < max i j) (hk : ¬null s.heads[k]) : ¬s.Sees cyclic null i j

An intervening head that is not null at the interface blocks conditioning.

theorem DistributedMorphology.Spine.not_seesRoot_of_not_null {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i k : Fin s.heads.length} {null : H → Prop} (hki : k < i) (hk : ¬null s.heads[k]) : ¬s.SeesRoot cyclic null i

theorem DistributedMorphology.Spine.sees_congr {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i j : Fin s.heads.length} {null null' : H → Prop} (h : ∀ (k : Fin s.heads.length), min i j < k → k < max i j → (null s.heads[k] ↔ null' s.heads[k])) : s.Sees cyclic null i j ↔ s.Sees cyclic null' i j

The interface domains agree wherever the two kinds of nullness agree between the heads: one cycle bounds both.

theorem DistributedMorphology.Spine.seesRoot_congr {H : Type u_1} {s : Spine H} {cyclic : H → Prop} [DecidablePred cyclic] {i : Fin s.heads.length} {null null' : H → Prop} (h : ∀ k < i, null s.heads[k] ↔ null' s.heads[k]) : s.SeesRoot cyclic null i ↔ s.SeesRoot cyclic null' i

The idiom domain

def DistributedMorphology.Spine.IdiomLocal {H : Type u_1} (s : Spine H) (agentive : H → Prop) (i : Fin s.heads.length) : Prop

The heads below an agentive Voice: special meaning may be assigned to any structure not containing an external-argument-introducing head, across cyclic heads.

Equations

• s.IdiomLocal agentive i = ∀ j ≤ i, ¬agentive s.heads[j]

@[instance_reducible]

instance DistributedMorphology.Spine.instDecidableIdiomLocalOfDecidablePred {H : Type u_1} (s : Spine H) (agentive : H → Prop) [DecidablePred agentive] (i : Fin s.heads.length) : Decidable (s.IdiomLocal agentive i)

Equations

• s.instDecidableIdiomLocalOfDecidablePred agentive i = DistributedMorphology.Spine.instDecidableIdiomLocalOfDecidablePred._aux_1 s agentive i

theorem DistributedMorphology.Spine.IdiomLocal.of_le {H : Type u_1} {s : Spine H} {i j : Fin s.heads.length} {agentive : H → Prop} (h : s.IdiomLocal agentive i) (hji : j ≤ i) : s.IdiomLocal agentive j