Documentation

Studies.Dixon1994

Dixon (1994): Ergativity #

Dixon analyzes every language in terms of three universal syntactic-semantic relations, S, A and O (§1.1). A level of grammar is ergative when it treats S like O and unlike A, and accusative when it treats S like A and unlike O (§8.2). Morphological marking may be split by the verb (§4.1), by the NP along the Nominal Hierarchy (§4.2), or by tense, aspect or mood (§4.3), and inter-clausal syntax pivots on S/A or on S/O (Chapter 6).

In an NP-conditioned split, accusative marking of O extends in from the top of the hierarchy and ergative marking of A from the bottom. The two segments meet, as in Dyirbal and Kuku-Yalanji, or overlap in a tripartite zone, as in Cashinawa and Yidiny; a gap where neither applies is unattested, type (g) of the Appendix to Chapter 4. Passive alone feeds an S/A pivot for an NP in O function and antipassive alone an S/O pivot for one in A function, so a language with a thoroughgoing S/O pivot must have an antipassive (§6.2.3). English with its S/A pivot passivizes a clause in which the common NP is O, and Dyirbal with its S/O pivot antipassivizes one in which it is A (§6.2.2).

Implementation notes #

S, A and O are ArgumentRole.S, .A and .P, following the substrate's Comrie letters, and a marking of the core relations is any function out of ArgumentRole, so that ergativity and accusativity are the identifications of S the marking makes, Alignment.IsErgative and Alignment.IsAccusative. The Nominal Hierarchy is a linear order with first person at the top; an NP-conditioned split is a marking conditioned by the position, O accusative and A ergative on two sets of positions, and its alignment at a position is the substrate's. That the accusative marking is an upper set and the ergative a lower set is the fit of the split to the hierarchy (Alignment.Fits), proved for each table rather than built into the type. The tables of §4.2 are given as cutoffs, with the optional accusative of Yidiny's proper names and kin terms counted as marking; Latin and Waga-Waga, the types with one marking absent or total, are given directly. Pivots and derivations are the framework of §6.2.1 over core functions, with the periphery as none; the constructions that satisfy a pivot without derivation, such as Dyirbal's -ŋurra and instrumentive, are recorded in the rows only. Not formalized: the markedness generalizations of §3.4, the bound-versus-free split of §4.2.1, the main-versus- subordinate split of §4.4, the universal category of subject of Chapter 5, and the mixed pivots of §6.2.4.

References #

Splits conditioned by the verb, §4.1 #

inductive Dixon1994.SClass :

A split-S or fluid-S language divides S into two subtypes, Sa, marked like A, and So, marked like O.

sa : SClass
so : SClass

Instances For

@[instance_reducible]

instance Dixon1994.instDecidableEqSClass :

DecidableEq SClass

Equations

Dixon1994.instDecidableEqSClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dixon1994.instReprSClass :

Equations

Dixon1994.instReprSClass = { reprPrec := Dixon1994.instReprSClass.repr }

def Dixon1994.instReprSClass.repr :

SClass → ℕ → Std.Format

Equations

Dixon1994.instReprSClass.repr Dixon1994.SClass.sa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dixon1994.SClass.sa")).group prec✝
Dixon1994.instReprSClass.repr Dixon1994.SClass.so prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dixon1994.SClass.so")).group prec✝

Instances For

def Dixon1994.fluidS {I : Type u_2} (control : I → Prop) [DecidablePred control] (i : I) :

In a fluid-S system (§4.1.2) the S of an instance of use is Sa when its referent controls the activity and So otherwise. A split-S system (§4.1.1) instead fixes a class for each verb.

Equations

Dixon1994.fluidS control i = if control i then Dixon1994.SClass.sa else Dixon1994.SClass.so

Instances For

def Dixon1994.SClass.marking {κ : Type u_1} (m : ArgumentRole → κ) :

SClass → ArgumentRole → κ

Under the transitive marking m, an S of class c is marked like A or like O.

Equations

Dixon1994.SClass.marking m Dixon1994.SClass.sa ArgumentRole.S = m ArgumentRole.A
Dixon1994.SClass.marking m Dixon1994.SClass.so ArgumentRole.S = m ArgumentRole.P
Dixon1994.SClass.marking m x✝¹ x✝ = m x✝

Instances For

theorem Dixon1994.marking_sa_so {κ : Type u_1} {m : ArgumentRole → κ} (h : m ArgumentRole.A ≠ m ArgumentRole.P) :

