Haspelmath (2007): Coordination

Haspelmath's chapter classifies coordinate constructions by where their coordinators go. A binary pattern, (17), is the pair of the markings of the two coordinands. The two diachronic sources of conjunction, §1.2, a comitative modifier 'A with B' and an additive focus particle 'A, also B', yield patterns from the order of their parts, and no source whose modifier order and adposition order are harmonic yields co-A B, the pattern no language attests. Table 1.1 derives the patterns of multiple coordination from the binary one.

The chapter's examples are the rows of Data/Examples/Haspelmath2007.json. Each construction is analysed by its coordinators, one coordinator or a correlative pair. Of the binary examples, the chapter calls emphatic exactly the correlative ones, and the bisyndetic ones that are not correlative are postpositive, §1.3 and §2.1. The file also classifies the correlatives of (45) by their forms and states Payne's implicational sequence of coordinand types, §3, with the counterexample from Tinrin the chapter records.

Main statements

• coAB_unsourced: no harmonic source yields co-A B.
• emphatic_iff_correlative: the emphatic constructions are the correlative ones.
• normal_bisyndetic_postpositive: normal bisyndesis is postpositive.

Implementation notes

• A construction's coordinators are its language's Fragment entries where they exist, and are written inline otherwise. A pair of coordinators is a Coordinator.Correlative; the single coordinator of a mixed pair, (27) and (28), is taken to be its second, as in (45b).
• The rows record emphasis only where the chapter states it. Keeping every coordinator of a multiple coordination is emphatic in European languages, p. 12, which is not emphasis by correlatives, so emphatic_iff_correlative is about binary coordination.
• Classical Tibetan -daŋ and Turkish -le, which the chapter says "come from a former case-marker" without naming the case, have no source in the rows; the Fragments record, after Beyer and after Göksel and Kerslake, that both are still comitative markers (former_case_marker_isAlsoComitative).

References

• [Has07]
• [Bey92]
• [Dry92]
• [GK05]
• [Gre63]
• [Sta00]

Binary patterns, (17)

inductive Haspelmath2007.Slot : Type

A coordinand is bare or carries a prepositive coordinator, co-A, or a postpositive one, A-co.

• bare : Slot
• pre : Slot
• post : Slot

@[instance_reducible]

instance Haspelmath2007.instDecidableEqSlot : DecidableEq Slot

Equations

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

@[instance_reducible]

instance Haspelmath2007.instReprSlot : Repr Slot

Equations

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

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

Equations

• Haspelmath2007.instReprSlot.repr Haspelmath2007.Slot.bare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Haspelmath2007.Slot.bare")).group prec✝
• Haspelmath2007.instReprSlot.repr Haspelmath2007.Slot.pre prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Haspelmath2007.Slot.pre")).group prec✝
• Haspelmath2007.instReprSlot.repr Haspelmath2007.Slot.post prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Haspelmath2007.Slot.post")).group prec✝

def Haspelmath2007.Slot.ofSide : Morphology.Morph.Side → Slot

The marking of a coordinand by a coordinator on the given side of it.

Equations

• Haspelmath2007.Slot.ofSide Morphology.Morph.Side.before = Haspelmath2007.Slot.pre
• Haspelmath2007.Slot.ofSide Morphology.Morph.Side.after = Haspelmath2007.Slot.post

@[reducible, inline]

abbrev Haspelmath2007.Pattern : Type

A binary pattern, (17), is the pair of the markings of the two coordinands, so that A co-B is (.bare, .pre) and A-co B-co is (.post, .post).

Equations

• Haspelmath2007.Pattern = (Haspelmath2007.Slot × Haspelmath2007.Slot)

def Haspelmath2007.Pattern.syndesis (p : Pattern) : ℕ

The syndesis of a pattern is its number of coordinators, none in asyndetic, one in monosyndetic and two in bisyndetic coordination, §1.

Equations

• p.syndesis = List.countP (fun (x : Haspelmath2007.Slot) => decide (x ≠ Haspelmath2007.Slot.bare)) [p.1, p.2]

