Branan and Erlewine (2023): Anti-pied-piping

A language marks a focus on some constituent, by a particle or by moving it, and that constituent need not be the focus. It may properly contain the focus, which is Ross's pied-piping, or be properly contained in it, which Branan and Erlewine call anti-pied-piping and document in over sixty languages. They conclude that a focus particle has no meaning of its own. It flags an unpronounced operator that takes the whole focus in its scope, and it is adjoined, when a phase is spelled out, to a phrase left-aligned with the focus once the phrases that bear no prominence are skipped. Focus movement moves the phrase so marked, so one rule governs both, and it does not tell pied-piping from anti-pied-piping.

Main statements

• quantifierOnly_ne_only: a particle that quantified over alternatives to its sister could not associate with a focus properly containing that sister, whatever alternatives it was given.
• LeftAlignedOn.symmGen_le, LeftmostRequirement.allows_comm: a phrase left-aligned with the focus contains it or is contained in it, and the rule that places the particle does not tell the two apart.
• LeftAlignedOn.symmGen_le_of_common: of two separate phrases at most one is left-aligned with a given focus, the leftmost effect.
• acceptable_iff_favors: an example is unmarked on a reading exactly when its language's variant of the rule favors the phrase it marks for the focus of that reading.

Implementation notes

• A phase is a constituency tree over the categories of the functional sequence, in the order it is spelled out. Its spine is the path of categories extending to the category of the phase, and the prominent phrases, the paper's ●-marked ones, are the phrases off the spine that an example does not report as skipped.
• The examples name constituents (subject, predicate, the fronted phrase), and a frame finds each as the first node of its tree spelling a given string of words, so positions are read off bracketings and none is typed in. Clause frames are schematic, and the frames of the English, Latin and Russian examples carry their words.
• The judged readings are those the paper prints. Where it marks one string for two speakers' grammars, the weak variant stands for the language.

TODO

• The timing of placement: particles adjoin before scrambling, so a host need not be leftmost on the surface, and adjuncts merged late cannot host a particle for a focus on the predicate.
• The ratings of object fronting across accented and unaccented subjects in German, and the survey of languages by genus in the appendix.
• Narrow focus on a lexical verb, for which no phrase is left-aligned (sov_verb) and languages differ in what they do, and the obligatory anti-pied-piping of Miyara Yaeyaman, where the rule also allows the focused predicate itself to host the particle.
• The realization of prominence as phrasal stress, and the paper's argument from Hausa that placement does not track stress itself.

References

• [BE23]
• [Ros67]

The particle is not a quantifier

noncomputable def BrananErlewine2023.quantifierOnly {W : Type u_1} {σ : Type u_2} (C : Set σ) (α : σ) (β : σ → Set W) : W → SignType

On the quantificational theory a particle meaning only composes with its sister α and then with its scope β, presupposing β α and asserting that β is false of every other alternative to α in C ((72)).

Equations

• BrananErlewine2023.quantifierOnly C α β = (β α).indicator fun (w : W) => SignType.ofProp (∀ γ ∈ C, γ ≠ α → w ∉ β γ)

theorem BrananErlewine2023.quantifierOnly_eq_only {W : Type u_1} {σ : Type u_2} {C : Set σ} {α : σ} {β : σ → Set W} (hα : α ∈ C) (hβ : Set.InjOn β C) : quantifierOnly C α β = Focus.Particles.only (fun (x1 x2 : Set W) => x1 = x2) (β '' C) (β α)

The quantificational particle is the operator only of (73) restricted to the alternatives that differ from the prejacent in the particle's sister alone.

theorem BrananErlewine2023.quantifierOnly_ne_only {W : Type u_1} {σ : Type u_2} {α : σ} {β : σ → Set W} {D : Set (Set W)} {ψ : Set W} {w : W} (C : Set σ) (hψ : ψ ∈ D) (hne : ψ ≠ β α) (hw : w ∈ ψ) (hwα : w ∈ β α) (hβ : ∀ (γ : σ), γ ≠ α → w ∉ β γ) : quantifierOnly C α β ≠ Focus.Particles.only (fun (x1 x2 : Set W) => x1 = x2) D (β α)

