Lechner (2004): Ellipsis in comparatives

This file formalizes two of Lechner's binding arguments that the ellipsis sites of comparatives are projected in syntax. In a clausal comparative the site of Comparative Deletion is reconstructed at LF, where its copy of a name counts as a pronoun, so that coreference is out in (24) and restored in (25), whose site sits in a further clause; neither Kennedy's semantic resolution nor reconstruction of the name as an R-expression predicts both. A phrasal comparative is a Gapped clause, a copy of the matrix clause with the remnant in the position of its correlate, and the remnant inherits the correlate's c-command relations (Prediction V). Lechner's minimal pairs vary the height of the correlate against a coindexed matrix term, and the Gapped clause separates the halves of each pair, while Heim's direct analysis, which raises the remnant out of the clause, gives both halves one verdict.

Main definitions

• Lechner2004.Resolution: the resolution of a deletion site, semantic, syntactic, or syntactic under Fiengo and May's vehicle change.
• Lechner2004.PhrasalComparative.gapped, Lechner2004.PhrasalComparative.direct: the Gapped clause and the LF of the direct analysis.

Main results

• Lechner2004.resolution_fits_iff: only reconstruction under vehicle change predicts (24)–(25).
• Lechner2004.PhrasalComparative.gapped_cCommands_iff, Lechner2004.PhrasalComparative.cCommands_gapped_iff: Prediction V.
• Lechner2004.analysis_fits_iff, Lechner2004.direct_same: only the Gapped clause predicts the minimal pairs (83)–(91).

Implementation notes

Trees carry categories only, and German clauses have their underlying hierarchy, subject over dative over accusative. Binding is computed within the Gapped clause, which coordinates with the matrix clause outside the c-command domain of its terms. Heim's LF, in which -er takes the correlate and the remnant as a pair ((55), (88)), is rendered by adjoining both to the clause, the configuration in which Lechner reads c-command off (88) and (92)–(93); its base-position reading is computed on the surface tree. The ?? of (91) counts against coreference. The book calls the effect in (24) a Principle C violation, but with the copy a pronoun, as (25) shows it to be, (24) violates Condition B.

TODO

Prediction IV ((75)–(77)), Predictions I–III of §3.1, the arguments from reflexives and the Coordinate Structure Constraint of chapter 2, §§2.2–2.3, and the argument of (27)–(29) against a surface Principle B account of (24) are not formalized.

References

• [Lec04]
• [Ken99]
• [Hei85]
• [FM94]

Trees and coreference

@[reducible, inline]

abbrev Lechner2004.np : PhraseStructure.Tree PhraseStructure.Cat Unit

np is a nominal, a terminal noun phrase.

Equations

• Lechner2004.np = PhraseStructure.Tree.terminal PhraseStructure.Cat.N ()

@[reducible, inline]

abbrev Lechner2004.word (c : PhraseStructure.Cat) : PhraseStructure.Tree PhraseStructure.Cat Unit

word c is a word of category c.

Equations

• Lechner2004.word c = PhraseStructure.Tree.terminal c ()

@[reducible, inline]

abbrev Lechner2004.nominalIn : PhraseStructure.Tree PhraseStructure.Cat Unit

nominalIn is a noun phrase with a nominal beside its head noun, as in Peter's sister and die Frau des Präsidenten.

Equations

• Lechner2004.nominalIn = PhraseStructure.Tree.node PhraseStructure.Cat.N [Lechner2004.np, Lechner2004.word PhraseStructure.Cat.N]

@[reducible, inline]

abbrev Lechner2004.pairConfiguration (t : PhraseStructure.Tree PhraseStructure.Cat Unit) (p q : Core.Order.TreePath) : Binding.Configuration (Fin 2)

The binding configuration of the positions p and q of t reads them as 0 and 1.

Equations

• Lechner2004.pairConfiguration t p q = Binding.Configuration.comap ![p, q] t.clauseConfiguration

def Lechner2004.MayCorefer (t : PhraseStructure.Tree PhraseStructure.Cat Unit) (p q : Core.Order.TreePath) (k : Binding.BindingClass) : Prop

A nominal of class k at q of t may corefer with the nominal at p when, if a nominal occupies q, it meets its binding condition under the dependency relating the two.

Equations

• Lechner2004.MayCorefer t p q k = (RoseTree.subtreeAt t q.toList = some Lechner2004.np → (Lechner2004.pairConfiguration t p q).Condition (Binding.pair 0 1) ∅ 1 k)