theorem Haspelmath2007.monosyndetic_bare (p : Pattern) (h : p.syndesis = 1) : p.1 = Slot.bare ∨ p.2 = Slot.bare

Monosyndetic coordination is universally asymmetric, §1.2, with one coordinand bare.

Diachronic sources, §1.2

inductive Haspelmath2007.DiachronicSource : Type

A conjunctive coordinator comes from a comitative modifier 'A with B', given by the side of B its adposition goes on and the side of the noun the modifier goes on, or from an additive focus particle 'A, also B', given by the side of B it goes on, §1.2 and §5.1.

• comitative (adposition modifier : Morphology.Morph.Side) : DiachronicSource
• focusParticle (particle : Morphology.Morph.Side) : DiachronicSource

@[instance_reducible]

instance Haspelmath2007.instDecidableEqDiachronicSource : DecidableEq DiachronicSource

Equations

• Haspelmath2007.instDecidableEqDiachronicSource = Haspelmath2007.instDecidableEqDiachronicSource.decEq

def Haspelmath2007.instDecidableEqDiachronicSource.decEq (x✝ x✝¹ : DiachronicSource) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Haspelmath2007.instDecidableEqDiachronicSource.decEq (Haspelmath2007.DiachronicSource.comitative adposition modifier) (Haspelmath2007.DiachronicSource.focusParticle particle) = isFalse ⋯
• Haspelmath2007.instDecidableEqDiachronicSource.decEq (Haspelmath2007.DiachronicSource.focusParticle particle) (Haspelmath2007.DiachronicSource.comitative adposition modifier) = isFalse ⋯

def Haspelmath2007.instReprDiachronicSource.repr : DiachronicSource → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2007.instReprDiachronicSource : Repr DiachronicSource

Equations

• Haspelmath2007.instReprDiachronicSource = { reprPrec := Haspelmath2007.instReprDiachronicSource.repr }

def Haspelmath2007.DiachronicSource.pattern : DiachronicSource → Pattern

The binary pattern of a source construction, §1.2. The comitative phrase is the first coordinand when modifiers precede the noun and the second when they follow it, marked on the side of its adposition, and the focus particle marks the second conjunct on its own side, so that 'A, B too' gives A B-co and 'A, also B' gives A co-B.

Equations

• (Haspelmath2007.DiachronicSource.comitative adposition Morphology.Morph.Side.before).pattern = (Haspelmath2007.Slot.ofSide adposition, Haspelmath2007.Slot.bare)
• (Haspelmath2007.DiachronicSource.comitative adposition Morphology.Morph.Side.after).pattern = (Haspelmath2007.Slot.bare, Haspelmath2007.Slot.ofSide adposition)
• (Haspelmath2007.DiachronicSource.focusParticle particle).pattern = (Haspelmath2007.Slot.bare, Haspelmath2007.Slot.ofSide particle)

def Haspelmath2007.DiachronicSource.Harmonic : DiachronicSource → Prop

A comitative source is harmonic when modifiers precede the noun in a language with postpositions or follow it in one with prepositions, the orders that go together [Gre63] [Dry92]; a focus particle is not a modifier.

Equations

• (Haspelmath2007.DiachronicSource.comitative adposition modifier).Harmonic = (adposition ≠ modifier)
• (Haspelmath2007.DiachronicSource.focusParticle particle).Harmonic = True

@[instance_reducible]

instance Haspelmath2007.DiachronicSource.instDecidablePredHarmonic : DecidablePred Harmonic

Equations

• (Haspelmath2007.DiachronicSource.comitative adposition modifier).instDecidablePredHarmonic = { decide := !decide (adposition = modifier), reflects_decide := ⋯ }
• (Haspelmath2007.DiachronicSource.focusParticle particle).instDecidablePredHarmonic = { decide := true, reflects_decide := ⋯ }

theorem Haspelmath2007.DiachronicSource.pattern_eq_coAB_iff {s : DiachronicSource} : s.pattern = (Slot.pre, Slot.bare) ↔ s = comitative Morphology.Morph.Side.before Morphology.Morph.Side.before

The only source with the pattern co-A B is a prepositional comitative phrase before its noun.

