Arregi and Pietraszko (2021): The ups and downs of head displacement

Arregi and Pietraszko replace head raising and lowering by one syntactic operation, Generalized Head Movement, in which a head shares its M-value, the morphological features that Vocabulary Insertion spells out, with the head of its complement. The heads of a clause thus form a head chain around one complex head, pronounced in the chain's highest strong position, or in its highest position if none is strong. A chain that ends in a strong verb splits when a specifier intervenes or the verb phrase is elided or fronted, and the verb's terminal, an orphan in the half without the verb, is exponed as do.

Main statements

• HeadChain.terminals_ofHeads, HeadChain.isLeftComb_mvalue_ofHeads: the Mirror Principle, the terminals of a complex head ordered as its heads are, each attached outside the complex head of the heads below it.
• doSupport_iff: do-support arises exactly where the chain of a strong verb splits, whether the complex head is otherwise pronounced low or high.
• fronted_forms: the finite, pseudo-infinitive, infinitive and bare forms of a fronted verb are what Vocabulary Insertion gives when its orphan T is ignored, disregarded at its own insertion, impoverished or obliterated.
• mirror_class9, mul_not_assoc: regular vowel coalescence derives the Ndebele class 9 relative prefix from the Mirror-obeying complex head and not from another bracketing of the same terminals, which it could not tell apart if it were associative.

Implementation notes

• A Context holds what head displacement sees of a clause: the heads related to the verb, whether a pronounced specifier intervenes, and what becomes of the verb phrase. A negative imperative, where Σ keeps C out of the verb's chain, is thereby the context of a declarative.
• Split-by-Deletion applies in every language, the possibility the paper raises for its typology of splitting; Split-by-Intervention is a setting.
• A language's settings record what the paper's data settle, so the fate of an orphan T is absent where no do-support or fronting datum shows it. The fates are the library's impoverishment and obliteration rules, and the elsewhere exponent comes from impoverishing the orphan at its own insertion only, which leaves its features to condition the stem.
• An M-value is an element of the free magma over the terminals, each product listing the lower constituent first. The operation leaves linear order open, and only the Ndebele prefix is linearized. Negative Merger applies to a chain, which makes its terminal an orphan there, an ordering the paper notes is indistinguishable from its own.

References

• [AP21]
• [Bak85]
• [Pol89]
• [HG19]
• [AN12]

Head chains

inductive ArregiPietraszko2021.Head : Type

The syntactic terminals of the paper's derivations are the lexical verb, an auxiliary, Σ, T, C, the D and linker heads above an Ndebele relative clause, and the negation in the specifier of ΣP.

• V : Head
• Aux : Head
• sigma : Head
• T : Head
• C : Head
• D : Head
• Lnk : Head
• Neg : Head

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableEqHead : DecidableEq Head

Equations

• ArregiPietraszko2021.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArregiPietraszko2021.instReprHead : Repr Head

Equations

• ArregiPietraszko2021.instReprHead = { reprPrec := ArregiPietraszko2021.instReprHead.repr }

def ArregiPietraszko2021.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

structure ArregiPietraszko2021.HeadChain : Type

A head chain is a sequence of syntactic terminals, lowest first, that share one M-value, a complex head over morphological terminals.

• positions : List Head
• mvalue : FreeMagma Head

def ArregiPietraszko2021.HeadChain.terminals (c : HeadChain) : List Head

The morphological terminals of the M-value, lowest first.

Equations

• c.terminals = FreeMonoid.toList ((FreeMagma.lift FreeMonoid.of) c.mvalue)

def ArregiPietraszko2021.HeadChain.extend (x : Head) (c : HeadChain) : HeadChain

Generalized Head Movement, GenHM, relates a head to the chain of its complement's head. The head joins the chain, and its morphological terminal attaches outside the shared M-value.

Equations

• ArregiPietraszko2021.HeadChain.extend x c = { positions := c.positions ++ [x], mvalue := c.mvalue * FreeMagma.of x }

def ArregiPietraszko2021.HeadChain.ofHeads (bottom : Head) (above : List Head) : HeadChain

The chain that cyclic GenHM builds from bottom up through the heads above.

Equations

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

theorem ArregiPietraszko2021.HeadChain.extend_ofHeads (bottom x : Head) (above : List Head) : extend x (ofHeads bottom above) = ofHeads bottom (above ++ [x])

theorem ArregiPietraszko2021.HeadChain.terminals_ofHeads (bottom : Head) (above : List Head) : (ofHeads bottom above).terminals = bottom :: above

By the Mirror Principle, the terminals of a complex head are ordered as its heads are.

theorem ArregiPietraszko2021.HeadChain.isLeftComb_mvalue_ofHeads (bottom : Head) (above : List Head) : (ofHeads bottom above).mvalue.IsLeftComb

GenHM derives the Mirror Principle: each terminal of a complex head attaches outside the complex head of the heads below it.

def ArregiPietraszko2021.HeadChain.Orphan (c : HeadChain) (x : Head) : Prop

Orphan Assignment marks a morphological terminal in a chain that does not contain its syntactic terminal.

Equations

• c.Orphan x = (x ∈ c.terminals ∧ x ∉ c.positions)

@[instance_reducible]

instance ArregiPietraszko2021.HeadChain.instDecidableOrphan (c : HeadChain) (x : Head) : Decidable (c.Orphan x)

Equations

• c.instDecidableOrphan x = { decide := decide (x ∈ c.terminals) && decide (x ∉ c.positions), reflects_decide := ⋯ }

theorem ArregiPietraszko2021.HeadChain.not_orphan_ofHeads (bottom x : Head) (above : List Head) : ¬(ofHeads bottom above).Orphan x

GenHM creates no orphans.

def ArregiPietraszko2021.HeadChain.pronounced (strong : Finset Head) (c : HeadChain) : Option Head