A particle on a proper part of its focus is not a quantifier over alternatives to its sister. Where the scope holds of the sister and of nothing else, the quantifier is true whatever alternatives it is given, though an alternative ψ to the whole focus is true as well, so that the operator associating with that focus is false.

inductive BrananErlewine2023.Book : Type

• hamlet : Book
• macbeth : Book

inductive BrananErlewine2023.Deed : Type

• read (b : Book) : Deed
• swim : Deed

def BrananErlewine2023.read (b : Book) : Set (Set Deed)

Equations

• BrananErlewine2023.read b = {w : Set BrananErlewine2023.Deed | BrananErlewine2023.Deed.read b ∈ w}

def BrananErlewine2023.swam : Set (Set Deed)

Equations

• BrananErlewine2023.swam = {w : Set BrananErlewine2023.Deed | BrananErlewine2023.Deed.swim ∈ w}

theorem BrananErlewine2023.peter_read_only_hamlet : quantifierOnly Set.univ Book.hamlet read {Deed.read Book.hamlet, Deed.swim} = 1 ∧ Focus.Particles.only (fun (x1 x2 : Set (Set Deed)) => x1 = x2) {read Book.hamlet, read Book.macbeth, swam} (read Book.hamlet) {Deed.read Book.hamlet, Deed.swim} = -1

Peter read Hamlet and swam. The particle on the object, read as a quantifier, is true, since he read nothing else; the reading on which he only read Hamlet, the operator's over the predicate's alternatives, is false ((79)–(81)).

Prominence

When a phase is spelled out, every phrase outside the extended projection of the phase head bears abstract prominence, the paper's ●, unless it is indefinite, given or otherwise light ((115), (119)).

def BrananErlewine2023.OnSpine {W : Type u_1} (t : PhraseStructure.Tree Minimalist.Cat W) (p : Core.Order.TreePath) : Prop

A position is on the spine of a phase when its category and that of every node above it extend to the category of the phase, so that it belongs to the extended projection containing the phase head.

Equations

• BrananErlewine2023.OnSpine t p = ∀ l ∈ p.toList.inits, ∃ s ∈ RoseTree.subtreeAt t l, (PhraseStructure.Tree.cat s).ExtendsTo t.cat

@[instance_reducible]

instance BrananErlewine2023.instDecidableOnSpine {W : Type u_1} (t : PhraseStructure.Tree Minimalist.Cat W) (p : Core.Order.TreePath) : Decidable (OnSpine t p)

Equations

• BrananErlewine2023.instDecidableOnSpine t p = id inferInstance

def BrananErlewine2023.prominent {W : Type u_1} (t : PhraseStructure.Tree Minimalist.Cat W) (skipped : List Core.Order.TreePath) : List Core.Order.TreePath

The prominent phrases of a phase are the phrases off its spine other than the skipped ones, listed in document order.

Equations

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

Left-alignment relative to the prominent phrases

def BrananErlewine2023.leftmost (m : List Core.Order.TreePath) (X : Core.Order.TreePath) : Option Core.Order.TreePath

leftmost m X is the first phrase of m that the constituent at X contains. With m in document order it is the one that begins earliest, and the largest that does.

Equations

• BrananErlewine2023.leftmost m X = List.find? (fun (x : Core.Order.TreePath) => decide (X ≤ x)) m

theorem BrananErlewine2023.le_of_mem_leftmost {m : List Core.Order.TreePath} {X a : Core.Order.TreePath} (h : a ∈ leftmost m X) : X ≤ a

def BrananErlewine2023.LeftAlignedOn (m : List Core.Order.TreePath) (X Y : Core.Order.TreePath) : Prop

Two constituents are left-aligned on m when the leftmost phrase of m in the one and the leftmost in the other are left-aligned ((118)).

Equations

• BrananErlewine2023.LeftAlignedOn m X Y = ∃ a ∈ BrananErlewine2023.leftmost m X, ∃ b ∈ BrananErlewine2023.leftmost m Y, a.LeftAligned b

@[instance_reducible]

instance BrananErlewine2023.instDecidableLeftAlignedOn {m : List Core.Order.TreePath} {X Y : Core.Order.TreePath} : Decidable (LeftAlignedOn m X Y)

Equations

• BrananErlewine2023.instDecidableLeftAlignedOn = id inferInstance

