Register

This file defines the register of a linguistic form. A register is a way of speaking that a speech community ties to a kind of situation, and variation in register is variation within one speaker across situations rather than between speakers. The formality of the situation is the dimension recorded here: a form belongs to careful or written language, to casual speech, or to neither. English must and perhaps are formal beside have to and maybe, the German simple past is the narrative tense of writing, and Indonesian telah is the written counterpart of sudah.

Register is a property of the form and of the situation of use. The deference a form presents toward a person it refers to or addresses is a separate property, its honorific grade, a coordinate of the language's own paradigms (Syntax/Category/Pronoun/Personal.lean). The Korean speech-style particles present the same grade to the addressee and differ in the formality of the discourse.

Main definitions

• SocialMeaning.Register: the informal, neutral and formal registers, linearly ordered by formality.

References

• S. Rotter and M. Liu, A Register Approach to Modal (Non-)Concord in English: An Experimental Study of Linguistic and Social Meaning (2025)
• D. Alok and O. Bhalla, Allocutivity and the Syntax of Honorifics (2026)

inductive SocialMeaning.Register : Type

The register of a form is the formality of the situations in which speakers use it.

• informal : Register

  Colloquial, casual speech, such as have to and maybe.

• neutral : Register

  Unmarked for formality.

• formal : Register

  Written, literary or careful language, such as must, shall and perhaps.

@[instance_reducible]

instance SocialMeaning.instDecidableEqRegister : DecidableEq Register

Equations

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

@[instance_reducible]

instance SocialMeaning.instFintypeRegister : Fintype Register

Equations

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

def SocialMeaning.instReprRegister.repr : Register → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SocialMeaning.instReprRegister : Repr Register

Equations

• SocialMeaning.instReprRegister = { reprPrec := SocialMeaning.instReprRegister.repr }

@[instance_reducible]

instance SocialMeaning.Register.instLinearOrder : LinearOrder Register

Registers are ordered by formality, informal < neutral < formal.

Equations

• SocialMeaning.Register.instLinearOrder = LinearOrder.lift' SocialMeaning.Register.ctorIdx ⋯

@[instance_reducible]

instance SocialMeaning.Register.instBoundedOrder : BoundedOrder Register

Equations

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