Stassen (2000): AND-languages and WITH-languages

This file formalizes [Sta00]'s typology of noun phrase conjunction, the encoding of a single event predicated simultaneously of two participants conceived of as separate individuals, over a sample of 260 languages. The domain is encoded by a coordinate strategy or a comitative strategy, which contrast in four features: whether the two NPs have the same structural rank, form a constituent, govern dual or plural agreement, and are linked by an item distinct from the comitative marker (Feature). An encoding is the set of coordinate features it has, so the encodings form the Boolean lattice Finset Feature: the comitative strategy is ⊥, the coordinate strategy ⊤, and the in-between cases the paper allows for lie between the two focal positions.

Nearly every language has the comitative strategy. An AND-language also has an encoding with every coordinate feature relevant to it, and a WITH-language is one that is not an AND-language (Language.IsAnd). Plural agreement is relevant only where verbs agree with their subject (Language.relevant), since the paper's AND-languages include languages without verb agreement and its pattern schemes distinguish languages with and without it; where verbs agree, an AND-language is one with the coordinate strategy itself (Language.isAnd_iff_top_mem).

AND-languages are diachronically stable and pure WITH-languages rare: WITH-languages grammaticalize the comitative strategy, moving up the lattice while the linker stays lexically identical to the comitative marker. The resulting hybrids leave the language a WITH-language however far they go (Language.not_isAnd_of_forall_notMem). The most advanced hybrid has every relevant feature but the linker and is covered by the coordinate strategy (Language.erase_distinctMarker_covBy); it is the one hybrid that differentiating the linker turns into a coordinate strategy (Language.relevant_le_insert_iff), the mixed WITH-language the paper would call an AND-language but for the lexical identity of the markers.

The lexical identity is checked on the Fragments, where a coordinator is also comitative when its form is a form of a comitative marker of its language, an adposition or a case (Coordinator.IsAlsoComitative): English and is not with, while Hausa dà, Japanese to and the Yakut comitative suffix are both 'and' and 'with' (hausa_da_isAlsoComitative, japanese_to_isAlsoComitative, yakut_lin_isAlsoComitative).

The starting point of the drift is the language's pattern scheme, its basic word order with the comitative phrase in adverbial position (scheme). The subject and the comitative phrase are contiguous exactly when the verb is not medial (adjacent_scheme_iff). The constituent that grammaticalization creates therefore presupposes, in an SVO language, a shift of the comitative phrase across the verb (shift, adjacent_shift), which yields the SOV scheme (shift_scheme_svo), whereas verb-final and verb-initial schemes are contiguous already.

Implementation notes

The paper's schemes (107), (123) and (124) put the comitative phrase where the object stands in SVO, SOV and VSO order, so scheme places it there for every basic order and contiguity is derived from the order. As in the paper, schemes have intransitive predicates.

The correlational tendencies, that cased and tensed languages tend to AND-status and WITH-languages to be non-cased and non-tensed, with the AND-cased and WITH-non-cased combinations the frequent ones, are stated by the paper qualitatively, without a cross-tabulation, and the areal distribution is descriptive; neither is formalized. The sample is summarized only as containing roughly twice as many AND-languages as WITH-languages.

TODO

The paper argues that verb-final and verb-initial WITH-languages without agreement, (123a) and (124a), can mark the new constituent neither by position nor by agreement, so that they tend to stay pure WITH-languages, and that some verb-final ones double the comitative marker instead, (125). Stating this needs the formal means by which each feature is marked.

References

• [Sta00]

Encodings

inductive Stassen2000.Feature : Type

The features of the coordinate strategy, the paper's (83), each opposed to a feature of the comitative strategy. The two NPs have the same structural rank, form a constituent, govern dual or plural agreement, and are linked by an item distinct from the comitative marker. An encoding is the Finset of the features it has.

• equalRank : Feature
• constituent : Feature
• pluralAgreement : Feature
• distinctMarker : Feature

@[instance_reducible]

instance Stassen2000.instDecidableEqFeature : DecidableEq Feature

Equations

