Typology.Coordination

@cite{haspelmath-2007} @cite{stassen-2000} @cite{mitrovic-sauerland-2016} @cite{dryer-haspelmath-2013} @cite{wals-2013}

Per-language typological substrate for coordination across three frameworks:

1. @cite{haspelmath-2007} structural typology: syndesis (asyndetic / monosyndetic / bisyndetic), coordinator position, structural patterns, and diachronic source (comitative vs additive focus particle).
2. @cite{stassen-2000} AND/WITH typology: derived from WALS Ch 63 (lexical identity of "and" and "with").
3. WALS Ch 56/63/64: conjunction-quantifier relation, NP conjunction, nominal-vs-verbal conjunction.

Mirrors the Linglib/Typology/{Possession,Negation,Question,Comparison}.lean substrate-extension pattern. Fragment-importable; cross-linguistic theorems live in Studies/Haspelmath2007.lean (structural typology + 19-language sample) and Studies/Stassen2000.lean (AND/WITH typology + 15-language WALS sample).

What lives here

• Syndesis, CoordinatorPosition, CoordPattern, DiachronicSource enums (@cite{haspelmath-2007}).
• AndWithStatus enum (@cite{stassen-2000}); derivation from WALS Ch 63.
• WALS aliases: ConjQuantRelation, ConjComitativeRelation, NomVerbalConjRelation for Chs 56/63/64.
• SourcedEntry, ConjunctionSystem structs (M&S framework).
• CoordinationProfile struct (WALS profile bundle).
• Helper predicates: hasStrategy, muIsAdditive, hasSource, hasMonosyndetic, hasBisyndetic, muBoundness.
• WALS aggregate sample-size + corpus-only generalisations (Ch 56/63/64).

Theory-laden caveats

• DiachronicSource collapses Heine's full grammaticalization-source taxonomy to two main pathways relevant for coordination (comitative, focus particle); other pathways (e.g. coordinator from sequence adverbial) are conflated under .other.
• AndWithStatus is @cite{stassen-2000}'s binary classification; some authors (e.g. Mauri 2008) argue for a finer multi-way split.

inductive Typology.Coordination.Syndesis : Type

Syndesis: presence and number of overt coordinators (Haspelmath §1).

• asyndetic : Syndesis
• monosyndetic : Syndesis
• bisyndetic : Syndesis

@[implicit_reducible]

instance Typology.Coordination.instDecidableEqSyndesis : DecidableEq Syndesis

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instBEqSyndesis : BEq Syndesis

Equations

• Typology.Coordination.instBEqSyndesis = { beq := Typology.Coordination.instBEqSyndesis.beq }

def Typology.Coordination.instBEqSyndesis.beq : Syndesis → Syndesis → Bool

Equations

• Typology.Coordination.instBEqSyndesis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Coordination.instReprSyndesis : Repr Syndesis

Equations

• Typology.Coordination.instReprSyndesis = { reprPrec := Typology.Coordination.instReprSyndesis.repr }

def Typology.Coordination.instReprSyndesis.repr : Syndesis → Nat → Std.Format

Equations

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

inductive Typology.Coordination.CoordinatorPosition : Type

Coordinator position relative to its coordinand (Haspelmath §1.2).

@cite{haspelmath-2007} notes that co-A B (prepositive on first coordinand only) is unattested (cf. @cite{stassen-2000}, n=260).

• prepositive : CoordinatorPosition
• postpositive : CoordinatorPosition

@[implicit_reducible]

instance Typology.Coordination.instDecidableEqCoordinatorPosition : DecidableEq CoordinatorPosition

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instBEqCoordinatorPosition : BEq CoordinatorPosition

Equations

• Typology.Coordination.instBEqCoordinatorPosition = { beq := Typology.Coordination.instBEqCoordinatorPosition.beq }

def Typology.Coordination.instBEqCoordinatorPosition.beq : CoordinatorPosition → CoordinatorPosition → Bool

Equations

• Typology.Coordination.instBEqCoordinatorPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Coordination.instReprCoordinatorPosition : Repr CoordinatorPosition

Equations

• Typology.Coordination.instReprCoordinatorPosition = { reprPrec := Typology.Coordination.instReprCoordinatorPosition.repr }

def Typology.Coordination.instReprCoordinatorPosition.repr : CoordinatorPosition → Nat → Std.Format

Equations

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

inductive Typology.Coordination.CoordPattern : Type

Structural pattern for binary coordination (Haspelmath (17)).

Monosyndetic: 3 attested patterns (of 4 logically possible). A co-B (prepositive on 2nd: English "A and B") A-co B (postpositive on 1st: Tibetan "A-daŋ B") A B-co (postpositive on 2nd: Latin "A B-que") co-A B — UNATTESTED (@cite{haspelmath-2007})