Head Chain Pronunciation delinks every position of a chain but its highest strong one, or its highest if none is strong.

Equations

• ArregiPietraszko2021.HeadChain.pronounced strong c = (List.filter (fun (x : ArregiPietraszko2021.Head) => decide (x ∈ strong)) c.positions).getLast?.or c.positions.getLast?

theorem ArregiPietraszko2021.HeadChain.mem_positions_of_pronounced {strong : Finset Head} {c : HeadChain} {x : Head} (h : pronounced strong c = some x) : x ∈ c.positions

theorem ArregiPietraszko2021.HeadChain.pronounced_of_forall_not_mem {strong : Finset Head} {c : HeadChain} (h : ∀ x ∈ c.positions, x ∉ strong) : pronounced strong c = c.positions.getLast?

A chain with no strong position is pronounced in its highest, the effect of upward displacement.

theorem ArregiPietraszko2021.HeadChain.pronounced_extend_of_mem {strong : Finset Head} {x : Head} (hx : x ∈ strong) (c : HeadChain) : pronounced strong (extend x c) = some x

A chain extended by a strong head is pronounced there, wherever it was pronounced before: downward displacement feeds upward displacement.

Languages

inductive ArregiPietraszko2021.OrphanFate : Type

The fate of an orphan T at spell-out. The mark of an orphan does nothing to it, or makes insertion at it disregard its tense and agreement, or impoverishes them, or obliterates the terminal.

• ignored : OrphanFate
• elsewhere : OrphanFate
• impoverished : OrphanFate
• obliterated : OrphanFate

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableEqOrphanFate : DecidableEq OrphanFate

Equations

• ArregiPietraszko2021.instDecidableEqOrphanFate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArregiPietraszko2021.instReprOrphanFate : Repr OrphanFate

Equations

• ArregiPietraszko2021.instReprOrphanFate = { reprPrec := ArregiPietraszko2021.instReprOrphanFate.repr }

def ArregiPietraszko2021.instReprOrphanFate.repr : OrphanFate → ℕ → Std.Format

Equations

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

structure ArregiPietraszko2021.Language : Type

The settings of a language.

• strong : Finset Head

  The strong terminals, the positions that hold the pronunciation of a chain down.

• splitByIntervention : Bool

  Whether a chain splits at a strong verb below an intervening specifier.

• adverbialNegation : Bool

  Whether sentential negation is an adverbial, not the specifier of ΣP.

• orphanT : Option OrphanFate

  The fate of an orphan T.

def ArregiPietraszko2021.english : Language

English has strong lexical verbs and Split-by-Intervention, and obliterates an orphan T.

Equations

• ArregiPietraszko2021.english = { strong := {ArregiPietraszko2021.Head.V}, splitByIntervention := true, orphanT := some ArregiPietraszko2021.OrphanFate.obliterated }

def ArregiPietraszko2021.french : Language

French has no strong head.

Equations

• ArregiPietraszko2021.french = { }

def ArregiPietraszko2021.danish : Language

Danish has strong verbs, auxiliaries among them, and a strong C, and no Split-by-Intervention.

Equations

• ArregiPietraszko2021.danish = { strong := {ArregiPietraszko2021.Head.V, ArregiPietraszko2021.Head.Aux, ArregiPietraszko2021.Head.C} }

def ArregiPietraszko2021.swedish : Language

Swedish has the Danish settings and ignores an orphan T.

Equations

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

def ArregiPietraszko2021.monnese : Language

Monnese has strong lexical verbs, T and C, and Split-by-Intervention; its negation is an adverbial, and it impoverishes an orphan T.

Equations

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

def ArregiPietraszko2021.polish : Language

Polish has weak verbs and impoverishes an orphan T.

Equations

• ArregiPietraszko2021.polish = { orphanT := some ArregiPietraszko2021.OrphanFate.impoverished }

def ArregiPietraszko2021.hebrew : Language

Hebrew has weak verbs and impoverishes an orphan T.

Equations

• ArregiPietraszko2021.hebrew = { orphanT := some ArregiPietraszko2021.OrphanFate.impoverished }

def ArregiPietraszko2021.yiddish : Language

Yiddish has weak verbs and gives an orphan T its elsewhere exponent.

Equations

• ArregiPietraszko2021.yiddish = { orphanT := some ArregiPietraszko2021.OrphanFate.elsewhere }

def ArregiPietraszko2021.spanish : Language

Spanish has no strong head in imperatives.

Equations

• ArregiPietraszko2021.spanish = { }

def ArregiPietraszko2021.vallader : Language

The Vallader of Scuol has a strong imperative T.

Equations

• ArregiPietraszko2021.vallader = { strong := {ArregiPietraszko2021.Head.T} }

def ArregiPietraszko2021.ndebele : Language

Ndebele has a strong T.

Equations

• ArregiPietraszko2021.ndebele = { strong := {ArregiPietraszko2021.Head.T} }

The spell-out of orphans

inductive ArregiPietraszko2021.Feat : Type

The features of the terminals of a verbal word are the verb, T with its tense and agreement, negation, and the mark of an orphan.

• verb : Feat
• T : Feat
• tense : Feat
• agr : Feat
• neg : Feat
• orphan : Feat

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableEqFeat : DecidableEq Feat

Equations

• ArregiPietraszko2021.instDecidableEqFeat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArregiPietraszko2021.instReprFeat : Repr Feat

Equations

• ArregiPietraszko2021.instReprFeat = { reprPrec := ArregiPietraszko2021.instReprFeat.repr }

def ArregiPietraszko2021.instReprFeat.repr : Feat → ℕ → Std.Format

Equations

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

inductive ArregiPietraszko2021.Piece : Type

The pieces of a verbal word are the stem, the allomorph of the stem that tense conditions, the dummy verb, the finite and the infinitival exponent of T, and contracted negation.

