Fission

Fission lets one syntactic node be realized in several adjacent positions of exponence: a Vocabulary Item inserted at the node discharges only the features it spells out, and the remaining features fission off to a subsidiary position where insertion continues. The procedure here is strict scansion: the Vocabulary is scanned once, top to bottom; an item whose site one of the node's feature matrices contains is inserted and its features are discharged from that matrix; the residue stays available to the items below, and scansion halts at the bottom of the list — so no item is inserted twice, with no stipulation about elsewhere items.

A node may bear several matrices, one per argument it agrees with (the Yucatec Agr3 agrees with both the ergative subject and the nominative object), and the matrices are kept apart: an item's features must all come from one of them. Features carry multiplicity (List.diff), so two arguments' shared features are discharged one at a time.

Main definitions

• discharge: remove an item's features from the first matrix containing its site.
• scansion: the exponents a node's matrices receive under strict scansion with local Fission.

Main results

• scansion_sublist: the exponents are a subsequence of the Vocabulary's — each item at most once, in list order.
• scansion_nil: a node with no matrix receives nothing.
• head?_scansion_singleton: on a Vocabulary ordered by specificity, the first insertion at a single matrix is the Subset Principle's winner.

References

• R. Noyer, Features, positions and affixes in autonomous morphological structure
• M. Halle, Distributed Morphology: Impoverishment and Fission
• A. González Poot and M. McGinnis, Local versus long-distance Fission in Distributed Morphology

def DistributedMorphology.discharge {F : Type u_1} {E : Type u_2} [DecidableEq F] (i : VocabularyItem F E) (env : Neighborhood (List F)) : List (List F) → Option (List (List F))

Discharge the item's features from the first of the matrices containing its site, in the environment env (whose focus is ignored); none when no matrix does.

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.discharge i env [] = none

def DistributedMorphology.scansion {F : Type u_1} {E : Type u_2} [DecidableEq F] (items : List (VocabularyItem F E)) (env : Neighborhood (List F)) : List (List F) → List E

Strict scansion with local Fission: the exponents received by a node bearing the matrices ms in the environment env.

Equations

• DistributedMorphology.scansion items env x✝ = DistributedMorphology.scansion.go env items x✝

def DistributedMorphology.scansion.go {F : Type u_1} {E : Type u_2} [DecidableEq F] (env : Neighborhood (List F)) : List (VocabularyItem F E) → List (List F) → List E

Scan the remaining items against the remaining matrices.

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.scansion.go env [] a✝ = []

@[simp]

theorem DistributedMorphology.discharge_nil {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (i : VocabularyItem F E) : discharge i env [] = none

theorem DistributedMorphology.scansion_go_nil {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (items : List (VocabularyItem F E)) : scansion.go env items [] = []

@[simp]

theorem DistributedMorphology.scansion_nil {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {env : Neighborhood (List F)} : scansion items env [] = []

A node with no matrix receives nothing.

theorem DistributedMorphology.scansion_go_sublist {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (items : List (VocabularyItem F E)) (ms : List (List F)) : (scansion.go env items ms).Sublist (List.map (fun (x : VocabularyItem F E) => x.exponent) items)

Each item is inserted at most once, in Vocabulary order.

theorem DistributedMorphology.scansion_sublist {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {env : Neighborhood (List F)} (ms : List (List F)) : (scansion items env ms).Sublist (List.map (fun (x : VocabularyItem F E) => x.exponent) items)

theorem DistributedMorphology.length_scansion_le {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {env : Neighborhood (List F)} (ms : List (List F)) : (scansion items env ms).length ≤ items.length

theorem DistributedMorphology.discharge_singleton {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (i : VocabularyItem F E) (m : List F) : discharge i env [m] = if i.site ⊆ { focus := m, leftCtx := env.leftCtx, rightCtx := env.rightCtx } then some [m.diff i.site.focus] else none

At a single matrix, an item discharges iff it applies there.

theorem DistributedMorphology.head?_scansion_singleton {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : List (VocabularyItem F E)} {env : Neighborhood (List F)} (m : List F) (hsorted : List.Pairwise (fun (i j : VocabularyItem F E) => j.specificity ≤ i.specificity) items) : (scansion items env [m]).head? = Option.map (fun (x : VocabularyItem F E) => x.exponent) (winner? items { focus := m, leftCtx := env.leftCtx, rightCtx := env.rightCtx })

On a Vocabulary ordered by decreasing specificity, the first insertion at a single matrix is the Subset Principle's winner: scansion agrees with Elsewhere competition where both apply.