Spell-out of multidominance

When Merge applies to a term a second time, the linearized object lists that term at each of its occurrences: a term remerged inside its own root, moved, stands above its lower occurrences, and a term remerged with another root, shared, stands under mothers none of which dominates another. PF pronounces each term once, under one of its highest mothers, in Gračanin-Yuksek's sense, those no other mother of it dominates. A moved term has one highest mother and is pronounced at its highest occurrence. Accounts differ over which highest mother a shared term is pronounced under: de Vries takes the one pronounced last, so that right-node raising pronounces shared material in the last conjunct, and Yip's right dislocation the one pronounced first. The choice is a parameter, a pick among a term's candidate positions in left-to-right order.

Main definitions

• Minimalist.mothers, Minimalist.IsHighestMother: the terms a term is a daughter of, and those no other mother of it dominates.
• Minimalist.candidates, Minimalist.spellOutPosition: the positions at which a term may be pronounced, and the one the pick chooses.
• Minimalist.remergedYield: the pronounced tokens, left to right.

Main statements

• Minimalist.remergedYield_perm_tokens: each token is pronounced exactly once, whatever the pick.
• Minimalist.remergedYield_eq_of_chain: where the mothers of every term are ordered by dominance, as movement leaves them, the pick makes no difference.
• Minimalist.remergedYield_getLast?_eq_tokens: where no mother of a term dominates another, as sharing leaves them, the last pick pronounces each token at its last occurrence, as tokens keeps them.

Implementation notes

• De Vries's spell-out of remerged nodes, his (56), decides at each visit of a term from which of its mothers the traversal has reached, and his algorithm (71) counts a visit that omits a term as reaching it, which can pronounce a token twice (DeVries2009). Here the choice is made once per term, and the term is silent at its other occurrences.
• Each step of the recursion moves from a term to a strictly larger mother, so the size of the object bounds it.

TODO

• A copy object pronounced at the highest occurrence of each moved term as the externalization of its contraction (Copy/Marked.lean), Nunes's chain reduction.
• The conditions that exclude structures from linearization, such as Wilder's restriction of shared material to the right edge, as predicates on objects.

References

• de Vries 2009, On multidominance and linearization formalized
• Gračanin-Yuksek 2013, Linearizing multidominance structures
• Yip 2026, Right dislocation as multidominance, and beyond