theorem BrananErlewine2023.LeftAlignedOn.symm {m : List Core.Order.TreePath} {X Y : Core.Order.TreePath} (h : LeftAlignedOn m X Y) : LeftAlignedOn m Y X

theorem BrananErlewine2023.LeftAlignedOn.trans {m : List Core.Order.TreePath} {X Y Z : Core.Order.TreePath} (h₁ : LeftAlignedOn m X Y) (h₂ : LeftAlignedOn m Y Z) : LeftAlignedOn m X Z

theorem BrananErlewine2023.LeftAlignedOn.symmGen_le {m : List Core.Order.TreePath} {X Y : Core.Order.TreePath} (h : LeftAlignedOn m X Y) : Relation.SymmGen (fun (x1 x2 : Core.Order.TreePath) => x1 ≤ x2) X Y

Of two left-aligned constituents one contains the other.

theorem BrananErlewine2023.LeftAlignedOn.symmGen_le_of_common {m : List Core.Order.TreePath} {X Y Z : Core.Order.TreePath} (h₁ : LeftAlignedOn m X Z) (h₂ : LeftAlignedOn m Y Z) : Relation.SymmGen (fun (x1 x2 : Core.Order.TreePath) => x1 ≤ x2) X Y

Two constituents left-aligned with a third overlap, so of two separate phrases at most one is left-aligned with a given focus, which is the leftmost effect.

theorem BrananErlewine2023.leftAlignedOn_self {m : List Core.Order.TreePath} {X : Core.Order.TreePath} : LeftAlignedOn m X X ↔ (leftmost m X).isSome = true

A constituent is left-aligned with itself as soon as it contains a prominent phrase.

theorem BrananErlewine2023.not_leftAlignedOn_of_leftmost_eq_none {m : List Core.Order.TreePath} {X Y : Core.Order.TreePath} (h : leftmost m Y = none) : ¬LeftAlignedOn m X Y

A constituent containing no prominent phrase, as a lexical verb does not, is left-aligned with nothing (n. 45).

Particle placement

inductive BrananErlewine2023.LeftmostRequirement : Type

When a phase is spelled out, a particle adjoins to a phrase left-aligned with the focus, preferably to such a phrase, or to any phrase overlapping the focus, in the strong, the weak and the free variant of the rule ((117)).

• strong : LeftmostRequirement
• weak : LeftmostRequirement
• free : LeftmostRequirement

@[instance_reducible]

instance BrananErlewine2023.instDecidableEqLeftmostRequirement : DecidableEq LeftmostRequirement

Equations

• BrananErlewine2023.instDecidableEqLeftmostRequirement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BrananErlewine2023.instReprLeftmostRequirement.repr : LeftmostRequirement → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BrananErlewine2023.instReprLeftmostRequirement : Repr LeftmostRequirement

Equations

• BrananErlewine2023.instReprLeftmostRequirement = { reprPrec := BrananErlewine2023.instReprLeftmostRequirement.repr }

def BrananErlewine2023.LeftmostRequirement.Allows : LeftmostRequirement → List Core.Order.TreePath → Core.Order.TreePath → Core.Order.TreePath → Prop

The phrases a variant lets host the particle for a focus.

Equations

• BrananErlewine2023.LeftmostRequirement.strong.Allows x✝² x✝¹ x✝ = BrananErlewine2023.LeftAlignedOn x✝² x✝¹ x✝
• BrananErlewine2023.LeftmostRequirement.weak.Allows x✝² x✝¹ x✝ = Relation.SymmGen (fun (x1 x2 : Core.Order.TreePath) => x1 ≤ x2) x✝¹ x✝
• BrananErlewine2023.LeftmostRequirement.free.Allows x✝² x✝¹ x✝ = Relation.SymmGen (fun (x1 x2 : Core.Order.TreePath) => x1 ≤ x2) x✝¹ x✝

def BrananErlewine2023.LeftmostRequirement.Favors : LeftmostRequirement → List Core.Order.TreePath → Core.Order.TreePath → Core.Order.TreePath → Prop

The phrases a variant lets host the particle at no cost.

Equations