• stem : Piece
• finiteStem : Piece
• dummy : Piece
• finite : Piece
• infinitival : Piece
• contracted : Piece

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableEqPiece : DecidableEq Piece

Equations

• ArregiPietraszko2021.instDecidableEqPiece x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArregiPietraszko2021.instReprPiece : Repr Piece

Equations

• ArregiPietraszko2021.instReprPiece = { reprPrec := ArregiPietraszko2021.instReprPiece.repr }

def ArregiPietraszko2021.instReprPiece.repr : Piece → ℕ → Std.Format

Equations

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

def ArregiPietraszko2021.vocabulary : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem Feat Piece)

The Vocabulary of a verbal word. An orphan verb is the dummy verb, a verb beside a T that bears tense takes the allomorph that tense conditions, and the infinitival exponent is the elsewhere exponent of T.

Equations

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

theorem ArregiPietraszko2021.subsetPrinciple_eq_dummy_iff {n : DistributedMorphology.Neighborhood (List Feat)} (hT : Feat.T ∉ n.focus) : DistributedMorphology.subsetPrinciple vocabulary n = some Piece.dummy ↔ Feat.verb ∈ n.focus ∧ Feat.orphan ∈ n.focus

The dummy verb is inserted exactly at an orphan verb, whatever stands beside it.

def ArregiPietraszko2021.impoverishment : List (DistributedMorphology.ImpoverishmentRule (List Feat) Feat)

Impoverishment deletes the tense and the agreement of an orphan T.

Equations

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

def ArregiPietraszko2021.impoverish (n : DistributedMorphology.Neighborhood (List Feat)) : List Feat

The focus of a neighborhood after impoverishment.

Equations

• ArregiPietraszko2021.impoverish n = DistributedMorphology.runChain (DistributedMorphology.ImpoverishmentRule.apply List.erase) ArregiPietraszko2021.impoverishment n

def ArregiPietraszko2021.obliteration : DistributedMorphology.ObliterationRule (List Feat)

Obliteration deletes an orphan T.

Equations

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

def ArregiPietraszko2021.insertion : DistributedMorphology.Spellout (List Feat) Piece

Vocabulary Insertion at each terminal of a word, with no rule before it.

Equations

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

def ArregiPietraszko2021.OrphanFate.spellout : OrphanFate → DistributedMorphology.Spellout (List Feat) Piece

The spell-out of a word under each fate of an orphan T. Impoverishment applies before insertion, or to the orphan at its own insertion only, where its features still condition the stem beside it.

Equations

• ArregiPietraszko2021.OrphanFate.ignored.spellout = ArregiPietraszko2021.insertion
• ArregiPietraszko2021.OrphanFate.elsewhere.spellout = DistributedMorphology.Spellout.rewriteAt ArregiPietraszko2021.impoverish ArregiPietraszko2021.insertion
• ArregiPietraszko2021.OrphanFate.impoverished.spellout = DistributedMorphology.Spellout.rewriteBefore ArregiPietraszko2021.impoverish ArregiPietraszko2021.insertion
• ArregiPietraszko2021.OrphanFate.obliterated.spellout = { modules := [ArregiPietraszko2021.obliteration.apply], insert := ArregiPietraszko2021.insertion.insert }

def ArregiPietraszko2021.Head.feats : Head → Option (List Feat)

The features of a terminal that has an exponent in a verbal word.

Equations

• ArregiPietraszko2021.Head.V.feats = some [ArregiPietraszko2021.Feat.verb]
• ArregiPietraszko2021.Head.Aux.feats = some [ArregiPietraszko2021.Feat.verb]
• ArregiPietraszko2021.Head.T.feats = some [ArregiPietraszko2021.Feat.T, ArregiPietraszko2021.Feat.tense, ArregiPietraszko2021.Feat.agr]
• ArregiPietraszko2021.Head.Neg.feats = some [ArregiPietraszko2021.Feat.neg]
• x✝.feats = none

def ArregiPietraszko2021.HeadChain.domain (c : HeadChain) : DistributedMorphology.SpelloutDomain (List Feat)

c.domain is the word of c as Vocabulary Insertion meets it, its terminals that have exponents, each with the mark of an orphan if it is one.

Equations

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

def ArregiPietraszko2021.HeadChain.word (L : Language) (c : HeadChain) : Option (List (List Piece))

The pieces of the word that a chain is pronounced as, terminal by terminal, or none where its T is an orphan and what the language does to an orphan T is not recorded.

Equations

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

theorem ArregiPietraszko2021.fronted_forms : have fronted := { positions := [Head.V], mvalue := (HeadChain.ofHeads Head.V [Head.T]).mvalue }; OrphanFate.ignored.spellout.pf fronted.domain = [[Piece.finiteStem], [Piece.finite]] ∧ OrphanFate.elsewhere.spellout.pf fronted.domain = [[Piece.finiteStem], [Piece.infinitival]] ∧ OrphanFate.impoverished.spellout.pf fronted.domain = [[Piece.stem], [Piece.infinitival]] ∧ OrphanFate.obliterated.spellout.pf fronted.domain = [[Piece.stem]]

The four fates of an orphan T give the four forms of a fronted verb: a finite verb where the orphan is ignored, the infinitival exponent on the stem that tense conditions where insertion disregards the features of the orphan, a true infinitive under impoverishment, and a bare stem under obliteration.

Contexts and chain splitting

inductive ArregiPietraszko2021.VPFate : Type

A verb phrase is pronounced in place, elided, or fronted.

• inSitu : VPFate
• elided : VPFate
• fronted : VPFate

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableEqVPFate : DecidableEq VPFate

Equations

• ArregiPietraszko2021.instDecidableEqVPFate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArregiPietraszko2021.instReprVPFate : Repr VPFate

Equations

