Register

@cite{fiske-cuddy-glick-xu-2002}

Sociolinguistic register as a lexical feature. Register encodes the formality level of a linguistic form — whether it belongs to formal (literary, careful) speech, neutral (unmarked) speech, or informal (colloquial, casual) speech.

Register is currently stipulated as a lexical property of individual forms. A future direction is to derive register effects from pragmatic factors (e.g., RSA models where formality emerges from competing social goals, as in @cite{yoon-etal-2020} for politeness).

Connections

• Core.Pronouns.PronounEntry.register: pronoun register (T/V/honorific)
• Core.Pronouns.AllocutiveEntry.register: allocutive marker register
• Fragments.English.FunctionWords.AuxEntry.register: modal register
• Semantics.Lexical.Expressives.CIContext.formality: context formality (ℚ)

Binary T/V systems (Basque, Tamil, Galician, Punjabi) use .informal/.formal. Ternary honorific systems (Hindi, Magahi, Maithili, Korean) use all three levels.

inductive Core.Register.Level : Type

Register level: the formality of a linguistic form.

Three levels suffice for the phenomena currently formalized (modal concord, T/V pronouns, honorific systems). Finer-grained scales are possible (Biber's multi-dimensional analysis uses continuous features) but not yet needed.

• formal : Level
• neutral : Level
• informal : Level

instance Core.Register.instDecidableEqLevel : DecidableEq Level

Equations

• Core.Register.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Register.instBEqLevel.beq : Level → Level → Bool

Equations

• Core.Register.instBEqLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Register.instBEqLevel : BEq Level

Equations

• Core.Register.instBEqLevel = { beq := Core.Register.instBEqLevel.beq }

instance Core.Register.instReprLevel : Repr Level

Equations

• Core.Register.instReprLevel = { reprPrec := Core.Register.instReprLevel.repr }

def Core.Register.instReprLevel.repr : Level → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Register.instReprLevel.repr Core.Register.Level.formal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Register.Level.formal")).group prec✝

def Core.Register.instInhabitedLevel.default : Level

Equations

• Core.Register.instInhabitedLevel.default = Core.Register.Level.formal

instance Core.Register.instInhabitedLevel : Inhabited Level

Equations

• Core.Register.instInhabitedLevel = { default := Core.Register.instInhabitedLevel.default }

instance Core.Register.instToStringLevel : ToString Level

Equations

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

def Core.Register.Level.all : List Level

All register levels, ordered from informal to formal.

Equations

• Core.Register.Level.all = [Core.Register.Level.informal, Core.Register.Level.neutral, Core.Register.Level.formal]

def Core.Register.Level.toNat : Level → ℕ

Numeric encoding: informal=0 < neutral=1 < formal=2.

Equations

• Core.Register.Level.informal.toNat = 0
• Core.Register.Level.neutral.toNat = 1
• Core.Register.Level.formal.toNat = 2

def Core.Register.Level.fromNat : ℕ → Level

Inverse of toNat: 0 → informal, 1 → neutral, 2+ → formal.

Equations

• Core.Register.Level.fromNat 0 = Core.Register.Level.informal
• Core.Register.Level.fromNat 1 = Core.Register.Level.neutral
• Core.Register.Level.fromNat x✝ = Core.Register.Level.formal

instance Core.Register.instOrdLevel : Ord Level

Ordering: informal < neutral < formal.

Equations

• Core.Register.instOrdLevel = { compare := fun (a b : Core.Register.Level) => compare a.toNat b.toNat }

instance Core.Register.instLTLevel : LT Level

Equations

• Core.Register.instLTLevel = { lt := fun (a b : Core.Register.Level) => a.toNat < b.toNat }

instance Core.Register.instLELevel : LE Level

Equations

• Core.Register.instLELevel = { le := fun (a b : Core.Register.Level) => a.toNat ≤ b.toNat }

instance Core.Register.instDecidableLtLevel (a b : Level) : Decidable (a < b)

Equations

• Core.Register.instDecidableLtLevel a b = a.toNat.decLt b.toNat

instance Core.Register.instDecidableLeLevel (a b : Level) : Decidable (a ≤ b)

Equations

• Core.Register.instDecidableLeLevel a b = a.toNat.decLe b.toNat

theorem Core.Register.informal_lt_neutral : Level.informal < Level.neutral

theorem Core.Register.neutral_lt_formal : Level.neutral < Level.formal

theorem Core.Register.informal_lt_formal : Level.informal < Level.formal

theorem Core.Register.ofNat_toNat (l : Level) : Level.fromNat l.toNat = l

Round-trip: ofNat inverts toNat.

def Core.Register.Level.toRat : Level → ℚ

Rational-valued encoding: informal=0, neutral=1/2, formal=1. Bridges to CIContext.formality : ℚ (0=casual, 1=formal).

Equations

• Core.Register.Level.informal.toRat = 0
• Core.Register.Level.neutral.toRat = 1 / 2
• Core.Register.Level.formal.toRat = 1

def Core.Register.areVariants (a b : Level) : Bool

Two forms are register variants if they differ in register level. This is the structural precondition for register mixing and split-register constructions.

Equations

• Core.Register.areVariants a b = (a != b)

Social indexation

inductive Core.Register.SocialIndex : Type

Social indexation of grammatical doubling.

Concord phenomena carry social meaning along a competence/solidarity axis (drawing on the competence/warmth dichotomy in social cognition; Fiske, Cuddy, @cite{fiske-cuddy-glick-xu-2002}).

• competence: standard dialect, educated, formal, high-SES, confident.
• solidarity: non-standard, friendly, warm, in-group, casual.

• competence : SocialIndex
• solidarity : SocialIndex

instance Core.Register.instDecidableEqSocialIndex : DecidableEq SocialIndex

Equations

• Core.Register.instDecidableEqSocialIndex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Register.instBEqSocialIndex : BEq SocialIndex

Equations

• Core.Register.instBEqSocialIndex = { beq := Core.Register.instBEqSocialIndex.beq }

def Core.Register.instBEqSocialIndex.beq : SocialIndex → SocialIndex → Bool

Equations

• Core.Register.instBEqSocialIndex.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Register.instReprSocialIndex : Repr SocialIndex

Equations

• Core.Register.instReprSocialIndex = { reprPrec := Core.Register.instReprSocialIndex.repr }

def Core.Register.instReprSocialIndex.repr : SocialIndex → ℕ → Std.Format

Equations

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

def Core.Register.instInhabitedSocialIndex.default : SocialIndex

Equations

• Core.Register.instInhabitedSocialIndex.default = Core.Register.SocialIndex.competence

instance Core.Register.instInhabitedSocialIndex : Inhabited SocialIndex

Equations

• Core.Register.instInhabitedSocialIndex = { default := Core.Register.instInhabitedSocialIndex.default }