Alignment

A marking of the argument roles, by case, agreement or constituent order, is a function out of ArgumentRole, and its alignment is which of the three core roles S, A and P it identifies, the kernel of the marking on the core roles, as Comrie and Dixon define it. A three-element set has five partitions, so a marking has one of five alignments: neutral, accusative, with S marked like A, ergative, with S marked like P, horizontal, with A marked like P, and tripartite. The case labels a marking uses are a further dimension: the Mayan non-perfective pattern with Set A on every subject and the Kaqchikel progressive with Set A on the object are accusative alignments in genitive rather than nominative clothing.

Main declarations

• Alignment.IsNeutral, Alignment.IsAccusative, Alignment.IsErgative, Alignment.IsHorizontal, Alignment.IsTripartite: the five alignments of a marking, one of which every marking has (Alignment.marking_cases).
• Alignment.accusative, Alignment.ergative, Alignment.tripartite, Alignment.extendedErgative, Alignment.invertedErgative: the canonical case markings.
• Alignment.AlignmentType: Comrie's observational classification of WALS chapters 98 to 100, with AlignmentType.MarksAgent and AlignmentType.MarksPatient.
• Alignment.AlignmentType.Classifies: the alignment a type names, as a property of a marking.
• Alignment.overt, Alignment.Fits: the conditions under which a role of a conditioned marking is overtly coded, and the fit of a conditioned marking to an order on its conditions.

Implementation notes

The alignment predicates read the three core roles only. The values a canonical marking gives the ditransitive roles R and T, a dative recipient in the accusative marking and the theme with the patient elsewhere, are placeholders with no audit trail, and no consumer reads them. AlignmentType.active, the split-S systems, identifies no fixed pair of roles and so is not the alignment of a single marking.

References

• [BWMZ15]
• [Com78]
• [Com13a]
• [Coo13]
• [Dix94]
• [Ima14]
• [Ima20]
• [Sco23]

def Alignment.IsNeutral {κ : Type u_1} (m : ArgumentRole → κ) : Prop

The marking treats S, A and P alike.

Equations

• Alignment.IsNeutral m = (m ArgumentRole.S = m ArgumentRole.A ∧ m ArgumentRole.S = m ArgumentRole.P)

def Alignment.IsAccusative {κ : Type u_1} (m : ArgumentRole → κ) : Prop

The marking treats S like A and unlike P.

Equations

• Alignment.IsAccusative m = (m ArgumentRole.S = m ArgumentRole.A ∧ m ArgumentRole.S ≠ m ArgumentRole.P)

def Alignment.IsErgative {κ : Type u_1} (m : ArgumentRole → κ) : Prop

The marking treats S like P and unlike A.

Equations

• Alignment.IsErgative m = (m ArgumentRole.S = m ArgumentRole.P ∧ m ArgumentRole.S ≠ m ArgumentRole.A)

def Alignment.IsHorizontal {κ : Type u_1} (m : ArgumentRole → κ) : Prop

The marking treats A like P and unlike S.

Equations

• Alignment.IsHorizontal m = (m ArgumentRole.A = m ArgumentRole.P ∧ m ArgumentRole.S ≠ m ArgumentRole.A)

def Alignment.IsTripartite {κ : Type u_1} (m : ArgumentRole → κ) : Prop

The marking treats S, A and P all differently.

Equations

• Alignment.IsTripartite m = (m ArgumentRole.S ≠ m ArgumentRole.A ∧ m ArgumentRole.S ≠ m ArgumentRole.P ∧ m ArgumentRole.A ≠ m ArgumentRole.P)

@[instance_reducible]

instance Alignment.instDecidableIsNeutral {κ : Type u_1} (m : ArgumentRole → κ) [DecidableEq κ] : Decidable (IsNeutral m)

Equations

• Alignment.instDecidableIsNeutral m = { decide := decide (m ArgumentRole.S = m ArgumentRole.A) && decide (m ArgumentRole.S = m ArgumentRole.P), reflects_decide := ⋯ }

@[instance_reducible]

instance Alignment.instDecidableIsAccusative {κ : Type u_1} (m : ArgumentRole → κ) [DecidableEq κ] : Decidable (IsAccusative m)

Equations

• Alignment.instDecidableIsAccusative m = { decide := decide (m ArgumentRole.S = m ArgumentRole.A) && decide (m ArgumentRole.S ≠ m ArgumentRole.P), reflects_decide := ⋯ }

@[instance_reducible]

instance Alignment.instDecidableIsErgative {κ : Type u_1} (m : ArgumentRole → κ) [DecidableEq κ] : Decidable (IsErgative m)

Equations

• Alignment.instDecidableIsErgative m = { decide := decide (m ArgumentRole.S = m ArgumentRole.P) && decide (m ArgumentRole.S ≠ m ArgumentRole.A), reflects_decide := ⋯ }

