Harizanov and Gribanova (2019): Whither head movement?

Harizanov and Gribanova divide the work of head movement between two operations. Words are formed by postsyntactic amalgamation: a head whose feature is [M:+] Raises into the next head up, a head whose feature is [M:−] Lowers into the nearest head below, and the result is a head-adjunction structure in the position of the target. Displacement is syntactic movement of a head to the root, which comes first and forms no word. How complex a verb is and where it is pronounced therefore vary independently, the same verbal complex surfacing in T in French, in Neg in Russian and in V in Danish.

Main statements

• flatMap_members_amalgamateSpine: the complex heads partition the spine into contiguous stretches in the order of syntactic composition, which gives the Head Movement Constraint, the mirror generalization and the ban on excorporation.
• amalgamateSpine_raising_lowering: the complex head of a spine can sit at any of its heads.
• forall_isLeftComb_iff: the complex heads add one head at a time exactly when no head Lowers right after a head has Raised into it.
• verb_placement: the finite verbs of French, Danish and Russian precede a low adverb, negation or a floating quantifier exactly where their complex head is pronounced in T or above.

Implementation notes

• A spine lists the heads of an extended projection, lowest first, each with its [M] feature; specifiers and adjuncts, which are islands for amalgamation, are left out. A head that has moved in the syntax occupies two positions of the spine, the paper's multidominance.
• A complex head is an element of the free magma over the heads, each product listing the lower constituent first. The paper's adjunction structures are unordered.
• Chain Reduction pronounces the highest occurrence, as in the paper's German, Danish and Russian derivations.
• The paper also places the English verbal complex in v, but takes T to join the English verb by an operation other than amalgamation, one that an intervening specifier blocks. No English derivation is given here.

TODO

• The pronunciation of both occurrences of the verb in Hebrew bare-infinitive fronting.
• French nonfinite clauses, whose verbs stay low; the paper gives their [M] features no derivation.

References

• [HG19]
• [EN01]
• [Tra84]

Amalgamation

inductive HarizanovGribanova2019.Direction : Type

The direction of amalgamation that the [M] feature of a head demands. A head with [M:+] Raises into the next head up and a head with [M:−] Lowers into the nearest head below.

• raising : Direction
• lowering : Direction

@[instance_reducible]

instance HarizanovGribanova2019.instDecidableEqDirection : DecidableEq Direction

Equations

• HarizanovGribanova2019.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HarizanovGribanova2019.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HarizanovGribanova2019.instReprDirection : Repr Direction

Equations

• HarizanovGribanova2019.instReprDirection = { reprPrec := HarizanovGribanova2019.instReprDirection.repr }

structure HarizanovGribanova2019.Amalgam (H : Type u_2) : Type u_2

A complex head in the course of the postsyntactic derivation.

• site : H

  The head whose position the complex head occupies.

• complex : FreeMagma H

  The head-adjunction structure, each product listing the lower constituent first.

• m : Option Direction

  The [M] feature projected from the site.

@[instance_reducible]

instance HarizanovGribanova2019.instDecidableEqAmalgam {H✝ : Type u_2} [DecidableEq H✝] : DecidableEq (Amalgam H✝)

Equations

• HarizanovGribanova2019.instDecidableEqAmalgam = HarizanovGribanova2019.instDecidableEqAmalgam.decEq

def HarizanovGribanova2019.instDecidableEqAmalgam.decEq {H✝ : Type u_2} [DecidableEq H✝] (x✝ x✝¹ : Amalgam H✝) : Decidable (x✝ = x✝¹)

Equations

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

def HarizanovGribanova2019.instReprAmalgam.repr {H✝ : Type u_2} [Repr H✝] : Amalgam H✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HarizanovGribanova2019.instReprAmalgam {H✝ : Type u_2} [Repr H✝] : Repr (Amalgam H✝)

Equations

• HarizanovGribanova2019.instReprAmalgam = { reprPrec := HarizanovGribanova2019.instReprAmalgam.repr }

def HarizanovGribanova2019.Amalgam.single {H : Type u_1} (h : H) (m : Option Direction) : Amalgam H