@[instance_reducible]

instance Lechner2004.instDecidableMayCorefer (t : PhraseStructure.Tree PhraseStructure.Cat Unit) (p q : Core.Order.TreePath) (k : Binding.BindingClass) : Decidable (MayCorefer t p q k)

Equations

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

def Lechner2004.Attested (e : Datum) : Prop

A judgment attests the coreferential reading when it is acceptable or marginal.

Equations

• Lechner2004.Attested e = (Judgment.marginal ≤ e.judgment)

@[instance_reducible]

instance Lechner2004.instDecidableAttested (e : Datum) : Decidable (Attested e)

Equations

• Lechner2004.instDecidableAttested e = { decide := (↑Judgment.marginal.rank).ble ↑e.judgment.rank, reflects_decide := ⋯ }

Comparative Deletion (chapter 2, §2.1)

structure Lechner2004.CDComparative : Type

A clausal comparative with Comparative Deletion is given by its than-clause, with a trace at the deletion site, the position of the pronoun, the antecedent adjective phrase, and the address of the name inside the antecedent.

• thanClause : PhraseStructure.Tree PhraseStructure.Cat Unit

  The than-clause, a trace at the deletion site.

• site : Core.Order.TreePath

  The deletion site.

• pronoun : Core.Order.TreePath

  The pronoun coindexed with the name.

• antecedent : PhraseStructure.Tree PhraseStructure.Cat Unit

  The antecedent adjective phrase of the matrix clause.

• name : List ℕ

  The address of the name inside the antecedent.

def Lechner2004.CDComparative.copy (c : CDComparative) : Core.Order.TreePath

c.copy is the position the copy of the name would occupy in the than-clause.

Equations

• c.copy = { toList := c.site.toList ++ c.name }

def Lechner2004.CDComparative.reconstructed (c : CDComparative) : PhraseStructure.Tree PhraseStructure.Cat Unit

c.reconstructed is the than-clause with the antecedent reconstructed at the site.

Equations

• c.reconstructed = RoseTree.replaceAt c.thanClause c.site.toList c.antecedent

inductive Lechner2004.Resolution : Type

A deletion site is resolved in the semantics, leaving no syntactic copy, by syntactic reconstruction of its antecedent, or by syntactic reconstruction under vehicle change, which makes the copied name a pronoun.

• semantic : Resolution
• syntactic : Resolution
• vehicleChange : Resolution

@[instance_reducible]

instance Lechner2004.instDecidableEqResolution : DecidableEq Resolution

Equations

• Lechner2004.instDecidableEqResolution x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lechner2004.instFintypeResolution : Fintype Resolution

Equations

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

def Lechner2004.instReprResolution.repr : Resolution → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Lechner2004.instReprResolution : Repr Resolution

Equations

• Lechner2004.instReprResolution = { reprPrec := Lechner2004.instReprResolution.repr }

def Lechner2004.Resolution.lf : Resolution → CDComparative → PhraseStructure.Tree PhraseStructure.Cat Unit

r.lf c is the than-clause at LF, which semantic resolution leaves with its trace and syntactic resolution reconstructs.

Equations

• Lechner2004.Resolution.semantic.lf x✝ = x✝.thanClause
• Lechner2004.Resolution.syntactic.lf x✝ = x✝.reconstructed
• Lechner2004.Resolution.vehicleChange.lf x✝ = x✝.reconstructed

def Lechner2004.Resolution.copyClass : Resolution → Binding.BindingClass

The copied name is a pronoun under vehicle change and an R-expression otherwise.

Equations

• Lechner2004.Resolution.vehicleChange.copyClass = Binding.BindingClass.pronoun
• Lechner2004.Resolution.semantic.copyClass = Binding.BindingClass.rExpression
• Lechner2004.Resolution.syntactic.copyClass = Binding.BindingClass.rExpression

def Lechner2004.Resolution.Permits (r : Resolution) (c : CDComparative) : Prop

A resolution permits coreference between the pronoun and the name when the copy of the name at LF, if there is one, meets its binding condition.

Equations

• r.Permits c = Lechner2004.MayCorefer (r.lf c) c.pronoun c.copy r.copyClass

@[instance_reducible]

instance Lechner2004.instDecidablePermits (r : Resolution) (c : CDComparative) : Decidable (r.Permits c)