theorem Haspelmath2007.DiachronicSource.coAB_unsourced {s : DiachronicSource} (h : s.Harmonic) : s.pattern ≠ (Slot.pre, Slot.bare)

No harmonic source has the pattern co-A B, which §1.2 offers as the explanation of its absence from [Sta00]'s sample of 260 languages.

Multiple coordination, Table 1.1

def Haspelmath2007.full (p : Pattern) (n : ℕ) : Option (List Slot)

The full n-ary pattern of a binary one, §1.4. A bisyndetic pattern of one shape marks every coordinand, and a monosyndetic pattern leaves bare the coordinand bare in the binary construction and marks every other one as its marked coordinand is marked; the mixed patterns have no full pattern in the chapter.

Equations

• Haspelmath2007.full (Haspelmath2007.Slot.bare, s) n = some (Haspelmath2007.Slot.bare :: List.replicate (n - 1) s)
• Haspelmath2007.full (s, Haspelmath2007.Slot.bare) n = some (List.replicate (n - 1) s ++ [Haspelmath2007.Slot.bare])
• Haspelmath2007.full (s, t) n = if s = t then some (List.replicate n s) else none

def Haspelmath2007.keepLastRev : List Slot → List Slot

Keep the last coordinator of a construction read from the end.

Equations

• Haspelmath2007.keepLastRev [] = []
• Haspelmath2007.keepLastRev (Haspelmath2007.Slot.bare :: l) = Haspelmath2007.Slot.bare :: Haspelmath2007.keepLastRev l
• Haspelmath2007.keepLastRev (s :: l) = s :: List.map (fun (x : Haspelmath2007.Slot) => Haspelmath2007.Slot.bare) l

def Haspelmath2007.omitted (p : Pattern) (n : ℕ) : Option (List Slot)

Coordinator omission, §1.4, eliminates all but the last coordinator.

Equations

• Haspelmath2007.omitted p n = Option.map (fun (l : List Haspelmath2007.Slot) => (Haspelmath2007.keepLastRev l.reverse).reverse) (Haspelmath2007.full p n)

theorem Haspelmath2007.table_1_1 : full (Slot.bare, Slot.pre) 4 = some [Slot.bare, Slot.pre, Slot.pre, Slot.pre] ∧ omitted (Slot.bare, Slot.pre) 4 = some [Slot.bare, Slot.bare, Slot.bare, Slot.pre] ∧ full (Slot.post, Slot.bare) 4 = some [Slot.post, Slot.post, Slot.post, Slot.bare] ∧ omitted (Slot.post, Slot.bare) 4 = some [Slot.bare, Slot.bare, Slot.post, Slot.bare] ∧ full (Slot.post, Slot.post) 4 = some [Slot.post, Slot.post, Slot.post, Slot.post] ∧ omitted (Slot.post, Slot.post) 4 = some [Slot.bare, Slot.bare, Slot.bare, Slot.post] ∧ full (Slot.pre, Slot.pre) 4 = some [Slot.pre, Slot.pre, Slot.pre, Slot.pre] ∧ omitted (Slot.pre, Slot.pre) 4 = some [Slot.bare, Slot.bare, Slot.bare, Slot.pre] ∧ full (Slot.bare, Slot.post) 4 = some [Slot.bare, Slot.post, Slot.post, Slot.post] ∧ omitted (Slot.bare, Slot.post) 4 = some [Slot.bare, Slot.bare, Slot.bare, Slot.post]

Table 1.1 for four coordinands gives the full pattern and the pattern with coordinator omission of each of the five binary patterns it lists.

The chapter's examples

def Haspelmath2007.Pattern.labels : List (String × Pattern)

The labels of the patterns in the rows, A co-B as a_co_b.

Equations

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

def Haspelmath2007.pattern? (d : Datum) : Option Pattern

The binary pattern of a row, for a multiple coordination that of its binary construction.

Equations

• Haspelmath2007.pattern? d = d.parse? "pattern" Haspelmath2007.Pattern.labels

def Haspelmath2007.emphatic? (d : Datum) : Option Bool

