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 → Nat → Std.Format

Equations

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

instance Phenomena.Politeness.Honorifics.instReprAMType : Repr AMType

Equations

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

instance Phenomena.Politeness.Honorifics.instDecidableEqAMType : DecidableEq AMType

Equations

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

instance Phenomena.Politeness.Honorifics.instBEqAMType : BEq AMType

Equations

• Phenomena.Politeness.Honorifics.instBEqAMType = { beq := Phenomena.Politeness.Honorifics.instBEqAMType.beq }

def Phenomena.Politeness.Honorifics.instBEqAMType.beq : AMType → AMType → Bool

Equations

• Phenomena.Politeness.Honorifics.instBEqAMType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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 → Nat → Std.Format

Equations

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

instance Phenomena.Politeness.Honorifics.instReprEmbeddability : Repr Embeddability

Equations

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

instance Phenomena.Politeness.Honorifics.instDecidableEqEmbeddability : DecidableEq Embeddability

Equations

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

def Phenomena.Politeness.Honorifics.instBEqEmbeddability.beq : Embeddability → Embeddability → Bool

Equations

• Phenomena.Politeness.Honorifics.instBEqEmbeddability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Politeness.Honorifics.instBEqEmbeddability : BEq Embeddability

Equations

• Phenomena.Politeness.Honorifics.instBEqEmbeddability = { beq := Phenomena.Politeness.Honorifics.instBEqEmbeddability.beq }

inductive Phenomena.Politeness.Honorifics.HonDomain : Type

Where honorification surfaces.

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

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 → Nat → Std.Format

Equations

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

instance Phenomena.Politeness.Honorifics.instDecidableEqHonDomain : DecidableEq HonDomain

Equations

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

def Phenomena.Politeness.Honorifics.instBEqHonDomain.beq : HonDomain → HonDomain → Bool

Equations

• Phenomena.Politeness.Honorifics.instBEqHonDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Politeness.Honorifics.instBEqHonDomain : BEq HonDomain

Equations

• Phenomena.Politeness.Honorifics.instBEqHonDomain = { beq := Phenomena.Politeness.Honorifics.instBEqHonDomain.beq }

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

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

Equations

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

instance Phenomena.Politeness.Honorifics.instReprAllocDatum : Repr AllocDatum

Equations

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

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.

instance Phenomena.Politeness.Honorifics.instDecidableEqAllocDatum : DecidableEq AllocDatum

Equations

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

instance Phenomena.Politeness.Honorifics.instBEqAllocDatum : BEq AllocDatum

Equations

• Phenomena.Politeness.Honorifics.instBEqAllocDatum = { beq := Phenomena.Politeness.Honorifics.instBEqAllocDatum.beq }

def Phenomena.Politeness.Honorifics.instBEqAllocDatum.beq : AllocDatum → AllocDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Politeness.Honorifics.instBEqAllocDatum.beq x✝¹ x✝ = false

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 : AllocDatum), d ∈ allAllocData ∧ d.embeddability = Embeddability.rootOnly

At least one language restricts allocutive marking to root clauses.

theorem Phenomena.Politeness.Honorifics.freelyEmbed_languages_exist : ∃ (d : AllocDatum), 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.