Typology.Alignment

@cite{comrie-1978} @cite{comrie-2013} @cite{dixon-1994} @cite{dixon-1972} @cite{dryer-haspelmath-2013} @cite{haspelmath-2005} @cite{haspelmath-2021} @cite{wals-2013}

Per-language typological substrate for morphosyntactic alignment, covering how languages mark the core grammatical relations S (sole argument of intransitive), A (agent of transitive), and P (patient of transitive). Three WALS chapters by @cite{comrie-2013}:

• Ch 98: alignment of case marking of full noun phrases.
• Ch 99: alignment of case marking of pronouns.
• Ch 100: alignment of verbal person marking.

Plus ditransitive alignment from @cite{haspelmath-2005}.

Mirrors the Linglib/Typology/{Possession,Negation,Comparison,Coordination, Modality,Gender} substrate-extension pattern. Fragment-importable.

What lives here

• AlignmentType (5-way: neutral / accusative / ergative / tripartite / active) + projection helpers.
• AlignmentProfile per-language struct + cross-domain helpers.
• DitransitiveAlignment (4-way: neutral / indirective / secundative / tripartite) + projection helpers.
• DitransitiveProfile per-language struct.
• WALS converters: fromWALS98A, fromWALS99A, fromWALS100A.
• WALS aggregate sample-size + corpus-only generalisations from Ch 98/99/100.

Theory-laden caveats

• AlignmentType collapses some WALS distinctions. WALS Ch 98 distinguishes "marked nominative" from canonical accusative; we merge both into .accusative. WALS Ch 100 has .hierarchical and .split values that don't map cleanly to our 5-way enum (fromWALS100A returns Option AlignmentType for these).
• active vs split-S. What we call .active covers both semantically-conditioned split-S (Georgian, Guarani) and aspect-conditioned split (Yukatek). The split mechanism differs, but WALS lumps them.

Out of scope

The 22-language sample, cross-linguistic generalisations (Dixon, Silverstein), ditransitive sample, and Fragment-bridge theorems live in Phenomena/Alignment/Studies/Dixon1994.lean. @cite{comrie-1989}'s typology generalisations are in Phenomena/Case/Studies/Comrie1989.lean.

inductive Typology.Alignment.AlignmentType : Type

Morphosyntactic alignment type for case marking or verbal person marking. Five categories classifying how a language groups the three core grammatical relations S, A, P.

• neutral : AlignmentType

  S = A = P: no morphological distinction (e.g. Mandarin, Thai).

• accusative : AlignmentType

  S = A ≠ P: subject + agent grouped, patient distinct (most common).

• ergative : AlignmentType

  S = P ≠ A: absolutive grouping, agent distinct (e.g. Basque).

• tripartite : AlignmentType

  S ≠ A ≠ P: all three distinctly marked (rare; Nez Perce).

• active : AlignmentType

  Active / split-S: S splits into agent-like and patient-like (e.g. Georgian, Guarani).

@[implicit_reducible]

instance Typology.Alignment.instDecidableEqAlignmentType : DecidableEq AlignmentType

Equations

• Typology.Alignment.instDecidableEqAlignmentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Alignment.instBEqAlignmentType.beq : AlignmentType → AlignmentType → Bool

Equations

• Typology.Alignment.instBEqAlignmentType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Alignment.instBEqAlignmentType : BEq AlignmentType

Equations

• Typology.Alignment.instBEqAlignmentType = { beq := Typology.Alignment.instBEqAlignmentType.beq }

@[implicit_reducible]

instance Typology.Alignment.instReprAlignmentType : Repr AlignmentType

Equations

• Typology.Alignment.instReprAlignmentType = { reprPrec := Typology.Alignment.instReprAlignmentType.repr }

def Typology.Alignment.instReprAlignmentType.repr : AlignmentType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Alignment.instInhabitedAlignmentType : Inhabited AlignmentType

Equations

• Typology.Alignment.instInhabitedAlignmentType = { default := Typology.Alignment.AlignmentType.neutral }

def Typology.Alignment.AlignmentType.marksAgent : AlignmentType → Bool

Whether this alignment marks the agent (A) distinctly from S.

Equations

• Typology.Alignment.AlignmentType.ergative.marksAgent = true
• Typology.Alignment.AlignmentType.tripartite.marksAgent = true
• x✝.marksAgent = false

def Typology.Alignment.AlignmentType.marksPatient : AlignmentType → Bool

Whether this alignment marks the patient (P) distinctly from S.

Equations

• Typology.Alignment.AlignmentType.accusative.marksPatient = true
• Typology.Alignment.AlignmentType.tripartite.marksPatient = true
• x✝.marksPatient = false