A lexical head with its [M] feature, before any amalgamation.

Equations

• HarizanovGribanova2019.Amalgam.single h m = { site := h, complex := FreeMagma.of h, m := m }

def HarizanovGribanova2019.Amalgam.members {H : Type u_1} (a : Amalgam H) : List H

The heads that a complex head contains, lowest first.

Equations

• a.members = FreeMonoid.toList ((FreeMagma.lift FreeMonoid.of) a.complex)

def HarizanovGribanova2019.amalgamate {H : Type u_1} : List (Amalgam H) → Option (FreeMagma H) → List (Amalgam H) → Option (List (Amalgam H))

Bottom-up amalgamation. below lists the complex heads already formed, nearest first, pending is the complex head that has Raised and awaits the next head up, and above lists the heads still to be considered, lowest first. A Raising head adjoins to the next head up, whose [M] feature the complex keeps, a Lowering head adjoins to the nearest complex head below, and a demanded operation with no target is a derivation that does not converge.

Equations

• One or more equations did not get rendered due to their size.
• HarizanovGribanova2019.amalgamate x✝ none [] = some x✝
• HarizanovGribanova2019.amalgamate x✝ (some val) [] = none
• HarizanovGribanova2019.amalgamate below✝ x✝ (a :: above) = HarizanovGribanova2019.amalgamate below✝ (some (x✝.elim a.complex fun (x : FreeMagma H) => x * a.complex)) above
• HarizanovGribanova2019.amalgamate [] x✝ (a :: above) = none

def HarizanovGribanova2019.amalgamateSpine {H : Type u_1} (spine : List (Amalgam H)) : Option (List (Amalgam H))

The complex heads that amalgamation forms on a spine, lowest first, or none when the postsyntactic derivation does not converge.

Equations

• HarizanovGribanova2019.amalgamateSpine spine = Option.map List.reverse (HarizanovGribanova2019.amalgamate [] none spine)

def HarizanovGribanova2019.moveToRoot {H : Type u_1} (spine : List (Amalgam H)) (y : H) : List (Amalgam H)

Syntactic movement of the head y to the root, which precedes amalgamation, gives y a second occurrence at the top of the spine.

Equations

• HarizanovGribanova2019.moveToRoot spine y = spine ++ [HarizanovGribanova2019.Amalgam.single y none]

theorem HarizanovGribanova2019.flatMap_members_amalgamateSpine {H : Type u_1} {spine out : List (Amalgam H)} (h : amalgamateSpine spine = some out) : List.flatMap Amalgam.members out = List.flatMap Amalgam.members spine

The complex heads partition the spine in the order of syntactic composition: the affixes of a complex head mirror that order, and no head gains or loses an occurrence.

theorem HarizanovGribanova2019.members_infix_of_mem_amalgamateSpine {H : Type u_1} {spine out : List (Amalgam H)} (h : amalgamateSpine spine = some out) {a : Amalgam H} (ha : a ∈ out) : a.members <:+: List.flatMap Amalgam.members spine

Each complex head is a contiguous stretch of the spine, which is the Head Movement Constraint and the ban on excorporation.

theorem HarizanovGribanova2019.mem_of_mem_amalgamateSpine_of_nodup {H : Type u_1} [DecidableEq H] {spine out : List (Amalgam H)} (h : amalgamateSpine spine = some out) (hnd : (List.flatMap Amalgam.members spine).Nodup) {a : Amalgam H} (ha : a ∈ out) {x y z : H} (hx : x ∈ a.members) (hy : y ∈ a.members) (hz : z ∈ List.flatMap Amalgam.members spine) (hxz : List.idxOf x (List.flatMap Amalgam.members spine) ≤ List.idxOf z (List.flatMap Amalgam.members spine)) (hzy : List.idxOf z (List.flatMap Amalgam.members spine) ≤ List.idxOf y (List.flatMap Amalgam.members spine)) : z ∈ a.members

Without syntactic movement no head is skipped. A head of the spine that lies between two members of a complex head is a member of it, so a complex head that skips a head shows that one of its heads has a second occurrence.

