Documentation

Studies.DechaineWiltschko2002

Déchaine and Wiltschko (2002): Decomposing Pronouns #

This file formalizes the categorial typology of proforms of Déchaine and Wiltschko. The notion "pronoun" is not a primitive: a proform is a DP, a φP or an NP by the layers it projects, and its category fixes its distribution and its binding-theoretic status, table (24). A DP is an argument and an R-expression under Condition C, a φP an argument or a predicate and a variable under Condition B, and an NP a predicate and undefined for binding theory, its behaviour following from its inherent semantics as a constant. Halkomelem independent pronouns are DPs, Shuswap ones φPs and Japanese kare an NP. In English, one is an NP, first and second person pronouns are DPs, which is why they precede nouns, we linguists, and third person pronouns are φPs, *they linguists, the dialect that says them linguists having reanalyzed them as the D-morpheme th- over the clitic φP 'em. The English categories are derived from the Fragment's person features, and the determiner and bound-variable data are rows.

References #

[DW02]

The categories #

inductive DechaineWiltschko2002.Layer :

The layers a proform may project.

D : Layer
phi : Layer
N : Layer

Instances For

@[instance_reducible]

instance DechaineWiltschko2002.instDecidableEqLayer :

DecidableEq Layer

Equations

DechaineWiltschko2002.instDecidableEqLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DechaineWiltschko2002.instReprLayer.repr :

Layer → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance DechaineWiltschko2002.instReprLayer :

Repr Layer

Equations

DechaineWiltschko2002.instReprLayer = { reprPrec := DechaineWiltschko2002.instReprLayer.repr }

inductive DechaineWiltschko2002.Category :

The three categories, by size: a full DP over a φP over an NP, a φP over an NP, or a bare NP, (1).

proDP : Category
prophiP : Category
proNP : Category

Instances For

@[instance_reducible]

instance DechaineWiltschko2002.instDecidableEqCategory :

DecidableEq Category

Equations

DechaineWiltschko2002.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DechaineWiltschko2002.instReprCategory.repr :

Category → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance DechaineWiltschko2002.instReprCategory :

Equations

DechaineWiltschko2002.instReprCategory = { reprPrec := DechaineWiltschko2002.instReprCategory.repr }

def DechaineWiltschko2002.Category.layers :

Category → List Layer

The layers of a category, from the top down.

Equations

Instances For

theorem DechaineWiltschko2002.layers_suffix :

Category.proNP.layers <:+ Category.prophiP.layers ∧ Category.prophiP.layers <:+ Category.proDP.layers

The categories nest: each is the next larger one without its top layer.

def DechaineWiltschko2002.Category.top :

Category → Layer

The top layer of a category.

Equations

Instances For

inductive DechaineWiltschko2002.BindingStatus :

Binding-theoretic status: an R-expression under Condition C, a variable under Condition B, or undefined, the behaviour following from inherent semantics.

rExpression : BindingStatus
variable : BindingStatus
undefined : BindingStatus

Instances For

@[instance_reducible]

instance DechaineWiltschko2002.instDecidableEqBindingStatus :

DecidableEq BindingStatus

Equations

DechaineWiltschko2002.instDecidableEqBindingStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DechaineWiltschko2002.instReprBindingStatus :

Repr BindingStatus

Equations

DechaineWiltschko2002.instReprBindingStatus = { reprPrec := DechaineWiltschko2002.instReprBindingStatus.repr }

def DechaineWiltschko2002.instReprBindingStatus.repr :

BindingStatus → ℕ → Std.Format

Equations

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

Instances For

def DechaineWiltschko2002.Category.bindingStatus (c : Category) :

Binding status is defined by the top layer, (24): R-expressions are DPs, variables are φPs, and NPs, constants, are undefined for binding theory.

Equations

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

Instances For

inductive DechaineWiltschko2002.Position :

The positions a nominal fills.

argument : Position
predicate : Position

Instances For

@[instance_reducible]

instance DechaineWiltschko2002.instDecidableEqPosition :

DecidableEq Position

Equations

DechaineWiltschko2002.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DechaineWiltschko2002.instReprPosition.repr :

Position → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance DechaineWiltschko2002.instReprPosition :

Equations

DechaineWiltschko2002.instReprPosition = { reprPrec := DechaineWiltschko2002.instReprPosition.repr }

def DechaineWiltschko2002.Category.CanBe :

Category → Position → Prop

Distribution, (25): a DP is an argument, an NP a predicate, and a φP is type flexible.

Equations

Instances For

theorem DechaineWiltschko2002.canBe_argument_iff (c : Category) :

c.CanBe Position.argument ↔ c ≠ Category.proNP

(25c) and (25d): not every argument is a DP, and not every nominal predicate an NP.

theorem DechaineWiltschko2002.canBe_predicate_iff (c : Category) :

c.CanBe Position.predicate ↔ c ≠ Category.proDP

English (§3) #

def DechaineWiltschko2002.english (p : PersonalPronoun) :

The category of an English personal pronoun, from its person: first and second person pronouns are DPs and third person pronouns φPs, (33).

Equations

DechaineWiltschko2002.english p = if p.person = some Person.third then DechaineWiltschko2002.Category.prophiP else DechaineWiltschko2002.Category.proDP

Instances For

def DechaineWiltschko2002.dialectB (p : PersonalPronoun) :

Dialect B, (34) and (37c): the accusative third person plural them is reanalyzed as the D-morpheme th- over the clitic φP 'em, a DP.

Equations

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

Instances For

The rows #

def DechaineWiltschko2002.categoryOf (e : Datum) :

Option Category

The category of a row's proform: the English pronouns' from the Fragment, dialect B's them reanalyzed, and one and Japanese kare the NPs of sections 3.1 and 2.3.

Equations

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

Instances For

theorem DechaineWiltschko2002.determiner_rows (e : Datum) :

e ∈ Examples.all → e.feature? "test" = some "precedesNoun" → ∀ c ∈ categoryOf e, e.judgment = Judgment.acceptable ↔ c = Category.proDP

A pronoun precedes a noun exactly when it is a DP, whose D takes an overt NP: we linguists and us linguists against *they linguists, and dialect B's them linguists.

def DechaineWiltschko2002.boundJudgment (e : Datum) :

The judgment of a row's bound-variable construal: under VP-ellipsis its sloppy reading's, otherwise the row's own, whose indices mark the bound construal.

Equations

DechaineWiltschko2002.boundJudgment e = (List.lookup "sloppy" e.readings).getD e.judgment

Instances For

theorem DechaineWiltschko2002.bound_variable_rows (e : Datum) :

e ∈ Examples.all → e.feature? "test" = some "boundVariable" → ∀ c ∈ categoryOf e, boundJudgment e = Judgment.acceptable ↔ c.bindingStatus = BindingStatus.variable

A proform is construed as a bound variable exactly when its category makes it a variable: he under every candidate, but not me under VP-ellipsis, the sloppy reading of (40), nor one or kare under a quantifier, (30) and (22).