Clause chaining

A clause chain is a sequence of medial clauses, dependent and morphologically reduced, closed by one final clause that supplies tense, mood and often agreement for the whole chain; it is the prototypical cosubordinate combination of clauses, dependent but not embedded ([GFvV84]; [Lon07]). This file provides the vocabulary in which a language's inventory of medial forms is described and the notions a typology of chaining reads off it ([SA25]; [dV25]). A fragment's carrier of medial forms is an instance of MedialForm, which records for each form the switch-reference value it marks, the interclausal relations it encodes and whether it indexes the subject of its clause; the switch-reference and agreement properties of the language are definitions over the instance. How far medial verbs retain an inflectional category is a CategoryRetention, and a language's profile over the five categories is a point of the product order MedialMorphProfile, whose top is the profile of a finite verb.

Main definitions

• CategoryRetention — the scale absent < restricted < full on which a medial verb retains a category, a bounded linear order; CategoryRetention.ofPred reads a category's retention off which of a language's medial forms admit it, fully when all do, restrictedly when some do, not at all when none does
• InflectionalCategory, MedialMorphProfile — the five categories and a profile over them, ordered pointwise; MedialMorphProfile.udVerbForm is the finite verb form at the top of the order and the converb everywhere else
• SwitchReference, InterclauseRelation, BridgingType — the same-subject or different-subject value a form marks, the relations a form can encode, of which InterclauseRelation.Temporal are the two temporal ones, and the two bridging constructions across chains
• MedialForm — the class of a language's medial forms, with MedialForm.HasSR, MedialForm.SRObligatory and MedialForm.SSUnmarked for its switch-reference system, MedialForm.agreement for the retention of subject agreement and MedialForm.relationsMarked for the relations some form encodes

References

• [SA25]
• [dV25]
• [GFvV84]
• [Lon07]

Retention of inflectional categories

inductive Clause.Chaining.CategoryRetention : Type

How much of an inflectional category a medial verb retains relative to an independent verb: none, the value coming from the final verb; fewer values than an independent verb; or the same range of values.

• absent : CategoryRetention

  Unmarked on medial verbs; the value is inherited from the final verb.

• restricted : CategoryRetention

  Fewer values than independent verbs, such as relative tense or a binary realis/irrealis split.

• full : CategoryRetention

  The same range of values as independent verbs.

@[instance_reducible]

instance Clause.Chaining.instDecidableEqCategoryRetention : DecidableEq CategoryRetention

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprCategoryRetention : Repr CategoryRetention

Equations

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

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.instFintypeCategoryRetention : Fintype CategoryRetention

Equations

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

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.CategoryRetention.instLinearOrder : LinearOrder CategoryRetention

The retention scale absent < restricted < full.

Equations

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

@[instance_reducible]

instance Clause.Chaining.CategoryRetention.instBoundedOrder : BoundedOrder CategoryRetention

Equations

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

@[simp]

theorem Clause.Chaining.CategoryRetention.top_eq_full : ⊤ = full

@[simp]

theorem Clause.Chaining.CategoryRetention.bot_eq_absent : ⊥ = absent

def Clause.Chaining.CategoryRetention.ofPred {ι : Type u_1} [Fintype ι] (p : ι → Prop) [DecidablePred p] : CategoryRetention

How far a language's medial forms retain a category, given which of them admit it, fully when every form does, restrictedly when some do, and not at all when none does.

Equations

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

theorem Clause.Chaining.CategoryRetention.ofPred_eq_full_iff {ι : Type u_1} [Fintype ι] (p : ι → Prop) [DecidablePred p] : ofPred p = full ↔ ∀ (i : ι), p i

theorem Clause.Chaining.CategoryRetention.ofPred_eq_restricted_iff {ι : Type u_1} [Fintype ι] (p : ι → Prop) [DecidablePred p] : ofPred p = restricted ↔ (∃ (i : ι), p i) ∧ ∃ (i : ι), ¬p i

theorem Clause.Chaining.CategoryRetention.ofPred_eq_absent_iff {ι : Type u_1} [Fintype ι] (p : ι → Prop) [DecidablePred p] [Nonempty ι] : ofPred p = absent ↔ ∀ (i : ι), ¬p i