Alignment.IsAccusative (SClass.marking m SClass.sa) ∧ Alignment.IsErgative (SClass.marking m SClass.so)

A split system mixes the two simple patterns (§4.1.1), accusative over Sa verbs and ergative over So verbs, whenever A and O are distinguished.

Splits conditioned by the NP: the Nominal Hierarchy, §4.2 #

inductive Dixon1994.Nominal :

The Nominal Hierarchy (Figure 4.5) orders NPs by their likelihood of being in A rather than in O function, from first person pronouns, second person pronouns, demonstratives and third person pronouns, and proper names down to common nouns with human, animate and inanimate reference, the common nouns ordered by the animacy of their referents.

firstPerson : Nominal
secondPerson : Nominal
thirdPerson : Nominal
properName : Nominal
common (a : Reference.Animacy) : Nominal

Instances For

@[instance_reducible]

instance Dixon1994.instDecidableEqNominal :

DecidableEq Nominal

Equations

Dixon1994.instDecidableEqNominal = Dixon1994.instDecidableEqNominal.decEq

def Dixon1994.instDecidableEqNominal.decEq (x✝ x✝¹ : Nominal) :

Decidable (x✝ = x✝¹)

Equations

Instances For

def Dixon1994.instReprNominal.repr :

Nominal → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Dixon1994.instReprNominal :

Equations

Dixon1994.instReprNominal = { reprPrec := Dixon1994.instReprNominal.repr }

@[instance_reducible]

instance Dixon1994.instFintypeNominal :

Fintype Nominal

Equations

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

def Dixon1994.Nominal.rank :

Nominal → ℕ

Position on the hierarchy, higher to the left.

Equations

Dixon1994.Nominal.firstPerson.rank = 6
Dixon1994.Nominal.secondPerson.rank = 5
Dixon1994.Nominal.thirdPerson.rank = 4
Dixon1994.Nominal.properName.rank = 3
(Dixon1994.Nominal.common a).rank = a.rank

Instances For

@[instance_reducible]

instance Dixon1994.instLinearOrderNominal :

LinearOrder Nominal

Equations

Dixon1994.instLinearOrderNominal = LinearOrder.lift' Dixon1994.Nominal.rank Dixon1994.instLinearOrderNominal._proof_1

def Dixon1994.Nominal.nominality :

Nominal → Reference.Nominality

The pronoun positions of the Nominal Hierarchy are pronouns, the proper-name position names, and the rest common nouns.

Equations

Instances For

theorem Dixon1994.Nominal.nominality_monotone :

Monotone nominality

The Nominal Hierarchy refines nominality.

def Dixon1994.split {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] :

ArgumentRole → H → Option Case

In an NP-conditioned split (§4.2), O is marked accusative at the positions of the hierarchy where acc holds and A ergative where erg holds, and S is unmarked.

Equations

Dixon1994.split acc erg ArgumentRole.A x✝ = if erg x✝ then some Case.erg else none
Dixon1994.split acc erg ArgumentRole.P x✝ = if acc x✝ then some Case.acc else none
Dixon1994.split acc erg x✝¹ x✝ = none

Instances For

@[simp]

theorem Dixon1994.overt_split_A {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] :

Alignment.overt (split acc erg) ArgumentRole.A = {p : H | erg p}

@[simp]

theorem Dixon1994.overt_split_P {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] :

Alignment.overt (split acc erg) ArgumentRole.P = {p : H | acc p}

theorem Dixon1994.fits_split_iff {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] [Preorder H] :

Alignment.Fits (split acc erg) ↔ IsUpperSet {p : H | acc p} ∧ IsLowerSet {p : H | erg p}

A split fits the hierarchy exactly when its accusative marking is an upper set and its ergative marking a lower set.

theorem Dixon1994.isAccusative_split_iff {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] (p : H) :

(Alignment.IsAccusative fun (x : ArgumentRole) => split acc erg x p) ↔ acc p ∧ ¬erg p

theorem Dixon1994.isErgative_split_iff {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] (p : H) :

(Alignment.IsErgative fun (x : ArgumentRole) => split acc erg x p) ↔ ¬acc p ∧ erg p

theorem Dixon1994.isTripartite_split_iff {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] (p : H) :

(Alignment.IsTripartite fun (x : ArgumentRole) => split acc erg x p) ↔ acc p ∧ erg p

