Clause chaining

[SA25]

Typology of clause chaining: multi-clause constructions in which one or more medial clauses (dependent, morphologically reduced) combine with a single final clause (independent, fully inflected) that supplies tense, mood, and often agreement for the whole chain. Chaining is the prototypical cosubordinate combining scheme (Clause.CombiningScheme): the medial clause is dependent but not embedded ([GFvV84]; [Lon07]). Anchors: [SA25] and [dV25], with per-language bundles and generalizations in Studies/SarvasyAikhenvald2025.lean.

Main definitions

• Clause.CombiningScheme (+ Embedded, Dependent) — the [scancarelli-2003] combination schemes
• ClauseStatus, ChainDirection — medial/final and chain order
• CategoryRetention, MedialMorphProfile — the medial verb's per-category finiteness profile
• SRSystem, SRTarget, SRMarkedness — switch-reference
• InterclauseRelation — marked interclausal semantic relations
• BridgingType — discourse bridging across chain boundaries
• System — a language's clause-chaining system; per-language instances live in Studies/SarvasyAikhenvald2025.lean

Combining schemes

inductive Clause.CombiningScheme : Type

How a clause combines with its neighbors into a larger structure ([scancarelli-2003]): relatively independent conjuncts, dependence on a main clause, chained cosubordination (dependent but not embedded, [GFvV84]), or serialization with the relationship left unmarked. Languages differ in which schemes they use at all.

• coordinate : CombiningScheme
• subordinate : CombiningScheme
• cosubordinate : CombiningScheme
• serial : CombiningScheme

@[instance_reducible]

instance Clause.instDecidableEqCombiningScheme : DecidableEq CombiningScheme

Equations

• Clause.instDecidableEqCombiningScheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.instReprCombiningScheme.repr : CombiningScheme → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.instReprCombiningScheme : Repr CombiningScheme

Equations

• Clause.instReprCombiningScheme = { reprPrec := Clause.instReprCombiningScheme.repr }

def Clause.CombiningScheme.Embedded (s : CombiningScheme) : Prop

The dependent clause is embedded as a syntactic constituent of the other.

Equations

• s.Embedded = (s = Clause.CombiningScheme.subordinate)

@[instance_reducible]

instance Clause.CombiningScheme.instDecidablePredEmbedded : DecidablePred Embedded

Equations

• x✝.instDecidablePredEmbedded = Clause.CombiningScheme.instDecidablePredEmbedded._aux_1 x✝

def Clause.CombiningScheme.Dependent (s : CombiningScheme) : Prop

The dependent clause is morphologically reduced (cannot stand alone).

Equations

• s.Dependent = (s = Clause.CombiningScheme.subordinate ∨ s = Clause.CombiningScheme.cosubordinate)

@[instance_reducible]

instance Clause.CombiningScheme.instDecidablePredDependent : DecidablePred Dependent

Equations

• x✝.instDecidablePredDependent = Clause.CombiningScheme.instDecidablePredDependent._aux_1 x✝

def Clause.Chaining.scheme : CombiningScheme

Clause chaining is cosubordination — dependent but not embedded ([GFvV84]).

Equations

• Clause.Chaining.scheme = Clause.CombiningScheme.cosubordinate

Clause status and chain direction

inductive Clause.Chaining.ClauseStatus : Type

Structural status of a clause within a chain.

• medial : ClauseStatus

  Dependent clause with reduced morphology. Typically carries converbal or participial marking (UD VerbForm.Conv); may encode switch-reference and interclausal relations but lacks full tense/agreement.

• final : ClauseStatus

  Independent clause with full inflection. Supplies tense, mood, and often agreement for the entire chain; exactly one per chain.

@[instance_reducible]

instance Clause.Chaining.instDecidableEqClauseStatus : DecidableEq ClauseStatus

Equations

• Clause.Chaining.instDecidableEqClauseStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.Chaining.instReprClauseStatus.repr : ClauseStatus → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprClauseStatus : Repr ClauseStatus

Equations

• Clause.Chaining.instReprClauseStatus = { reprPrec := Clause.Chaining.instReprClauseStatus.repr }

@[instance_reducible]