def Typology.Alignment.AlignmentType.IsNomAcc (a : AlignmentType) : Prop

Whether this alignment groups S with A (nominative-accusative pattern).

Equations

• a.IsNomAcc = (a = Typology.Alignment.AlignmentType.accusative)

@[implicit_reducible]

instance Typology.Alignment.instDecidablePredAlignmentTypeIsNomAcc : DecidablePred AlignmentType.IsNomAcc

Equations

• Typology.Alignment.instDecidablePredAlignmentTypeIsNomAcc x✝ = Typology.Alignment.instDecidablePredAlignmentTypeIsNomAcc._aux_1 x✝

def Typology.Alignment.AlignmentType.IsAbsErg (a : AlignmentType) : Prop

Whether this alignment groups S with P (absolutive-ergative pattern).

Equations

• a.IsAbsErg = (a = Typology.Alignment.AlignmentType.ergative)

@[implicit_reducible]

instance Typology.Alignment.instDecidablePredAlignmentTypeIsAbsErg : DecidablePred AlignmentType.IsAbsErg

Equations

• Typology.Alignment.instDecidablePredAlignmentTypeIsAbsErg x✝ = Typology.Alignment.instDecidablePredAlignmentTypeIsAbsErg._aux_1 x✝

structure Typology.Alignment.AlignmentProfile : Type

A language's alignment profile across WALS Chs 98/99/100.

• name : String

  Language name.

• iso639 : String

  ISO 639-3 code.

• npAlignment : AlignmentType

  Ch 98: alignment of case marking of full NPs.

• pronAlignment : AlignmentType

  Ch 99: alignment of case marking of pronouns.

• verbAlignment : AlignmentType

  Ch 100: alignment of verbal person marking.

• notes : String

  Notes on the alignment system.

@[implicit_reducible]

instance Typology.Alignment.instReprAlignmentProfile : Repr AlignmentProfile

Equations

• Typology.Alignment.instReprAlignmentProfile = { reprPrec := Typology.Alignment.instReprAlignmentProfile.repr }

def Typology.Alignment.instReprAlignmentProfile.repr : AlignmentProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Alignment.instDecidableEqAlignmentProfile : DecidableEq AlignmentProfile

Equations

• Typology.Alignment.instDecidableEqAlignmentProfile = Typology.Alignment.instDecidableEqAlignmentProfile.decEq