• ArregiPietraszko2021.instReprVPFate = { reprPrec := ArregiPietraszko2021.instReprVPFate.repr }

def ArregiPietraszko2021.instReprVPFate.repr : VPFate → ℕ → Std.Format

Equations

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

structure ArregiPietraszko2021.Context : Type

A context holds what head displacement sees of a clause.

• above : List Head

  The heads GenHM relates to the verb, lowest first.

• intervener : Bool

  Whether a pronounced specifier intervenes between the highest of them and the verb.

• vp : VPFate

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableEqContext : DecidableEq Context

Equations

• ArregiPietraszko2021.instDecidableEqContext = ArregiPietraszko2021.instDecidableEqContext.decEq

def ArregiPietraszko2021.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance ArregiPietraszko2021.instReprContext : Repr Context

Equations

• ArregiPietraszko2021.instReprContext = { reprPrec := ArregiPietraszko2021.instReprContext.repr }

def ArregiPietraszko2021.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

def ArregiPietraszko2021.Context.declarative : Context

T is related to the verb, with no specifier between them.

Equations

• ArregiPietraszko2021.Context.declarative = { above := [ArregiPietraszko2021.Head.T] }

def ArregiPietraszko2021.Context.polarity : Context

Σ stands between T and the verb, and its specifier, negation or verum focus, intervenes.

Equations

• ArregiPietraszko2021.Context.polarity = { above := [ArregiPietraszko2021.Head.sigma, ArregiPietraszko2021.Head.T], intervener := true }

def ArregiPietraszko2021.Context.negation (L : Language) : Context

Sentential negation in a language.

Equations

• ArregiPietraszko2021.Context.negation L = if L.adverbialNegation = true then ArregiPietraszko2021.Context.declarative else ArregiPietraszko2021.Context.polarity

def ArregiPietraszko2021.Context.toC : Context

C is related to T and no pronounced specifier intervenes, as in a subject question, whose Spec,TP holds a lower copy, a subject-initial verb-second clause, and an affirmative imperative.

Equations

• ArregiPietraszko2021.Context.toC = { above := [ArregiPietraszko2021.Head.T, ArregiPietraszko2021.Head.C] }

def ArregiPietraszko2021.Context.inversion : Context

C is related to T across the subject in Spec,TP.

Equations

• ArregiPietraszko2021.Context.inversion = { above := ArregiPietraszko2021.Context.toC.above, intervener := true, vp := ArregiPietraszko2021.Context.toC.vp }

def ArregiPietraszko2021.Splits (L : Language) (cx : Context) (verb : Head) : Prop

A chain that ends in a strong verb splits at the verb when the language has Split-by-Intervention and a specifier intervenes, or when the verb is unpronounced under ellipsis or as the lower copy of a fronted verb phrase.

Equations

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

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableSplits (L : Language) (cx : Context) (verb : Head) : Decidable (Splits L cx verb)

Equations

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

structure ArregiPietraszko2021.Chains : Type

The head chains of a clause at Spell-Out.

• verb : HeadChain

  The chain of the verb's own position.

• finite : HeadChain

  The chain of the highest head, whose word carries finite inflection.

• fronted : Option HeadChain

  The chain of the verb in a fronted copy of the verb phrase.

def ArregiPietraszko2021.derive (L : Language) (cx : Context) (verb : Head) : Chains

derive L cx verb holds the chains of a clause. GenHM relates the verb to the heads above it, a split leaves the verb alone in one half, and a fronted verb phrase carries a copy of the verb with the whole M-value.

Equations

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

def ArregiPietraszko2021.Chains.finitePosition (L : Language) (d : Chains) : Option Head

The position in which the finite word is pronounced.

Equations

• ArregiPietraszko2021.Chains.finitePosition L d = ArregiPietraszko2021.HeadChain.pronounced L.strong d.finite

def ArregiPietraszko2021.Chains.DoSupport (d : Chains) : Prop

The finite word contains an orphan verb, exponed as do.

Equations

• d.DoSupport = d.finite.Orphan ArregiPietraszko2021.Head.V

@[instance_reducible]

instance ArregiPietraszko2021.Chains.instDecidableDoSupport (d : Chains) : Decidable d.DoSupport

Equations

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

def ArregiPietraszko2021.Chains.HasC (d : Chains) : Prop

The verb's M-value contains C, which conditions the imperative allomorphs of the verb.

Equations

• d.HasC = (ArregiPietraszko2021.Head.C ∈ d.verb.terminals)

@[instance_reducible]

instance ArregiPietraszko2021.Chains.instDecidableHasC (d : Chains) : Decidable d.HasC

Equations

• d.instDecidableHasC = { decide := decide (List.elem ArregiPietraszko2021.Head.C d.verb.terminals = true), reflects_decide := ⋯ }

theorem ArregiPietraszko2021.splits_of_doSupport {L : Language} {cx : Context} {verb : Head} (h : (derive L cx verb).DoSupport) : Splits L cx verb

theorem ArregiPietraszko2021.doSupport_iff {L : Language} {cx : Context} {verb : Head} (h : Head.V ∉ cx.above) : (derive L cx verb).DoSupport ↔ Splits L cx verb

Do-support arises exactly where the chain of a strong verb splits.

theorem ArregiPietraszko2021.not_doSupport_aux {L : Language} {cx : Context} : ¬(derive L cx Head.Aux).DoSupport

No auxiliary takes do-support.

theorem ArregiPietraszko2021.doSupport_iff_strong_of_ne_inSitu {L : Language} {cx : Context} (h : Head.V ∉ cx.above) (hne : cx.above ≠ []) (hvp : cx.vp ≠ VPFate.inSitu) : (derive L cx Head.V).DoSupport ↔ Head.V ∈ L.strong

Under ellipsis and fronting a strong verb takes do-support and a weak verb is stranded.