theorem Dixon1994.isNeutral_split_iff {H : Type u_2} (acc erg : H → Prop) [DecidablePred acc] [DecidablePred erg] (p : H) :

(Alignment.IsNeutral fun (x : ArgumentRole) => split acc erg x p) ↔ ¬acc p ∧ ¬erg p

theorem Dixon1994.IsAccusative.of_le {H : Type u_2} {acc erg : H → Prop} [DecidablePred acc] [DecidablePred erg] {p q : H} [Preorder H] (h : Alignment.Fits (split acc erg)) (hp : Alignment.IsAccusative fun (x : ArgumentRole) => split acc erg x p) (hpq : p ≤ q) :

Alignment.IsAccusative fun (x : ArgumentRole) => split acc erg x q

In a split that fits, the pattern stays accusative above an accusative position.

theorem Dixon1994.IsErgative.of_le {H : Type u_2} {acc erg : H → Prop} [DecidablePred acc] [DecidablePred erg] {p q : H} [Preorder H] (h : Alignment.Fits (split acc erg)) (hq : Alignment.IsErgative fun (x : ArgumentRole) => split acc erg x q) (hpq : p ≤ q) :

Alignment.IsErgative fun (x : ArgumentRole) => split acc erg x p

In a split that fits, the pattern stays ergative below an ergative position.

theorem Dixon1994.not_isTripartite_and_isNeutral {H : Type u_2} {acc erg : H → Prop} [DecidablePred acc] [DecidablePred erg] {p q : H} [LinearOrder H] (h : Alignment.Fits (split acc erg)) (ht : Alignment.IsTripartite fun (x : ArgumentRole) => split acc erg x p) (hn : Alignment.IsNeutral fun (x : ArgumentRole) => split acc erg x q) :

False

In a split that fits, an overlap of the two markings and a gap between them exclude each other, so a split is of type (d) of the Appendix to Chapter 4 or of the unattested type (g), never both.

def Dixon1994.ofCutoffs {H : Type u_2} [Preorder H] [DecidableLE H] (a e : H) :

ArgumentRole → H → Option Case

The split with accusative marking from the top of the hierarchy down to a and ergative marking from the bottom up to e.

Equations

Dixon1994.ofCutoffs a e = Dixon1994.split (fun (x : H) => a ≤ x) fun (x : H) => x ≤ e

Instances For

theorem Dixon1994.fits_ofCutoffs {H : Type u_2} [Preorder H] [DecidableLE H] (a e : H) :

Alignment.Fits (ofCutoffs a e)

def Dixon1994.dyirbal :

ArgumentRole → Nominal → Option Case

Dyirbal (Table 4.1) marks first and second person pronouns accusatively and NPs from third person pronouns rightwards ergatively, the two meeting without overlap.

Equations

Dixon1994.dyirbal = Dixon1994.ofCutoffs Dixon1994.Nominal.secondPerson Dixon1994.Nominal.thirdPerson

Instances For

def Dixon1994.cashinawa :

ArgumentRole → Nominal → Option Case

Cashinawa (Table 4.2) marks NPs down to third person pronouns accusatively and from third person pronouns rightwards ergatively, the two overlapping there.

Equations

Dixon1994.cashinawa = Dixon1994.ofCutoffs Dixon1994.Nominal.thirdPerson Dixon1994.Nominal.thirdPerson

Instances For

def Dixon1994.yidiny :

ArgumentRole → Nominal → Option Case

Yidiny (Table 4.3) marks NPs down to proper names and kin terms accusatively and from human deictics rightwards ergatively, the two overlapping over the middle of the hierarchy.

Equations

Dixon1994.yidiny = Dixon1994.ofCutoffs Dixon1994.Nominal.properName Dixon1994.Nominal.thirdPerson

Instances For

def Dixon1994.latin :

ArgumentRole → Nominal → Option Case

Latin, of type (a), marks pronouns and masculine and feminine nouns accusatively and has no ergative, so that neuter nouns have one form for S, A and O.

Equations

Dixon1994.latin = Dixon1994.split (fun (x : Dixon1994.Nominal) => Dixon1994.Nominal.common Reference.Animacy.human ≤ x) fun (x : Dixon1994.Nominal) => False

Instances For

def Dixon1994.wagaWaga :

ArgumentRole → Nominal → Option Case

