Particle

This file defines Particle, the lexical core for uninflectable function words ([zwicky-1985-clitics]): form, position, and a recorded distribution over licensing cells — pairs of a [sadock-zwicky-1985] sentence type (interrogatives subtyped by the Semantics/Questions constructions) and a Clause.EmbeddingContext. The distribution records distributional felicity, not licensing mechanism (analytical, study-side); a none cell means the source records nothing, not exclusion. Sentence-type and embedding-context profiles are marginals of the table, derived by existential projection (LicensedIn, LicensedInEmbed), never stored separately.

Main declarations

• Particle, Particle.ClauseType, Particle.Position, ParticleStatus
• Particle.Licensed, 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).

@[instance_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✝

@[instance_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

@[instance_reducible]

instance instDecidableEqParticleStatus : DecidableEq ParticleStatus

Equations

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

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✝

@[instance_reducible]

instance instReprParticleStatus : Repr ParticleStatus

Equations

• instReprParticleStatus = { reprPrec := instReprParticleStatus.repr }

inductive Particle.ClauseType : Type

Sentence-type cells of the particle licensing space: the [sadock-zwicky-1985] types, interrogatives subtyped.

• declarative : ClauseType
• polar : ClauseType

  Polar (yes/no) interrogative.

• alternative : ClauseType

  Alternative interrogative (p or q?).

• constituent : ClauseType

  Constituent (wh) interrogative.

• imperative : ClauseType
• exclamative : ClauseType

@[instance_reducible]

instance Particle.instDecidableEqClauseType : DecidableEq ClauseType

Equations

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

def Particle.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Particle.instReprClauseType : Repr ClauseType

Equations

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

@[instance_reducible]

instance Particle.instFintypeClauseType : Fintype ClauseType

Equations

• Particle.instFintypeClauseType = { elems := { val := ↑Particle.ClauseType.enumList, nodup := Particle.ClauseType.enumList_nodup }, complete := Particle.instFintypeClauseType._proof_1 }

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 : Option Position

  Host/position class; none when the source records no placement.

• distribution : ClauseType → Clause.EmbeddingContext → Option ParticleStatus

  Recorded status per licensing cell (sentence type × embedding context); none when the source records nothing for that cell.

@[instance_reducible]

instance instDecidableEqParticle : DecidableEq Particle

Equations

• instDecidableEqParticle = instDecidableEqParticle.decEq

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

Equations

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

def Particle.Licensed (p : Particle) (c : ClauseType) (e : Clause.EmbeddingContext) : Prop

The particle is positively recorded as available (obligatorily or optionally) in the sentence-type × embedding cell (c, e).

Equations

• p.Licensed c e = match p.distribution c e with | some ParticleStatus.obligatory => True | some ParticleStatus.optional => True | x => False

@[instance_reducible]

instance Particle.instDecidableLicensed (p : Particle) (c : ClauseType) (e : Clause.EmbeddingContext) : Decidable (p.Licensed c e)

Equations

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

def Particle.LicensedIn (p : Particle) (c : ClauseType) : Prop

Positively recorded in sentence type c, in some embedding context.

Equations

• p.LicensedIn c = ∃ (e : Clause.EmbeddingContext), p.Licensed c e

@[instance_reducible]

instance Particle.instDecidableLicensedIn (p : Particle) (c : ClauseType) : Decidable (p.LicensedIn c)

Equations

• p.instDecidableLicensedIn c = Particle.instDecidableLicensedIn._aux_1 p c

def Particle.LicensedInEmbed (p : Particle) (e : Clause.EmbeddingContext) : Prop

Positively recorded in embedding context e, for some sentence type.

Equations

• p.LicensedInEmbed e = ∃ (c : Particle.ClauseType), p.Licensed c e

@[instance_reducible]

instance Particle.instDecidableLicensedInEmbed (p : Particle) (e : Clause.EmbeddingContext) : Decidable (p.LicensedInEmbed e)

Equations

• p.instDecidableLicensedInEmbed e = Particle.instDecidableLicensedInEmbed._aux_1 p e

def Particle.IsSentential (p : Particle) : Prop

Some cell is recorded (the sentential/illocutionary particle family: question, modal, sentence-final particles).

Equations

• p.IsSentential = ∃ (c : Particle.ClauseType) (e : Clause.EmbeddingContext), (p.distribution c e).isSome = true

@[instance_reducible]

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

Equations

• p.instDecidableIsSentential = Particle.instDecidableIsSentential._aux_1 p

def Particle.toWord (p : Particle) : Morphology.Word

Projection to Word (UD PART).

Equations

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