instance Clause.Chaining.instInhabitedClauseStatus : Inhabited ClauseStatus

Equations

• Clause.Chaining.instInhabitedClauseStatus = { default := Clause.Chaining.instInhabitedClauseStatus.default }

inductive Clause.Chaining.ChainDirection : Type

Linear order of medial and final clauses ([SA25] §1.2).

• medialFinal : ChainDirection

  Medial clauses precede the final clause — by far the most common, strongly correlated with verb-final word order (Nungon, Turkish, Korean, Manambu, Ku Waru).

• initialMedial : ChainDirection

  An initial independent clause precedes medial dependent clauses — rare, attested in some verb-initial languages (Barai).

@[instance_reducible]

instance Clause.Chaining.instDecidableEqChainDirection : DecidableEq ChainDirection

Equations

• Clause.Chaining.instDecidableEqChainDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.Chaining.instReprChainDirection.repr : ChainDirection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprChainDirection : Repr ChainDirection

Equations

• Clause.Chaining.instReprChainDirection = { reprPrec := Clause.Chaining.instReprChainDirection.repr }

@[instance_reducible]

instance Clause.Chaining.instInhabitedChainDirection : Inhabited ChainDirection

Equations

• Clause.Chaining.instInhabitedChainDirection = { default := Clause.Chaining.instInhabitedChainDirection.default }

def Clause.Chaining.ChainDirection.predictedHeadDirection : ChainDirection → HeadDirection

Predicted head direction: the final verb determines the chain's TAM and patterns as its head, so chain direction mirrors the language's head direction ([Dry92]-style correlation; [SA25] §1.2).

Equations

• Clause.Chaining.ChainDirection.medialFinal.predictedHeadDirection = HeadDirection.headFinal
• Clause.Chaining.ChainDirection.initialMedial.predictedHeadDirection = HeadDirection.headInitial

Medial-verb morphology

inductive Clause.Chaining.CategoryRetention : Type

How much of a morphological category a medial verb retains relative to independent verbs — the three-point scale absent < restricted < full ([SA25] §§1.3–1.5; [dV25] §2).

• absent : CategoryRetention

  Unmarked on medial verbs; the value is inherited from the final verb (Nungon medial verbs lack tense entirely).

• restricted : CategoryRetention

  Fewer values than independent verbs (e.g. binary realis/irrealis rather than a full mood paradigm).

• full : CategoryRetention

  The same range of values as independent verbs (Turkish converbs retain aspect).

@[instance_reducible]

instance Clause.Chaining.instDecidableEqCategoryRetention : DecidableEq CategoryRetention

Equations

• Clause.Chaining.instDecidableEqCategoryRetention x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.Chaining.instReprCategoryRetention.repr : CategoryRetention → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprCategoryRetention : Repr CategoryRetention

Equations

• Clause.Chaining.instReprCategoryRetention = { reprPrec := Clause.Chaining.instReprCategoryRetention.repr }

@[instance_reducible]

instance Clause.Chaining.instInhabitedCategoryRetention : Inhabited CategoryRetention

Equations

• Clause.Chaining.instInhabitedCategoryRetention = { default := Clause.Chaining.instInhabitedCategoryRetention.default }

def Clause.Chaining.CategoryRetention.rank : CategoryRetention → ℕ

Position on the retention scale.

Equations

• Clause.Chaining.CategoryRetention.absent.rank = 0
• Clause.Chaining.CategoryRetention.restricted.rank = 1
• Clause.Chaining.CategoryRetention.full.rank = 2

@[instance_reducible]

instance Clause.Chaining.instLinearOrderCategoryRetention : LinearOrder CategoryRetention

The retention scale as a linear order: absent < restricted < full.

Equations

• Clause.Chaining.instLinearOrderCategoryRetention = LinearOrder.lift' Clause.Chaining.CategoryRetention.rank Clause.Chaining.instLinearOrderCategoryRetention._proof_1

theorem Clause.Chaining.CategoryRetention.absent_le (r : CategoryRetention) : absent ≤ r

absent is the bottom of the retention scale.

structure Clause.Chaining.MedialMorphProfile : Type

Morphological profile of medial verbs along five TAM dimensions — a per-category finiteness vector, of which the binary finite/non-finite cut is a coarsening.