Waga-Waga, of type (f) (fn. 14), marks every NP constituent ergatively and NPs down to human common nouns accusatively, so that the left and middle of the hierarchy are tripartite.

Equations

Dixon1994.wagaWaga = Dixon1994.split (fun (x : Dixon1994.Nominal) => Dixon1994.Nominal.common Reference.Animacy.human ≤ x) fun (x : Dixon1994.Nominal) => True

Instances For

theorem Dixon1994.splits_fit :

Alignment.Fits dyirbal ∧ Alignment.Fits cashinawa ∧ Alignment.Fits yidiny ∧ Alignment.Fits latin ∧ Alignment.Fits wagaWaga

Every split of §4.2 fits the Nominal Hierarchy.

theorem Dixon1994.patterns :

(∀ (p : Nominal), (¬Alignment.IsTripartite fun (x : ArgumentRole) => dyirbal x p) ∧ ¬Alignment.IsNeutral fun (x : ArgumentRole) => dyirbal x p) ∧ (Alignment.IsAccusative fun (x : ArgumentRole) => dyirbal x Nominal.secondPerson) ∧ (Alignment.IsErgative fun (x : ArgumentRole) => dyirbal x Nominal.thirdPerson) ∧ (Alignment.IsTripartite fun (x : ArgumentRole) => cashinawa x Nominal.thirdPerson) ∧ (Alignment.IsErgative fun (x : ArgumentRole) => cashinawa x Nominal.properName) ∧ (Alignment.IsTripartite fun (x : ArgumentRole) => yidiny x Nominal.thirdPerson) ∧ (Alignment.IsTripartite fun (x : ArgumentRole) => yidiny x Nominal.properName) ∧ (Alignment.IsErgative fun (x : ArgumentRole) => yidiny x (Nominal.common Reference.Animacy.human)) ∧ (Alignment.IsNeutral fun (x : ArgumentRole) => latin x (Nominal.common Reference.Animacy.animate)) ∧ (Alignment.IsTripartite fun (x : ArgumentRole) => wagaWaga x (Nominal.common Reference.Animacy.human)) ∧ Alignment.IsErgative fun (x : ArgumentRole) => wagaWaga x (Nominal.common Reference.Animacy.animate)

The cutoffs induce the alignments of the types. Dyirbal's markings meet at third person pronouns, type (c); Cashinawa and Yidiny overlap in tripartite zones, type (d); Latin leaves neuter nouns neutral, type (a); and Waga-Waga is tripartite down to human nouns and ergative below, type (f).

Splits conditioned by tense, aspect or mood, §4.3 #

def Dixon1994.AspectOriented (s : Aspect.Perfectivity → Alignment.AlignmentType) :

An aspect-conditioned split is aspect-oriented when, as Dixon generalizes, the ergative marking is found in the perfective and never in the imperfective alone.

Equations

Dixon1994.AspectOriented s = (s Aspect.Perfectivity.imperfective = Alignment.AlignmentType.ergative → s Aspect.Perfectivity.perfective = Alignment.AlignmentType.ergative)

Instances For

theorem Dixon1994.aspectOriented_hindi :

AspectOriented HindiUrdu.alignment

Passive, antipassive and pivots, §6.1 and §6.2 #

inductive Dixon1994.Pivot :

A pivot (§6.2) is the pair of functions an NP common to two linked clauses must bear in each, S or A in a language with accusative syntax and S or O in one with ergative syntax.

SA : Pivot
SO : Pivot

Instances For

@[instance_reducible]

instance Dixon1994.instDecidableEqPivot :

DecidableEq Pivot

Equations

Dixon1994.instDecidableEqPivot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dixon1994.instReprPivot.repr :

Pivot → ℕ → Std.Format

Equations

Dixon1994.instReprPivot.repr Dixon1994.Pivot.SA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dixon1994.Pivot.SA")).group prec✝
Dixon1994.instReprPivot.repr Dixon1994.Pivot.SO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dixon1994.Pivot.SO")).group prec✝

Instances For

@[instance_reducible]

instance Dixon1994.instReprPivot :

Repr Pivot

Equations

Dixon1994.instReprPivot = { reprPrec := Dixon1994.instReprPivot.repr }

@[instance_reducible]

instance Dixon1994.instFintypePivot :

Fintype Pivot

Equations

Dixon1994.instFintypePivot = { elems := { val := ↑Dixon1994.Pivot.enumList, nodup := Dixon1994.Pivot.enumList_nodup }, complete := Dixon1994.instFintypePivot._proof_1 }