inductive Clause.Chaining.InflectionalCategory : Type

The inflectional categories along which a medial verb is reduced.

• tense : InflectionalCategory

  Tense.

• agreement : InflectionalCategory

  Subject agreement.

• mood : InflectionalCategory

  Mood.

• polarity : InflectionalCategory

  Independent negation of the medial clause.

• aspect : InflectionalCategory

  Aspect.

@[instance_reducible]

instance Clause.Chaining.instDecidableEqInflectionalCategory : DecidableEq InflectionalCategory

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprInflectionalCategory : Repr InflectionalCategory

Equations

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

def Clause.Chaining.instReprInflectionalCategory.repr : InflectionalCategory → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instFintypeInflectionalCategory : Fintype InflectionalCategory

Equations

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

@[reducible, inline]

abbrev Clause.Chaining.MedialMorphProfile : Type

A medial verb's retention of each inflectional category, ordered pointwise; the top is the profile of an independent verb and the bottom a bare converb.

Equations

• Clause.Chaining.MedialMorphProfile = (Clause.Chaining.InflectionalCategory → Clause.Chaining.CategoryRetention)

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

The UD verb form of a medial verb with a profile, finite when every category is fully retained and a converb otherwise.

Equations

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

theorem Clause.Chaining.MedialMorphProfile.udVerbForm_eq_fin_iff (p : MedialMorphProfile) : p.udVerbForm = UD.VerbForm.Fin ↔ p = ⊤

Switch-reference, relations and bridging

inductive Clause.Chaining.SwitchReference : Type

The switch-reference value a medial form marks: the subject of its clause is the same as that of the reference clause, or different.

• ss : SwitchReference

  Same subject.

• ds : SwitchReference

  Different subject.

@[instance_reducible]

instance Clause.Chaining.instDecidableEqSwitchReference : DecidableEq SwitchReference

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprSwitchReference : Repr SwitchReference

Equations

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

def Clause.Chaining.instReprSwitchReference.repr : SwitchReference → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.Chaining.instFintypeSwitchReference : Fintype SwitchReference

Equations

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

inductive Clause.Chaining.InterclauseRelation : Type

A semantic relation between a medial clause and the next clause that a medial form can encode ([SA25]; [Lon07]).

• sequential : InterclauseRelation

  The medial event precedes the next event, in iconic order.

• simultaneous : InterclauseRelation

  The medial event overlaps the next event.

• causal : InterclauseRelation

  The medial event is the reason for the next event.

• conditional : InterclauseRelation

  The medial event is a condition on the next event.

• concessive : InterclauseRelation

  The medial event holds despite the next event.

• manner : InterclauseRelation

  The medial event specifies how the next event occurs.

• contrastive : InterclauseRelation

  The events contrast.

• additive : InterclauseRelation

  The medial event is added without temporal or causal import.

• purpose : InterclauseRelation

  The medial event is the purpose of the next event.

@[instance_reducible]

instance Clause.Chaining.instDecidableEqInterclauseRelation : DecidableEq InterclauseRelation

Equations

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

@[instance_reducible]

instance Clause.Chaining.instReprInterclauseRelation : Repr InterclauseRelation

Equations

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

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.instFintypeInterclauseRelation : Fintype InterclauseRelation

Equations

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

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

The temporal relations, sequence and simultaneity.

Equations

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

@[instance_reducible]

instance Clause.Chaining.instDecidablePredInterclauseRelationTemporal : DecidablePred InterclauseRelation.Temporal

Equations

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

inductive Clause.Chaining.BridgingType : Type

The bridging constructions spanning chain boundaries in oral narrative.

• recapitulative : BridgingType

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

• summary : BridgingType

  Summary linkage: a generic verb such as 'do' or 'be' summarizes the preceding chain.

@[instance_reducible]

instance Clause.Chaining.instDecidableEqBridgingType : DecidableEq BridgingType

Equations

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

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.instReprBridgingType : Repr BridgingType