• Stassen2000.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stassen2000.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stassen2000.instReprFeature : Repr Feature

Equations

• Stassen2000.instReprFeature = { reprPrec := Stassen2000.instReprFeature.repr }

@[instance_reducible]

instance Stassen2000.instFintypeFeature : Fintype Feature

Equations

• Stassen2000.instFintypeFeature = { elems := { val := ↑Stassen2000.Feature.enumList, nodup := Stassen2000.Feature.enumList_nodup }, complete := Stassen2000.instFintypeFeature._proof_1 }

AND-languages and WITH-languages

structure Stassen2000.Language : Type

A language records whether its verbs agree with their subject, and its encodings of the domain.

• Agrees : Prop

  The verbs agree with their subject in person, number and gender.

• decidableAgrees : Decidable self.Agrees
• encodings : Finset (Finset Feature)

  The encodings of noun phrase conjunction.

def Stassen2000.Language.relevant (l : Language) : Finset Feature

The coordinate features relevant to the language, plural agreement only where its verbs agree.

Equations

• l.relevant = if l.Agrees then ⊤ else {Stassen2000.Feature.pluralAgreement}ᶜ

def Stassen2000.Language.IsAnd (l : Language) : Prop

An AND-language has an encoding with every relevant coordinate feature.

Equations

• l.IsAnd = ∃ e ∈ l.encodings, l.relevant ⊆ e

@[instance_reducible]

instance Stassen2000.Language.instDecidableIsAnd (l : Language) : Decidable l.IsAnd

Equations

• l.instDecidableIsAnd = { decide := decide (∃ (a : Finset Stassen2000.Feature) (_ : a ∈ l.encodings), l.relevant ⊆ a), reflects_decide := ⋯ }

theorem Stassen2000.Language.relevant_of_agrees {l : Language} (h : l.Agrees) : l.relevant = ⊤

theorem Stassen2000.Language.isAnd_iff_top_mem {l : Language} (h : l.Agrees) : l.IsAnd ↔ ⊤ ∈ l.encodings

Where verbs agree, an AND-language is one with the coordinate strategy itself.

theorem Stassen2000.Language.distinctMarker_mem_relevant {l : Language} : Feature.distinctMarker ∈ l.relevant

theorem Stassen2000.Language.not_isAnd_of_forall_notMem {l : Language} (h : ∀ e ∈ l.encodings, Feature.distinctMarker ∉ e) : ¬l.IsAnd

The paper's guideline for rating. A language whose every encoding links with the comitative marker is a WITH-language, however far its hybrids have grammaticalized.

theorem Stassen2000.Language.erase_distinctMarker_covBy (l : Language) : l.relevant.erase Feature.distinctMarker ⋖ l.relevant

The most advanced hybrid, with every relevant feature but the linker, is one feature short of the coordinate strategy.

theorem Stassen2000.Language.relevant_le_insert_iff {l : Language} {e : Finset Feature} (he : e ⊆ l.relevant) (hm : Feature.distinctMarker ∉ e) : l.relevant ⊆ insert Feature.distinctMarker e ↔ e = l.relevant.erase Feature.distinctMarker

Differentiating the linker of a hybrid yields every relevant feature exactly when the hybrid is the most advanced one.

The linker in the Fragments

theorem Stassen2000.english_and_not_isAlsoComitative : ¬English.Coordination.and_.IsAlsoComitative English.Adpositions.with_.morphs English.Adpositions.with_.functions

English, the paper's example of an AND-language, links its coordinate strategy by and, distinct from its comitative with.

theorem Stassen2000.hausa_da_isAlsoComitative : Hausa.Coordination.da.IsAlsoComitative Hausa.Adpositions.da.morphs Hausa.Adpositions.da.functions

Hausa dà 'and' is the comitative preposition dà 'with', (109).

theorem Stassen2000.japanese_to_isAlsoComitative : Japanese.Coordination.to_.IsAlsoComitative Japanese.Adpositions.to.morphs Japanese.Adpositions.to.functions

Japanese, one of the verb-final WITH-languages of the paper, links its noun phrases by the comitative postposition to.