Equations

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

theorem Lechner2004.cCommands_copy_iff (c : CDComparative) {p : Core.Order.TreePath} (hsp : ¬c.site ≤ p) (hps : ¬p ≤ c.site) : RoseTree.CCommands c.reconstructed p c.copy ↔ RoseTree.CCommands c.thanClause p c.site

Reconstruction puts the copy of the name in the c-command domain of whatever c-commands the deletion site.

def Lechner2004.proudOfJohn : PhraseStructure.Tree PhraseStructure.Cat Unit

proudOfJohn is the antecedent d-proud of John of (24) and (25).

Equations

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

def Lechner2004.cd24 : CDComparative

cd24 is the than-clause of (24), than he is △.

Equations

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

def Lechner2004.cd25 : CDComparative

cd25 is the than-clause of (25), than he believes that I am △.

Equations

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

def Lechner2004.cdData : List (CDComparative × Datum)

cdData pairs each clausal comparative with its row.

Equations

• Lechner2004.cdData = [(Lechner2004.cd24, Lechner2004.Examples.ch2_24), (Lechner2004.cd25, Lechner2004.Examples.ch2_25)]

theorem Lechner2004.copy_present (d : CDComparative × Datum) : d ∈ cdData → RoseTree.subtreeAt d.1.thanClause d.1.pronoun.toList = some np ∧ RoseTree.subtreeAt d.1.reconstructed d.1.copy.toList = some np ∧ RoseTree.subtreeAt d.1.thanClause d.1.copy.toList = none

The pronoun is a nominal of each than-clause, and the copy of the name is a nominal of the reconstructed clause and absent from the unresolved one.

theorem Lechner2004.resolution_fits_iff (r : Resolution) : (∀ d ∈ cdData, r.Permits d.1 ↔ Attested d.2) ↔ r = Resolution.vehicleChange

Of the three resolutions only syntactic reconstruction under vehicle change predicts the judgments of (24) and (25).

Phrasal comparatives (chapter 4, §3.2)

inductive Lechner2004.TestContext : Type

In Lechner's test context A (82) for Prediction V the matrix term is a pronoun and the remnant contains a name, and in test context B (89) the matrix term is a name and the remnant is a pronoun.

• a : TestContext
• b : TestContext

@[instance_reducible]

instance Lechner2004.instDecidableEqTestContext : DecidableEq TestContext

Equations

• Lechner2004.instDecidableEqTestContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lechner2004.instReprTestContext.repr : TestContext → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Lechner2004.instReprTestContext : Repr TestContext

Equations

• Lechner2004.instReprTestContext = { reprPrec := Lechner2004.instReprTestContext.repr }

def Lechner2004.TestContext.pronounName : TestContext → Core.Order.TreePath → Core.Order.TreePath → Core.Order.TreePath × Core.Order.TreePath

k.pronounName m r orders a matrix term at m and a remnant's nominal at r as pronoun and name.

Equations

• Lechner2004.TestContext.a.pronounName x✝¹ x✝ = (x✝¹, x✝)
• Lechner2004.TestContext.b.pronounName x✝¹ x✝ = (x✝, x✝¹)

structure Lechner2004.PhrasalComparative : Type

A phrasal comparative with a coindexed pair is given by its matrix clause, with a trace at the base of the than-phrase, its correlate, its remnant, the matrix term, and the address of the remnant's coindexed nominal.

• matrix : PhraseStructure.Tree PhraseStructure.Cat Unit

  The matrix clause, a trace at the base of the than-phrase.

• thanPhrase : Core.Order.TreePath

  The base of the than-phrase.

• correlate : Core.Order.TreePath

  The correlate of the remnant.

• remnant : PhraseStructure.Tree PhraseStructure.Cat Unit

  The remnant.

• mTerm : Core.Order.TreePath

  The matrix term coindexed with the remnant's nominal.

• inRemnant : List ℕ

  The address of the coindexed nominal inside the remnant.

• context : TestContext

  Which of the two is the pronoun.

def Lechner2004.PhrasalComparative.gapped (e : PhrasalComparative) : PhraseStructure.Tree PhraseStructure.Cat Unit

The Gapped clause of the PC-Hypothesis, the matrix clause with the remnant in the position of the correlate.

Equations

• e.gapped = RoseTree.replaceAt e.matrix e.correlate.toList e.remnant

