Bhatt and Takahashi (2011): Reduced and unreduced phrasal comparatives

This file formalizes Bhatt and Takahashi's argument that a phrasal comparative is either the reduction of a clausal source, with the two-place degree head, or genuinely phrasal, with a three-place head taking an individual standard. Their binding generalization (10), that the standard is c-commanded by everything that c-commands the associate, holds in English, the signature of reduction, and fails in Hindi-Urdu, where the standard is an external PP that the matrix pronoun never c-commands. Their scope generalization of §4, that a quantifier in the than-phrase must scope out exactly when its base position c-commands the degree trace, sorts the two languages the same way. Japanese realizes both analyses through the subcategorization of yori, and §6 proposes that both degree heads are available crosslinguistically.

Main results

• BhattTakahashi2011.standard_cCommanded_of_associate: (10) holds under reduction.
• BhattTakahashi2011.english_binding, BhattTakahashi2011.hindi_urdu_binding: the binding data (11)–(13) and (35).
• BhattTakahashi2011.english_scope, BhattTakahashi2011.hindi_urdu_scope: the scope data (43) and (40).
• BhattTakahashi2011.three_cells: the three languages realize distinct analyses.

Implementation notes

Generalization (10) is derived from Lechner's Gapped clause, whose remnant inherits the c-command relations of the correlate. The binding rows code whether the pronoun c-commands the associate as a feature (BindingDatum), and the scope rows are read into the reduced than-clause LFs of (43a) and (43b), where the Heim–Kennedy constraint at the quantifier's base position decides than-phrase-internal scope. The Single Standard Restriction and the Precedence Constraint of §3 and the derivation of Japanese's analyses from yori are not formalized.

TODO

Derive the c-command feature of the binding rows from trees of (11)–(13), as Lechner2004.PhrasalComparative does for Lechner's minimal pairs, so that (10) is checked against the rows rather than presupposed by their coding.

References

• [BT11]
• [Lec04]
• [Lec01]
• [Mer09]

The binding generalization (§2)

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

Generalization (10) holds under reduction, where the standard occupies the position of the associate in the reduced clause, so that whatever c-commands the associate in the matrix clause c-commands every position of the standard.

structure BhattTakahashi2011.BindingDatum : Type

A binding row records whether the matrix pronoun c-commands the associate and whether coreference between the pronoun and an R-expression inside the standard is attested, with the row's label.

• citationId : String
• pronCCommandsAssociate : Bool
• corefAttested : Bool