• tense : CategoryRetention

  Tense (absent in Nungon and Ku Waru; restricted in Manambu; full in some Turkic and Caucasian languages).

• agreement : CategoryRetention

  Subject agreement (often inherited from the final verb under same-subject marking).

• mood : CategoryRetention

  Mood (typically at most a binary realis/irrealis split).

• polarity : CategoryRetention

  Independent negation of the medial clause (some languages restrict negation to the final clause, so polarity scopes over the chain).

• aspect : CategoryRetention

  Aspect (some languages retain perfective/imperfective to distinguish completed vs ongoing subevents).

def Clause.Chaining.instReprMedialMorphProfile.repr : MedialMorphProfile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprMedialMorphProfile : Repr MedialMorphProfile

Equations

• Clause.Chaining.instReprMedialMorphProfile = { reprPrec := Clause.Chaining.instReprMedialMorphProfile.repr }

def Clause.Chaining.instDecidableEqMedialMorphProfile.decEq (x✝ x✝¹ : MedialMorphProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Clause.Chaining.instDecidableEqMedialMorphProfile : DecidableEq MedialMorphProfile

Equations

• Clause.Chaining.instDecidableEqMedialMorphProfile = Clause.Chaining.instDecidableEqMedialMorphProfile.decEq

def Clause.Chaining.MedialMorphProfile.MaximallyReduced (p : MedialMorphProfile) : Prop

Every category is absent: a bare converb.

Equations

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

@[instance_reducible]

instance Clause.Chaining.MedialMorphProfile.instDecidablePredMaximallyReduced : DecidablePred MaximallyReduced

Equations

• x✝.instDecidablePredMaximallyReduced = Clause.Chaining.MedialMorphProfile.instDecidablePredMaximallyReduced._aux_1 x✝

def Clause.Chaining.MedialMorphProfile.FullyRetained (p : MedialMorphProfile) : Prop

Every category is full: the profile of an independent verb (though a medial verb still lacks illocutionary force).

Equations

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

@[instance_reducible]

instance Clause.Chaining.MedialMorphProfile.instDecidablePredFullyRetained : DecidablePred FullyRetained

Equations

• x✝.instDecidablePredFullyRetained = Clause.Chaining.MedialMorphProfile.instDecidablePredFullyRetained._aux_1 x✝

def Clause.Chaining.MedialMorphProfile.udVerbForm (p : MedialMorphProfile) : UD.VerbForm

Expected UD verb form for a medial verb with this profile: converb unless fully retained.

Equations

• p.udVerbForm = if p.FullyRetained then UD.VerbForm.Fin else UD.VerbForm.Conv

Switch-reference

inductive Clause.Chaining.SRSystem : Type

Type of switch-reference system: morphology on medial verbs tracking referential continuity across clause boundaries — orthogonal to binding theory, which constrains intra-clausal coreference configurationally ([SA25] §§1.4–1.5, §3; [dV25] §§3–4).

• none : SRSystem

  No SR morphology; the language may still chain (Korean, Turkish, Japanese).

• ssDs : SRSystem

  Binary same-subject vs different-subject marking — the canonical system (Nungon, Ku Waru, many Papuan and Amerindian languages).

• ssDsTemporal : SRSystem

  SS/DS fused with temporal relation: SS-sequential, SS-simultaneous, DS-sequential, DS-simultaneous as distinct forms (Nungon, Amele, many Trans-New Guinea languages).

• multiTrack : SRSystem

  Tracks more than one argument (e.g. subject and object) — rare (Panoan).

@[instance_reducible]

instance Clause.Chaining.instDecidableEqSRSystem : DecidableEq SRSystem

Equations

• Clause.Chaining.instDecidableEqSRSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.Chaining.instReprSRSystem.repr : SRSystem → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprSRSystem : Repr SRSystem

Equations

• Clause.Chaining.instReprSRSystem = { reprPrec := Clause.Chaining.instReprSRSystem.repr }

@[instance_reducible]

instance Clause.Chaining.instInhabitedSRSystem : Inhabited SRSystem

Equations

• Clause.Chaining.instInhabitedSRSystem = { default := Clause.Chaining.instInhabitedSRSystem.default }

inductive Clause.Chaining.SRTarget : Type

What the SR system tracks.

• subjectOnly : SRTarget

  Syntactic subject only — the canonical pattern.

• subjectAndObject : SRTarget

  Subject and object — rare (some Panoan languages).

• topicBased : SRTarget

  The topical participant, determined by discourse prominence rather than grammatical function (Greater Awyu, [dV25] §4.4).

@[instance_reducible]

instance Clause.Chaining.instDecidableEqSRTarget : DecidableEq SRTarget

Equations

• Clause.Chaining.instDecidableEqSRTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.Chaining.instReprSRTarget.repr : SRTarget → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprSRTarget : Repr SRTarget

Equations

• Clause.Chaining.instReprSRTarget = { reprPrec := Clause.Chaining.instReprSRTarget.repr }

@[instance_reducible]

instance Clause.Chaining.instInhabitedSRTarget : Inhabited SRTarget

Equations

• Clause.Chaining.instInhabitedSRTarget = { default := Clause.Chaining.instInhabitedSRTarget.default }

inductive Clause.Chaining.SRMarkedness : Type

Markedness asymmetry between the SS and DS forms. Subject continuity is the discourse default, so SS is usually the unmarked member.

• ssUnmarked : SRMarkedness

  SS shorter, zero, or suffix-only; DS overtly marked — the dominant pattern.

• dsUnmarked : SRMarkedness

  DS unmarked — rare.

• symmetric : SRMarkedness

  Both overtly marked with comparable weight.

@[instance_reducible]

instance Clause.Chaining.instDecidableEqSRMarkedness : DecidableEq SRMarkedness

Equations

• Clause.Chaining.instDecidableEqSRMarkedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Clause.Chaining.instReprSRMarkedness : Repr SRMarkedness

Equations

• Clause.Chaining.instReprSRMarkedness = { reprPrec := Clause.Chaining.instReprSRMarkedness.repr }

def Clause.Chaining.instReprSRMarkedness.repr : SRMarkedness → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instInhabitedSRMarkedness : Inhabited SRMarkedness

Equations

• Clause.Chaining.instInhabitedSRMarkedness = { default := Clause.Chaining.instInhabitedSRMarkedness.default }

Interclausal relations and bridging

inductive Clause.Chaining.InterclauseRelation : Type

Semantic relation between a medial clause and the next clause, encoded on the medial verb, inferred, or signaled by the SR system ([SA25] §1.4; [Lon07]).

• sequential : InterclauseRelation
• simultaneous : InterclauseRelation
• causal : InterclauseRelation
• conditional : InterclauseRelation
• concessive : InterclauseRelation
• manner : InterclauseRelation
• contrastive : InterclauseRelation
• additive : InterclauseRelation
• purpose : InterclauseRelation

@[instance_reducible]

instance Clause.Chaining.instDecidableEqInterclauseRelation : DecidableEq InterclauseRelation

Equations

• Clause.Chaining.instDecidableEqInterclauseRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.Chaining.instReprInterclauseRelation.repr : InterclauseRelation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprInterclauseRelation : Repr InterclauseRelation

Equations

• Clause.Chaining.instReprInterclauseRelation = { reprPrec := Clause.Chaining.instReprInterclauseRelation.repr }

@[instance_reducible]

instance Clause.Chaining.instInhabitedInterclauseRelation : Inhabited InterclauseRelation

Equations

• Clause.Chaining.instInhabitedInterclauseRelation = { default := Clause.Chaining.instInhabitedInterclauseRelation.default }

def Clause.Chaining.InterclauseRelation.Temporal (r : InterclauseRelation) : Prop

The temporal relations — exactly the ones SR morphology can encode without additional marking (SRSystem.ssDsTemporal).

Equations

• r.Temporal = (r = Clause.Chaining.InterclauseRelation.sequential ∨ r = Clause.Chaining.InterclauseRelation.simultaneous)

@[instance_reducible]

instance Clause.Chaining.instDecidablePredInterclauseRelationTemporal : DecidablePred InterclauseRelation.Temporal

Equations

• Clause.Chaining.instDecidablePredInterclauseRelationTemporal x✝ = Clause.Chaining.instDecidablePredInterclauseRelationTemporal._aux_1 x✝

inductive Clause.Chaining.BridgingType : Type

Discourse bridging constructions spanning chain boundaries, characteristic of oral narrative ([SA25] §1.6, §3.3).

• recapitulative : BridgingType

  Recapitulative (tail-head) linkage: the first medial clause of a new chain repeats the final clause of the preceding one (Nungon, Ku Waru).

• summary : BridgingType

  Summary linkage: a generic verb ('do', 'say') summarizes the preceding episode (Ku Waru, Manambu).

@[instance_reducible]

instance Clause.Chaining.instDecidableEqBridgingType : DecidableEq BridgingType

Equations

• Clause.Chaining.instDecidableEqBridgingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Clause.Chaining.instReprBridgingType : Repr BridgingType

Equations

• Clause.Chaining.instReprBridgingType = { reprPrec := Clause.Chaining.instReprBridgingType.repr }

def Clause.Chaining.instReprBridgingType.repr : BridgingType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instInhabitedBridgingType : Inhabited BridgingType

Equations

• Clause.Chaining.instInhabitedBridgingType = { default := Clause.Chaining.instInhabitedBridgingType.default }

The per-language bundle

structure Clause.Chaining.System : Type

A language's clause-chaining system: chain structure, switch-reference, medial morphology, marked relations, and bridging. Per-language instances and generalizations over them live in Studies/SarvasyAikhenvald2025.lean.

• direction : ChainDirection

  Linear order of medial and final clauses.

• srSystem : SRSystem

  Type of switch-reference system, if any.

• srTarget : Option SRTarget

  What SR tracks, when present.

• srObligatory : Bool

  Whether SR marking is obligatory on every medial verb.

• srMarkedness : Option SRMarkedness

  Markedness asymmetry of the SR system, when recorded.

• medialMorph : MedialMorphProfile

  Morphological profile of medial verbs.

• relationsMarked : List InterclauseRelation

  Interclausal relations grammatically marked on medial verbs.

• hasRecapLinkage : Bool

  Recapitulative (tail-head) linkage attested.

• hasSummaryLinkage : Bool

  Summary linkage attested.

• medialCanStandAlone : Bool

  Medial clauses can stand without a final clause — the non-canonical stand-alone medial ([Sar15]).

@[instance_reducible]

instance Clause.Chaining.instReprSystem : Repr System

Equations

• Clause.Chaining.instReprSystem = { reprPrec := Clause.Chaining.instReprSystem.repr }

def Clause.Chaining.instReprSystem.repr : System → ℕ → Std.Format

Equations

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

def Clause.Chaining.instBEqSystem.beq : System → System → Bool

Equations

• One or more equations did not get rendered due to their size.
• Clause.Chaining.instBEqSystem.beq x✝¹ x✝ = false

@[instance_reducible]

instance Clause.Chaining.instBEqSystem : BEq System

Equations

• Clause.Chaining.instBEqSystem = { beq := Clause.Chaining.instBEqSystem.beq }

def Clause.Chaining.System.hasSR (p : System) : Bool

The language has an SR system.

Equations

• p.hasSR = (p.srSystem != Clause.Chaining.SRSystem.none)

def Clause.Chaining.System.tenseFromFinalVerb (p : System) : Bool

Medial tense is inherited from the final verb (no medial tense marking).

Equations

• p.tenseFromFinalVerb = (p.medialMorph.tense == Clause.Chaining.CategoryRetention.absent)

def Clause.Chaining.System.hasBridging (p : System) : Bool

Some discourse bridging construction is attested.

Equations

• p.hasBridging = (p.hasRecapLinkage || p.hasSummaryLinkage)

def Clause.Chaining.System.temporalViaSR (p : System) : Bool

Temporal relations are encoded by the SR morphology itself.

Equations

• p.temporalViaSR = (p.srSystem == Clause.Chaining.SRSystem.ssDsTemporal)

def Clause.Chaining.System.medialVerbForm (p : System) : UD.VerbForm

Expected UD verb form for this language's medial verbs.

Equations

• p.medialVerbForm = p.medialMorph.udVerbForm