theorem Stassen2000.yakut_lin_isAlsoComitative : Yakut.Coordination.lin.IsAlsoComitative Yakut.Case.com.exponents {Yakut.Case.com.label}

Yakut, another verb-final WITH-language of the paper, links its noun phrases by the comitative suffix -LĪn.

Pattern schemes

inductive Stassen2000.Slot : Type

The elements of a pattern scheme with an intransitive predicate are the subject, the verb, and the comitative phrase.

• subject : Slot
• verb : Slot
• comitative : Slot

@[instance_reducible]

instance Stassen2000.instDecidableEqSlot : DecidableEq Slot

Equations

• Stassen2000.instDecidableEqSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stassen2000.instReprSlot : Repr Slot

Equations

• Stassen2000.instReprSlot = { reprPrec := Stassen2000.instReprSlot.repr }

def Stassen2000.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

• Stassen2000.instReprSlot.repr Stassen2000.Slot.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stassen2000.Slot.subject")).group prec✝
• Stassen2000.instReprSlot.repr Stassen2000.Slot.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stassen2000.Slot.verb")).group prec✝
• Stassen2000.instReprSlot.repr Stassen2000.Slot.comitative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stassen2000.Slot.comitative")).group prec✝

@[instance_reducible]

instance Stassen2000.instFintypeSlot : Fintype Slot

Equations

• Stassen2000.instFintypeSlot = { elems := { val := ↑Stassen2000.Slot.enumList, nodup := Stassen2000.Slot.enumList_nodup }, complete := Stassen2000.instFintypeSlot._proof_1 }

def Stassen2000.Slot.equivConstituent : Slot ≃ WordOrder.Constituent

The slots of a scheme as the constituents of a clause, the comitative phrase in the object's position.

Equations

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

def Stassen2000.scheme (a : WordOrder.Arrangement WordOrder.Constituent 3) : WordOrder.Arrangement Slot 3

The pattern scheme of a basic word order, the paper's (107), (123) and (124). The comitative phrase stands in the canonical position of adverbial phrases, which in these schemes is the object's.

Equations

• Stassen2000.scheme a = Stassen2000.Slot.equivConstituent.trans a

theorem Stassen2000.adjacent_scheme_iff (a : WordOrder.Arrangement WordOrder.Constituent 3) : (scheme a).Adjacent Slot.subject Slot.comitative ↔ ¬a.IsMedial WordOrder.Constituent.verb

The subject and the comitative phrase of a scheme are contiguous exactly when the verb is not medial.

theorem Stassen2000.not_adjacent_scheme_svo : ¬(scheme WordOrder.Arrangement.svo).Adjacent Slot.subject Slot.comitative

In an SVO language the verb separates the two NPs, (107).

theorem Stassen2000.adjacent_scheme_sov : (scheme WordOrder.Arrangement.sov).Adjacent Slot.subject Slot.comitative

SOV and VSO schemes are contiguous already, (123) and (124).

theorem Stassen2000.adjacent_scheme_vso : (scheme WordOrder.Arrangement.vso).Adjacent Slot.subject Slot.comitative

def Stassen2000.shift (s : WordOrder.Arrangement Slot 3) : WordOrder.Arrangement Slot 3

The shift of the comitative phrase, the paper's (108), is the transposition of the verb and the comitative phrase, which moves the comitative phrase across a medial verb.

Equations

• Stassen2000.shift s = Equiv.trans (Equiv.swap Stassen2000.Slot.verb Stassen2000.Slot.comitative) s

theorem Stassen2000.adjacent_shift {s : WordOrder.Arrangement Slot 3} (h : s.IsMedial Slot.verb) : (shift s).Adjacent Slot.subject Slot.comitative

Where the verb is medial, the shift makes the subject and the comitative phrase contiguous, so that the string can be reanalyzed as a constituent.

theorem Stassen2000.shift_scheme_svo : shift (scheme WordOrder.Arrangement.svo) = scheme WordOrder.Arrangement.sov

The shifted SVO scheme is the SOV scheme: (108) has the order of (123).