Sadakane and Koizumi (1995)

Japanese particles after a noun phrase divide into case markers, which cliticize onto the noun phrase, and postpositions, which head a phrase over it. The particle ni seems to behave as both. Sadakane and Koizumi argue that it is four homophonous particles: the dative case marker, a postposition, the ni inserted on a caseless subject, and a form of the copula. Three tests separate them, a floating numeral quantifier and a cleft with and without the particle. The uses of ni that pass all three are ambiguous between the case marker and the postposition, and the paper ties the choice between the two to how affected the referent of the noun phrase is.

Main definitions

• Attachment: whether a particle cliticizes onto its noun phrase or heads a phrase over it.
• Particle, Test, Particle.Passes: the four classes of particle, the three tests, and which classes pass which tests.
• Position: the argument positions of the affectedness hierarchy (45).

Main statements

• Attachment.hostsQuantifier_iff: a numeral quantifier and its host c-command each other exactly when the particle cliticizes.
• Particle.passes_caseMarker, Particle.passes_postposition, Particle.passes_insertion, Particle.not_passes_copula: the tables (14), (29) and (32).
• exists_passes_and_exists_passes_iff: a use of ni passing both of the first two tests is ambiguous between the case marker and the postposition.
• judgment_eq_acceptable_iff: every test example is acceptable exactly when its particle passes the test.
• judgment_eq_acceptable_iff_affected: a floating quantifier goes with a ni phrase exactly when its referent may be affected.
• Position.lt_iff_cCommands: the hierarchy (45) orders the arguments of Koizumi's tree (44) by c-command.

Implementation notes

• A test is passed when the paper marks it OK without qualification, so the postposition's cleft without the particle, */?/OK in (14), fails. An example printed with two marks records the first as its judgment and the second as alsoJudged.
• The cleft with the particle follows Nakayama's account, which the paper offers for concreteness without adopting it.
• Martin's 31 uses of ni are the category labels of the examples, and the class the paper assigns each is a particle label, two for an ambiguous use.
• The judgments are those of the innovating variety (note 9). Morii's acquisition study, which the paper reports, is not formalized.

References

• [SK95]
• [Kur65]
• [Mar75]
• [Miy89]
• [Nak89]
• [Tak87]
• [Koi94]
• [Mor93]

Case markers and postpositions

inductive SadakaneKoizumi1995.Attachment : Type

A particle either cliticizes onto the noun phrase it follows, as a case marker does, [NP John-ga], or takes the noun phrase as its complement and heads a phrase, as a postposition does, [PP [NP John] kara] ((1)).

• clitic : Attachment

  The particle cliticizes onto the noun phrase.

• head (u : UD.UPOS) : Attachment

  The particle heads a phrase of part of speech u over the noun phrase.

def SadakaneKoizumi1995.instDecidableEqAttachment.decEq (x✝ x✝¹ : Attachment) : Decidable (x✝ = x✝¹)

Equations