def Dixon1994.Pivot.Admits :

Pivot → ArgumentRole → Prop

Whether a core function is a pivot function.

Equations

Dixon1994.Pivot.SA.Admits ArgumentRole.S = True
Dixon1994.Pivot.SA.Admits ArgumentRole.A = True
Dixon1994.Pivot.SO.Admits ArgumentRole.S = True
Dixon1994.Pivot.SO.Admits ArgumentRole.P = True
x✝¹.Admits x✝ = False

Instances For

@[instance_reducible]

instance Dixon1994.instDecidableAdmits (π : Pivot) (r : ArgumentRole) :

Decidable (π.Admits r)

Equations

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

inductive Dixon1994.Derivation :

The two derivations of §6.1, each forming an intransitive from a transitive clause.

passive : Derivation
antipassive : Derivation

Instances For

@[instance_reducible]

instance Dixon1994.instDecidableEqDerivation :

DecidableEq Derivation

Equations

Dixon1994.instDecidableEqDerivation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Dixon1994.instReprDerivation.repr :

Derivation → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Dixon1994.instReprDerivation :

Repr Derivation

Equations

Dixon1994.instReprDerivation = { reprPrec := Dixon1994.instReprDerivation.repr }

@[instance_reducible]

instance Dixon1994.instFintypeDerivation :

Fintype Derivation

Equations

Dixon1994.instFintypeDerivation = { elems := { val := ↑Dixon1994.Derivation.enumList, nodup := Dixon1994.Derivation.enumList_nodup }, complete := Dixon1994.instFintypeDerivation._proof_1 }

def Dixon1994.Derivation.apply :

Derivation → ArgumentRole → Option ArgumentRole

d.apply r is the function the derivation d gives the core function r. Passive puts O into S and A into the periphery, antipassive puts A into S and O into the periphery, and the ditransitive roles are peripheral.

Equations

Dixon1994.Derivation.passive.apply ArgumentRole.P = some ArgumentRole.S
Dixon1994.Derivation.antipassive.apply ArgumentRole.A = some ArgumentRole.S
x✝.apply ArgumentRole.S = some ArgumentRole.S
x✝¹.apply x✝ = none

Instances For

def Dixon1994.Feeds (π : Pivot) (d : Derivation) (r : ArgumentRole) :

A derivation feeds a pivot for an NP in function r when the derived function is a pivot function.

Equations

Dixon1994.Feeds π d r = ∃ (g : ArgumentRole), d.apply r = some g ∧ π.Admits g

Instances For

theorem Dixon1994.not_admits_iff :

(∀ r ∈ ArgumentRole.core, ¬Pivot.SA.Admits r ↔ r = ArgumentRole.P) ∧ ∀ r ∈ ArgumentRole.core, ¬Pivot.SO.Admits r ↔ r = ArgumentRole.A

A common NP needs a derivation in a clause exactly when its function there is not a pivot function, O under an S/A pivot and A under an S/O pivot.

theorem Dixon1994.feeds_iff :

(∀ (d : Derivation), Feeds Pivot.SA d ArgumentRole.P ↔ d = Derivation.passive) ∧ (∀ (d : Derivation), Feeds Pivot.SO d ArgumentRole.A ↔ d = Derivation.antipassive) ∧ ¬Feeds Pivot.SA Derivation.passive ArgumentRole.A ∧ ¬Feeds Pivot.SO Derivation.antipassive ArgumentRole.P

Passive alone feeds an S/A pivot for an NP in O function, and antipassive alone feeds an S/O pivot for an NP in A function, §6.2.1 and §6.2.2; each derivation demotes the other function to the periphery. So a language with a thoroughgoing S/O pivot must have an antipassive, §6.2.3.

def Dixon1994.swapAO :

ArgumentRole → ArgumentRole

Interchange A and O, leaving S and the ditransitive roles alone.

Equations

Dixon1994.swapAO ArgumentRole.A = ArgumentRole.P
Dixon1994.swapAO ArgumentRole.P = ArgumentRole.A
Dixon1994.swapAO x✝ = x✝

Instances For

theorem Dixon1994.apply_swapAO (r : ArgumentRole) :

Derivation.passive.apply r = Derivation.antipassive.apply (swapAO r)

Passive and antipassive are parallel with A and O interchanged, §6.1.