def Lechner2004.PhrasalComparative.sentence (e : PhrasalComparative) : PhraseStructure.Tree PhraseStructure.Cat Unit

The sentence, the than-phrase in its base with the remnant as its complement.

Equations

• e.sentence = RoseTree.replaceAt e.matrix e.thanPhrase.toList (PhraseStructure.Tree.node PhraseStructure.Cat.P [Lechner2004.word PhraseStructure.Cat.P, e.remnant])

def Lechner2004.PhrasalComparative.direct (e : PhrasalComparative) : PhraseStructure.Tree PhraseStructure.Cat Unit

The LF of the direct analysis adjoins the remnant and the correlate to the clause they leave traces in, so that the clause is one category of three segments.

Equations

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

theorem Lechner2004.PhrasalComparative.gapped_cCommands_iff (e : PhrasalComparative) (m : Core.Order.TreePath) : RoseTree.CCommands e.gapped e.correlate m ↔ RoseTree.CCommands e.matrix e.correlate m

In the Gapped clause the remnant c-commands a matrix term exactly when the correlate c-commands it in the matrix clause (Prediction V).

theorem Lechner2004.PhrasalComparative.cCommands_gapped_iff (e : PhrasalComparative) {m : Core.Order.TreePath} (hcm : ¬e.correlate ≤ m) (hmc : ¬m ≤ e.correlate) (q : List ℕ) : RoseTree.CCommands e.gapped m { toList := e.correlate.toList ++ q } ↔ RoseTree.CCommands e.matrix m e.correlate

A matrix term outside the correlate c-commands a position of the remnant in the Gapped clause exactly when it c-commands the correlate in the matrix clause.

theorem Lechner2004.PhrasalComparative.cCommands_sentence_iff (e : PhrasalComparative) {m : Core.Order.TreePath} (htm : ¬e.thanPhrase ≤ m) (hmt : ¬m ≤ e.thanPhrase) (q : List ℕ) : RoseTree.CCommands e.sentence m { toList := e.thanPhrase.toList ++ q } ↔ RoseTree.CCommands e.matrix m e.thanPhrase

In the sentence a matrix term outside the than-phrase c-commands a position of the remnant exactly when it c-commands the than-phrase, wherever the correlate sits.

theorem Lechner2004.PhrasalComparative.not_cCommands_direct (e : PhrasalComparative) (m q : List ℕ) : ¬RoseTree.CCommands e.direct { toList := 1 :: 1 :: m } { toList := 0 :: q }

At the raised position of the direct analysis no term of the clause c-commands the remnant.

theorem Lechner2004.PhrasalComparative.direct_cCommands (e : PhrasalComparative) (m : List ℕ) : RoseTree.CCommands e.direct { toList := [0] } { toList := 1 :: m }

At the raised position of the direct analysis the remnant c-commands every term of the clause.

inductive Lechner2004.Analysis : Type

A phrasal comparative is analyzed as a Gapped clause, or directly, with Condition C read at the raised position of the remnant or at its base in the than-phrase.

• reduction : Analysis
• directRaised : Analysis
• directBase : Analysis

@[instance_reducible]

instance Lechner2004.instDecidableEqAnalysis : DecidableEq Analysis

Equations

• Lechner2004.instDecidableEqAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lechner2004.instFintypeAnalysis : Fintype Analysis

Equations

• Lechner2004.instFintypeAnalysis = { elems := { val := ↑Lechner2004.Analysis.enumList, nodup := Lechner2004.Analysis.enumList_nodup }, complete := Lechner2004.instFintypeAnalysis._proof_1 }

def Lechner2004.instReprAnalysis.repr : Analysis → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Lechner2004.instReprAnalysis : Repr Analysis

Equations

• Lechner2004.instReprAnalysis = { reprPrec := Lechner2004.instReprAnalysis.repr }

def Lechner2004.Analysis.rep : Analysis → PhrasalComparative → PhraseStructure.Tree PhraseStructure.Cat Unit × Core.Order.TreePath × Core.Order.TreePath

a.rep e is the representation of e under a, with the positions of the matrix term and of the remnant's nominal.

Equations