• BrananErlewine2023.LeftmostRequirement.strong.Favors x✝² x✝¹ x✝ = BrananErlewine2023.LeftAlignedOn x✝² x✝¹ x✝
• BrananErlewine2023.LeftmostRequirement.weak.Favors x✝² x✝¹ x✝ = BrananErlewine2023.LeftAlignedOn x✝² x✝¹ x✝
• BrananErlewine2023.LeftmostRequirement.free.Favors x✝² x✝¹ x✝ = Relation.SymmGen (fun (x1 x2 : Core.Order.TreePath) => x1 ≤ x2) x✝¹ x✝

@[instance_reducible]

instance BrananErlewine2023.LeftmostRequirement.instDecidableAllows {r : LeftmostRequirement} {m : List Core.Order.TreePath} {host focus : Core.Order.TreePath} : Decidable (r.Allows m host focus)

Equations

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

@[instance_reducible]

instance BrananErlewine2023.LeftmostRequirement.instDecidableFavors {r : LeftmostRequirement} {m : List Core.Order.TreePath} {host focus : Core.Order.TreePath} : Decidable (r.Favors m host focus)

Equations

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

theorem BrananErlewine2023.LeftmostRequirement.Favors.allows {r : LeftmostRequirement} {m : List Core.Order.TreePath} {host focus : Core.Order.TreePath} (h : r.Favors m host focus) : r.Allows m host focus

theorem BrananErlewine2023.LeftmostRequirement.Allows.symmGen_le {r : LeftmostRequirement} {m : List Core.Order.TreePath} {host focus : Core.Order.TreePath} (h : r.Allows m host focus) : Relation.SymmGen (fun (x1 x2 : Core.Order.TreePath) => x1 ≤ x2) host focus

A phrase that may host the particle overlaps the focus.

theorem BrananErlewine2023.LeftmostRequirement.allows_comm {r : LeftmostRequirement} {m : List Core.Order.TreePath} {host focus : Core.Order.TreePath} : r.Allows m host focus ↔ r.Allows m focus host

The rule does not tell pied-piping from anti-pied-piping, since a phrase may host the particle for a focus exactly when the focus, as a phrase, might host it for a focus on that phrase (§6.4).

theorem BrananErlewine2023.LeftmostRequirement.favors_comm {r : LeftmostRequirement} {m : List Core.Order.TreePath} {host focus : Core.Order.TreePath} : r.Favors m host focus ↔ r.Favors m focus host

theorem BrananErlewine2023.LeftmostRequirement.Allows.exactlyTargets_or_piedPipes_or_antiPiedPipes {r : LeftmostRequirement} {m : List Core.Order.TreePath} {host focus : Core.Order.TreePath} (h : r.Allows m host focus) {s : Finset (Reflex Core.Order.TreePathᵒᵈ)} (hs : s.Nonempty) (hhost : Reflex.ExactlyTargets s (OrderDual.toDual host)) : Reflex.ExactlyTargets s (OrderDual.toDual focus) ∨ Reflex.PiedPipes s (OrderDual.toDual focus) ∨ Reflex.AntiPiedPipes s (OrderDual.toDual focus)

Every overt reflex of a focus sits on the phrase hosting its particle, where the particle is pronounced and from where the phrase moves. The reflexes of an allowed placement therefore target the focus exactly, pied-pipe or anti-pied-pipe, and none is hosted outside the focus.

Phases and their constituents

inductive BrananErlewine2023.Part : Type

The constituents the examples name.

• sentence : Part
• subject : Part
• predicate : Part
• object : Part
• verb : Part
• goal : Part
• theme : Part
• adjective : Part
• phrase : Part
• wh : Part
• demonstrative : Part

@[instance_reducible]

instance BrananErlewine2023.instDecidableEqPart : DecidableEq Part

Equations

• BrananErlewine2023.instDecidableEqPart x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BrananErlewine2023.instReprPart.repr : Part → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BrananErlewine2023.instReprPart : Repr Part

Equations

• BrananErlewine2023.instReprPart = { reprPrec := BrananErlewine2023.instReprPart.repr }

structure BrananErlewine2023.Frame : Type

A phase as it is spelled out, with the words of the constituents the examples name.

• phase : PhraseStructure.Tree Minimalist.Cat String

  The phase, in the order in which it is linearized.

• brackets : List (Part × List String)

  The words each named constituent spells.

def BrananErlewine2023.Frame.site (fr : Frame) (c : Part) : Option Core.Order.TreePath

The position of a named constituent, the first node spelling its words.

Equations

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