Whether the chapter presents a row as emphatic, where it says.

Equations

• Haspelmath2007.emphatic? d = d.parse? "emphatic" [("yes", true), ("no", false)]

theorem Haspelmath2007.pattern?_isSome (d : Datum) : d ∈ Examples.all → (d.feature? "pattern").isSome = true → (pattern? d).isSome = true

Every pattern label of the rows is one of (17).

theorem Haspelmath2007.pattern?_ne_coAB (d : Datum) : d ∈ Examples.all → pattern? d ≠ some (Slot.pre, Slot.bare)

The pattern co-A B is absent from the chapter's examples, as from Stassen's sample.

theorem Haspelmath2007.prepositive_bisyndetic_emphatic (d : Datum) : d ∈ Examples.all → pattern? d = some (Slot.pre, Slot.pre) → emphatic? d = some true

Prepositive bisyndesis occurs only as emphatic coordination, §1.3 after [Sta00].

theorem Haspelmath2007.comitative_patterns (d : Datum) : d ∈ Examples.all → d.feature? "source" = some "comitative" → ∀ p ∈ pattern? d, (∃ (a : Morphology.Morph.Side) (m : Morphology.Morph.Side), (DiachronicSource.comitative a m).Harmonic ∧ (DiachronicSource.comitative a m).pattern = p) ∨ d.source.paperLabel = "(85b)" ∧ p = (Slot.post, Slot.post) ∨ d.source.paperLabel ∈ ["(81)", "(86)"] ∧ p = (DiachronicSource.comitative Morphology.Morph.Side.after Morphology.Morph.Side.after).pattern

The comitative-sourced coordinators of the rows have the patterns of a harmonic comitative source, A co-B and A-co B, except Tauya -sou, (85b), doubled on both conjuncts as §5.1 describes, and Amele ca, (81), and Huallaga Quechua -wan, (86), postpositive on the second conjunct, A B-co, the pattern of a postpositional comitative after its noun.

The coordinators of the constructions

inductive Haspelmath2007.Coordinators : Type

A construction has one coordinator, on each coordinand its pattern marks, or a pair of correlative coordinators.

• plain (c : Coordinator) : Coordinators
• correlative (k : Coordinator.Correlative) : Coordinators

def Haspelmath2007.instReprCoordinators.repr : Coordinators → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Haspelmath2007.instReprCoordinators : Repr Coordinators

Equations

• Haspelmath2007.instReprCoordinators = { reprPrec := Haspelmath2007.instReprCoordinators.repr }

def Haspelmath2007.Coordinators.IsCorrelative : Coordinators → Prop

The coordinators are a correlative pair.

Equations

• (Haspelmath2007.Coordinators.plain c).IsCorrelative = False
• (Haspelmath2007.Coordinators.correlative k).IsCorrelative = True

@[instance_reducible]

instance Haspelmath2007.instDecidablePredCoordinatorsIsCorrelative : DecidablePred Coordinators.IsCorrelative

Equations

• Haspelmath2007.instDecidablePredCoordinatorsIsCorrelative (Haspelmath2007.Coordinators.plain c) = { decide := false, reflects_decide := ⋯ }
• Haspelmath2007.instDecidablePredCoordinatorsIsCorrelative (Haspelmath2007.Coordinators.correlative k) = { decide := true, reflects_decide := ⋯ }

def Haspelmath2007.Coordinators.marking : Coordinators → Pattern → List (Slot × Morphology.Morph)

The forms on the coordinands a pattern marks, each with its marking.

Equations

• (Haspelmath2007.Coordinators.plain c).marking (s, t) = List.filter (fun (x : Haspelmath2007.Slot × Morphology.Morph) => decide (x.1 ≠ Haspelmath2007.Slot.bare)) [(s, c.morph), (t, c.morph)]
• (Haspelmath2007.Coordinators.correlative k).marking (s, t) = List.map (fun (x : Morphology.Morph) => (s, x)) k.first ++ List.map (fun (x : Morphology.Morph) => (t, x)) k.second

structure Haspelmath2007.Attestation : Type