theorem ArregiPietraszko2021.doSupport_iff_of_intervener {L : Language} {cx : Context} (h : Head.V ∉ cx.above) (hne : cx.above ≠ []) (hvp : cx.vp = VPFate.inSitu) (hi : cx.intervener = true) : (derive L cx Head.V).DoSupport ↔ Head.V ∈ L.strong ∧ L.splitByIntervention = true

Below an intervening specifier a verb takes do-support exactly when it is strong and the language has Split-by-Intervention.

theorem ArregiPietraszko2021.finitePosition_declarative {L : Language} (hT : Head.T ∉ L.strong) : Chains.finitePosition L (derive L Context.declarative Head.V) = some (if Head.V ∈ L.strong then Head.V else Head.T)

Below a weak T a verb is pronounced in V when it is strong and in T when it is weak, so the verbs of English and Danish are low for one reason.

theorem ArregiPietraszko2021.danish_verb_second : Chains.finitePosition danish (derive danish Context.declarative Head.V) = some Head.V ∧ Chains.finitePosition danish (derive danish Context.inversion Head.V) = some Head.C

The complex head of a Danish clause is pronounced in V without C and in C with it, never in T: each step of GenHM is local, and the strong positions are not adjacent.

theorem ArregiPietraszko2021.directionality_no_correlation : Chains.finitePosition english (derive english Context.declarative Head.V) = some Head.V ∧ Chains.finitePosition monnese (derive monnese Context.declarative Head.V) = some Head.T ∧ (derive english Context.inversion Head.V).DoSupport ∧ (derive monnese Context.inversion Head.V).DoSupport

Do-support alternates with downward displacement in English and with upward displacement in Monnese: without an intervener the English verb is pronounced in V and the Monnese verb in T, and both take do-support under inversion.

theorem ArregiPietraszko2021.danish_do_support : (derive danish (have __src := Context.toC; { above := __src.above, intervener := __src.intervener, vp := VPFate.elided }) Head.V).DoSupport ∧ ¬(derive danish Context.inversion Head.V).DoSupport

Danish has do-support under ellipsis in a verb-second clause, where its verb is otherwise pronounced in C, and none under inversion.

theorem ArregiPietraszko2021.monnese_ellipsis : (derive monnese (have __src := Context.declarative; { above := __src.above, intervener := __src.intervener, vp := VPFate.elided }) Head.V).DoSupport

The paper predicts of Monnese, which has no attested verb phrase ellipsis, that under ellipsis its verb would take do-support though it is otherwise pronounced in T.

theorem ArregiPietraszko2021.imperatives : Chains.finitePosition spanish (derive spanish Context.toC Head.V) = some Head.C ∧ Chains.finitePosition vallader (derive vallader Context.toC Head.V) = some Head.T ∧ ∀ (L : Language), (derive L Context.toC Head.V).HasC ∧ ¬(derive L Context.declarative Head.V).HasC

Negation blocks the relation of the verb to C in an imperative whether that relation would displace the verb upward, as in Spanish, or downward, as in Vallader: the affirmative verb has C in its M-value and is pronounced in C in Spanish and in T in Vallader.

Negative Merger

def ArregiPietraszko2021.HeadChain.negativeMerger (c : HeadChain) : HeadChain

Negative Merger, a postsyntactic rule, adjoins the M-value of the negation in the specifier of ΣP to the M-value of a chain that contains Σ, outside what GenHM has built.

Equations

• c.negativeMerger = if ArregiPietraszko2021.Head.sigma ∈ c.positions then { positions := c.positions, mvalue := c.mvalue * FreeMagma.of ArregiPietraszko2021.Head.Neg } else c

theorem ArregiPietraszko2021.HeadChain.terminals_negativeMerger {c : HeadChain} (h : Head.sigma ∈ c.positions) : c.negativeMerger.terminals = c.terminals ++ [Head.Neg]

def ArregiPietraszko2021.Chains.negativeMerger (d : Chains) : Chains

Negative Merger in a clause applies to each chain that contains Σ.

Equations

• d.negativeMerger = { verb := d.verb.negativeMerger, finite := d.finite.negativeMerger, fronted := d.fronted }

theorem ArregiPietraszko2021.Chains.doSupport_negativeMerger (d : Chains) : d.negativeMerger.DoSupport ↔ d.DoSupport

Contracted negation takes do-support exactly where full negation does.

theorem ArregiPietraszko2021.Chains.finitePosition_negativeMerger (L : Language) (d : Chains) : finitePosition L d.negativeMerger = finitePosition L d

theorem ArregiPietraszko2021.contracted_negation : have negated := (derive english (Context.negation english) Head.V).negativeMerger; have question := { above := [Head.sigma, Head.T, Head.C], intervener := true }; HeadChain.word english negated.finite = some [[Piece.dummy], [Piece.finite], [Piece.contracted]] ∧ HeadChain.word english negated.verb = some [[Piece.stem]] ∧ HeadChain.word english (derive english (Context.negation english) Head.Aux).negativeMerger.finite = some [[Piece.finiteStem], [Piece.finite], [Piece.contracted]] ∧ Chains.finitePosition english (derive english question Head.V).negativeMerger = some Head.C

With a lexical verb the finite word is the dummy verb, its inflection, and contracted negation outside both, and the verb is bare. With an auxiliary the negation is outside the inflection of the auxiliary. In a negative question the word is pronounced in C.

theorem ArregiPietraszko2021.negation_outside_inflection : HeadChain.word english (HeadChain.ofHeads Head.Aux [Head.Neg, Head.T]) = some [[Piece.stem], [Piece.contracted], [Piece.finite]] ∧ (HeadChain.ofHeads Head.Aux [Head.sigma, Head.T]).negativeMerger.terminals = [Head.Aux, Head.sigma, Head.T, Head.Neg]

