Particle

This file defines Particle, the lexical core for uninflectable function words ([zwicky-1985-clitics]): form, position, and optional three-valued distribution facets over Clause.Context and Clause.Embedding. Facets record distributional felicity, not licensing mechanism (analytical, study-side); a none cell means the source records nothing, not exclusion.

Main declarations

• Particle, Particle.Position
• ParticleStatus, ClauseDistribution, EmbedDistribution
• Particle.LicensedIn, Particle.LicensedInEmbed — derived, decidable
• Particle.toWord — projection to Word (UD PART)

inductive Particle.Position : Type

Where a particle sits relative to its host domain — the [zwicky-1985-clitics] positional diagnostic.

• clauseInitial : Position
• secondPosition : Position

  Second position (Wackernagel; Slavic li).

• clauseMedial : Position

  Clause-medial / middle field (German denn, Swedish väl).

• clauseFinal : Position
• preHost : Position

  Immediately before a host constituent (adnominal focus particles).

• postHost : Position

  Immediately after a host constituent.

• free : Position

  No fixed position (Hindi-Urdu kya:, [BD20] §2).

@[implicit_reducible]

instance Particle.instDecidableEqPosition : DecidableEq Position

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Particle.instReprPosition.repr Particle.Position.preHost prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Particle.Position.preHost")).group prec✝
• Particle.instReprPosition.repr Particle.Position.postHost prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Particle.Position.postHost")).group prec✝
• Particle.instReprPosition.repr Particle.Position.free prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Particle.Position.free")).group prec✝

@[implicit_reducible]

instance Particle.instReprPosition : Repr Position

Equations

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

inductive ParticleStatus : Type

Three-valued distribution status of a particle in a licensing context (cf. WALS ch. 116).

• obligatory : ParticleStatus
• optional : ParticleStatus
• excluded : ParticleStatus

@[implicit_reducible]

instance instDecidableEqParticleStatus : DecidableEq ParticleStatus

Equations

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

@[implicit_reducible]

instance instReprParticleStatus : Repr ParticleStatus

Equations

• instReprParticleStatus = { reprPrec := instReprParticleStatus.repr }

def instReprParticleStatus.repr : ParticleStatus → ℕ → Std.Format

Equations

• instReprParticleStatus.repr ParticleStatus.obligatory prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ParticleStatus.obligatory")).group prec✝
• instReprParticleStatus.repr ParticleStatus.optional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ParticleStatus.optional")).group prec✝
• instReprParticleStatus.repr ParticleStatus.excluded prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ParticleStatus.excluded")).group prec✝

structure ClauseDistribution : Type

Per-clause-context distribution record. Each cell is Option-valued: none means the anchoring source records nothing for that context — distinct from some .excluded, which is a positive claim.

• declarative : Option ParticleStatus
• polarInterrogative : Option ParticleStatus
• alternativeInterrogative : Option ParticleStatus
• constituentInterrogative : Option ParticleStatus
• imperative : Option ParticleStatus
• exclamative : Option ParticleStatus

def instDecidableEqClauseDistribution.decEq (x✝ x✝¹ : ClauseDistribution) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqClauseDistribution : DecidableEq ClauseDistribution

Equations

• instDecidableEqClauseDistribution = instDecidableEqClauseDistribution.decEq

@[implicit_reducible]

instance instReprClauseDistribution : Repr ClauseDistribution

Equations

• instReprClauseDistribution = { reprPrec := instReprClauseDistribution.repr }

def instReprClauseDistribution.repr : ClauseDistribution → ℕ → Std.Format

Equations

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

def ClauseDistribution.status? (d : ClauseDistribution) : Clause.Context → Option ParticleStatus

Recorded status in context c, if any.

Equations

• d.status? Clause.Context.declarative = d.declarative
• d.status? Clause.Context.polarInterrogative = d.polarInterrogative
• d.status? Clause.Context.alternativeInterrogative = d.alternativeInterrogative
• d.status? Clause.Context.constituentInterrogative = d.constituentInterrogative
• d.status? Clause.Context.imperative = d.imperative
• d.status? Clause.Context.exclamative = d.exclamative

structure EmbedDistribution : Type