• SadakaneKoizumi1995.instDecidableEqAttachment.decEq SadakaneKoizumi1995.Attachment.clitic SadakaneKoizumi1995.Attachment.clitic = isTrue ⋯
• SadakaneKoizumi1995.instDecidableEqAttachment.decEq SadakaneKoizumi1995.Attachment.clitic (SadakaneKoizumi1995.Attachment.head u) = isFalse ⋯
• SadakaneKoizumi1995.instDecidableEqAttachment.decEq (SadakaneKoizumi1995.Attachment.head u) SadakaneKoizumi1995.Attachment.clitic = isFalse ⋯
• SadakaneKoizumi1995.instDecidableEqAttachment.decEq (SadakaneKoizumi1995.Attachment.head a) (SadakaneKoizumi1995.Attachment.head b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SadakaneKoizumi1995.instDecidableEqAttachment : DecidableEq Attachment

Equations

• SadakaneKoizumi1995.instDecidableEqAttachment = SadakaneKoizumi1995.instDecidableEqAttachment.decEq

def SadakaneKoizumi1995.CaseAssignable (c : PhraseStructure.Cat) : Prop

A category can bear Case when it is an NP or a PP; an AP cannot ((10)).

Equations

• SadakaneKoizumi1995.CaseAssignable c = (c = PhraseStructure.Cat.N ∨ c = PhraseStructure.Cat.P)

@[instance_reducible]

instance SadakaneKoizumi1995.instDecidablePredCatCaseAssignable : DecidablePred CaseAssignable

Equations

• SadakaneKoizumi1995.instDecidablePredCatCaseAssignable x✝ = { decide := decide (x✝ = PhraseStructure.Cat.N) || decide (x✝ = PhraseStructure.Cat.P), reflects_decide := ⋯ }

def SadakaneKoizumi1995.Attachment.phrase : Attachment → PhraseStructure.Tree PhraseStructure.Cat Unit

a.phrase is the phrase a particle forms with its noun phrase.

Equations

• One or more equations did not get rendered due to their size.
• SadakaneKoizumi1995.Attachment.clitic.phrase = PhraseStructure.Tree.terminal PhraseStructure.Cat.N ()

def SadakaneKoizumi1995.Attachment.quantifierTree (a : Attachment) : PhraseStructure.Tree PhraseStructure.Cat Unit

In the clause of (6) and (7), the particle's phrase, a floating numeral quantifier and the verb are sisters.

Equations

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

def SadakaneKoizumi1995.Attachment.host : Attachment → Core.Order.TreePath

a.host is the position of the noun phrase in a.quantifierTree.

Equations

• SadakaneKoizumi1995.Attachment.clitic.host = { toList := [0] }
• (SadakaneKoizumi1995.Attachment.head u).host = { toList := [0, 0] }

def SadakaneKoizumi1995.Attachment.HostsQuantifier (a : Attachment) : Prop

A noun phrase hosts a floating numeral quantifier when the two c-command each other ([Miy89]), with c-command as note 4 defines it.

Equations

• a.HostsQuantifier = (RoseTree.CCommands a.quantifierTree a.host { toList := [1] } ∧ RoseTree.CCommands a.quantifierTree { toList := [1] } a.host)

@[instance_reducible]

instance SadakaneKoizumi1995.Attachment.instDecidablePredHostsQuantifier : DecidablePred HostsQuantifier

Equations

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

theorem SadakaneKoizumi1995.Attachment.hostsQuantifier_iff {a : Attachment} : a.HostsQuantifier ↔ a = clitic

A noun phrase hosts a floating quantifier exactly when its particle cliticizes. A particle that heads a phrase puts a branching node above the noun phrase that does not dominate the quantifier, as "the PP node prevents the NP from c-commanding the numeral quantifier" (§2) and the copula's VP does the same (§3).

def SadakaneKoizumi1995.Attachment.Focusable (a : Attachment) : Prop

A particle's phrase can be the focus of a cleft when it can bear Case and bears none yet. On [Nak89]'s account the copula da assigns Case to its complement, so a case-marked NP would be doubly case-marked ((8)) while a PP can be the focus ((9)).

Equations

• a.Focusable = (SadakaneKoizumi1995.CaseAssignable a.phrase.cat ∧ a ≠ SadakaneKoizumi1995.Attachment.clitic)

@[instance_reducible]

instance SadakaneKoizumi1995.Attachment.instDecidablePredFocusable : DecidablePred Focusable

Equations

• x✝.instDecidablePredFocusable = { decide := decide (SadakaneKoizumi1995.CaseAssignable x✝.phrase.cat) && decide (x✝ ≠ SadakaneKoizumi1995.Attachment.clitic), reflects_decide := ⋯ }

theorem SadakaneKoizumi1995.Attachment.not_hostsQuantifier_and_focusable (a : Attachment) : ¬(a.HostsQuantifier ∧ a.Focusable)

No particle both lets its noun phrase host a floating quantifier and lets its phrase be the focus of a cleft, so none behaves as a case marker and as a postposition at once (§4).

The four particles

inductive SadakaneKoizumi1995.Particle : Type

The tests separate four classes of particle, [Kur65]'s case markers and postpositions together with the ni of ni insertion and the copula.

• caseMarker : Particle

  A case marker, such as ga, o and the dative ni.

• postposition : Particle

  A postposition, such as kara, de and the postposition ni.

• insertion : Particle

  The ni inserted on a caseless noun phrase ([Tak87]).

• copula : Particle

  The copula, one of whose forms is ni.

@[instance_reducible]

instance SadakaneKoizumi1995.instDecidableEqParticle : DecidableEq Particle

Equations

• SadakaneKoizumi1995.instDecidableEqParticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SadakaneKoizumi1995.instFintypeParticle : Fintype Particle

Equations

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

def SadakaneKoizumi1995.instReprParticle.repr : Particle → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SadakaneKoizumi1995.instReprParticle : Repr Particle

Equations

• SadakaneKoizumi1995.instReprParticle = { reprPrec := SadakaneKoizumi1995.instReprParticle.repr }

inductive SadakaneKoizumi1995.Test : Type

The paper tests a use of a particle in three constructions (§2).

• quantifierFloat : Test

  A floating numeral quantifier goes with the noun phrase ((6), (7)).

• cleftWithParticle : Test

  The noun phrase and its particle are the focus of a cleft ((8), (9)).

• cleftWithoutParticle : Test

  The noun phrase without its particle is the focus of a cleft ((11), (12)).

@[instance_reducible]

instance SadakaneKoizumi1995.instDecidableEqTest : DecidableEq Test

Equations

• SadakaneKoizumi1995.instDecidableEqTest x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SadakaneKoizumi1995.instFintypeTest : Fintype Test

Equations

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

@[instance_reducible]

instance SadakaneKoizumi1995.instReprTest : Repr Test

Equations

• SadakaneKoizumi1995.instReprTest = { reprPrec := SadakaneKoizumi1995.instReprTest.repr }

def SadakaneKoizumi1995.instReprTest.repr : Test → ℕ → Std.Format

Equations

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

def SadakaneKoizumi1995.Particle.attachment : Particle → Attachment

A case marker cliticizes. A postposition heads a PP, and so does the ni of ni insertion, which is a postposition; the copula heads a VP (§3).

Equations

• SadakaneKoizumi1995.Particle.caseMarker.attachment = SadakaneKoizumi1995.Attachment.clitic
• SadakaneKoizumi1995.Particle.postposition.attachment = SadakaneKoizumi1995.Attachment.head UD.UPOS.ADP
• SadakaneKoizumi1995.Particle.insertion.attachment = SadakaneKoizumi1995.Attachment.head UD.UPOS.ADP
• SadakaneKoizumi1995.Particle.copula.attachment = SadakaneKoizumi1995.Attachment.head UD.UPOS.VERB

def SadakaneKoizumi1995.Particle.MarksSubject : Particle → Prop

The ni of ni insertion marks only a noun phrase in the subject position, Spec,IP (§3).

Equations

• SadakaneKoizumi1995.Particle.insertion.MarksSubject = True
• x✝.MarksSubject = False

@[instance_reducible]

instance SadakaneKoizumi1995.Particle.instDecidablePredMarksSubject : DecidablePred MarksSubject

Equations

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

def SadakaneKoizumi1995.Particle.Passes : Particle → Test → Prop

A particle passes a test when its noun phrase hosts a floating quantifier, when its phrase is focusable and not confined to subjects, or, with the particle left out, when what the particle contributes can be recovered. A case marker contributes nothing, and the noun phrase of the ni of ni insertion is the subject, the most accessible relation of (13).

Equations

• x✝.Passes SadakaneKoizumi1995.Test.quantifierFloat = x✝.attachment.HostsQuantifier
• x✝.Passes SadakaneKoizumi1995.Test.cleftWithParticle = (x✝.attachment.Focusable ∧ ¬x✝.MarksSubject)
• x✝.Passes SadakaneKoizumi1995.Test.cleftWithoutParticle = (x✝.attachment = SadakaneKoizumi1995.Attachment.clitic ∨ x✝.MarksSubject)

@[instance_reducible]

instance SadakaneKoizumi1995.Particle.instDecidablePredTestPasses (p : Particle) : DecidablePred p.Passes

Equations

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

theorem SadakaneKoizumi1995.Particle.passes_quantifierFloat_iff {p : Particle} : p.Passes Test.quantifierFloat ↔ p = caseMarker

theorem SadakaneKoizumi1995.Particle.passes_cleftWithParticle_iff {p : Particle} : p.Passes Test.cleftWithParticle ↔ p = postposition

theorem SadakaneKoizumi1995.Particle.passes_caseMarker {t : Test} : caseMarker.Passes t ↔ t ≠ Test.cleftWithParticle

A case marker passes the numeral quantifier test and the cleft without the particle ((14)).

theorem SadakaneKoizumi1995.Particle.passes_postposition {t : Test} : postposition.Passes t ↔ t = Test.cleftWithParticle

A postposition passes only the cleft with the particle ((14)).

theorem SadakaneKoizumi1995.Particle.passes_insertion {t : Test} : insertion.Passes t ↔ t = Test.cleftWithoutParticle

The ni of ni insertion passes only the cleft without the particle ((29)).

theorem SadakaneKoizumi1995.Particle.not_passes_copula (t : Test) : ¬copula.Passes t

The copula passes none of the tests ((32)).

theorem SadakaneKoizumi1995.Particle.passes_injective : Function.Injective Passes

The three tests tell the four particles apart.

Ambiguity

theorem SadakaneKoizumi1995.exists_passes_and_exists_passes_iff {S : List Particle} : ((∃ p ∈ S, p.Passes Test.quantifierFloat) ∧ ∃ p ∈ S, p.Passes Test.cleftWithParticle) ↔ Particle.caseMarker ∈ S ∧ Particle.postposition ∈ S

A use of ni that passes both the numeral quantifier test and the cleft with the particle can be read both as the case marker and as the postposition. Such uses are what mislead the view of ni as a third kind of particle (§4).

theorem SadakaneKoizumi1995.exists_passes_of_ambiguous (t : Test) : ∃ p ∈ [Particle.caseMarker, Particle.postposition], p.Passes t

A use of ni that can be read as the case marker or as the postposition passes every test ((27)).

Affectedness

inductive SadakaneKoizumi1995.Reading : Type

The paper reads the referent of a noun phrase as affected or not by the action the verb denotes (§4).

• affected : Reading

  The referent is affected, as a recipient who comes to possess something is.

• nonaffected : Reading

  The referent is less affected, or not at all.

@[instance_reducible]

instance SadakaneKoizumi1995.instDecidableEqReading : DecidableEq Reading

Equations

• SadakaneKoizumi1995.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SadakaneKoizumi1995.instFintypeReading : Fintype Reading

Equations

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

@[instance_reducible]

instance SadakaneKoizumi1995.instReprReading : Repr Reading

Equations

• SadakaneKoizumi1995.instReprReading = { reprPrec := SadakaneKoizumi1995.instReprReading.repr }

def SadakaneKoizumi1995.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

def SadakaneKoizumi1995.Reading.particle : Reading → Particle

The case marker ni marks a noun phrase whose referent is affected, and the postposition one whose referent is less affected (§4).

Equations

• SadakaneKoizumi1995.Reading.affected.particle = SadakaneKoizumi1995.Particle.caseMarker
• SadakaneKoizumi1995.Reading.nonaffected.particle = SadakaneKoizumi1995.Particle.postposition

inductive SadakaneKoizumi1995.Position : Type

The affectedness hierarchy (45) places a noun phrase in a PP below the dative, and the dative below the upper and the lower accusative.

• npInPP : Position

  A noun phrase in a PP, the least affected.

• dative : Position

  The dative, the indirect object.

• upperAccusative : Position

  The upper accusative, a nonaffected theme.

• lowerAccusative : Position

  The lower accusative, an affected theme.

@[instance_reducible]

instance SadakaneKoizumi1995.instDecidableEqPosition : DecidableEq Position

Equations

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

@[instance_reducible]

instance SadakaneKoizumi1995.instFintypePosition : Fintype Position

Equations

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

def SadakaneKoizumi1995.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SadakaneKoizumi1995.instReprPosition : Repr Position

Equations

• SadakaneKoizumi1995.instReprPosition = { reprPrec := SadakaneKoizumi1995.instReprPosition.repr }

def SadakaneKoizumi1995.Position.rank : Position → Fin 4

p.rank is the place of p in (45), counting from the least affected.

Equations

• SadakaneKoizumi1995.Position.npInPP.rank = 0
• SadakaneKoizumi1995.Position.dative.rank = 1
• SadakaneKoizumi1995.Position.upperAccusative.rank = 2
• SadakaneKoizumi1995.Position.lowerAccusative.rank = 3

@[instance_reducible]

instance SadakaneKoizumi1995.Position.instLinearOrder : LinearOrder Position

Equations

• SadakaneKoizumi1995.Position.instLinearOrder = LinearOrder.lift' SadakaneKoizumi1995.Position.rank SadakaneKoizumi1995.Position.instLinearOrder._proof_1

def SadakaneKoizumi1995.Position.tree44 : PhraseStructure.Tree Unit Unit

Koizumi's tree (44) puts the affected goal above the nonaffected theme above the affected theme, [VP NP-dat [V' [VP NP-acc [V' NP-acc V]] V]].

Equations

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

def SadakaneKoizumi1995.Position.site? : Position → Option Core.Order.TreePath

p.site? is the position of the argument p in tree44; the noun phrase in a PP, which the paper adds to Koizumi's hierarchy, has none.

Equations

• SadakaneKoizumi1995.Position.npInPP.site? = none
• SadakaneKoizumi1995.Position.dative.site? = some { toList := [0] }
• SadakaneKoizumi1995.Position.upperAccusative.site? = some { toList := [1, 0, 0] }
• SadakaneKoizumi1995.Position.lowerAccusative.site? = some { toList := [1, 0, 1, 0] }

theorem SadakaneKoizumi1995.Position.lt_iff_cCommands (p q : Position) (a : Core.Order.TreePath) : a ∈ p.site? → ∀ b ∈ q.site?, p < q ↔ RoseTree.CCommands tree44 a b

Of two arguments of (44), the less affected c-commands the more affected, since [Koi94] links an argument's structural height inversely to its affectedness (§4).

The examples

def SadakaneKoizumi1995.particleLabels : List (String × Particle)

The examples name the four particles by their constructors.

Equations

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

def SadakaneKoizumi1995.testLabels : List (String × Test)

The examples name the three tests by their constructors.

Equations

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

def SadakaneKoizumi1995.readingLabels : List (String × Reading)

The examples name the two readings by their constructors.

Equations

• SadakaneKoizumi1995.readingLabels = [("affected", SadakaneKoizumi1995.Reading.affected), ("nonaffected", SadakaneKoizumi1995.Reading.nonaffected)]

def SadakaneKoizumi1995.focusLabels : List (String × PhraseStructure.Cat)

The examples of (10) name the category of the copula's complement.

Equations

• SadakaneKoizumi1995.focusLabels = [("NP", PhraseStructure.Cat.N), ("AP", PhraseStructure.Cat.Adj), ("PP", PhraseStructure.Cat.P)]

def SadakaneKoizumi1995.particles (x : Datum) : List Particle

particles x lists the particles the paper reads in x, two for an ambiguous ni.

Equations

• SadakaneKoizumi1995.particles x = List.filterMap (fun (x : String) => List.lookup x SadakaneKoizumi1995.particleLabels) (x.features "particle")

def SadakaneKoizumi1995.readings (x : Datum) : List Reading

readings x lists the readings the paper gives the ni phrase of x.

Equations

• SadakaneKoizumi1995.readings x = List.filterMap (fun (x : String) => List.lookup x SadakaneKoizumi1995.readingLabels) (x.features "reading")

def SadakaneKoizumi1995.test? (x : Datum) : Option Test

test? x is the test the example x applies, if any.

Equations

• SadakaneKoizumi1995.test? x = x.parse? "test" SadakaneKoizumi1995.testLabels

theorem SadakaneKoizumi1995.judgment_eq_acceptable_iff (x : Datum) : x ∈ Examples.all → ∀ (t : Test), test? x = some t → (x.judgment = Judgment.acceptable ↔ ∃ p ∈ particles x, p.Passes t)

Every test example is acceptable exactly when a particle the paper reads in it passes the test.

theorem SadakaneKoizumi1995.judgment_eq_acceptable_iff_caseAssignable (x : Datum) : x ∈ Examples.all → ∀ (c : PhraseStructure.Cat), x.parse? "focus" focusLabels = some c → (x.judgment = Judgment.acceptable ↔ CaseAssignable c)

The copula da takes an NP or a PP but not an AP ((10)).

theorem SadakaneKoizumi1995.particles_eq_map_readings (x : Datum) : x ∈ Examples.all → readings x ≠ [] → particles x = List.map Reading.particle (readings x)

Where the paper reads an example for affectedness, ni is the case marker on an affected reading and the postposition on a nonaffected one ((35)–(38)).

theorem SadakaneKoizumi1995.judgment_eq_acceptable_iff_affected {x : Datum} (hx : x ∈ Examples.all) (ht : test? x = some Test.quantifierFloat) (hr : readings x ≠ []) : x.judgment = Judgment.acceptable ↔ Reading.affected ∈ readings x

A ni phrase hosts a floating quantifier exactly when its referent may be affected ((24b), (38b)).

theorem SadakaneKoizumi1995.caseMarker_form (x : Datum) : x ∈ Examples.all → ∀ (s : String), x.feature? "form" = some s → Particle.caseMarker ∈ particles x → ∃ (c : Japanese.Case), s ∈ List.map (fun (x : Morphology.Morph) => x.form) c.exponents

The case markers of the examples have the forms of the fragment's case particles.

theorem SadakaneKoizumi1995.postposition_form (x : Datum) : x ∈ Examples.all → ∀ (s : String), x.feature? "form" = some s → Particle.postposition ∈ particles x → s ∈ List.map (fun (x : Morphology.Morph) => x.form) Japanese.Case.dat.exponents ∨ ∃ p ∈ Japanese.Adpositions.inventory, List.map (fun (x : Morphology.Morph) => x.form) p.morphs = [s]

The postpositions of the examples have the forms of the fragment's postpositions or the form of the dative ni, of which the paper's postposition ni is a homophone.