Funakoshi (2016): Verb-Stranding Verb Phrase Ellipsis in Japanese

This file formalizes [Fun16]'s argument that Japanese has verb-stranding verb phrase ellipsis. Adjuncts in Japanese were held never to be null; the paper shows that a manner, instrumental or temporal adjunct is understood as null when the clause-mate object is null too or the clause is intransitive, and never when an object stays overt, unless that object is contrastively focused (its generalizations (12) and (59)). Pro and argument ellipsis reach arguments only, so a null adjunct needs ellipsis of the verb phrase with the verb raised out of it: [E] on Voice in the clausal spine of Minimalist.Ellipsis ([Mer01]), the verb stranded above it. Everything in the site goes, so the object goes with the adjunct or escapes by scrambling, and an object scrambled out of the site is a pseudogapping remnant, which must be contrastively focused. Reason adverbial clauses scope above negation and so sit above the site; they cannot be null even beside a null object. NullAdjunct states the derivation of the reading and nullAdjunct_iff reads the generalizations off the spine: the adjunct attaches inside the verb phrase and the object is not an unfocused overt remnant. The rival that keeps argument ellipsis as the only strategy, the oblique movement of the adjunct onto a null argument, undergenerates in intransitive clauses and overgenerates with null subjects and with reason clauses (rows_not_oblique), and argument ellipsis alone derives no null adjunct at all. The rows are the paper's ellipsis clauses under the null adjunct reading (rows_predicted).

Implementation notes

• The paper's (40), where okurete 'late' resists the null reading in an intransitive clause, is left out: the paper attributes it to the adverb's degradation under negation in non-elliptical sentences as well.
• An overt object is recorded as contrastively focused or not; givenness is not recorded, so the functional account of §2.1, which the paper refutes with the new objects of (26) and (27), stays in the prose.
• The examples are Data.Examples.Funakoshi2016.

References

• [Fun16]
• [Mer01]

inductive Funakoshi2016.Attachment : Type

Where the adjunct attaches: inside the verb phrase, as manner, instrumental and temporal adjuncts do, or above negation, as reason adverbial clauses do.

• vp : Attachment
• reason : Attachment

@[instance_reducible]

instance Funakoshi2016.instDecidableEqAttachment : DecidableEq Attachment

Equations

• Funakoshi2016.instDecidableEqAttachment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Funakoshi2016.instFintypeAttachment : Fintype Attachment

Equations

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

@[instance_reducible]

instance Funakoshi2016.instReprAttachment : Repr Attachment

Equations

• Funakoshi2016.instReprAttachment = { reprPrec := Funakoshi2016.instReprAttachment.repr }

def Funakoshi2016.instReprAttachment.repr : Attachment → ℕ → Std.Format

Equations

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

def Funakoshi2016.Attachment.site : Attachment → Minimalist.ClauseSpine.Site

The site of the adjunct, adjoined to VP, or to TP above the negation a reason clause outscopes.

Equations

• Funakoshi2016.Attachment.vp.site = Minimalist.ClauseSpine.Site.adjunct Minimalist.Cat.V
• Funakoshi2016.Attachment.reason.site = Minimalist.ClauseSpine.Site.adjunct Minimalist.Cat.T

inductive Funakoshi2016.ObjectStatus : Type

The clause-mate object of the ellipsis clause: absent in an intransitive clause, null, overt without contrastive focus, or overt and contrastively focused.

• absent : ObjectStatus
• null : ObjectStatus
• overt : ObjectStatus
• focused : ObjectStatus

@[instance_reducible]

instance Funakoshi2016.instDecidableEqObjectStatus : DecidableEq ObjectStatus

Equations

• Funakoshi2016.instDecidableEqObjectStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Funakoshi2016.instFintypeObjectStatus : Fintype ObjectStatus

Equations

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

@[instance_reducible]

instance Funakoshi2016.instReprObjectStatus : Repr ObjectStatus

Equations

• Funakoshi2016.instReprObjectStatus = { reprPrec := Funakoshi2016.instReprObjectStatus.repr }