Per-embedding-context distribution record ([BD20] axis). Same Option-valued honesty convention as ClauseDistribution.

• matrix : Option ParticleStatus
• subordinated : Option ParticleStatus
• quasiSubordinated : Option ParticleStatus
• quotation : Option ParticleStatus

def instDecidableEqEmbedDistribution.decEq (x✝ x✝¹ : EmbedDistribution) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqEmbedDistribution : DecidableEq EmbedDistribution

Equations

• instDecidableEqEmbedDistribution = instDecidableEqEmbedDistribution.decEq

@[implicit_reducible]

instance instReprEmbedDistribution : Repr EmbedDistribution

Equations

• instReprEmbedDistribution = { reprPrec := instReprEmbedDistribution.repr }

def instReprEmbedDistribution.repr : EmbedDistribution → ℕ → Std.Format

Equations

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

def EmbedDistribution.status? (d : EmbedDistribution) : Clause.Embedding → Option ParticleStatus

Recorded status in embedding context c, if any.

Equations

• d.status? Clause.Embedding.matrix = d.matrix
• d.status? Clause.Embedding.subordinated = d.subordinated
• d.status? Clause.Embedding.quasiSubordinated = d.quasiSubordinated
• d.status? Clause.Embedding.quotation = d.quotation

structure Particle : Type

An uninflectable function word associated with a host constituent ([zwicky-1985-clitics]).

• form : String

  Surface form (romanization or orthographic).

• script : Option String

  Native-script form, when form is a romanization (Mandarin 吗).

• position : Position

  Host/position class.

• distribution : Option ClauseDistribution

  Clause-type distribution facet; none for particles with no clause-type restriction (focus particles, case particles).

• embedding : Option EmbedDistribution

  Interrogative-embedding distribution facet ([BD20] axis); none when the source records no embedding data.

def instDecidableEqParticle.decEq (x✝ x✝¹ : Particle) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqParticle : DecidableEq Particle

Equations

• instDecidableEqParticle = instDecidableEqParticle.decEq

@[implicit_reducible]

instance instReprParticle : Repr Particle

Equations

• instReprParticle = { reprPrec := instReprParticle.repr }

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

Equations

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

def Particle.status? (p : Particle) (c : Clause.Context) : Option ParticleStatus

Recorded clause-type distribution status in context c, if any.

Equations

• p.status? c = p.distribution.bind fun (x : ClauseDistribution) => x.status? c

def Particle.LicensedIn (p : Particle) (c : Clause.Context) : Prop

The particle is positively recorded as available (obligatorily or optionally) in context c.

Equations

• p.LicensedIn c = match p.status? c with | some ParticleStatus.obligatory => True | some ParticleStatus.optional => True | x => False

@[implicit_reducible]

instance Particle.instDecidableLicensedIn (p : Particle) (c : Clause.Context) : Decidable (p.LicensedIn c)

Equations

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

def Particle.embedStatus? (p : Particle) (c : Clause.Embedding) : Option ParticleStatus

Recorded embedding-distribution status in context c, if any.

Equations

• p.embedStatus? c = p.embedding.bind fun (x : EmbedDistribution) => x.status? c

def Particle.LicensedInEmbed (p : Particle) (c : Clause.Embedding) : Prop

The particle is positively recorded as available in embedding context c.

Equations

• p.LicensedInEmbed c = match p.embedStatus? c with | some ParticleStatus.obligatory => True | some ParticleStatus.optional => True | x => False

@[implicit_reducible]

instance Particle.instDecidableLicensedInEmbed (p : Particle) (c : Clause.Embedding) : Decidable (p.LicensedInEmbed c)

Equations

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

def Particle.IsSentential (p : Particle) : Prop

Carries a clause-type distribution (the sentential/illocutionary particle family: question, modal, sentence-final particles).

Equations

• p.IsSentential = (p.distribution.isSome = true)

@[implicit_reducible]

instance Particle.instDecidableIsSentential (p : Particle) : Decidable p.IsSentential

Equations

• p.instDecidableIsSentential = Particle.instDecidableIsSentential._aux_1 p

def Particle.toWord (p : Particle) : Word

Projection to Word (UD PART).

Equations

• p.toWord = { form := p.form, cat := UD.UPOS.PART }