Were contracted negation a head between T and the verb, GenHM would put its terminal inside the inflection, the order the paper stars. Negative Merger applies after syntax, so its terminal is outside every terminal of the chain, though the negation stands below T.

def ArregiPietraszko2021.segmentPieces : List (String × Piece)

The pieces that the segments of the paper's contracted forms write.

Equations

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

def ArregiPietraszko2021.verbHead : Forms.Verb → Head

The head the paper takes a contracted form's verb to be.

Equations

• ArregiPietraszko2021.verbHead ArregiPietraszko2021.Forms.Verb.dummy = ArregiPietraszko2021.Head.V
• ArregiPietraszko2021.verbHead ArregiPietraszko2021.Forms.Verb.auxiliary = ArregiPietraszko2021.Head.Aux

theorem ArregiPietraszko2021.contracted_forms (a : Forms.Analysis) : a ∈ Forms.analyses → a.form.languageId = "stan1293" → ∃ verb ∈ Option.map verbHead a.verb, HeadChain.word english (derive english (Context.negation english) verb).negativeMerger.finite = some (List.map (fun (s : String) => (List.lookup s segmentPieces).toList) a.form.segments)

The paper's doe-s-n't and ha-d-n't have their pieces in the order that Negative Merger derives.

The paper's examples

def ArregiPietraszko2021.languages : List (String × Language)

The settings of a row's language, by Glottocode.

Equations

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

def ArregiPietraszko2021.contexts (L : Language) : List (String × Context)

The context each label of the rows names in a language. The elided verb-second clause is subject-initial, and in the fronting ones the subject follows the finite verb.

Equations

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

def ArregiPietraszko2021.headLabels : List (String × Head)

The rows' labels for positions, verb forms and truth values.

Equations

• ArregiPietraszko2021.headLabels = [("V", ArregiPietraszko2021.Head.V), ("T", ArregiPietraszko2021.Head.T), ("C", ArregiPietraszko2021.Head.C)]

def ArregiPietraszko2021.formLabels : List (String × List (List Piece))

The rows' labels for positions, verb forms and truth values.

Equations

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

def ArregiPietraszko2021.boolLabels : List (String × Bool)

The rows' labels for positions, verb forms and truth values.

Equations

• ArregiPietraszko2021.boolLabels = [("true", true), ("false", false)]

def ArregiPietraszko2021.Agrees {α : Type u_1} (r : Datum) (key : String) (table : List (String × α)) (y : Option α) : Prop

A row that records key records under it the value y.

Equations

• ArregiPietraszko2021.Agrees r key table y = (r.feature? key = none ∨ ∃ x ∈ r.parse? key table, y = some x)

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableAgreesOfDecidableEq {α : Type u_1} [DecidableEq α] (r : Datum) (key : String) (table : List (String × α)) (y : Option α) : Decidable (Agrees r key table y)

Equations

• ArregiPietraszko2021.instDecidableAgreesOfDecidableEq r key table y = { decide := decide (r.feature? key = none) || decide (∃ x ∈ r.parse? key table, y = some x), reflects_decide := ⋯ }

def ArregiPietraszko2021.Chains.Matches (L : Language) (d : Chains) (r : Datum) : Prop

The surface properties a row records are those of the chains.

Equations

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

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableMatches (L : Language) (d : Chains) (r : Datum) : Decidable (Chains.Matches L d r)

Equations

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

def ArregiPietraszko2021.derivation? (r : Datum) : Option (Language × Chains)

The settings of a row's language and the chains of its clause.

Equations

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

theorem ArregiPietraszko2021.rows_derived (r : Datum) : r ∈ Examples.all → r.language ≠ "nort2795" → ∃ p ∈ derivation? r, Chains.Matches p.1 p.2 r

Every verb placement, do-support, imperative, ellipsis and fronting example of the paper surfaces as the settings of its language derive.

theorem ArregiPietraszko2021.split_words : HeadChain.word english (derive english (Context.negation english) Head.V).finite = some [[Piece.dummy], [Piece.finite]] ∧ HeadChain.word english (derive english (Context.negation english) Head.V).verb = some [[Piece.stem]] ∧ HeadChain.word monnese (derive monnese Context.inversion Head.V).verb = some [[Piece.stem], [Piece.infinitival]]

A split chain is pronounced as two words. Under English negation the higher is the dummy verb with finite inflection and the lower a bare stem, and under Monnese inversion the lower is an infinitive.

Pollock's paradigm

def ArregiPietraszko2021.ofPollock : Pollock1989.Language → Language

The settings of the languages Pollock compares.

Equations

• ArregiPietraszko2021.ofPollock Pollock1989.Language.french = ArregiPietraszko2021.french
• ArregiPietraszko2021.ofPollock Pollock1989.Language.english = ArregiPietraszko2021.english

theorem ArregiPietraszko2021.pollock_finite (l : Pollock1989.Language) (v : Pollock1989.Verb) : have verb := match v with | Pollock1989.Verb.lexical => Head.V | Pollock1989.Verb.auxiliary => Head.Aux; (Chains.finitePosition (ofPollock l) (derive (ofPollock l) Context.declarative verb) = some Head.T ↔ Pollock1989.top { language := l, finite := true } v = Pollock1989.Height.tense) ∧ ((derive (ofPollock l) (Context.negation (ofPollock l)) verb).DoSupport ↔ Pollock1989.NeedsDo { language := l, finite := true } v)

In the finite clauses of French and English the finite word is pronounced in T exactly where Pollock's verb reaches T, and negation brings do-support exactly where his tense affix needs do: a strong verb is a verb below his opaque Agr.

Ndebele relative prefixes

def ArregiPietraszko2021.relative : HeadChain

The chain of an Ndebele relative clause holds T, a null C, the augment in D and the linker.

Equations