Bisyndetic: 4 attested patterns.

• a_co_b : CoordPattern

  A co-B: medial prepositive (English "A and B").

• a'co_b : CoordPattern

  A-co B: medial postpositive on 1st (Tibetan "A-daŋ B").

• a_b'co : CoordPattern

  A B-co: final postpositive (Latin "senatus populus-que").

• co'a_co'b : CoordPattern

  co-A co-B: prepositive bisyndetic (Yoruba "àtí A àtí B").

• a'co_b'co : CoordPattern

  A-co B-co: postpositive bisyndetic (Martuthunira "A-thurti B-thurti").

• a'co_co'b : CoordPattern

  A-co co-B: mixed bisyndetic (Homeric Greek "A-te kaì B").

• co'a_b'co : CoordPattern

  co-A B-co: mixed bisyndetic (Latin "et A B-que").

@[implicit_reducible]

instance Typology.Coordination.instDecidableEqCoordPattern : DecidableEq CoordPattern

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instBEqCoordPattern : BEq CoordPattern

Equations

• Typology.Coordination.instBEqCoordPattern = { beq := Typology.Coordination.instBEqCoordPattern.beq }

def Typology.Coordination.instBEqCoordPattern.beq : CoordPattern → CoordPattern → Bool

Equations

• Typology.Coordination.instBEqCoordPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Coordination.instReprCoordPattern : Repr CoordPattern

Equations

• Typology.Coordination.instReprCoordPattern = { reprPrec := Typology.Coordination.instReprCoordPattern.repr }

def Typology.Coordination.instReprCoordPattern.repr : CoordPattern → Nat → Std.Format

Equations

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

def Typology.Coordination.CoordPattern.syndesis : CoordPattern → Syndesis

Classify a pattern's syndesis.

Equations

• Typology.Coordination.CoordPattern.a_co_b.syndesis = Typology.Coordination.Syndesis.monosyndetic
• Typology.Coordination.CoordPattern.a'co_b.syndesis = Typology.Coordination.Syndesis.monosyndetic
• Typology.Coordination.CoordPattern.a_b'co.syndesis = Typology.Coordination.Syndesis.monosyndetic
• Typology.Coordination.CoordPattern.co'a_co'b.syndesis = Typology.Coordination.Syndesis.bisyndetic
• Typology.Coordination.CoordPattern.a'co_b'co.syndesis = Typology.Coordination.Syndesis.bisyndetic
• Typology.Coordination.CoordPattern.a'co_co'b.syndesis = Typology.Coordination.Syndesis.bisyndetic
• Typology.Coordination.CoordPattern.co'a_b'co.syndesis = Typology.Coordination.Syndesis.bisyndetic

inductive Typology.Coordination.DiachronicSource : Type

Diachronic source of conjunction constructions (Haspelmath §5.1).

• comitative : DiachronicSource
• focusParticle : DiachronicSource
• other : DiachronicSource

@[implicit_reducible]

instance Typology.Coordination.instDecidableEqDiachronicSource : DecidableEq DiachronicSource

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instBEqDiachronicSource : BEq DiachronicSource

Equations

• Typology.Coordination.instBEqDiachronicSource = { beq := Typology.Coordination.instBEqDiachronicSource.beq }

def Typology.Coordination.instBEqDiachronicSource.beq : DiachronicSource → DiachronicSource → Bool

Equations

• Typology.Coordination.instBEqDiachronicSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Typology.Coordination.instReprDiachronicSource.repr : DiachronicSource → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instReprDiachronicSource : Repr DiachronicSource

Equations

• Typology.Coordination.instReprDiachronicSource = { reprPrec := Typology.Coordination.instReprDiachronicSource.repr }

def Typology.Coordination.DiachronicSource.expectedPattern : DiachronicSource → Syndesis

Haspelmath's key insight connecting diachronic source to structural pattern.

Equations

• Typology.Coordination.DiachronicSource.comitative.expectedPattern = Typology.Coordination.Syndesis.monosyndetic
• Typology.Coordination.DiachronicSource.focusParticle.expectedPattern = Typology.Coordination.Syndesis.bisyndetic
• Typology.Coordination.DiachronicSource.other.expectedPattern = Typology.Coordination.Syndesis.monosyndetic

inductive Typology.Coordination.AndWithStatus : Type

@cite{stassen-2000} AND/WITH classification of languages. AND-languages have structurally distinct coordinate and comitative strategies. WITH-languages use comitative encoding as the only strategy for NP conjunction (lexical identity of "and" and "with").