@[instance_reducible]

instance Alignment.instDecidableIsHorizontal {κ : Type u_1} (m : ArgumentRole → κ) [DecidableEq κ] : Decidable (IsHorizontal m)

Equations

• Alignment.instDecidableIsHorizontal m = { decide := decide (m ArgumentRole.A = m ArgumentRole.P) && decide (m ArgumentRole.S ≠ m ArgumentRole.A), reflects_decide := ⋯ }

@[instance_reducible]

instance Alignment.instDecidableIsTripartite {κ : Type u_1} (m : ArgumentRole → κ) [DecidableEq κ] : Decidable (IsTripartite m)

Equations

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

theorem Alignment.marking_cases {κ : Type u_1} (m : ArgumentRole → κ) : IsNeutral m ∨ IsAccusative m ∨ IsErgative m ∨ IsHorizontal m ∨ IsTripartite m

Every marking has one of the five alignments, the five partitions of a three-element set.

theorem Alignment.IsAccusative.not_isErgative {κ : Type u_1} {m : ArgumentRole → κ} (h : IsAccusative m) : ¬IsErgative m

No marking is accusative and ergative at once, since it identifies S with at most one of A and P.

theorem Alignment.IsErgative.not_isAccusative {κ : Type u_1} {m : ArgumentRole → κ} (h : IsErgative m) : ¬IsAccusative m

Canonical case markings

def Alignment.accusative : ArgumentRole → Case

The accusative marking makes S and A nominative and P accusative.

Equations

• Alignment.accusative ArgumentRole.S = Case.nom
• Alignment.accusative ArgumentRole.A = Case.nom
• Alignment.accusative ArgumentRole.P = Case.acc
• Alignment.accusative ArgumentRole.T = Case.acc
• Alignment.accusative ArgumentRole.R = Case.dat

def Alignment.ergative : ArgumentRole → Case

The ergative marking makes A ergative and S and P absolutive.

Equations

• Alignment.ergative ArgumentRole.A = Case.erg
• Alignment.ergative ArgumentRole.S = Case.abs
• Alignment.ergative ArgumentRole.P = Case.abs
• Alignment.ergative ArgumentRole.R = Case.abs
• Alignment.ergative ArgumentRole.T = Case.abs

def Alignment.tripartite : ArgumentRole → Case

The tripartite marking makes A ergative, P accusative and S absolutive, as in San Juan Atitán Mam ([Sco23]) and several Australian languages ([Dix94]).

Equations

• Alignment.tripartite ArgumentRole.A = Case.erg
• Alignment.tripartite ArgumentRole.S = Case.abs
• Alignment.tripartite ArgumentRole.P = Case.acc
• Alignment.tripartite ArgumentRole.R = Case.acc
• Alignment.tripartite ArgumentRole.T = Case.acc

def Alignment.extendedErgative : ArgumentRole → Case