• ArregiPietraszko2021.relative = ArregiPietraszko2021.HeadChain.ofHeads ArregiPietraszko2021.Head.T [ArregiPietraszko2021.Head.C, ArregiPietraszko2021.Head.D, ArregiPietraszko2021.Head.Lnk]

theorem ArregiPietraszko2021.relative_low : HeadChain.pronounced ndebele.strong relative = some Head.T ∧ ∀ r ∈ Examples.all, Agrees r "relPrefixPosition" headLabels (HeadChain.pronounced ndebele.strong relative)

The relative prefix is pronounced low, in the strong T below the subject, as the example with an overt subject shows.

def ArregiPietraszko2021.resolve (j : Phonology.Hiatus.Juncture) : List Phonology.Segment

Where two vowels meet, identical vowels merge, /a/ coalesces with a following /i/ into /e/ and with a following /u/ into /o/, and /e/ elides before a vowel.

Equations

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

def ArregiPietraszko2021.join (x y : List Phonology.Segment) : List Phonology.Segment

Two exponents joined, with the hiatus between them resolved if there is one.

Equations

• One or more equations did not get rendered due to their size.
• ArregiPietraszko2021.join x y✝ = x ++ y✝

structure ArregiPietraszko2021.Exponent : Type

The exponent of a constituent of a complex head of prefixes.

• segments : List Phonology.Segment

def ArregiPietraszko2021.instDecidableEqExponent.decEq (x✝ x✝¹ : Exponent) : Decidable (x✝ = x✝¹)

Equations