def Typology.Alignment.instDecidableEqAlignmentProfile.decEq (x✝ x✝¹ : AlignmentProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Typology.Alignment.AlignmentProfile.caseUniform (p : AlignmentProfile) : Bool

Whether NP and pronoun alignment match (no split ergativity in case).

Equations

• p.caseUniform = (p.npAlignment == p.pronAlignment)

def Typology.Alignment.AlignmentProfile.dixonSplit (p : AlignmentProfile) : Bool

Whether the language shows the classic NP-ergative / pronoun-accusative split (@cite{dixon-1994}'s generalization).

Equations

• p.dixonSplit = (p.npAlignment == Typology.Alignment.AlignmentType.ergative && p.pronAlignment == Typology.Alignment.AlignmentType.accusative)

def Typology.Alignment.AlignmentProfile.fullyUniform (p : AlignmentProfile) : Bool

Whether all three domains have the same alignment.

Equations

• p.fullyUniform = (p.npAlignment == p.pronAlignment && p.pronAlignment == p.verbAlignment)

def Typology.Alignment.AlignmentProfile.hasAnyErgative (p : AlignmentProfile) : Bool

Whether the language has any ergative alignment in any domain.

Equations

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

def Typology.Alignment.AlignmentProfile.accusativeCase (p : AlignmentProfile) : Bool

Whether the language has accusative alignment in both NP and pronoun case-marking domains.

Equations

• p.accusativeCase = (p.npAlignment == Typology.Alignment.AlignmentType.accusative && p.pronAlignment == Typology.Alignment.AlignmentType.accusative)

inductive Typology.Alignment.DitransitiveAlignment : Type

Ditransitive alignment classifies how R (recipient) and T (theme) are coded relative to monotransitive P (@cite{haspelmath-2005}).

• neutral : DitransitiveAlignment

  R = T = P: no distinction among non-agent arguments.

• indirective : DitransitiveAlignment

  T = P ≠ R: R distinctly marked, T patterns with P. Indirective — analogous to accusative for monotransitives. E.g. English "give the book TO Mary".

• secundative : DitransitiveAlignment

  R = P ≠ T: T distinctly marked, R patterns with P. Secundative — analogous to ergative. E.g. many Bantu applicatives.

• tripartite : DitransitiveAlignment

  R ≠ T ≠ P: all three roles distinctly marked.

@[implicit_reducible]

instance Typology.Alignment.instDecidableEqDitransitiveAlignment : DecidableEq DitransitiveAlignment

Equations

• Typology.Alignment.instDecidableEqDitransitiveAlignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Alignment.instBEqDitransitiveAlignment : BEq DitransitiveAlignment

Equations

• Typology.Alignment.instBEqDitransitiveAlignment = { beq := Typology.Alignment.instBEqDitransitiveAlignment.beq }

def Typology.Alignment.instBEqDitransitiveAlignment.beq : DitransitiveAlignment → DitransitiveAlignment → Bool

Equations

• Typology.Alignment.instBEqDitransitiveAlignment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Alignment.instReprDitransitiveAlignment : Repr DitransitiveAlignment

Equations

• Typology.Alignment.instReprDitransitiveAlignment = { reprPrec := Typology.Alignment.instReprDitransitiveAlignment.repr }

def Typology.Alignment.instReprDitransitiveAlignment.repr : DitransitiveAlignment → Nat → Std.Format

Equations

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

def Typology.Alignment.DitransitiveAlignment.marksR : DitransitiveAlignment → Bool

Whether this ditransitive alignment marks R distinctly from P.

Equations

• Typology.Alignment.DitransitiveAlignment.indirective.marksR = true
• Typology.Alignment.DitransitiveAlignment.tripartite.marksR = true
• x✝.marksR = false

def Typology.Alignment.DitransitiveAlignment.marksT : DitransitiveAlignment → Bool

Whether this ditransitive alignment marks T distinctly from P.

Equations

• Typology.Alignment.DitransitiveAlignment.secundative.marksT = true
• Typology.Alignment.DitransitiveAlignment.tripartite.marksT = true
• x✝.marksT = false

structure Typology.Alignment.DitransitiveProfile : Type

A language's ditransitive alignment profile.

• name : String
• iso639 : String
• alignment : DitransitiveAlignment
• notes : String

@[implicit_reducible]

instance Typology.Alignment.instReprDitransitiveProfile : Repr DitransitiveProfile

Equations

• Typology.Alignment.instReprDitransitiveProfile = { reprPrec := Typology.Alignment.instReprDitransitiveProfile.repr }

def Typology.Alignment.instReprDitransitiveProfile.repr : DitransitiveProfile → Nat → Std.Format

Equations

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

def Typology.Alignment.instDecidableEqDitransitiveProfile.decEq (x✝ x✝¹ : DitransitiveProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Typology.Alignment.instDecidableEqDitransitiveProfile : DecidableEq DitransitiveProfile

Equations

• Typology.Alignment.instDecidableEqDitransitiveProfile = Typology.Alignment.instDecidableEqDitransitiveProfile.decEq

def Typology.Alignment.fromWALS98A : Data.WALS.F98A.NPCaseAlignment → AlignmentType

WALS Ch 98A → AlignmentType. WALS distinguishes standard and marked- nominative accusative; we merge both.

Equations

• Typology.Alignment.fromWALS98A Data.WALS.F98A.NPCaseAlignment.neutral = Typology.Alignment.AlignmentType.neutral
• Typology.Alignment.fromWALS98A Data.WALS.F98A.NPCaseAlignment.nominativeAccusative = Typology.Alignment.AlignmentType.accusative
• Typology.Alignment.fromWALS98A Data.WALS.F98A.NPCaseAlignment.nominativeAccusative_3 = Typology.Alignment.AlignmentType.accusative
• Typology.Alignment.fromWALS98A Data.WALS.F98A.NPCaseAlignment.ergativeAbsolutive = Typology.Alignment.AlignmentType.ergative
• Typology.Alignment.fromWALS98A Data.WALS.F98A.NPCaseAlignment.tripartite = Typology.Alignment.AlignmentType.tripartite
• Typology.Alignment.fromWALS98A Data.WALS.F98A.NPCaseAlignment.activeInactive = Typology.Alignment.AlignmentType.active

def Typology.Alignment.fromWALS99A : Data.WALS.F99A.PronounCaseAlignment → AlignmentType

WALS Ch 99A → AlignmentType. WALS has a .none value (no pronouns or no case on pronouns); we map it to .neutral.

Equations

• Typology.Alignment.fromWALS99A Data.WALS.F99A.PronounCaseAlignment.neutral = Typology.Alignment.AlignmentType.neutral
• Typology.Alignment.fromWALS99A Data.WALS.F99A.PronounCaseAlignment.nominativeAccusative = Typology.Alignment.AlignmentType.accusative
• Typology.Alignment.fromWALS99A Data.WALS.F99A.PronounCaseAlignment.nominativeAccusative_3 = Typology.Alignment.AlignmentType.accusative
• Typology.Alignment.fromWALS99A Data.WALS.F99A.PronounCaseAlignment.ergativeAbsolutive = Typology.Alignment.AlignmentType.ergative
• Typology.Alignment.fromWALS99A Data.WALS.F99A.PronounCaseAlignment.tripartite = Typology.Alignment.AlignmentType.tripartite
• Typology.Alignment.fromWALS99A Data.WALS.F99A.PronounCaseAlignment.activeInactive = Typology.Alignment.AlignmentType.active
• Typology.Alignment.fromWALS99A Data.WALS.F99A.PronounCaseAlignment.none = Typology.Alignment.AlignmentType.neutral

def Typology.Alignment.fromWALS100A : Data.WALS.F100A.VerbalPersonAlignment → Option AlignmentType

WALS Ch 100A → Option AlignmentType. The .hierarchical and .split values don't map cleanly to our 5-way enum and return none.

Equations

• Typology.Alignment.fromWALS100A Data.WALS.F100A.VerbalPersonAlignment.neutral = some Typology.Alignment.AlignmentType.neutral
• Typology.Alignment.fromWALS100A Data.WALS.F100A.VerbalPersonAlignment.accusative = some Typology.Alignment.AlignmentType.accusative
• Typology.Alignment.fromWALS100A Data.WALS.F100A.VerbalPersonAlignment.ergative = some Typology.Alignment.AlignmentType.ergative
• Typology.Alignment.fromWALS100A Data.WALS.F100A.VerbalPersonAlignment.active = some Typology.Alignment.AlignmentType.active
• Typology.Alignment.fromWALS100A Data.WALS.F100A.VerbalPersonAlignment.hierarchical = none
• Typology.Alignment.fromWALS100A Data.WALS.F100A.VerbalPersonAlignment.split = none

theorem Typology.Alignment.ch98_neutral_modal : have neutral := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.neutral) Typology.Alignment.ch98✝).length; neutral > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.ergativeAbsolutive) Typology.Alignment.ch98✝).length ∧ neutral > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.tripartite) Typology.Alignment.ch98✝).length ∧ neutral > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.activeInactive) Typology.Alignment.ch98✝).length