def BhattTakahashi2011.instDecidableEqBindingDatum.decEq (x✝ x✝¹ : BindingDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance BhattTakahashi2011.instDecidableEqBindingDatum : DecidableEq BindingDatum

Equations

• BhattTakahashi2011.instDecidableEqBindingDatum = BhattTakahashi2011.instDecidableEqBindingDatum.decEq

def BhattTakahashi2011.instReprBindingDatum.repr : BindingDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BhattTakahashi2011.instReprBindingDatum : Repr BindingDatum

Equations

• BhattTakahashi2011.instReprBindingDatum = { reprPrec := BhattTakahashi2011.instReprBindingDatum.repr }

def BhattTakahashi2011.RAPredictsCoref (d : BindingDatum) : Prop

With Condition C, (10) predicts coreference into the standard exactly when the pronoun does not c-command the associate.

Equations

• BhattTakahashi2011.RAPredictsCoref d = (d.pronCCommandsAssociate = false ↔ d.corefAttested = true)

@[instance_reducible]

instance BhattTakahashi2011.instDecidableRAPredictsCoref (d : BindingDatum) : Decidable (RAPredictsCoref d)

Equations

• BhattTakahashi2011.instDecidableRAPredictsCoref d = { decide := decide (d.pronCCommandsAssociate = false) == decide (d.corefAttested = true), reflects_decide := ⋯ }

def BhattTakahashi2011.DAPredictsCoref (d : BindingDatum) : Prop

The direct analysis predicts coreference throughout, since at LF (15) the matrix pronoun does not c-command the standard.

Equations

• BhattTakahashi2011.DAPredictsCoref d = (d.corefAttested = true)

@[instance_reducible]

instance BhattTakahashi2011.instDecidableDAPredictsCoref (d : BindingDatum) : Decidable (DAPredictsCoref d)

Equations

• BhattTakahashi2011.instDecidableDAPredictsCoref d = BhattTakahashi2011.instDecidableDAPredictsCoref._aux_1 d

def BhattTakahashi2011.realizesReduction (data : List BindingDatum) : Prop

Binding data realize the reduction analysis when every datum fits its prediction.

Equations

• BhattTakahashi2011.realizesReduction data = ∀ d ∈ data, BhattTakahashi2011.RAPredictsCoref d

@[instance_reducible]

instance BhattTakahashi2011.instDecidableRealizesReduction (data : List BindingDatum) : Decidable (realizesReduction data)

Equations

• BhattTakahashi2011.instDecidableRealizesReduction data = BhattTakahashi2011.instDecidableRealizesReduction._aux_1 data

def BhattTakahashi2011.realizesDirect (data : List BindingDatum) : Prop

Binding data realize the direct analysis when every datum attests coreference.

Equations

• BhattTakahashi2011.realizesDirect data = ∀ d ∈ data, BhattTakahashi2011.DAPredictsCoref d

@[instance_reducible]

instance BhattTakahashi2011.instDecidableRealizesDirect (data : List BindingDatum) : Decidable (realizesDirect data)

Equations

• BhattTakahashi2011.instDecidableRealizesDirect data = BhattTakahashi2011.instDecidableRealizesDirect._aux_1 data

The rows

def BhattTakahashi2011.bindingOf (e : Datum) : Option BindingDatum

bindingOf e reads a binding row into a BindingDatum, recording whether the matrix pronoun c-commands the associate and whether the coreferential reading the row states is attested.

Equations

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

def BhattTakahashi2011.rowsOf (glottocode : String) : List Datum

rowsOf g lists the rows of the language with Glottocode g.

Equations

• BhattTakahashi2011.rowsOf glottocode = List.filter (fun (x : Datum) => decide (x.language = glottocode)) BhattTakahashi2011.Examples.all

def BhattTakahashi2011.englishBindingPairs : List BindingDatum

englishBindingPairs holds the English minimal pairs (11)–(13).

Equations

• BhattTakahashi2011.englishBindingPairs = List.filterMap BhattTakahashi2011.bindingOf (BhattTakahashi2011.rowsOf "stan1293")

def BhattTakahashi2011.hindiUrduBindingPairs : List BindingDatum

hindiUrduBindingPairs holds the Hindi-Urdu datum (35).

Equations

• BhattTakahashi2011.hindiUrduBindingPairs = List.filterMap BhattTakahashi2011.bindingOf (BhattTakahashi2011.rowsOf "hind1269")

The binding diagnostic (§2, §3.4)

theorem BhattTakahashi2011.english_binding : realizesReduction englishBindingPairs ∧ ¬realizesDirect englishBindingPairs

The English data (11)–(13) realize the reduction analysis, coreference into the standard being possible exactly when the pronoun does not c-command the associate, and rule out the direct analysis.

theorem BhattTakahashi2011.hindi_urdu_binding : realizesDirect hindiUrduBindingPairs ∧ ¬realizesReduction hindiUrduBindingPairs

The Hindi-Urdu datum (35) realizes the direct analysis and rules out reduction, the pronoun c-commanding the associate yet coreferring into the standard.

The scope diagnostic (§4)

structure BhattTakahashi2011.ThanClause : Type

A reduced than-clause LF is given by its tree, the quantifier's base position and the degree trace.

• tree : PhraseStructure.Tree Unit String
• qp : Core.Order.TreePath
• trace : Core.Order.TreePath

def BhattTakahashi2011.thanClause43a : ThanClause

In the reduced than-clause of (43a), than Craige assigned every second year student d-many papers, in a VP shell, the quantifier's base position c-commands the degree trace.

Equations

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

def BhattTakahashi2011.thanClause43b : ThanClause

In the reduced than-clause of (43b), than Craige assigned d-many students every paper by Klein, the quantifier's base position does not c-command the degree trace.

Equations

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

def BhattTakahashi2011.thanClauseOf (e : Datum) : Option ThanClause

A scope row's than-clause has the configuration of (43a) when the quantifier's base position c-commands the degree trace and that of (43b) when it does not.

Equations

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

def BhattTakahashi2011.RAPredictsScope (e : Datum) : Prop

Under reduction, as (43) shows, than-phrase-internal scope is available exactly when the quantifier in its base position satisfies the Heim–Kennedy constraint against the degree abstraction at the root of the than-clause.

Equations

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

@[instance_reducible]

instance BhattTakahashi2011.instDecidableRAPredictsScope (e : Datum) : Decidable (RAPredictsScope e)

Equations

• BhattTakahashi2011.instDecidableRAPredictsScope e = BhattTakahashi2011.instDecidableRAPredictsScope._aux_1 e

theorem BhattTakahashi2011.english_scope (e : Datum) : e ∈ rowsOf "stan1293" → RAPredictsScope e

The English scope data (43a–b) follow the reduction generalization.

theorem BhattTakahashi2011.hindi_urdu_scope : ∃ e ∈ rowsOf "hind1269", ¬RAPredictsScope e

Hindi-Urdu (40) does not follow it, since a quantifier whose base position is below the degree trace still scopes out, as the direct analysis, with no degree trace in the than-phrase, predicts.

The typology (§6)

structure BhattTakahashi2011.HeadAvailability : Type

HeadAvailability records which analyses a language's phrasal comparatives realize.

• reductionRealized : Bool
• directRealized : Bool

def BhattTakahashi2011.instDecidableEqHeadAvailability.decEq (x✝ x✝¹ : HeadAvailability) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance BhattTakahashi2011.instDecidableEqHeadAvailability : DecidableEq HeadAvailability

Equations

• BhattTakahashi2011.instDecidableEqHeadAvailability = BhattTakahashi2011.instDecidableEqHeadAvailability.decEq

def BhattTakahashi2011.instReprHeadAvailability.repr : HeadAvailability → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BhattTakahashi2011.instReprHeadAvailability : Repr HeadAvailability

Equations

• BhattTakahashi2011.instReprHeadAvailability = { reprPrec := BhattTakahashi2011.instReprHeadAvailability.repr }

def BhattTakahashi2011.headAvailabilityFromBinding (data : List BindingDatum) : HeadAvailability

headAvailabilityFromBinding data decides from the two predictions which analyses the binding data realize.

Equations

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

inductive BhattTakahashi2011.Language : Type

Language enumerates the surveyed languages.

• english : Language
• hindiUrdu : Language
• japanese : Language

@[instance_reducible]

instance BhattTakahashi2011.instDecidableEqLanguage : DecidableEq Language

Equations

• BhattTakahashi2011.instDecidableEqLanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BhattTakahashi2011.instReprLanguage : Repr Language

Equations

• BhattTakahashi2011.instReprLanguage = { reprPrec := BhattTakahashi2011.instReprLanguage.repr }

def BhattTakahashi2011.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

def BhattTakahashi2011.headAvailability : Language → HeadAvailability

English and Hindi-Urdu realize the analyses their binding data decide, and Japanese realizes both, a clausal or multiple-standard complement of yori taking the two-place head and a DP complement the three-place one (§6).

Equations

• BhattTakahashi2011.headAvailability BhattTakahashi2011.Language.english = BhattTakahashi2011.headAvailabilityFromBinding BhattTakahashi2011.englishBindingPairs
• BhattTakahashi2011.headAvailability BhattTakahashi2011.Language.hindiUrdu = BhattTakahashi2011.headAvailabilityFromBinding BhattTakahashi2011.hindiUrduBindingPairs
• BhattTakahashi2011.headAvailability BhattTakahashi2011.Language.japanese = { reductionRealized := true, directRealized := true }

theorem BhattTakahashi2011.three_cells : headAvailability Language.english = { reductionRealized := true, directRealized := false } ∧ headAvailability Language.hindiUrdu = { reductionRealized := false, directRealized := true } ∧ ∀ (l l' : Language), headAvailability l = headAvailability l' → l = l'

English realizes reduction alone and Hindi-Urdu the direct analysis alone, so the three languages occupy three cells of the grid.