theorem HarizanovGribanova2019.amalgamate_append {H : Type u_1} {below : List (Amalgam H)} {pending : Option (FreeMagma H)} {above out : List (Amalgam H)} (extra : List (Amalgam H)) (h : amalgamate below pending above = some out) : amalgamate below pending (above ++ extra) = amalgamate out none extra

theorem HarizanovGribanova2019.amalgamateSpine_moveToRoot {H : Type u_1} {spine out : List (Amalgam H)} (y : H) (h : amalgamateSpine spine = some out) : amalgamateSpine (moveToRoot spine y) = some (out ++ [Amalgam.single y none])

Syntactic movement leaves the derivation below the root as it was. The high occurrence of the moved head is one more complex head, containing that head alone.

theorem HarizanovGribanova2019.exists_site_eq_of_append {H : Type u_1} {spine extra out out' : List (Amalgam H)} (h : amalgamateSpine spine = some out) (h' : amalgamateSpine (spine ++ extra) = some out') {a : Amalgam H} (ha : a ∈ out) : ∃ a' ∈ out', a'.site = a.site ∧ a.members <+: a'.members

Amalgamation proceeds bottom-up: heads added above a spine leave each of its complex heads in the same position with the same members, to which a Lowering head may add.

theorem HarizanovGribanova2019.site_eq_of_append {H : Type u_1} {spine extra out out' : List (Amalgam H)} (h : amalgamateSpine spine = some out) (h' : amalgamateSpine (spine ++ extra) = some out') (hnd : (List.flatMap Amalgam.members (spine ++ extra)).Nodup) {a a' : Amalgam H} (ha : a ∈ out) (ha' : a' ∈ out') {x : H} (hx : x ∈ a.members) (hx' : x ∈ a'.members) : a'.site = a.site

Where no head repeats, the heads added above a spine do not change the position in which a head of the spine is pronounced: a higher position takes syntactic movement.

theorem HarizanovGribanova2019.raising_and_lowering {H : Type u_1} (x y z : H) : amalgamateSpine [Amalgam.single z (some Direction.raising), Amalgam.single y none, Amalgam.single x (some Direction.lowering)] = some [{ site := y, complex := FreeMagma.of z * FreeMagma.of y * FreeMagma.of x, m := none }]

A head that Raises and a head that Lowers meet in the head between them.

theorem HarizanovGribanova2019.lowering_twice {H : Type u_1} (x y z : H) : amalgamateSpine [Amalgam.single z none, Amalgam.single y (some Direction.lowering), Amalgam.single x (some Direction.lowering)] = some [{ site := z, complex := FreeMagma.of z * FreeMagma.of y * FreeMagma.of x, m := none }]

A head Lowers past the position of a head that has itself Lowered, into a head that is not the head of its complement.

theorem HarizanovGribanova2019.lowering_without_target {H : Type u_1} (x y z : H) : amalgamateSpine [Amalgam.single z (some Direction.raising), Amalgam.single y (some Direction.lowering), Amalgam.single x none] = none

Once the lowest head has Raised into a Lowering head, the complex head has no head below it to Lower into, and the derivation does not converge.

theorem HarizanovGribanova2019.amalgamateSpine_raising_lowering {H : Type u_1} {lo hi rest : List H} {s b : H} (h : lo ++ s :: hi = b :: rest) : amalgamateSpine (List.map (fun (x : H) => Amalgam.single x (some Direction.raising)) lo ++ Amalgam.single s none :: List.map (fun (x : H) => Amalgam.single x (some Direction.lowering)) hi) = some [{ site := s, complex := List.foldl (fun (x1 : FreeMagma H) (x2 : H) => x1 * FreeMagma.of x2) (FreeMagma.of b) rest, m := none }]

The complex head of a spine can sit at any of its heads. With the heads below Raising and the heads above Lowering, all the heads form one complex head there, each added to the complex head of the heads below it.

theorem HarizanovGribanova2019.forall_isLeftComb_iff {H : Type u_1} {hs : List (H × Option Direction)} {out : List (Amalgam H)} (h : amalgamateSpine (List.map (fun (p : H × Option Direction) => Amalgam.single p.1 p.2) hs) = some out) : (∀ a ∈ out, a.complex.IsLeftComb) ↔ List.IsChain (fun (p q : Option Direction) => ¬(p = some Direction.raising ∧ q = some Direction.lowering)) (List.map (fun (x : H × Option Direction) => x.2) hs)

Every complex head of a convergent derivation adds one head at a time, the bracketing that mirrors the order of syntactic composition, exactly when no head Lowers right after a head has Raised into it.

def HarizanovGribanova2019.PronouncedFrom {H : Type u_1} [DecidableEq H] (spine : List (Amalgam H)) (h x : H) : Prop

Chain Reduction pronounces the highest occurrence of a head, and a complex head formed at one occurrence of a moved head belongs to all of them. PronouncedFrom spine h x says that the complex head containing h is thereby pronounced in the position of x or above it.

Equations

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

@[instance_reducible]

instance HarizanovGribanova2019.instDecidablePronouncedFrom {H : Type u_1} [DecidableEq H] (spine : List (Amalgam H)) (h x : H) : Decidable (PronouncedFrom spine h x)

Equations

• HarizanovGribanova2019.instDecidablePronouncedFrom spine h x = HarizanovGribanova2019.instDecidablePronouncedFrom._aux_1 spine h x

The clausal spine

inductive HarizanovGribanova2019.ClausalHead : Type

The heads of the clausal spine in the paper's derivations.

• V : ClausalHead
• v : ClausalHead
• Asp : ClausalHead
• Neg : ClausalHead
• T : ClausalHead
• Top : ClausalHead

@[instance_reducible]

instance HarizanovGribanova2019.instDecidableEqClausalHead : DecidableEq ClausalHead

Equations

• HarizanovGribanova2019.instDecidableEqClausalHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HarizanovGribanova2019.instReprClausalHead : Repr ClausalHead

Equations

• HarizanovGribanova2019.instReprClausalHead = { reprPrec := HarizanovGribanova2019.instReprClausalHead.repr }

def HarizanovGribanova2019.instReprClausalHead.repr : ClausalHead → ℕ → Std.Format

Equations

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

def HarizanovGribanova2019.russian : List (Amalgam ClausalHead)

The Russian clause, in which V, v and Asp Raise and T Lowers.

Equations

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

def HarizanovGribanova2019.danish : List (Amalgam ClausalHead)

The Danish clause, in which v and T Lower.

Equations

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

def HarizanovGribanova2019.french : List (Amalgam ClausalHead)

The French finite clause, in which V, v and Neg Raise. The negator pas is a specifier and not on the spine.

Equations

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

def HarizanovGribanova2019.german : List (Amalgam ClausalHead)

The German clause, in which V Raises into T.

Equations

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

def HarizanovGribanova2019.hebrew : List (Amalgam ClausalHead)

The Hebrew clause with a topic, in which V Raises into T.

Equations

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

theorem HarizanovGribanova2019.russian_amalgamateSpine : amalgamateSpine russian = some [{ site := ClausalHead.Neg, complex := FreeMagma.of ClausalHead.V * FreeMagma.of ClausalHead.v * FreeMagma.of ClausalHead.Asp * FreeMagma.of ClausalHead.Neg * FreeMagma.of ClausalHead.T, m := none }]

The Russian verbal complex is pronounced in Neg, above V and below T.

theorem HarizanovGribanova2019.danish_amalgamateSpine : amalgamateSpine danish = some [{ site := ClausalHead.V, complex := FreeMagma.of ClausalHead.V * FreeMagma.of ClausalHead.v * FreeMagma.of ClausalHead.T, m := none }]

The Danish verbal complex is pronounced in V.

theorem HarizanovGribanova2019.french_amalgamateSpine : amalgamateSpine french = some [{ site := ClausalHead.T, complex := FreeMagma.of ClausalHead.V * FreeMagma.of ClausalHead.v * FreeMagma.of ClausalHead.Neg * FreeMagma.of ClausalHead.T, m := none }]

The French verbal complex is pronounced in T.

Syntactic movement of a head

theorem HarizanovGribanova2019.german_root : amalgamateSpine (moveToRoot german ClausalHead.T) = some [{ site := ClausalHead.T, complex := FreeMagma.of ClausalHead.V * FreeMagma.of ClausalHead.T, m := none }, Amalgam.single ClausalHead.T none]

In a German root clause T moves to the C domain and V Raises into its low occurrence, so the complex head T pronounced at the root contains V.

theorem HarizanovGribanova2019.danish_root : amalgamateSpine (moveToRoot danish ClausalHead.V) = some [{ site := ClausalHead.V, complex := FreeMagma.of ClausalHead.V * FreeMagma.of ClausalHead.v * FreeMagma.of ClausalHead.T, m := none }, Amalgam.single ClausalHead.V none]

In a Danish root clause V moves to the C domain and v and T Lower into its low occurrence, so the complex head V pronounced at the root contains them.

theorem HarizanovGribanova2019.russian_polarity_focus : amalgamateSpine (moveToRoot russian ClausalHead.Neg) = some [{ site := ClausalHead.Neg, complex := FreeMagma.of ClausalHead.V * FreeMagma.of ClausalHead.v * FreeMagma.of ClausalHead.Asp * FreeMagma.of ClausalHead.Neg * FreeMagma.of ClausalHead.T, m := none }, Amalgam.single ClausalHead.Neg none]

In a Russian clause with polarity focus Neg moves to Pol and the verbal complex forms at its low occurrence, so the whole complex is pronounced before the subject.

theorem HarizanovGribanova2019.hebrew_fronting : amalgamateSpine (moveToRoot hebrew ClausalHead.V) = some [{ site := ClausalHead.T, complex := FreeMagma.of ClausalHead.V * FreeMagma.of ClausalHead.T, m := none }, Amalgam.single ClausalHead.Top none, Amalgam.single ClausalHead.V none]

In Hebrew bare-infinitive fronting V moves to the topic position and its low occurrence Raises into T, so the fronted occurrence is the verb alone, an infinitive, and the verb with tense and agreement is in T.

theorem HarizanovGribanova2019.skipping : amalgamateSpine [Amalgam.single 0 none, Amalgam.single 5 (some Direction.lowering), Amalgam.single 4 none, Amalgam.single 3 none, Amalgam.single 2 (some Direction.raising), Amalgam.single 1 (some Direction.raising), Amalgam.single 0 none] = some [{ site := 0, complex := FreeMagma.of 0 * FreeMagma.of 5, m := none }, Amalgam.single 4 none, Amalgam.single 3 none, { site := 0, complex := FreeMagma.of 2 * FreeMagma.of 1 * FreeMagma.of 0, m := none }]

With H1 to H6 as 0 to 5, the moved H1 occupies the bottom and the top of the spine. H6 Lowers into its low occurrence and the complex of H3 and H2 Raises into its high one, so H1 has gained three heads across the inert H4 and H5.

Verb placement

def HarizanovGribanova2019.spine? (r : Datum) : Option (List (Amalgam ClausalHead))

spine? r is the spine of the clause of r, a French or Russian finite clause, a Danish embedded clause, or a Danish root clause, in which V has moved.

Equations

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

theorem HarizanovGribanova2019.verb_placement (r : Datum) : r ∈ Examples.all → r.feature? "phenomenon" = some "finiteVerbPlacement" → r.feature? "diagnostic" ≠ some "coordination" → ∃ s ∈ spine? r, ∃ b ∈ r.parse? "verbPrecedes" [("true", true), ("false", false)], r.judgment = Judgment.acceptable ↔ (b = true ↔ PronouncedFrom s ClausalHead.V ClausalHead.T)

The canonical tests for verb movement place a finite verb before a low adverb, sentential negation or a floating quantifier exactly when it is pronounced in T or above. The paper's examples of French, Danish and Russian finite clauses are acceptable in exactly the order that the position of the verbal complex predicts.