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. Here this is strict scansion: the Vocabulary is scanned once, top to bottom, and an item is inserted when one of the node's matrices bears every feature of its site, discharging one occurrence of each; scansion halts at the bottom of the list, so no item is inserted twice.

An item's site is a set of features, as applicability and specificity already treat it, while a matrix is a multiset, so that a feature borne twice is two repetitions in Marcolli, Chomsky and Berwick's sense and two items may discharge it one at a time. Lists represent both for computation, and the theorems are stated in the free commutative monoid Multiset F, where discharge is truncated subtraction and scansion a greedy decomposition of the node. A node may bear several matrices, one per argument it agrees with, as the Yucatec Agr3 agrees with both subject and object, and an item draws on one of them.

Main definitions

• discharge: remove one occurrence of each feature of an item's site from the first matrix bearing them all.
• scan, insertions, residue, scansion: the items a node's matrices receive under strict scansion with local Fission, the matrices left over, and the items' exponents.

Main results

• bind_insertions_add_residue: in the free commutative monoid on the features, the inserted items' sites and the residue sum to the node.
• bind_insertions_le, pairwise_disjoint_insertions: the inserted items' sites fit inside the node, and on a node without repetitions they are disjoint.
• head?_insertions_singleton, head?_scansion_singleton: at a single matrix the first insertion is the first applicable item, so on a Vocabulary ordered by specificity it 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
• M. Marcolli, N. Chomsky and R. C. Berwick, Mathematical Structure of Syntactic Merge

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))

Discharging an item removes one occurrence of each feature of its site from the first of the matrices bearing them all, in the environment env (whose focus is ignored), and fails when no matrix does.

Equations

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

def DistributedMorphology.scan {F : Type u_1} {E : Type u_2} [DecidableEq F] : Morphology.Exponence.RuleSet (VocabularyItem F E) → Neighborhood (List F) → List (List F) → List (VocabularyItem F E) × List (List F)

Strict scansion with local Fission at a node bearing the matrices ms in the environment env yields the items inserted, in Vocabulary order, and the matrices left over.

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.scan [] x✝¹ x✝ = ([], x✝)

def DistributedMorphology.insertions {F : Type u_1} {E : Type u_2} [DecidableEq F] (items : Morphology.Exponence.RuleSet (VocabularyItem F E)) (env : Neighborhood (List F)) (ms : List (List F)) : List (VocabularyItem F E)

insertions lists the items scansion inserts.

Equations

• DistributedMorphology.insertions items env ms = (DistributedMorphology.scan items env ms).1

def DistributedMorphology.residue {F : Type u_1} {E : Type u_2} [DecidableEq F] (items : Morphology.Exponence.RuleSet (VocabularyItem F E)) (env : Neighborhood (List F)) (ms : List (List F)) : List (List F)

residue lists the matrices scansion leaves, the features no inserted item discharged.

Equations

• DistributedMorphology.residue items env ms = (DistributedMorphology.scan items env ms).2

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

A node bearing the matrices ms in the environment env receives these exponents.

Equations

• DistributedMorphology.scansion items env ms = List.map (fun (x : DistributedMorphology.VocabularyItem F E) => x.exponent) (DistributedMorphology.insertions items env ms)

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

@[simp]

theorem DistributedMorphology.scan_nil {F : Type u_1} {E : Type u_2} [DecidableEq F] (env : Neighborhood (List F)) (ms : List (List F)) : scan [] env ms = ([], ms)

theorem DistributedMorphology.scan_cons_of_discharge_eq_some {F : Type u_1} {E : Type u_2} [DecidableEq F] {rest : Morphology.Exponence.RuleSet (VocabularyItem F E)} {env : Neighborhood (List F)} {i : VocabularyItem F E} {ms ms' : List (List F)} (h : discharge i env ms = some ms') : scan (i :: rest) env ms = (i :: insertions rest env ms', residue rest env ms')

theorem DistributedMorphology.scan_cons_of_discharge_eq_none {F : Type u_1} {E : Type u_2} [DecidableEq F] {rest : Morphology.Exponence.RuleSet (VocabularyItem F E)} {env : Neighborhood (List F)} {i : VocabularyItem F E} {ms : List (List F)} (h : discharge i env ms = none) : scan (i :: rest) env ms = scan rest env ms

theorem DistributedMorphology.val_add_discharge {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} {i : VocabularyItem F E} {ms ms' : List (List F)} : discharge i env ms = some ms' → i.site.focus.toFinset.val + ↑ms'.flatten = ↑ms.flatten

Discharge subtracts the item's site, a set of features, from the node's multiset.

theorem DistributedMorphology.bind_insertions_add_residue {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (items : Morphology.Exponence.RuleSet (VocabularyItem F E)) (ms : List (List F)) : ((↑(insertions items env ms)).bind fun (x : VocabularyItem F E) => x.site.focus.toFinset.val) + ↑(residue items env ms).flatten = ↑ms.flatten

Conservation. In the free commutative monoid on the features, the inserted items' sites and the residue sum to the node.

theorem DistributedMorphology.bind_insertions_le {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (items : Morphology.Exponence.RuleSet (VocabularyItem F E)) (ms : List (List F)) : ((↑(insertions items env ms)).bind fun (x : VocabularyItem F E) => x.site.focus.toFinset.val) ≤ ↑ms.flatten

No multiple exponence. The inserted items' sites fit inside the node, so no feature is discharged more often than the node bears it.

theorem DistributedMorphology.pairwise_disjoint_insertions {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : Morphology.Exponence.RuleSet (VocabularyItem F E)} {env : Neighborhood (List F)} {ms : List (List F)} (h : ms.flatten.Nodup) : List.Pairwise (fun (i j : VocabularyItem F E) => i.site.focus.Disjoint j.site.focus) (insertions items env ms)

On a node without repetitions the inserted items' sites are disjoint, so the items partition the features they discharge.

@[simp]

theorem DistributedMorphology.insertions_nil_right {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (items : Morphology.Exponence.RuleSet (VocabularyItem F E)) : insertions items env [] = []

A node with no matrix receives nothing.

@[simp]

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

theorem DistributedMorphology.insertions_sublist {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (items : Morphology.Exponence.RuleSet (VocabularyItem F E)) (ms : List (List F)) : (insertions items env ms).Sublist 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 : Morphology.Exponence.RuleSet (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 : Morphology.Exponence.RuleSet (VocabularyItem F E)} {env : Neighborhood (List F)} (ms : List (List F)) : (scansion items env ms).length ≤ List.length items

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.dedup] else none

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

theorem DistributedMorphology.head?_insertions_singleton {F : Type u_1} {E : Type u_2} [DecidableEq F] {env : Neighborhood (List F)} (m : List F) (items : Morphology.Exponence.RuleSet (VocabularyItem F E)) : (insertions items env [m]).head? = (items.applicable { focus := m, leftCtx := env.leftCtx, rightCtx := env.rightCtx }).head?

At a single matrix, the first item inserted is the first item that applies there.

theorem DistributedMorphology.head?_scansion_singleton {F : Type u_1} {E : Type u_2} [DecidableEq F] {items : Morphology.Exponence.RuleSet (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, so scansion agrees with Elsewhere competition where both apply.