Ch 98: neutral NP alignment is the modal pattern (no case marking).

theorem Typology.Alignment.ch98_accusative_gt_ergative : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.nominativeAccusative) Typology.Alignment.ch98✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.nominativeAccusative_3) Typology.Alignment.ch98✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.ergativeAbsolutive) Typology.Alignment.ch98✝).length

Ch 98: among case-marking systems, accusative outnumbers ergative.

theorem Typology.Alignment.ch99_accusative_gt_ergative : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F99A.PronounCaseAlignment) => x.value == Data.WALS.F99A.PronounCaseAlignment.nominativeAccusative) Typology.Alignment.ch99✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F99A.PronounCaseAlignment) => x.value == Data.WALS.F99A.PronounCaseAlignment.nominativeAccusative_3) Typology.Alignment.ch99✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F99A.PronounCaseAlignment) => x.value == Data.WALS.F99A.PronounCaseAlignment.ergativeAbsolutive) Typology.Alignment.ch99✝).length

Ch 99: accusative outnumbers ergative for pronoun case marking.

theorem Typology.Alignment.ch100_accusative_dominant : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F100A.VerbalPersonAlignment) => x.value == Data.WALS.F100A.VerbalPersonAlignment.accusative) Typology.Alignment.ch100✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F100A.VerbalPersonAlignment) => x.value == Data.WALS.F100A.VerbalPersonAlignment.ergative) Typology.Alignment.ch100✝).length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F100A.VerbalPersonAlignment) => x.value == Data.WALS.F100A.VerbalPersonAlignment.accusative) Typology.Alignment.ch100✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F100A.VerbalPersonAlignment) => x.value == Data.WALS.F100A.VerbalPersonAlignment.active) Typology.Alignment.ch100✝).length

Ch 100: accusative is the dominant verbal-person-marking pattern.

theorem Typology.Alignment.ch98_tripartite_rare : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F98A.NPCaseAlignment) => x.value == Data.WALS.F98A.NPCaseAlignment.tripartite) Typology.Alignment.ch98✝).length * 30 < Typology.Alignment.ch98✝.length

Ch 98: tripartite NP alignment is extremely rare.

theorem Typology.Alignment.ch99_tripartite_rare : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F99A.PronounCaseAlignment) => x.value == Data.WALS.F99A.PronounCaseAlignment.tripartite) Typology.Alignment.ch99✝).length * 30 < Typology.Alignment.ch99✝.length

Ch 99: tripartite pronoun alignment is extremely rare.