• andLang : AndWithStatus
• withLang : AndWithStatus

@[implicit_reducible]

instance Typology.Coordination.instDecidableEqAndWithStatus : DecidableEq AndWithStatus

Equations

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

def Typology.Coordination.instBEqAndWithStatus.beq : AndWithStatus → AndWithStatus → Bool

Equations

• Typology.Coordination.instBEqAndWithStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Typology.Coordination.instBEqAndWithStatus : BEq AndWithStatus

Equations

• Typology.Coordination.instBEqAndWithStatus = { beq := Typology.Coordination.instBEqAndWithStatus.beq }

def Typology.Coordination.instReprAndWithStatus.repr : AndWithStatus → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instReprAndWithStatus : Repr AndWithStatus

Equations

• Typology.Coordination.instReprAndWithStatus = { reprPrec := Typology.Coordination.instReprAndWithStatus.repr }

@[reducible, inline]

abbrev Typology.Coordination.ConjQuantRelation : Type

WALS Ch 56: conjunction-quantifier relation.

Equations

• Typology.Coordination.ConjQuantRelation = Data.WALS.F56A.ConjunctionsAndUniversalQuantifiers

@[reducible, inline]

abbrev Typology.Coordination.ConjComitativeRelation : Type

WALS Ch 63: noun-phrase conjunction (and-vs-with).

Equations

• Typology.Coordination.ConjComitativeRelation = Data.WALS.F63A.NounPhraseConjunction

@[reducible, inline]

abbrev Typology.Coordination.NomVerbalConjRelation : Type

WALS Ch 64: nominal-vs-verbal conjunction.

Equations

• Typology.Coordination.NomVerbalConjRelation = Data.WALS.F64A.NominalAndVerbalConjunction

def Typology.Coordination.ConjComitativeRelation.toAndWithStatus : ConjComitativeRelation → AndWithStatus

Derive AND/WITH status from the conjunction-comitative relation (@cite{stassen-2000}'s diagnostic).

Equations

• Typology.Coordination.ConjComitativeRelation.toAndWithStatus Data.WALS.F63A.NounPhraseConjunction.andDifferentFromWith = Typology.Coordination.AndWithStatus.andLang
• Typology.Coordination.ConjComitativeRelation.toAndWithStatus Data.WALS.F63A.NounPhraseConjunction.andIdenticalToWith = Typology.Coordination.AndWithStatus.withLang

structure Typology.Coordination.SourcedEntry : Type

A coordination entry annotated with its diachronic source. Wraps CoordEntry (from Features.Coordination) with typological metadata. For languages with Fragment files, entry references the Fragment entry directly — no data duplication.

• entry : Features.Coordination.CoordEntry

  The coordination morpheme entry.

• source : Option DiachronicSource

  Likely diachronic source, if known.

@[implicit_reducible]

instance Typology.Coordination.instReprSourcedEntry : Repr SourcedEntry

Equations

• Typology.Coordination.instReprSourcedEntry = { reprPrec := Typology.Coordination.instReprSourcedEntry.repr }

def Typology.Coordination.instReprSourcedEntry.repr : SourcedEntry → Nat → Std.Format

Equations

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

structure Typology.Coordination.ConjunctionSystem : Type

A language's conjunction system (M&S framework).

• language : String
• morphemes : List SourcedEntry

  Available conjunction morphemes (sourced entries).

• strategies : List Features.Coordination.ConjunctionStrategy

  Which conjunction strategies are available (M&S classification).

• patterns : List CoordPattern

  Structural patterns attested (Haspelmath classification).

• iso : String

  ISO 639-3 code.

def Typology.Coordination.instReprConjunctionSystem.repr : ConjunctionSystem → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instReprConjunctionSystem : Repr ConjunctionSystem

Equations

• Typology.Coordination.instReprConjunctionSystem = { reprPrec := Typology.Coordination.instReprConjunctionSystem.repr }

structure Typology.Coordination.CoordinationProfile : Type

A language's coordination typology profile across WALS Chs 56, 63, 64.

• language : String
• iso : String
• family : String
• conjQuant : Option ConjQuantRelation

  Ch 56: conjunction-vs-universal-quantifier.

• conjComitative : Option ConjComitativeRelation

  Ch 63: "and" vs "with".

• nomVerbalConj : Option NomVerbalConjRelation

  Ch 64: NP-vs-VP conjunction.

• walsNotes : String

def Typology.Coordination.instReprCoordinationProfile.repr : CoordinationProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Coordination.instReprCoordinationProfile : Repr CoordinationProfile

Equations

• Typology.Coordination.instReprCoordinationProfile = { reprPrec := Typology.Coordination.instReprCoordinationProfile.repr }

def Typology.Coordination.CoordinationProfile.andWithStatus (p : CoordinationProfile) : Option AndWithStatus

Derive AND/WITH status for a coordination profile from its Ch 63 value.

Equations

• p.andWithStatus = Option.map (fun (x : Typology.Coordination.ConjComitativeRelation) => x.toAndWithStatus) p.conjComitative

def Typology.Coordination.ConjunctionSystem.hasStrategy (sys : ConjunctionSystem) (s : Features.Coordination.ConjunctionStrategy) : Bool

Does a language have a given strategy?

Equations

• sys.hasStrategy s = sys.strategies.contains s

def Typology.Coordination.ConjunctionSystem.muIsAdditive (sys : ConjunctionSystem) : Bool

Does a language have a MU morpheme that also serves as additive?

Equations

• sys.muIsAdditive = sys.morphemes.any fun (m : Typology.Coordination.SourcedEntry) => m.entry.role == Features.Coordination.CoordRole.mu && m.entry.alsoAdditive

def Typology.Coordination.ConjunctionSystem.hasSource (sys : ConjunctionSystem) (s : DiachronicSource) : Bool

Does a language have a morpheme with a given diachronic source?

Equations

• sys.hasSource s = sys.morphemes.any fun (m : Typology.Coordination.SourcedEntry) => m.source == some s

def Typology.Coordination.ConjunctionSystem.hasMonosyndetic (sys : ConjunctionSystem) : Bool

Does a language have at least one monosyndetic pattern?

Equations

• sys.hasMonosyndetic = sys.patterns.any fun (p : Typology.Coordination.CoordPattern) => p.syndesis == Typology.Coordination.Syndesis.monosyndetic

def Typology.Coordination.ConjunctionSystem.hasBisyndetic (sys : ConjunctionSystem) : Bool

Does a language have at least one bisyndetic pattern?

Equations

• sys.hasBisyndetic = sys.patterns.any fun (p : Typology.Coordination.CoordPattern) => p.syndesis == Typology.Coordination.Syndesis.bisyndetic

def Typology.Coordination.ConjunctionSystem.muBoundness (sys : ConjunctionSystem) : Option Features.Coordination.Boundness

Get the boundness of a language's MU particle, if it has one.

Equations

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

theorem Typology.Coordination.and_languages_majority : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F63A.NounPhraseConjunction) => x.value == Data.WALS.F63A.NounPhraseConjunction.andDifferentFromWith) Typology.Coordination.ch63✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F63A.NounPhraseConjunction) => x.value == Data.WALS.F63A.NounPhraseConjunction.andIdenticalToWith) Typology.Coordination.ch63✝).length