The extended-ergative marking of the Mayan non-perfective and aspectless clause: genitive on S and A, from D under nominalization, absolutive on P ([Coo13], [Ima20]; the label is [Dix94]'s).

Equations

• Alignment.extendedErgative ArgumentRole.S = Case.gen
• Alignment.extendedErgative ArgumentRole.A = Case.gen
• Alignment.extendedErgative ArgumentRole.P = Case.abs
• Alignment.extendedErgative ArgumentRole.R = Case.abs
• Alignment.extendedErgative ArgumentRole.T = Case.abs

def Alignment.invertedErgative : ArgumentRole → Case

The inverted marking of the Kaqchikel progressive ([Ima14]): absolutive on S and A, genitive on P, the object being the only Case-less DP of a nominalized clause under the unaccusative requirement.

Equations

• Alignment.invertedErgative ArgumentRole.S = Case.abs
• Alignment.invertedErgative ArgumentRole.A = Case.abs
• Alignment.invertedErgative ArgumentRole.R = Case.abs
• Alignment.invertedErgative ArgumentRole.T = Case.abs
• Alignment.invertedErgative ArgumentRole.P = Case.gen

theorem Alignment.isAccusative_accusative : IsAccusative accusative

theorem Alignment.isErgative_ergative : IsErgative ergative

theorem Alignment.isTripartite_tripartite : IsTripartite tripartite

theorem Alignment.isAccusative_extendedErgative : IsAccusative extendedErgative

Extended ergativity is accusative alignment in genitive clothing.

theorem Alignment.isAccusative_invertedErgative : IsAccusative invertedErgative

The inverted marking is likewise an accusative alignment.

The observational classification

inductive Alignment.AlignmentType : Type

Morphosyntactic alignment type, the classification of WALS chapters 98 to 100 ([Com13a]): how a language groups S, A and P.

• neutral : AlignmentType

  S, A and P alike.

• accusative : AlignmentType

  S with A, P apart.

• ergative : AlignmentType

  S with P, A apart.

• tripartite : AlignmentType

  S, A and P all distinct.

• active : AlignmentType

  Split-S: S is marked like A for some predicates and like P for others.

@[instance_reducible]

instance Alignment.instDecidableEqAlignmentType : DecidableEq AlignmentType

Equations

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

@[instance_reducible]

instance Alignment.instReprAlignmentType : Repr AlignmentType

Equations

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

def Alignment.instReprAlignmentType.repr : AlignmentType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Alignment.instInhabitedAlignmentType : Inhabited AlignmentType

Equations

• Alignment.instInhabitedAlignmentType = { default := Alignment.instInhabitedAlignmentType.default }

@[instance_reducible]

instance Alignment.instFintypeAlignmentType : Fintype AlignmentType

Equations

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

def Alignment.AlignmentType.MarksAgent (a : AlignmentType) : Prop

The type marks A apart from S.

Equations

• a.MarksAgent = (a = Alignment.AlignmentType.ergative ∨ a = Alignment.AlignmentType.tripartite)

@[instance_reducible]

instance Alignment.instDecidableMarksAgent (a : AlignmentType) : Decidable a.MarksAgent

Equations

• Alignment.instDecidableMarksAgent a = { decide := decide (a = Alignment.AlignmentType.ergative) || decide (a = Alignment.AlignmentType.tripartite), reflects_decide := ⋯ }

def Alignment.AlignmentType.MarksPatient (a : AlignmentType) : Prop

The type marks P apart from S.

Equations

• a.MarksPatient = (a = Alignment.AlignmentType.accusative ∨ a = Alignment.AlignmentType.tripartite)

@[instance_reducible]

instance Alignment.instDecidableMarksPatient (a : AlignmentType) : Decidable a.MarksPatient

Equations

• Alignment.instDecidableMarksPatient a = { decide := decide (a = Alignment.AlignmentType.accusative) || decide (a = Alignment.AlignmentType.tripartite), reflects_decide := ⋯ }

def Alignment.AlignmentType.Classifies {κ : Type u_2} (a : AlignmentType) (m : ArgumentRole → κ) : Prop

The alignment a type names, as a property of a marking. The split-S type names none, since it identifies no fixed pair of roles.

Equations

• Alignment.AlignmentType.neutral.Classifies m = Alignment.IsNeutral m
• Alignment.AlignmentType.accusative.Classifies m = Alignment.IsAccusative m
• Alignment.AlignmentType.ergative.Classifies m = Alignment.IsErgative m
• Alignment.AlignmentType.tripartite.Classifies m = Alignment.IsTripartite m
• Alignment.AlignmentType.active.Classifies m = False

@[instance_reducible]

instance Alignment.instDecidableClassifiesOfDecidableEq {κ : Type u_2} [DecidableEq κ] (m : ArgumentRole → κ) (a : AlignmentType) : Decidable (a.Classifies m)

Equations

• One or more equations did not get rendered due to their size.
• Alignment.instDecidableClassifiesOfDecidableEq m Alignment.AlignmentType.active = { decide := false, reflects_decide := ⋯ }

Conditioned marking

A marking may depend on a condition besides the role, such as the referential properties of the argument or of its co-argument, or the tense of the clause. A conditioned marking m : ArgumentRole → C → Option κ codes role r under condition c by the marker m r c, or by none, and its alignment under c is that of (m · c). Bickel, Witzlack-Makarevich and Zakharko represent a case as a relation between roles and conditions, and test hierarchy effects as the fit of a marking to an order on the conditions: A overtly coded on a lower set of them, P on an upper set. The papers that posit a scale assert fit; the papers that test it count it.

def Alignment.overt {κ : Type u_1} {C : Type u_2} (m : ArgumentRole → C → Option κ) (r : ArgumentRole) : Set C

The conditions under which role r is overtly coded.

Equations

• Alignment.overt m r = {c : C | m r c ≠ none}

@[simp]

theorem Alignment.mem_overt {κ : Type u_1} {C : Type u_2} (m : ArgumentRole → C → Option κ) {r : ArgumentRole} {c : C} : c ∈ overt m r ↔ m r c ≠ none

def Alignment.Fits {κ : Type u_1} {C : Type u_2} (m : ArgumentRole → C → Option κ) [Preorder C] : Prop

A conditioned marking fits an order on its conditions when A is overtly coded on a lower set of them and P on an upper set.

Equations

• Alignment.Fits m = (IsLowerSet (Alignment.overt m ArgumentRole.A) ∧ IsUpperSet (Alignment.overt m ArgumentRole.P))