A coordinate construction the chapter cites, a row with its coordinators.

• datum : Datum
• coordinators : Coordinators

def Haspelmath2007.co (morph : Morphology.Morph) : Coordinator

A conjunctive coordinator with no Fragment entry.

Equations

• Haspelmath2007.co morph = { morph := morph, gloss := "and", role := Coordinator.Role.conjunctive }

def Haspelmath2007.dis (form : String) : Coordinator

A disjunctive coordinator with no Fragment entry.

Equations

• Haspelmath2007.dis form = { morph := Morphology.Morph.free form, gloss := "or", role := Coordinator.Role.disjunctive }

def Haspelmath2007.attestations : List Attestation

The constructions of the rows with a coordinator.

Equations

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

theorem Haspelmath2007.attestations_label : List.map (fun (x : Attestation) => x.datum.source.paperLabel) attestations = List.map (fun (x : Datum) => x.source.paperLabel) (List.filter (fun (d : Datum) => Option.any (fun (x : Pattern) => decide (x.syndesis ≠ 0)) (pattern? d)) Examples.all)

The attestations are the rows with a coordinator, in order.

theorem Haspelmath2007.marking_agrees_with_side (a : Attestation) : a ∈ attestations → ∀ p ∈ pattern? a.datum, ∀ m ∈ a.coordinators.marking p, ∀ s ∈ m.2.kind.side?, m.1 = Slot.ofSide s

The patterns agree with the morphology of the coordinators, since a coordinator that attaches on a side of its host marks its coordinand on that side.

theorem Haspelmath2007.emphatic_iff_correlative (a : Attestation) : a ∈ attestations → a.datum.nat? "coordinands" = none → ∀ e ∈ emphatic? a.datum, e = true ↔ a.coordinators.IsCorrelative

The chapter presents a binary coordination as emphatic exactly when its coordinators are correlative, §2.1.

theorem Haspelmath2007.normal_bisyndetic_postpositive (a : Attestation) : a ∈ attestations → ¬a.coordinators.IsCorrelative → ∀ p ∈ pattern? a.datum, p.syndesis = 2 → p = (Slot.post, Slot.post)

Normal bisyndesis is postpositive with one coordinator, §2.1 and §1.3. A construction whose coordinators are not correlative and mark both coordinands marks them after them, so that by emphatic_iff_correlative prepositive bisyndesis is emphatic, as [Sta00] finds.

theorem Haspelmath2007.comitative_source_isAlsoComitative : Hausa.Coordination.da.IsAlsoComitative Hausa.Adpositions.da.morphs Hausa.Adpositions.da.functions ∧ Lango.Coordination.kede.IsAlsoComitative Lango.Adpositions.kede.morphs Lango.Adpositions.kede.functions

The comitative-sourced coordinators with Fragment entries, Hausa dà and Lango kèdè, are still the comitative prepositions of their languages.

theorem Haspelmath2007.former_case_marker_isAlsoComitative : ClassicalTibetan.Coordination.dang.IsAlsoComitative ClassicalTibetan.Case.accompaniment.exponents ClassicalTibetan.Case.accompaniment.functions ∧ Turkish.Coordination.ile.IsAlsoComitative Turkish.Adpositions.ile.morphs Turkish.Adpositions.ile.functions

Classical Tibetan -daŋ and Turkish -le, which come from a former case-marker, (41), are still comitative markers, the accompaniment role particle and the comitative postposition.

Emphatic correlatives, (45)

inductive Haspelmath2007.CorrelativeShape : Type

A pair of correlative coordinators, (45), has both identical to the single coordinator, only its second identical to it, its two identical to each other but not to it, or all three different.

• bothSingle : CorrelativeShape
• secondSingle : CorrelativeShape
• sameNotSingle : CorrelativeShape
• allDifferent : CorrelativeShape

@[instance_reducible]

instance Haspelmath2007.instDecidableEqCorrelativeShape : DecidableEq CorrelativeShape

Equations

• Haspelmath2007.instDecidableEqCorrelativeShape x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Haspelmath2007.instReprCorrelativeShape : Repr CorrelativeShape

Equations