F63A: "and" being different from "with" is the majority pattern (131 > 103).

theorem Typology.Coordination.comitative_source_substantial_minority : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F63A.NounPhraseConjunction) => x.value == Data.WALS.F63A.NounPhraseConjunction.andIdenticalToWith) Typology.Coordination.ch63✝).length * 2 < Typology.Coordination.ch63✝.length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F63A.NounPhraseConjunction) => x.value == Data.WALS.F63A.NounPhraseConjunction.andIdenticalToWith) Typology.Coordination.ch63✝).length * 3 > Typology.Coordination.ch63✝.length

F63A: languages where "and" = "with" form a substantial minority (103/234, 44%) — comitative-to-coordinator grammaticalization is still transparent in many languages, but the AND-pattern dominates.

theorem Typology.Coordination.nom_verbal_identity_is_majority : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F64A.NominalAndVerbalConjunction) => x.value == Data.WALS.F64A.NominalAndVerbalConjunction.identity) Typology.Coordination.ch64✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F64A.NominalAndVerbalConjunction) => x.value == Data.WALS.F64A.NominalAndVerbalConjunction.differentiation) Typology.Coordination.ch64✝).length ∧ (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F64A.NominalAndVerbalConjunction) => x.value == Data.WALS.F64A.NominalAndVerbalConjunction.identity) Typology.Coordination.ch64✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F64A.NominalAndVerbalConjunction) => x.value == Data.WALS.F64A.NominalAndVerbalConjunction.bothExpressedByJuxtaposition) Typology.Coordination.ch64✝).length

F64A: identity of NP and VP conjunction is the majority pattern (161/301).

theorem Typology.Coordination.juxtaposition_rare : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F64A.NominalAndVerbalConjunction) => x.value == Data.WALS.F64A.NominalAndVerbalConjunction.bothExpressedByJuxtaposition) Typology.Coordination.ch64✝).length * 20 < Typology.Coordination.ch64✝.length

F64A: juxtaposition for both NP and VP conjunction is rare (15/301 = 5%).