inductive Phenomena.Politeness.Honorifics.AMType : Type

Morphosyntactic type of allocutive marker (§2).

• agreeMorpheme : AMType
• particle : AMType
• cliticPronoun : AMType

def Phenomena.Politeness.Honorifics.instReprAMType.repr : AMType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instReprAMType : Repr AMType

Equations

• Phenomena.Politeness.Honorifics.instReprAMType = { reprPrec := Phenomena.Politeness.Honorifics.instReprAMType.repr }

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instDecidableEqAMType : DecidableEq AMType

Equations

• Phenomena.Politeness.Honorifics.instDecidableEqAMType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Politeness.Honorifics.Embeddability : Type

Distribution across clause types (§3.1).

• rootOnly : Embeddability
• limitedEmbed : Embeddability
• freelyEmbed : Embeddability

def Phenomena.Politeness.Honorifics.instReprEmbeddability.repr : Embeddability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instReprEmbeddability : Repr Embeddability

Equations

• Phenomena.Politeness.Honorifics.instReprEmbeddability = { reprPrec := Phenomena.Politeness.Honorifics.instReprEmbeddability.repr }

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instDecidableEqEmbeddability : DecidableEq Embeddability

Equations

• Phenomena.Politeness.Honorifics.instDecidableEqEmbeddability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Politeness.Honorifics.HonDomain : Type

Where honorification surfaces.

• verbal : HonDomain
• nominal : HonDomain
• both : HonDomain

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instReprHonDomain : Repr HonDomain

Equations

• Phenomena.Politeness.Honorifics.instReprHonDomain = { reprPrec := Phenomena.Politeness.Honorifics.instReprHonDomain.repr }

def Phenomena.Politeness.Honorifics.instReprHonDomain.repr : HonDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instDecidableEqHonDomain : DecidableEq HonDomain

Equations

• Phenomena.Politeness.Honorifics.instDecidableEqHonDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Politeness.Honorifics.AllocDatum : Type

A single allocutive datum: one language's profile.

• language : String
• amType : AMType
• embeddability : Embeddability
• hasTV : Bool

  Whether the language has a T/V pronoun distinction

• has3PHon : Bool

  Whether 3rd person honorifics exist

• domain : HonDomain

  Where honorification is realized

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instReprAllocDatum : Repr AllocDatum

Equations

• Phenomena.Politeness.Honorifics.instReprAllocDatum = { reprPrec := Phenomena.Politeness.Honorifics.instReprAllocDatum.repr }

def Phenomena.Politeness.Honorifics.instReprAllocDatum.repr : AllocDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Politeness.Honorifics.instDecidableEqAllocDatum : DecidableEq AllocDatum

Equations

• Phenomena.Politeness.Honorifics.instDecidableEqAllocDatum = Phenomena.Politeness.Honorifics.instDecidableEqAllocDatum.decEq

def Phenomena.Politeness.Honorifics.instDecidableEqAllocDatum.decEq (x✝ x✝¹ : AllocDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Politeness.Honorifics.basque : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.magahi : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.korean : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.japanese : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.tamil : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.galician : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.hindi : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.maithili : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.punjabi : AllocDatum

Equations

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

def Phenomena.Politeness.Honorifics.allAllocData : List AllocDatum

Equations

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

theorem Phenomena.Politeness.Honorifics.rootOnly_languages_exist : ∃ d ∈ allAllocData, d.embeddability = Embeddability.rootOnly

At least one language restricts allocutive marking to root clauses.

theorem Phenomena.Politeness.Honorifics.freelyEmbed_languages_exist : ∃ d ∈ allAllocData, d.embeddability = Embeddability.freelyEmbed

At least one language freely embeds allocutive marking.

theorem Phenomena.Politeness.Honorifics.all_have_verbal : (allAllocData.all fun (d : AllocDatum) => d.domain == HonDomain.verbal || d.domain == HonDomain.both) = true

All allocutive languages in the survey mark the verbal domain (verbal or both).

theorem Phenomena.Politeness.Honorifics.all_have_tv : (allAllocData.all fun (d : AllocDatum) => d.hasTV) = true

All surveyed allocutive languages have a T/V pronoun distinction.