def BrananErlewine2023.Frame.Allows (fr : Frame) (r : LeftmostRequirement) (host focus : Part) (skipped : List Part := []) : Prop

A variant of the rule lets the constituent host of a frame host the particle for a focus on focus, the constituents of skipped bearing no prominence.

Equations

• fr.Allows r host focus skipped = ∃ h ∈ fr.site host, ∃ f ∈ fr.site focus, r.Allows (BrananErlewine2023.prominent fr.phase (List.filterMap fr.site skipped)) h f

@[instance_reducible]

instance BrananErlewine2023.Frame.instDecidableAllows (fr : Frame) (r : LeftmostRequirement) (host focus : Part) (skipped : List Part) : Decidable (fr.Allows r host focus skipped)

Equations

• fr.instDecidableAllows r host focus skipped = id inferInstance

def BrananErlewine2023.xp (c : Minimalist.Cat) (w : String) : PhraseStructure.Tree Minimalist.Cat String

A phrase over one word.

Equations

• BrananErlewine2023.xp c w = PhraseStructure.Tree.node c [PhraseStructure.Tree.terminal c w]

def BrananErlewine2023.sov : Frame

A verb-final transitive clause, [S [O V]].

Equations

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

def BrananErlewine2023.svo : Frame

A verb-medial transitive clause, [S [V O]].

Equations

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

def BrananErlewine2023.vso : Frame

A verb-initial transitive clause, [V S O].

Equations

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

def BrananErlewine2023.sv : Frame

An intransitive clause, [S [V]].

Equations

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

def BrananErlewine2023.themeGoalV : Frame

A verb-final ditransitive clause with the theme before the goal.

Equations

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

def BrananErlewine2023.goalThemeV : Frame

A verb-final ditransitive clause with the goal before the theme.

Equations

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

def BrananErlewine2023.vGoalTheme : Frame

A verb-medial ditransitive clause with the goal before the theme.

Equations

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

def BrananErlewine2023.adjectiveObject : Frame

A clause whose object holds an attributive adjective, [S [V [D [A N]]]].

Equations

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

def BrananErlewine2023.whosePicture : Frame

you frame [whose picture] ((122a)).

Equations

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

def BrananErlewine2023.pictureOfWhom : Frame

you frame [a picture of whom] ((122b)).

Equations

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

def BrananErlewine2023.whoseBrothersFriendsFather : Frame