• Lechner2004.Analysis.reduction.rep x✝ = (x✝.gapped, x✝.mTerm, { toList := x✝.correlate.toList ++ x✝.inRemnant })
• Lechner2004.Analysis.directRaised.rep x✝ = (x✝.direct, { toList := 1 :: 1 :: x✝.mTerm.toList }, { toList := 0 :: x✝.inRemnant })
• Lechner2004.Analysis.directBase.rep x✝ = (x✝.sentence, x✝.mTerm, { toList := x✝.thanPhrase.toList ++ 1 :: x✝.inRemnant })

def Lechner2004.Analysis.pronounName (a : Analysis) (e : PhrasalComparative) : Core.Order.TreePath × Core.Order.TreePath

a.pronounName e gives the positions of the pronoun and the name in a.rep e.

Equations

• a.pronounName e = e.context.pronounName (a.rep e).2.1 (a.rep e).2.2

def Lechner2004.Analysis.Permits (a : Analysis) (e : PhrasalComparative) : Prop

An analysis permits the coreferential reading when the name meets Condition C in its representation.

Equations

• a.Permits e = Lechner2004.MayCorefer (a.rep e).1 (a.pronounName e).1 (a.pronounName e).2 Binding.BindingClass.rExpression

@[instance_reducible]

instance Lechner2004.instDecidablePermits_1 (a : Analysis) (e : PhrasalComparative) : Decidable (a.Permits e)

Equations

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

def Lechner2004.introduced : PhraseStructure.Tree PhraseStructure.Cat Unit

introduced is the English clause subject introduced object to more friends, with a trace at the base of the than-phrase in the degree phrase.

Equations

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

def Lechner2004.ex83 : PhrasalComparative

In (83a), Sally introduced him to more friends than Peter's sister, the correlate, the subject, is higher than the pronoun.

Equations

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

def Lechner2004.ex85 : PhrasalComparative

In (85a), He introduced Sally to more friends than Peter's sister, the correlate, the object, is lower than the pronoun.

Equations

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

def Lechner2004.vorgestellt : PhraseStructure.Tree PhraseStructure.Cat Unit

vorgestellt is the German clause subject dative more people introduced, with a trace at the base of the than-phrase in the degree phrase.

Equations

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

def Lechner2004.ex87a : PhrasalComparative

In (87a), Sie hat ihm mehr Leute vorgestellt als Peters Schwester, with a nominative remnant, the correlate, the subject, is higher than the pronoun.

Equations

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

def Lechner2004.ex87b : PhrasalComparative

In (87b), Er hat ihr mehr Leute vorgestellt als Peters Schwester, with a dative remnant, the correlate, the dative, is lower than the pronoun.

Equations

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

def Lechner2004.schaetzt (subj obj : PhraseStructure.Tree PhraseStructure.Cat Unit) : PhraseStructure.Tree PhraseStructure.Cat Unit

schaetzt subj obj is the German clause subject object more appreciates, with a trace at the base of the than-phrase in the degree adverb.

Equations

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

def Lechner2004.ex90 : PhrasalComparative

In (90a), Die Frau des Präsidenten schätzt die Öffentlichkeit mehr als ihn, the correlate, the object, is lower than the name.

Equations

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

def Lechner2004.ex91 : PhrasalComparative

In (91a), Die Öffentlichkeit schätzt die Frau des Präsidenten mehr als er, the correlate, the subject, is higher than the name.

Equations

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

def Lechner2004.phrasalData : List (PhrasalComparative × Datum)

phrasalData pairs each phrasal comparative with its row.

Equations

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

theorem Lechner2004.rep_nominals (a : Analysis) (d : PhrasalComparative × Datum) : d ∈ phrasalData → RoseTree.subtreeAt (a.rep d.1).1 (a.rep d.1).2.1.toList = some np ∧ RoseTree.subtreeAt (a.rep d.1).1 (a.rep d.1).2.2.toList = some np

The matrix term and the remnant's nominal are nominals of every representation.

theorem Lechner2004.analysis_fits_iff (a : Analysis) : (∀ d ∈ phrasalData, a.Permits d.1 ↔ Attested d.2) ↔ a = Analysis.reduction

Of the three analyses only the Gapped clause predicts the judgments of the minimal pairs.

theorem Lechner2004.direct_same (a : Analysis) (ha : a ≠ Analysis.reduction) : (a.Permits ex83 ↔ a.Permits ex85) ∧ (a.Permits ex87a ↔ a.Permits ex87b) ∧ (a.Permits ex90 ↔ a.Permits ex91)

Each minimal pair receives a single verdict from each reading of the direct analysis.