Locality domains for contextual allomorphy and allosemy

The category-defining heads of a complex head 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

• DistributedMorphology.ComplexHead.cycle, DistributedMorphology.ComplexHead.insertionCycle: a head's cycle and the cycle of its insertion.
• DistributedMorphology.ComplexHead.Coactive, DistributedMorphology.ComplexHead.RootLocal: presence of one head at another's insertion, and of the root.
• DistributedMorphology.ComplexHead.Sees, DistributedMorphology.ComplexHead.SeesRoot: presence plus adjacency across heads null at an interface.
• DistributedMorphology.ComplexHead.lastCycle: the heads a probe merged above the word can find.
• DistributedMorphology.ComplexHead.IdiomLocal: the heads below an agentive Voice.

Main results

• 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, so there is 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

• D. Embick, Localism versus globalism in morphology and phonology
• A. Marantz, Locality domains for contextual allomorphy across the interfaces
• D. Embick, The motivation for roots in Distributed Morphology

Cycles

def DistributedMorphology.ComplexHead.cycle {R : Type u_1} {H : Type u_2} (s : ComplexHead R 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.ComplexHead.insertionCycle {R : Type u_1} {H : Type u_2} (s : ComplexHead R 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.ComplexHead.Coactive {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (cyclic : H → Prop) [DecidablePred cyclic] (i j : Fin s.heads.length) : Prop

Head j is present when head i is spelled out if 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.ComplexHead.RootLocal {R : Type u_1} {H : Type u_2} (s : ComplexHead R 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.ComplexHead.instDecidableCoactive {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (cyclic : H → Prop) [DecidablePred cyclic] (i j : Fin s.heads.length) : Decidable (s.Coactive cyclic i j)

Equations

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

@[instance_reducible]

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

Equations

• s.instDecidableRootLocal cyclic i = { decide := (s.cycle cyclic i).ble 1, reflects_decide := ⋯ }

theorem DistributedMorphology.ComplexHead.cycle_mono {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.one_le_cycle_of_cyclic {R : Type u_1} {H : Type u_2} {s : ComplexHead R H} {cyclic : H → Prop} [DecidablePred cyclic] {i : Fin s.heads.length} (hi : cyclic s.heads[i]) : 1 ≤ s.cycle cyclic i

theorem DistributedMorphology.ComplexHead.cycle_add_one_le_of_lt_of_cyclic {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.two_le_cycle_of_cyclic_of_cyclic {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.RootLocal.of_le {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.not_rootLocal_of_cyclic_of_cyclic {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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, since category change closes the root's domain.

theorem DistributedMorphology.ComplexHead.RootLocal.cyclic_first {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.coactive_self {R : Type u_1} {H : Type u_2} {s : ComplexHead R H} {cyclic : H → Prop} [DecidablePred cyclic] (i : Fin s.heads.length) : s.Coactive cyclic i i

theorem DistributedMorphology.ComplexHead.coactive_of_cycle_eq {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.not_coactive_of_lt_of_cyclic {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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, so there is no outward sensitivity to a further category head.

theorem DistributedMorphology.ComplexHead.not_coactive_of_cyclic_of_cyclic {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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, so category-defining heads do not fuse.

theorem DistributedMorphology.ComplexHead.not_coactive_of_add_two_le {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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 being closed off once the next cyclic head is spelled out.

The last cycle

Merging a cyclic head spells out the cyclic domains below it, so a probe merged above a word finds only the heads of its last cycle: the highest cyclic head and the noncyclic heads above it.

def DistributedMorphology.ComplexHead.lastCycle {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (cyclic : H → Prop) [DecidablePred cyclic] : List H

The heads of the last cycle, outermost first, which are the noncyclic heads above the highest cyclic head and that head.

Equations

• s.lastCycle cyclic = List.takeWhile (fun (h : H) => !decide (cyclic h)) s.heads.reverse ++ List.take 1 (List.dropWhile (fun (h : H) => !decide (cyclic h)) s.heads.reverse)

theorem DistributedMorphology.ComplexHead.lastCycle_mk_append {R : Type u_1} {H : Type u_2} {cyclic : H → Prop} [DecidablePred cyclic] {r : R} {hs above : List H} {h : H} (hc : cyclic h) (ha : ∀ a ∈ above, ¬cyclic a) : { root := r, heads := hs ++ h :: above }.lastCycle cyclic = above.reverse ++ [h]

The last cycle of a word whose highest cyclic head is h, with the noncyclic heads above over it.

Interface adjacency

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

Head i sees head j at an interface when j is present at i's insertion and every head between them is null there, pruned for allomorphy and 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.ComplexHead.SeesRoot {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (cyclic : H → Prop) [DecidablePred cyclic] (null : H → Prop) (i : Fin s.heads.length) : Prop

Head i sees the root when 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.ComplexHead.instDecidableSeesOfDecidablePred {R : Type u_1} {H : Type u_2} (s : ComplexHead R 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

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

@[instance_reducible]

instance DistributedMorphology.ComplexHead.instDecidableSeesRootOfDecidablePred {R : Type u_1} {H : Type u_2} (s : ComplexHead R 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 = { decide := decide (s.RootLocal cyclic i) && decide (∀ k < i, null s.heads[k]), reflects_decide := ⋯ }

theorem DistributedMorphology.ComplexHead.Sees.coactive {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.SeesRoot.rootLocal {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.not_sees_of_not_null {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.not_seesRoot_of_not_null {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.sees_congr {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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 bounding both.

theorem DistributedMorphology.ComplexHead.seesRoot_congr {R : Type u_1} {H : Type u_2} {s : ComplexHead R 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.ComplexHead.IdiomLocal {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (agentive : H → Prop) (i : Fin s.heads.length) : Prop

The heads below an agentive Voice, to whose structure special meaning may be assigned across cyclic heads.

Equations

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

@[instance_reducible]

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

Equations

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

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