Documentation

Linglib.Syntax.Case.Alignment

Alignment Case-Assignment Functions #

[Dix94] [Com89] [Mar91]

The SAP-indexed counterpart to Syntax/Case/Dependent.lean's configural algorithm. Each Alignment.X.assignCase is a function from Features.Prominence.ArgumentRole to Case capturing the canonical case pattern of alignment type X. The configural derivations in Dependent.lean (Marantz/Baker) and the observational AlignmentType enum (WALS-style classification, below) are checked against the case-assignment functions here as ground truth.

Coverage #

Alignment.nominativeAccusative.assignCase — accusative alignment (S = A, P distinct). The default for Indo-European, Niger-Congo, much of Eurasia.
Alignment.ergative.assignCase — canonical ergative-absolutive (S = P, A distinct). Found in Mayan perfective, Basque, Inuit, Australian languages.
Alignment.extendedErgative.assignCase — Mayan non-perfective pattern: S/A both bear genitive (Set A), P bears absolutive. Per [Coo13]
- [Ima20], this arises when a nominalized clause embeds the external argument so the subject receives genitive from D rather than ergative from v. The "extended ergative" label is from [Dix94].

Ditransitive defaults (R, T) #

ArgumentRole has 5 constructors covering ditransitives. Ditransitive case alignment (indirective vs secundative vs neutral, per [Has05]'s typology) is its own dimension orthogonal to monotransitive alignment. The R/T cases below pick conservative defaults intended to support monotransitive reasoning at zero cost; they have no published audit trail and no current consumers in linglib (no call site applies .assignCase .R or .T). Treat them as scaffolding subject to revision when ditransitive consumers arrive:

ergative.{R, T} → ABS: most ergative languages neutralize ditransitive R/T with monotransitive P, but secundative languages (some Bantu) override.
nominativeAccusative.R → DAT: typical for Indo-European and Uralic ditransitive paradigms; English/many Bantu/Tagalog have R → ACC instead ("double-object" / secundative). The DAT default is IE-biased.
nominativeAccusative.T → ACC: standard.
extendedErgative.{R, T} → ABS: UNVERIFIED — Cholan ditransitives in non-perfective aspect aren't well-documented in the published literature; this default may not survive empirical validation. Flagged for future audit when Mateo-Toledo 2008 / Pascual 2007 (Q'anjob'al) or detailed Cholan ditransitive data become available.

def Alignment.ergative.assignCase :

Features.Prominence.ArgumentRole → Case

Ergative-absolutive case assignment. Monotransitive: A → ERG, S | P → ABS. R/T default to ABS.

Equations

Instances For

def Alignment.nominativeAccusative.assignCase :

Features.Prominence.ArgumentRole → Case

Nominative-accusative case assignment. Monotransitive: S | A → NOM, P → ACC. R defaults to DAT (the recipient case found in Indo-European and Uralic ditransitive paradigms); T to ACC. R → DAT is IE-biased — secundative and double-accusative languages (English, many Bantu, Tagalog) assign R → ACC instead and would override this default.

Equations

Instances For

def Alignment.extendedErgative.assignCase :

Features.Prominence.ArgumentRole → Case

Cholan/Q'anjob'alan non-perfective: S | A → GEN (from D under nominalization), P → ABS (from Voice). Per [Coo13]; [Ima20] parameterizes the same surface pattern via inherent vs structural Case. R/T default to ABS.

Equations

Instances For

def Alignment.tripartite.assignCase :

Features.Prominence.ArgumentRole → Case

Tripartite case assignment: A → ERG, P → ACC, S → ABS — three distinct cases, one per argument. Found in San Juan Atitán Mam (Mayan, K'ichean-Mamean) per [Sco23] ch. 3, and (per [Dix94] §2.1.5) attested in Pitta-Pitta, Wangkumara, and several other Australian languages. Mam lacks independent DP case morphology — the tripartite analysis is recoverable only from agreement patterns (Set A on A, no agreement on P, Set B on S). R/T default to ACC (consistent with P) since Mam ditransitives aren't documented in the analyzed corpus.

Equations

Instances For

def Alignment.invertedErgative.assignCase :

Features.Prominence.ArgumentRole → Case

Kaqchikel-type non-perfective (specifically PROG sentences with the ajin matrix predicate): S | A → ABS, P → GEN. The OBJECT receives ergative/genitive case rather than the subject — opposite of the canonical extended-ergative pattern.

Per [Ima14] §3.3.1 ("Kaqchikel: ERG=OBJ", p. 122): "Kaqchikel exhibits a cross-linguistically rare alignment pattern in the nominative-accusative system found in the progressives and in the complement position of certain embedding verbs – the object of a transitive verb is aligned with an ergative or genitive agreement morpheme."

Imanishi's mechanism: the Unaccusative Requirement on Nominalization (eq. 90, p. 123) forces nominalized transitive verbs in Kaqchikel to passivize, removing the external argument. The object becomes the only Case-less DP in the nominalized clause and receives ergative Case from D as phase head ("phase head ergative Case", his central thesis). The subject is base-generated in the matrix (Spec-PredP headed by ajin) and gets absolutive from Infl.

Construction-specific: this pattern arises specifically in progressive ajin constructions and certain embedding-verb constructions (e.g., chäp 'begin' in (117), p. 137 — though that construction has a slightly different sub-pattern with all subjects getting ERG too). The chäp variant is not encoded here.

Dialectal variation (per [Ima14] fn. 26, p. 141): "My Kaqchikel consultants do not accept nominalized patterns as in (120). This is presumably because of dialectal differences." Some Kaqchikel varieties may not show the inverted pattern even in PROG sentences; [garcia-matzar-rodriguez-guajan-1997] document broader patterns that Imanishi's consultants don't accept. R/T default to ABS.

Equations

Instances For

An alignment is which of the core monotransitive roles {S, A, P} an analysis groups together — the partition of {S, A, P} that assign : ArgumentRole → Case induces (the kernel of assign, restricted to the three core roles: the full Setoid.ker over ArgumentRole would also constrain the ditransitive scaffolding roles R, T, which alignment does not). This is a point in the partition lattice of a three-element set, orthogonal to the Case labels used — nominativeAccusative, extendedErgative, and invertedErgative induce the same partition with different cases. A three-element set has exactly five partitions (Bell 3 = 5), hence five monotransitive alignments; coreSig is the decidable code for the partition.

This partition object replaces the scattered per-alignment _groups_S_with_X / _distinguishes_P theorems this file used to carry (restatements of it, now retired); only tripartite_distinguishes_all is kept, as it is re-exported by downstream consumers.

theorem Alignment.tripartite_distinguishes_all :

tripartite.assignCase Features.Prominence.ArgumentRole.A ≠ tripartite.assignCase Features.Prominence.ArgumentRole.P ∧ tripartite.assignCase Features.Prominence.ArgumentRole.A ≠ tripartite.assignCase Features.Prominence.ArgumentRole.S ∧ tripartite.assignCase Features.Prominence.ArgumentRole.P ≠ tripartite.assignCase Features.Prominence.ArgumentRole.S

Tripartite distinguishes all three SAP arguments — the defining property of tripartite alignment. Re-exported as the case-distinctness fact by Scott2023.voice_based_tripartite and Mam.Agreement.tripartite_alignment; the general partition picture is assignCase_partitions below.

def Alignment.coreSig (assign : Features.Prominence.ArgumentRole → Case) :

Bool × Bool × Bool

The core-role signature (S≈A, S≈P, A≈P) of an alignment — a faithful code for its partition of {S, A, P}: transitivity makes the three pairwise relations determine, and be determined by, the partition.

Equations

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

Instances For

def Alignment.ConsistentSig (s : Bool × Bool × Bool) :

Bool

A signature is consistent (realizable as a partition) iff, by transitivity, any two of the three role-equalities force the third — ruling out the three "exactly two true" triples.

Equations

Alignment.ConsistentSig s = ((!(s.1 && s.2.1) || s.2.2) && (!(s.1 && s.2.2) || s.2.1) && (!(s.2.1 && s.2.2) || s.1))

Instances For

theorem Alignment.coreSig_consistent (assign : Features.Prominence.ArgumentRole → Case) :

ConsistentSig (coreSig assign) = true

Every alignment's signature is consistent: it really is a partition.

theorem Alignment.consistent_sigs :

{s : Bool × Bool × Bool | ConsistentSig s = true} = {(true, true, true), (true, false, false), (false, true, false), (false, false, true), (false, false, false)}

Bell(3) = 5. Exactly five signatures are consistent — the five partitions of a three-element set: neutral (T,T,T), accusative (T,F,F), ergative (F,T,F), horizontal (F,F,T), tripartite (F,F,F). The three "exactly two equalities" triples are forbidden by transitivity.

theorem Alignment.bell_three_eq_five :

{s : Bool × Bool × Bool | ConsistentSig s = true}.card = 5

theorem Alignment.assignCase_partitions :

coreSig nominativeAccusative.assignCase = (true, false, false) ∧ coreSig extendedErgative.assignCase = (true, false, false) ∧ coreSig invertedErgative.assignCase = (true, false, false) ∧ coreSig ergative.assignCase = (false, true, false) ∧ coreSig tripartite.assignCase = (false, false, false)

The five assignCase functions realize only three of the five partitions: nominativeAccusative, extendedErgative, and invertedErgative all induce the accusative partition {S,A}|{P} — they differ only in Case labels, not alignment (the kernel generalizing the one instance noticed in Dixon1994.extendedErgative_groups_S_with_A_like_accusative).

theorem Alignment.horizontal_unrealized :

ConsistentSig (false, false, true) = true ∧ coreSig nominativeAccusative.assignCase ≠ (false, false, true) ∧ coreSig ergative.assignCase ≠ (false, false, true) ∧ coreSig tripartite.assignCase ≠ (false, false, true) ∧ coreSig extendedErgative.assignCase ≠ (false, false, true) ∧ coreSig invertedErgative.assignCase ≠ (false, false, true)

The horizontal partition {A,P}|{S} (A and P align, S apart — attested, Pamir-type) is a genuine partition of {S, A, P} realized by none of the assignCase functions here. (It is also absent from AlignmentType.)

inductive Alignment.DitransitiveAlignment :

Ditransitive alignment: how R (recipient) and T (theme) are coded relative to monotransitive P — the ditransitive analogue of the monotransitive alignment above, hence co-located with it (used by Dixon1994 and Haspelmath2021).

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 — English "give the book TO Mary").
secundative : DitransitiveAlignment
R = P ≠ T: T distinctly marked, R patterns with P (secundative; analogous to ergative — many Bantu applicatives).
tripartite : DitransitiveAlignment
R ≠ T ≠ P: all three roles distinctly marked.

Instances For

@[implicit_reducible]

instance Alignment.instDecidableEqDitransitiveAlignment :

DecidableEq DitransitiveAlignment

Equations

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

@[implicit_reducible]

instance Alignment.instBEqDitransitiveAlignment :

BEq DitransitiveAlignment

Equations

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

def Alignment.instBEqDitransitiveAlignment.beq :

DitransitiveAlignment → DitransitiveAlignment → Bool

Equations

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

Instances For

def Alignment.instReprDitransitiveAlignment.repr :

DitransitiveAlignment → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Alignment.instReprDitransitiveAlignment :

Repr DitransitiveAlignment

Equations

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

def Alignment.DitransitiveAlignment.marksR :

DitransitiveAlignment → Bool

Whether this ditransitive alignment marks R distinctly from P.

Equations

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

Instances For

def Alignment.DitransitiveAlignment.marksT :

DitransitiveAlignment → Bool

Whether this ditransitive alignment marks T distinctly from P.

Equations

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

Instances For

structure Alignment.DitransitiveProfile :

A language's ditransitive alignment profile.

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

Instances For

@[implicit_reducible]

instance Alignment.instReprDitransitiveProfile :

Repr DitransitiveProfile

Equations

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

def Alignment.instReprDitransitiveProfile.repr :

DitransitiveProfile → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Alignment.instDecidableEqDitransitiveProfile :

DecidableEq DitransitiveProfile

Equations

Alignment.instDecidableEqDitransitiveProfile = Alignment.instDecidableEqDitransitiveProfile.decEq

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

Observational alignment type (WALS Chs 98/99/100) #

The 5-way WALS classification ([Com13a]) of how a language groups S/A/P. The case-assignment functions above are the kernel; this enum is the observational label, grounded in the partition coreSig induces by partitionSig_grounded.

inductive Alignment.AlignmentType :

Morphosyntactic alignment type: 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.

Instances For

@[implicit_reducible]

instance Alignment.instDecidableEqAlignmentType :

DecidableEq AlignmentType

Equations

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

def Alignment.instBEqAlignmentType.beq :

AlignmentType → AlignmentType → Bool

Equations

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

Instances For

@[implicit_reducible]

instance Alignment.instBEqAlignmentType :

BEq AlignmentType

Equations

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

def Alignment.instReprAlignmentType.repr :

AlignmentType → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Alignment.instReprAlignmentType :

Repr AlignmentType

Equations

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

@[implicit_reducible]

instance Alignment.instInhabitedAlignmentType :

Inhabited AlignmentType

Equations

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

def Alignment.AlignmentType.marksAgent (a : AlignmentType) :

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

Equations

a.marksAgent = (a = Alignment.AlignmentType.ergative ∨ a = Alignment.AlignmentType.tripartite)

Instances For

@[implicit_reducible]

instance Alignment.instDecidableMarksAgent (a : AlignmentType) :

Decidable a.marksAgent

Equations

Alignment.instDecidableMarksAgent a = id inferInstance

def Alignment.AlignmentType.marksPatient (a : AlignmentType) :

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

Equations

a.marksPatient = (a = Alignment.AlignmentType.accusative ∨ a = Alignment.AlignmentType.tripartite)

Instances For

@[implicit_reducible]

instance Alignment.instDecidableMarksPatient (a : AlignmentType) :

Decidable a.marksPatient

Equations

Alignment.instDecidableMarksPatient a = id inferInstance

Split ergativity [Bla94b] [Dix94] #

A SplitErgativity Factor is parameterised by the conditioning factor (aspect, person, animacy, …); alignment projects to the ergative or accusative family. The Hindi aspect-conditioned split (hindiSplit) is the canonical worked example, used as the cross-linguistic reference point by the Yukatek/Hindi fragments and the Mayan/Silverstein studies.

structure Alignment.SplitErgativity (Factor : Type) :

A split-ergative system ([Bla94b], [Dix94]): alignment varies by some conditioning factor.

ergCondition : Factor → Bool

Instances For

def Alignment.SplitErgativity.alignment {Factor : Type} (split : SplitErgativity Factor) (f : Factor) :

Features.AlignmentFamily

Equations

split.alignment f = if split.ergCondition f = true then Features.AlignmentFamily.ergative else Features.AlignmentFamily.accusative

Instances For

inductive Alignment.Aspect :

perfective : Aspect
imperfective : Aspect

Instances For

@[implicit_reducible]

instance Alignment.instDecidableEqAspect :

DecidableEq Aspect

Equations

Alignment.instDecidableEqAspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Alignment.instReprAspect.repr :

Aspect → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Alignment.instReprAspect.repr Alignment.Aspect.perfective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alignment.Aspect.perfective")).group prec✝

Instances For

@[implicit_reducible]

instance Alignment.instReprAspect :

Equations

Alignment.instReprAspect = { reprPrec := Alignment.instReprAspect.repr }

def Alignment.hindiSplit :

SplitErgativity Aspect

The canonical aspect-conditioned split: perfective ⇒ ergative, imperfective ⇒ accusative (Hindi-Urdu). The reference instance other aspect-split languages are compared against.

Equations

Alignment.hindiSplit = { ergCondition := fun (a : Alignment.Aspect) => a == Alignment.Aspect.perfective }

Instances For

theorem Alignment.hindi_perfective_erg :

hindiSplit.alignment Aspect.perfective = Features.AlignmentFamily.ergative

theorem Alignment.hindi_imperfective_acc :

hindiSplit.alignment Aspect.imperfective = Features.AlignmentFamily.accusative

Grounding the enum in the partition object #

def Alignment.AlignmentType.partitionSig :

AlignmentType → Option (Bool × Bool × Bool)

AlignmentType as the core-role signature (S≈A, S≈P, A≈P) of the partition it denotes (coreSig vocabulary). active is not a partition of {S,A,P} — it splits S — so it has no signature (none).

Equations

Alignment.AlignmentType.neutral.partitionSig = some (true, true, true)
Alignment.AlignmentType.accusative.partitionSig = some (true, false, false)
Alignment.AlignmentType.ergative.partitionSig = some (false, true, false)
Alignment.AlignmentType.tripartite.partitionSig = some (false, false, false)
Alignment.AlignmentType.active.partitionSig = none

Instances For

theorem Alignment.partitionSig_grounded :

AlignmentType.accusative.partitionSig = some (coreSig nominativeAccusative.assignCase) ∧ AlignmentType.ergative.partitionSig = some (coreSig ergative.assignCase) ∧ AlignmentType.tripartite.partitionSig = some (coreSig tripartite.assignCase)

The four partition-denoting AlignmentTypes agree with the partitions the corresponding assignCase functions induce — grounding the enum in the kernel object rather than maintaining it independently.