• Haspelmath2007.instReprCorrelativeShape = { reprPrec := Haspelmath2007.instReprCorrelativeShape.repr }

def Haspelmath2007.instReprCorrelativeShape.repr : CorrelativeShape → ℕ → Std.Format

Equations

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

def Haspelmath2007.CorrelativeShape.classify (c : Coordinator.Correlative) : CorrelativeShape

The shape of a correlative pair, read off the forms.

Equations

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

def Haspelmath2007.correlatives : List (String × Coordinator.Correlative × CorrelativeShape)

The rows of (45), each with its language and the letter the chapter files it under; Polish tak (i) is recorded without its optional i.

Equations

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

theorem Haspelmath2007.correlatives_classified (r : String × Coordinator.Correlative × CorrelativeShape) : r ∈ correlatives → CorrelativeShape.classify r.2.1 = r.2.2

The letters of (45) are the shapes the forms give.

theorem Haspelmath2007.correlatives_conjunctive_or_disjunctive (r : String × Coordinator.Correlative × CorrelativeShape) : r ∈ correlatives → r.2.1.single.role = Coordinator.Role.conjunctive ∨ r.2.1.single.role = Coordinator.Role.disjunctive

The correlative coordinators of (45) emphasize a conjunction or a disjunction.

theorem Haspelmath2007.yoruba_bothSingle : CorrelativeShape.classify Yoruba.Coordination.atiAti = CorrelativeShape.bothSingle

Yoruba àtí … àtí, the emphatic construction of the attestations, has the shape of (45a).

Payne's implicational sequence, §3

inductive Haspelmath2007.CoordinandType : Type

The coordinand types of the sequence S – VP – AP – PP – NP.

• s : CoordinandType
• vp : CoordinandType
• ap : CoordinandType
• pp : CoordinandType
• np : CoordinandType

@[instance_reducible]

instance Haspelmath2007.instDecidableEqCoordinandType : DecidableEq CoordinandType

Equations

• Haspelmath2007.instDecidableEqCoordinandType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Haspelmath2007.instFintypeCoordinandType : Fintype CoordinandType

Equations

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

@[instance_reducible]

instance Haspelmath2007.instReprCoordinandType : Repr CoordinandType

Equations

• Haspelmath2007.instReprCoordinandType = { reprPrec := Haspelmath2007.instReprCoordinandType.repr }

def Haspelmath2007.instReprCoordinandType.repr : CoordinandType → ℕ → Std.Format

Equations

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

def Haspelmath2007.CoordinandType.rank : CoordinandType → ℕ

Position on the sequence.

Equations

• Haspelmath2007.CoordinandType.s.rank = 0
• Haspelmath2007.CoordinandType.vp.rank = 1
• Haspelmath2007.CoordinandType.ap.rank = 2
• Haspelmath2007.CoordinandType.pp.rank = 3
• Haspelmath2007.CoordinandType.np.rank = 4

def Haspelmath2007.Contiguous (r : Finset CoordinandType) : Prop

A coordinator's range is a contiguous stretch of the sequence.

Equations

• Haspelmath2007.Contiguous r = ∀ a ∈ r, ∀ b ∈ r, ∀ (c : Haspelmath2007.CoordinandType), a.rank ≤ c.rank → c.rank ≤ b.rank → c ∈ r

@[instance_reducible]

instance Haspelmath2007.instDecidablePredFinsetCoordinandTypeContiguous : DecidablePred Contiguous

Equations

• Haspelmath2007.instDecidablePredFinsetCoordinandTypeContiguous x✝ = id inferInstance

theorem Haspelmath2007.np_event_contiguous : Contiguous {CoordinandType.np} ∧ Contiguous {CoordinandType.vp, CoordinandType.s}

The NP against event split of Korean -(k)wa and -ko, (57), and Turkish -la and -ıp, (58): two contiguous ranges.

theorem Haspelmath2007.tinrin_not_contiguous : ¬Contiguous {CoordinandType.s, CoordinandType.np}

Tinrin mê coordinates sentences and NPs but not VPs, the counterexample to the sequence the chapter notes.