• ArregiPietraszko2021.instDecidableEqExponent.decEq { segments := a } { segments := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArregiPietraszko2021.instDecidableEqExponent : DecidableEq Exponent

Equations

• ArregiPietraszko2021.instDecidableEqExponent = ArregiPietraszko2021.instDecidableEqExponent.decEq

@[instance_reducible]

instance ArregiPietraszko2021.instMulExponent : Mul Exponent

The exponent of a complex head is the product of the exponents of its two constituents, lower first: the higher one is prefixed to the lower, and the hiatus between them resolved. Cyclic spell-out, each constituent before the one containing it, is thus the homomorphism of magmas FreeMagma.lift e that extends the exponents e of the terminals.

Equations

• ArregiPietraszko2021.instMulExponent = { mul := fun (x y : ArregiPietraszko2021.Exponent) => { segments := ArregiPietraszko2021.join y.segments x.segments } }

def ArregiPietraszko2021.letters : List (Char × Phonology.Segment)

The segments the letters of the prefix table write.

Equations

• ArregiPietraszko2021.letters = [('a', Ndebele.a), ('e', Ndebele.e), ('i', Ndebele.i), ('o', Ndebele.o), ('u', Ndebele.u), ('s', Ndebele.s), ('l', Ndebele.l)]

def ArregiPietraszko2021.transcribe? : List Char → Option (List Phonology.Segment)

A string of the prefix table as segments.

Equations

• ArregiPietraszko2021.transcribe? [] = some []
• ArregiPietraszko2021.transcribe? (c :: cs) = do let __do_lift ← List.lookup c ArregiPietraszko2021.letters let __do_lift_1 ← ArregiPietraszko2021.transcribe? cs pure (__do_lift :: __do_lift_1)

def ArregiPietraszko2021.exponents? (a : Forms.Analysis) : Option (Head → Exponent)

The exponents a row of the prefix table gives the heads of the relative prefix.

Equations

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

theorem ArregiPietraszko2021.relative_prefixes (a : Forms.Analysis) : a ∈ Forms.analyses → a.form.languageId = "nort2795" → ∃ e ∈ exponents? a, some ((FreeMagma.lift e) relative.mvalue).segments = transcribe? a.form.form.toList ∧ Phonology.Hiatus.Free ((FreeMagma.lift e) relative.mvalue).segments ∧ ¬Phonology.Hiatus.Free (List.flatMap (fun (h : Head) => (e h).segments) relative.terminals.reverse)

Cyclic coalescence over the Mirror-obeying complex head derives the relative prefix of each class, free of the hiatus its exponents present.

def ArregiPietraszko2021.nonMirror : FreeMagma Head

The same terminals in the same order with the opposite bracketing, the linker innermost.

Equations

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

theorem ArregiPietraszko2021.mirror_class9 : FreeMonoid.toList ((FreeMagma.lift FreeMonoid.of) nonMirror) = relative.terminals ∧ ∃ e ∈ exponents? Forms.f_19_cl9.analysis, ((FreeMagma.lift e) relative.mvalue).segments = [Ndebele.e] ∧ ((FreeMagma.lift e) nonMirror).segments = [Ndebele.i]

In class 9 the Mirror-obeying complex head spells out as the attested e- and the opposite bracketing of the same terminals as i-.

theorem ArregiPietraszko2021.mul_not_assoc : ¬∀ (x y z : Exponent), x * y * z = x * (y * z)

Coalescence is not associative. An associative juncture rule would spell out every bracketing of the same terminals alike, and the two bracketings of the class 9 prefix come out differently, /i/ and /i/ merging before /a/ coalesces with them in one and after in the other.

Amalgamation

theorem ArregiPietraszko2021.amalgamation_bracketing (x y z : Head) : HarizanovGribanova2019.amalgamateSpine [HarizanovGribanova2019.Amalgam.single z none, HarizanovGribanova2019.Amalgam.single y (some HarizanovGribanova2019.Direction.lowering), HarizanovGribanova2019.Amalgam.single x (some HarizanovGribanova2019.Direction.lowering)] = some [{ site := z, complex := (HeadChain.ofHeads z [y, x]).mvalue, m := none }] ∧ HarizanovGribanova2019.amalgamateSpine [HarizanovGribanova2019.Amalgam.single z none, HarizanovGribanova2019.Amalgam.single y (some HarizanovGribanova2019.Direction.raising), HarizanovGribanova2019.Amalgam.single x (some HarizanovGribanova2019.Direction.lowering)] = some [{ site := z, complex := FreeMagma.of z * (FreeMagma.of y * FreeMagma.of x), m := none }]

Harizanov and Gribanova's amalgamation builds the complex head of GenHM when each head Lowers, and another bracketing of the same terminals in the same order when a head Raises into a head that then Lowers: it allows the Mirror Principle and does not derive it.

theorem ArregiPietraszko2021.amalgamation_class9 : HarizanovGribanova2019.amalgamateSpine [HarizanovGribanova2019.Amalgam.single Head.T none, HarizanovGribanova2019.Amalgam.single Head.C (some HarizanovGribanova2019.Direction.lowering), HarizanovGribanova2019.Amalgam.single Head.D (some HarizanovGribanova2019.Direction.lowering), HarizanovGribanova2019.Amalgam.single Head.Lnk (some HarizanovGribanova2019.Direction.lowering)] = some [{ site := Head.T, complex := relative.mvalue, m := none }] ∧ ∃ (a : HarizanovGribanova2019.Amalgam Head), HarizanovGribanova2019.amalgamateSpine [HarizanovGribanova2019.Amalgam.single Head.T none, HarizanovGribanova2019.Amalgam.single Head.C (some HarizanovGribanova2019.Direction.lowering), HarizanovGribanova2019.Amalgam.single Head.D (some HarizanovGribanova2019.Direction.raising), HarizanovGribanova2019.Amalgam.single Head.Lnk (some HarizanovGribanova2019.Direction.lowering)] = some [a] ∧ a.members = relative.terminals ∧ a.complex ≠ relative.mvalue ∧ ∃ e ∈ exponents? Forms.f_19_cl9.analysis, ((FreeMagma.lift e) a.complex).segments = [Ndebele.i]

With C, D and the linker all Lowering, amalgamation builds the complex head of the Ndebele relative chain. With D Raising into the linker before the linker Lowers, it builds a complex head with the same terminals in the same order that spells out the class 9 prefix as i-.

theorem ArregiPietraszko2021.amalgamation_at_pronounced {lo hi rest : List Head} {s b : Head} (h : lo ++ s :: hi = b :: rest) (hnd : (b :: rest).Nodup) : HeadChain.pronounced {s} (HeadChain.ofHeads b rest) = some s ∧ HarizanovGribanova2019.amalgamateSpine (List.map (fun (x : Head) => HarizanovGribanova2019.Amalgam.single x (some HarizanovGribanova2019.Direction.raising)) lo ++ HarizanovGribanova2019.Amalgam.single s none :: List.map (fun (x : Head) => HarizanovGribanova2019.Amalgam.single x (some HarizanovGribanova2019.Direction.lowering)) hi) = some [{ site := s, complex := (HeadChain.ofHeads b rest).mvalue, m := none }]

The two accounts meet on a single complex head. Wherever a chain is pronounced, [M] features that Raise the heads below that position and Lower the heads above it make amalgamation build the same complex head there.

theorem ArregiPietraszko2021.amalgamation_keeps_verb_site (m : Head → Option HarizanovGribanova2019.Direction) {out out' : List (HarizanovGribanova2019.Amalgam Head)} {a a' : HarizanovGribanova2019.Amalgam Head} (h : HarizanovGribanova2019.amalgamateSpine (List.map (fun (x : Head) => HarizanovGribanova2019.Amalgam.single x (m x)) [Head.V, Head.T]) = some out) (h' : HarizanovGribanova2019.amalgamateSpine (List.map (fun (x : Head) => HarizanovGribanova2019.Amalgam.single x (m x)) [Head.V, Head.T, Head.C]) = some out') (ha : a ∈ out) (ha' : a' ∈ out') (hV : Head.V ∈ a.members) (hV' : Head.V ∈ a'.members) : a'.site = a.site

Whatever [M] features V and T bear, amalgamation pronounces a verb in the same position with C above it as without, since heads added above a spine do not change where its heads are pronounced. The amalgamation account of Danish verb second therefore moves V in the syntax, across T, where the GenHM chain is pronounced in its strong C.

theorem ArregiPietraszko2021.doSupport_iff_intervener {L : Language} (hV : Head.V ∈ L.strong) (hs : L.splitByIntervention = true) : Context.inversion.above = Context.toC.above ∧ (derive L Context.inversion Head.V).DoSupport ∧ ¬(derive L Context.toC Head.V).DoSupport

Do-support turns on a specifier. A strong verb in a language with Split-by-Intervention takes it when the subject intervenes between C and the verb, and not when the same heads are related across a lower copy of the subject. A spine of heads is the same in both clauses, and Harizanov and Gribanova leave the union of English T with its verb to another operation.

def ArregiPietraszko2021.clauseOf (r : Datum) : Option (Language × Context)

The settings and context of a French or Danish clause among the verb-placement examples of the amalgamation study.

Equations

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

theorem ArregiPietraszko2021.amalgamation_rows (r : Datum) : r ∈ HarizanovGribanova2019.Examples.all → r.feature? "phenomenon" = some "finiteVerbPlacement" → r.feature? "diagnostic" ≠ some "coordination" → r.language ≠ "russ1263" → ∃ p ∈ clauseOf r, ∃ b ∈ r.parse? "verbPrecedes" boolLabels, ∀ verb ∈ [Head.V, Head.Aux], r.judgment = Judgment.acceptable ↔ (b = true ↔ Chains.finitePosition p.1 (derive p.1 p.2 verb) ∈ [some Head.T, some Head.C])

On the French and Danish verb-placement examples of the amalgamation study the two accounts agree. Each example is acceptable in exactly the order that the position of the finite word predicts, whether the finite verb is a lexical verb or an auxiliary.