def Funakoshi2016.instReprObjectStatus.repr : ObjectStatus → ℕ → Std.Format

Equations

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

structure Funakoshi2016.Config : Type

An ellipsis clause under the null adjunct reading.

• adjunct : Attachment
• object : ObjectStatus
• subjectNull : Bool

def Funakoshi2016.instDecidableEqConfig.decEq (x✝ x✝¹ : Config) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Funakoshi2016.instDecidableEqConfig : DecidableEq Config

Equations

• Funakoshi2016.instDecidableEqConfig = Funakoshi2016.instDecidableEqConfig.decEq

def Funakoshi2016.instReprConfig.repr : Config → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Funakoshi2016.instReprConfig : Repr Config

Equations

• Funakoshi2016.instReprConfig = { reprPrec := Funakoshi2016.instReprConfig.repr }

def Funakoshi2016.NullAdjunct (c : Config) : Prop

The null adjunct reading by verb-stranding ellipsis, [E] on Voice deleting the verb phrase with its adjuncts while the verb, raised to tense, is stranded: the adjunct sits in the site, and the object, if any, is elided with it or extracted as a contrastively focused remnant.

Equations

• Funakoshi2016.NullAdjunct c = (Minimalist.Ellipsis.vpEllipsis.Deletes c.adjunct.site ∧ c.object ≠ Funakoshi2016.ObjectStatus.overt)

@[instance_reducible]

instance Funakoshi2016.instDecidablePredConfigNullAdjunct : DecidablePred NullAdjunct

Equations

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

theorem Funakoshi2016.nullAdjunct_iff (c : Config) : NullAdjunct c ↔ c.adjunct = Attachment.vp ∧ c.object ≠ ObjectStatus.overt

Generalizations (12) and (59) with the prediction of §2.2: an adjunct is null only inside the verb phrase and only with the object null, absent, or a contrastively focused remnant.

def Funakoshi2016.ObliqueMovement (c : Config) : Prop

Takahashi's oblique movement: the adjunct adjoins to a null argument, and argument ellipsis takes both.

Equations

• Funakoshi2016.ObliqueMovement c = (c.object = Funakoshi2016.ObjectStatus.null ∨ c.subjectNull = true)

@[instance_reducible]

instance Funakoshi2016.instDecidablePredConfigObliqueMovement : DecidablePred ObliqueMovement

Equations

• Funakoshi2016.instDecidablePredConfigObliqueMovement x✝ = { decide := decide (x✝.object = Funakoshi2016.ObjectStatus.null) || decide (x✝.subjectNull = true), reflects_decide := ⋯ }

The paper's ellipsis clauses

structure Funakoshi2016.Row : Type

An ellipsis clause of the paper and whether its null adjunct reading is available.

• config : Config
• available : Bool

@[instance_reducible]

instance Funakoshi2016.instDecidableEqRow : DecidableEq Row

Equations

• Funakoshi2016.instDecidableEqRow = Funakoshi2016.instDecidableEqRow.decEq

def Funakoshi2016.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• Funakoshi2016.instDecidableEqRow.decEq { config := a, available := a_1 } { config := b, available := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Funakoshi2016.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Funakoshi2016.rows : List Row

Equations

• Funakoshi2016.rows = List.filterMap Funakoshi2016.Row.ofDatum Funakoshi2016.Examples.all

theorem Funakoshi2016.rows_predicted (r : Row) : r ∈ rows → (r.available = true ↔ NullAdjunct r.config)

The null adjunct reading is available exactly where verb-stranding ellipsis derives it.

theorem Funakoshi2016.rows_exists_available : ∃ r ∈ rows, r.available = true

Adjuncts can be null, which argument ellipsis alone never derives.

theorem Funakoshi2016.rows_not_oblique : ¬∀ r ∈ rows, r.available = true ↔ ObliqueMovement r.config

Oblique movement undergenerates the intransitive (39) and overgenerates the null-subject clauses (43) and (44) and the reason clause (32).