you see [[[whose brother]'s friend]'s father].

Equations

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

def BrananErlewine2023.fatherOfWhoseBrothersFriend : Frame

you see [the father of [[whose brother]'s friend]].

Equations

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

def BrananErlewine2023.toWhichStudentsFriend : Frame

you speak [to [[which student]'s friend]].

Equations

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

def BrananErlewine2023.obEasRes : Frame

Latin [ob [eās rēs]] 'because of these things'. The source prints the phrase alone, so it is the root here and bears no prominence whether or not its preposition is light.

Equations

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

def BrananErlewine2023.naSestreDrugaCejMateri : Frame

Russian on ženilsja [na sestre [druga [č’ej materi]]].

Equations

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

def BrananErlewine2023.heightOfTheLettering : Frame

the government prescribes [the height of the lettering on the covers of which].

Equations

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

The leftmost effect in a clause

theorem BrananErlewine2023.sov_strong : sov.Allows LeftmostRequirement.strong Part.subject Part.sentence ∧ ¬sov.Allows LeftmostRequirement.strong Part.object Part.sentence ∧ sov.Allows LeftmostRequirement.strong Part.object Part.predicate ∧ ¬sov.Allows LeftmostRequirement.strong Part.subject Part.predicate

Under the strong variant a verb-final clause marks a focus on the sentence at its subject and a focus on the predicate at its object, and neither at the other, the pattern of Miyara Yaeyaman du and Ishkashimi məs ((64)).

theorem BrananErlewine2023.svo_strong : svo.Allows LeftmostRequirement.strong Part.object Part.predicate ∧ ¬svo.Allows LeftmostRequirement.strong Part.subject Part.predicate

The object of a verb-medial predicate counts as its leftmost phrase, the verb being on the spine (n. 17).

theorem BrananErlewine2023.sov_strong_skipped : sov.Allows LeftmostRequirement.strong Part.object Part.sentence [Part.subject] ∧ ¬sov.Allows LeftmostRequirement.strong Part.subject Part.sentence [Part.subject]

A subject that bears no prominence is skipped, so a focus on the sentence is marked at the object and the subject cannot host the particle (§6.1).

theorem BrananErlewine2023.sov_verb (c : Part) : ¬sov.Allows LeftmostRequirement.strong c Part.verb

No phrase is left-aligned with a narrowly focused verb (n. 45).

theorem BrananErlewine2023.toWhichStudentsFriend_strong : toWhichStudentsFriend.Allows LeftmostRequirement.strong Part.phrase Part.wh [Part.phrase] ∧ ¬toWhichStudentsFriend.Allows LeftmostRequirement.strong Part.phrase Part.wh

A preposition stands between the edge of to which student's friend and its question word, and the phrase is left-aligned with the question word only because the phrase a light preposition heads is skipped ((123)).

theorem BrananErlewine2023.not_strong_of_free : ¬naSestreDrugaCejMateri.Allows LeftmostRequirement.strong Part.phrase Part.wh ∧ ¬heightOfTheLettering.Allows LeftmostRequirement.strong Part.phrase Part.wh

The phrases fronted in a Russian question and an English relative clause are ones the strong variant excludes ((125), (126)).

The examples

inductive BrananErlewine2023.Mismatch : Type

The constituent the morphosyntax marks is the focus, properly contains it, or is properly contained in it ((76)–(78)).

• none : Mismatch
• piedPiping : Mismatch
• antiPiedPiping : Mismatch

@[instance_reducible]

instance BrananErlewine2023.instDecidableEqMismatch : DecidableEq Mismatch

Equations

• BrananErlewine2023.instDecidableEqMismatch x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BrananErlewine2023.instReprMismatch.repr : Mismatch → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BrananErlewine2023.instReprMismatch : Repr Mismatch

Equations

• BrananErlewine2023.instReprMismatch = { reprPrec := BrananErlewine2023.instReprMismatch.repr }

inductive BrananErlewine2023.Process : Type

A focus is marked by a particle on a phrase or by movement of the phrase.

• particle : Process
• movement : Process

@[instance_reducible]

instance BrananErlewine2023.instDecidableEqProcess : DecidableEq Process

Equations

• BrananErlewine2023.instDecidableEqProcess x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BrananErlewine2023.instReprProcess : Repr Process

Equations

• BrananErlewine2023.instReprProcess = { reprPrec := BrananErlewine2023.instReprProcess.repr }

def BrananErlewine2023.instReprProcess.repr : Process → ℕ → Std.Format

Equations

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

def BrananErlewine2023.Mismatch.Holds : Mismatch → Core.Order.TreePath → Core.Order.TreePath → Prop

The relation of host to focus that a label names.

Equations

• BrananErlewine2023.Mismatch.none.Holds x✝¹ x✝ = (x✝¹ = x✝)
• BrananErlewine2023.Mismatch.piedPiping.Holds x✝¹ x✝ = (x✝¹ < x✝)
• BrananErlewine2023.Mismatch.antiPiedPiping.Holds x✝¹ x✝ = (x✝ < x✝¹)

@[instance_reducible]

instance BrananErlewine2023.instDecidableHolds (k : Mismatch) (host focus : Core.Order.TreePath) : Decidable (k.Holds host focus)

Equations

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

def BrananErlewine2023.frame : String → Option Frame

The phase of each example, by the paper's number.

Equations

• BrananErlewine2023.frame "(2)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(4)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(17b)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(18b)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(21)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(30a)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(30b)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(38)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(66a)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(66b)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(111a)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(111b)" = some BrananErlewine2023.sov
• BrananErlewine2023.frame "(7)" = some BrananErlewine2023.svo
• BrananErlewine2023.frame "(109a)" = some BrananErlewine2023.svo
• BrananErlewine2023.frame "(109b)" = some BrananErlewine2023.svo
• BrananErlewine2023.frame "(114a)" = some BrananErlewine2023.svo
• BrananErlewine2023.frame "(114b)" = some BrananErlewine2023.svo
• BrananErlewine2023.frame "(8)" = some BrananErlewine2023.sv
• BrananErlewine2023.frame "(70a)" = some BrananErlewine2023.vso
• BrananErlewine2023.frame "(70b)" = some BrananErlewine2023.vso
• BrananErlewine2023.frame "(68a)" = some BrananErlewine2023.themeGoalV
• BrananErlewine2023.frame "(68b)" = some BrananErlewine2023.themeGoalV
• BrananErlewine2023.frame "(65)" = some BrananErlewine2023.goalThemeV
• BrananErlewine2023.frame "(67)" = some BrananErlewine2023.goalThemeV
• BrananErlewine2023.frame "(1)" = some BrananErlewine2023.vGoalTheme
• BrananErlewine2023.frame "(69a)" = some BrananErlewine2023.vGoalTheme
• BrananErlewine2023.frame "(69b)" = some BrananErlewine2023.vGoalTheme
• BrananErlewine2023.frame "(3)" = some BrananErlewine2023.adjectiveObject
• BrananErlewine2023.frame "(120a)" = some BrananErlewine2023.whosePicture
• BrananErlewine2023.frame "(120b)" = some BrananErlewine2023.pictureOfWhom
• BrananErlewine2023.frame "(121a)" = some BrananErlewine2023.whoseBrothersFriendsFather
• BrananErlewine2023.frame "(121b)" = some BrananErlewine2023.fatherOfWhoseBrothersFriend
• BrananErlewine2023.frame "(123)" = some BrananErlewine2023.toWhichStudentsFriend
• BrananErlewine2023.frame "(124)" = some BrananErlewine2023.obEasRes
• BrananErlewine2023.frame "(125)" = some BrananErlewine2023.naSestreDrugaCejMateri
• BrananErlewine2023.frame "(126)" = some BrananErlewine2023.heightOfTheLettering
• BrananErlewine2023.frame x✝ = none

def BrananErlewine2023.partLabels : List (String × Part)

The examples name constituents by these labels.

Equations

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

structure BrananErlewine2023.Row : Type

A row records of an example how it marks focus, the prominent phrases of its phase, the phrase that hosts the particle or moves, the focus of each reading with its judgment, the variant of the rule the paper reports for the construction, and the mismatch the paper labels it with.

• process : Process
• prominent : List Core.Order.TreePath
• host : Core.Order.TreePath
• readings : List (Core.Order.TreePath × Judgment)
• requirement : Option LeftmostRequirement
• mismatch : Option Mismatch

def BrananErlewine2023.Row.ofDatum (d : Datum) : Option Row

The row of an example.

Equations

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

def BrananErlewine2023.data : List Row

The examples.

Equations

• BrananErlewine2023.data = List.filterMap BrananErlewine2023.Row.ofDatum BrananErlewine2023.Examples.all

theorem BrananErlewine2023.data_length : data.length = Examples.all.length

Every example has its row.

theorem BrananErlewine2023.acceptable_iff_favors (d : Row) : d ∈ data → ∀ r ∈ d.requirement, ∀ rd ∈ d.readings, rd.2 = Judgment.acceptable ↔ r.Favors d.prominent d.host rd.1

An example is unmarked on a reading exactly when the variant of the rule that the paper reports for its construction favors the phrase it marks for the focus of that reading.

theorem BrananErlewine2023.allows_of_marginal (d : Row) : d ∈ data → ∀ r ∈ d.requirement, ∀ rd ∈ d.readings, rd.2 = Judgment.marginal → r.Allows d.prominent d.host rd.1

A reading the paper marks as dispreferred marks its focus at a phrase the variant allows.

theorem BrananErlewine2023.not_allows_of_ungrammatical (d : Row) : d ∈ data → ∀ r ∈ d.requirement, ∀ rd ∈ d.readings, rd.2 = Judgment.ungrammatical → ¬r.Allows d.prominent d.host rd.1

A starred reading marks its focus at a phrase the variant does not allow.

theorem BrananErlewine2023.mismatch_holds (d : Row) : d ∈ data → ∀ k ∈ d.mismatch, ∀ rd ∈ d.readings, k.Holds d.host rd.1

The mismatch the paper labels an example with is the relation of its host to its focus.

theorem BrananErlewine2023.exists_mismatch (p : Process) (k : Mismatch) : ∃ d ∈ data, d.process = p ∧ d.mismatch = some k

Particle placement and movement each mark the focus itself, a phrase containing it, and a phrase it contains ((1)–(8)).