Equations

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

@[instance_reducible]

instance Clause.Chaining.instFintypeBridgingType : Fintype BridgingType

Equations

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

A language's medial forms

class Clause.Chaining.MedialForm (M : Type u_1) : Type u_1

A language's medial forms, each with the switch-reference value it marks, the interclausal relations it encodes, and whether it indexes the subject of its clause.

• sr : M → Option SwitchReference

  The switch-reference value a form marks, none for a form neutral to it.

• relations : M → Finset InterclauseRelation

  The interclausal relations a form encodes.

• IndexesSubject : M → Prop

  The form carries subject cross-referencing.

• decidableIndexesSubject : DecidablePred IndexesSubject

def Clause.Chaining.MedialForm.HasSR (M : Type u_1) [MedialForm M] : Prop

Some medial form marks switch-reference.

Equations

• Clause.Chaining.MedialForm.HasSR M = ∃ (m : M), Clause.Chaining.MedialForm.sr m ≠ none

def Clause.Chaining.MedialForm.SRObligatory (M : Type u_1) [MedialForm M] : Prop

Every medial form marks switch-reference.

Equations

• Clause.Chaining.MedialForm.SRObligatory M = ∀ (m : M), Clause.Chaining.MedialForm.sr m ≠ none

def Clause.Chaining.MedialForm.SSUnmarked (M : Type u_1) [MedialForm M] : Prop

The same-subject forms leave the subject unindexed and the different-subject forms index it, the dominant markedness pattern of switch-reference.

Equations

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

@[instance_reducible]

instance Clause.Chaining.MedialForm.instDecidableHasSR (M : Type u_1) [MedialForm M] [Fintype M] : Decidable (HasSR M)

Equations

• Clause.Chaining.MedialForm.instDecidableHasSR M = { decide := decide (∃ a ∈ Finset.univ, (fun (m : M) => Clause.Chaining.MedialForm.sr m ≠ none) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Clause.Chaining.MedialForm.instDecidableSRObligatory (M : Type u_1) [MedialForm M] [Fintype M] : Decidable (SRObligatory M)

Equations

• Clause.Chaining.MedialForm.instDecidableSRObligatory M = { decide := decide (∀ a ∈ Finset.univ, (fun (m : M) => Clause.Chaining.MedialForm.sr m ≠ none) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Clause.Chaining.MedialForm.instDecidableSSUnmarked (M : Type u_1) [MedialForm M] [Fintype M] : Decidable (SSUnmarked M)

Equations

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

def Clause.Chaining.MedialForm.agreement (M : Type u_1) [MedialForm M] [Fintype M] : CategoryRetention

How far the medial verbs retain subject agreement.

Equations

• Clause.Chaining.MedialForm.agreement M = Clause.Chaining.CategoryRetention.ofPred Clause.Chaining.MedialForm.IndexesSubject

def Clause.Chaining.MedialForm.relationsMarked (M : Type u_1) [MedialForm M] [Fintype M] : Finset InterclauseRelation

The relations some medial form encodes.

Equations

• Clause.Chaining.MedialForm.relationsMarked M = Finset.univ.biUnion Clause.Chaining.MedialForm.relations

theorem Clause.Chaining.MedialForm.SRObligatory.hasSR {M : Type u_1} [MedialForm M] [Nonempty M] (h : SRObligatory M) : HasSR M

@[simp]

theorem Clause.Chaining.MedialForm.mem_relationsMarked {M : Type u_1} [MedialForm M] [Fintype M] {r : InterclauseRelation} : r ∈ relationsMarked M ↔ ∃ (m : M), r ∈ relations m

theorem Clause.Chaining.MedialForm.agreement_eq_absent_iff {M : Type u_1} [MedialForm M] [Fintype M] [Nonempty M] : agreement M = CategoryRetention.absent ↔ ∀ (m : M), ¬IndexesSubject m

theorem Clause.Chaining.MedialForm.agreement_eq_full_iff {M : Type u_1} [MedialForm M] [Fintype M] : agreement M = CategoryRetention.full ↔ ∀ (m : M), IndexesSubject m