Creissels (2025): Transitivity, Valency, and Voice

[Cre25]

Formalization of key results from [Cre25], a comprehensive typological reference on transitivity, valency, and voice across the world's languages. The book proposes a unified framework based on:

• TR-roles (A, P, S, X): constructional categories defined by coding properties relative to prototypical transitive verbs (§1.3.3)
• Nucleativization/denucleativization: the two fundamental operations underlying all voice alternations (§8.1.3)
• Alignment and the Obligatory Coding Principle: A-alignment vs P-alignment as the fundamental typological parameter (§1.3.4)
• Voice marker polysemy: systematic cross-linguistic co-expression patterns where the same morpheme marks multiple voice alternation types (§8.2)

This study file bridges [Cre25]'s framework (formalized in Syntax/ArgumentStructure/Alternation.lean) to existing linglib infrastructure:

• Semantics/Causation/Morphological.lean: causativization and decausativization
• Typology/VoiceSystem.lean: pivot-based voice system typology
• Syntax/Minimalist/Applicative.lean: Pylkkänen's high/low applicatives

Bridge: Decausativization ↔ IntransitivizationType

§8.3.1.2: "Decausativization suppresses the referent of the initial A from participant structure and converts the initial P into the S term of an intransitive construction."

This corresponds to IntransitivizationType.anticausative in linglib's existing causation typology. Creissels prefers "decausativization" because the prefix de- transparently marks removal of the causation component, while "anticausative" misleadingly suggests a parallel with "antipassive" that doesn't hold (§8.3.1.2).

theorem Creissels2025.decausativization_matches_anticausative : Syntax.ArgumentStructure.Alternation.decausativization.fateOfA = Syntax.ArgumentStructure.Alternation.ParticipantFate.suppressed ∧ Causation.Morphological.IntransitivizationType.anticausative.isBieventive = false

Decausativization suppresses A from participant structure — same structural effect as anticausative intransitivization.

theorem Creissels2025.reflexive_not_decausativization : Causation.Morphological.IntransitivizationType.reflexive.isBieventive = true ∧ Syntax.ArgumentStructure.Alternation.decausativization.involvesCumulation = false

Reflexive intransitivization is NOT decausativization: the causer is coidentified with the causee (bieventive), not removed. In Creissels' terms, reflexive intransitives are a different structural operation.

Bridge: Causativization ↔ CausativeConstruction

§8.3.1.1 defines causativization as "the nucleativization of a participant (the causer) that instigates the event denoted by the initial construction or controls its realization."

The existing CausativeConstruction type adds the fine structure: morphological complexity (lexical/morphological/periphrastic) and semantic mediation (direct/indirect). Creissels' causativization is the structural frame; linglib's CausativeConstruction fills in the parameters.

§12.1.4 gives the tripartite morphological distinction:

• Synthetic (affixal): most common cross-linguistically
• Analytic (auxiliary + nonfinite): European passives, 'make/let' causatives
• Periphrastic (light verb): borderline voice/biclausal

theorem Creissels2025.causative_construction_nucleativizes : Syntax.ArgumentStructure.Alternation.causativization.involvesNucleativization = true ∧ Syntax.ArgumentStructure.Alternation.causativization.newParticipant = some Syntax.ArgumentStructure.Alternation.TRRole.A

Every CausativeConstruction instantiates the structural pattern of causativization: a new participant (causer) in A role.

theorem Creissels2025.causativization_decausativization_inverse : Syntax.ArgumentStructure.Alternation.causativization.newParticipant = some Syntax.ArgumentStructure.Alternation.TRRole.A ∧ Syntax.ArgumentStructure.Alternation.decausativization.fateOfA = Syntax.ArgumentStructure.Alternation.ParticipantFate.suppressed

Causativization and decausativization are inverse operations on the causality chain (§8.3.1): causativization adds a causer in A, decausativization suppresses A from participant structure.

theorem Creissels2025.complexity_alignment : Causation.Morphological.CausativeComplexity.lexical < Causation.Morphological.CausativeComplexity.morphological ∧ Causation.Morphological.CausativeComplexity.morphological < Causation.Morphological.CausativeComplexity.periphrastic

The three morphological complexity levels of [Com89] map to §12.1.4's synthetic/analytic/periphrastic distinction. Lexical = synthetic (most compact).

Bridge: Applicativization ↔ Pylkkänen's ApplType

§14.1 distinguishes three varieties:

• P-applicativization (§14.1.1): applied phrase fills P role
• D-applicativization (§14.1.3): applied phrase is dative oblique
• X-applicativization (§14.1.4): applied phrase is ordinary oblique

Pylkkänen (2008)'s high/low distinction is orthogonal to Creissels' P/D/X distinction. High applicatives introduce event-level participants (benefactives); low applicatives introduce transfer participants (recipients, sources). In Creissels' terms, high applicatives tend to produce P-applicativization (the applied phrase gets P coding), while low applicatives tend to produce D-applicativization (dative coding).

theorem Creissels2025.all_applicativizations_nucleativize : Syntax.ArgumentStructure.Alternation.pApplicativization.involvesNucleativization = true ∧ Syntax.ArgumentStructure.Alternation.dApplicativization.involvesNucleativization = true ∧ Syntax.ArgumentStructure.Alternation.xApplicativization.involvesNucleativization = true

All three applicativization types nucleativize a new participant.

theorem Creissels2025.p_applicativization_valency_increasing : Syntax.ArgumentStructure.Alternation.pApplicativization.isValencyIncreasing = true

P-applicativization is valency-increasing (the applied phrase becomes a new core term).

Bridge: symmetrical voices ↔ the Voice substrate

§8.5: symmetrical voice systems are those in which verb morphology marks the selection of a participant as the privileged syntactic term (pivot) WITHOUT AFFECTING TRANSITIVITY. This is a fundamentally different type of voice system from A/P-prominent systems (§1.3.3.3).

The Voice substrate's VoiceSystemSymmetry captures this with .symmetrical vs .asymmetrical, but doesn't encode Creissels' key insight: symmetrical voices are NOT instances of passivization, causativization, etc. — they are a distinct type that doesn't fit the nucleativization/denucleativization framework at all.

Example Toba Batak voice profiles illustrate that symmetrical systems have 2+ voices with equal morphological complexity (equipollent marking).

def Creissels2025.englishVoices : List Voice.VoiceEntry

An A/P-prominent transitive construction (e.g., English active/passive) is an asymmetrical voice system.

Equations

• Creissels2025.englishVoices = [{ name := "active", promotes := Voice.PivotTarget.agent }, { name := "passive", promotes := Voice.PivotTarget.patient }]

def Creissels2025.englishSymmetry : Voice.VoiceSystemSymmetry

Equations

• Creissels2025.englishSymmetry = Voice.VoiceSystemSymmetry.asymmetrical

theorem Creissels2025.english_is_asymmetrical : englishSymmetry = Voice.VoiceSystemSymmetry.asymmetrical

theorem Creissels2025.english_is_active_passive : Voice.isActivePassive englishVoices

Passivization vs Decausativization (§8.3.1.2 vs §8.3.2.1)

§8.3.2.1: "The maintenance of the initial A in participant structure is essential to distinguish passivization from decausativization."

Both operations denucleativize A and yield an intransitive construction, but they differ in whether A remains in participant structure:

• Passivization: A is .denucleativized (oblique or unexpressed, but still semantically present — can appear as oblique agent phrase)
• Decausativization: A is .suppressed (removed from participant structure entirely — no agent phrase possible)

This distinction is now directly encoded in ParticipantFate.

theorem Creissels2025.passive_decausative_distinct : Syntax.ArgumentStructure.Alternation.passivization.fateOfA ≠ Syntax.ArgumentStructure.Alternation.decausativization.fateOfA

Passivization and decausativization are structurally distinct despite both yielding intransitive constructions: they differ in whether A remains in participant structure.

Bridge: Passivization ↔ Antipassivization structural symmetry

§8.3.2: passivization, antipassivization, and S-denucleativization form a natural class — all three denucleativize a core term without nucleativizing any other participant, and the denucleativized participant remains in participant structure. They differ only in which core term is targeted:

• Passivization: A denucleativized
• Antipassivization: P denucleativized
• S-denucleativization: S denucleativized

theorem Creissels2025.passive_antipassive_mirror : Syntax.ArgumentStructure.Alternation.passivization.isValencyDecreasing = true ∧ Syntax.ArgumentStructure.Alternation.antipassivization.isValencyDecreasing = true ∧ Syntax.ArgumentStructure.Alternation.passivization.fateOfA = Syntax.ArgumentStructure.Alternation.ParticipantFate.denucleativized ∧ Syntax.ArgumentStructure.Alternation.antipassivization.fateOfP = Syntax.ArgumentStructure.Alternation.ParticipantFate.denucleativized

Passivization and antipassivization are structural mirrors: both denucleativize exactly one core term without nucleativizing any other.

theorem Creissels2025.denucleativization_paradigm : Syntax.ArgumentStructure.Alternation.passivization.fateOfA = Syntax.ArgumentStructure.Alternation.ParticipantFate.denucleativized ∧ Syntax.ArgumentStructure.Alternation.antipassivization.fateOfP = Syntax.ArgumentStructure.Alternation.ParticipantFate.denucleativized ∧ Syntax.ArgumentStructure.Alternation.sDenucleativization.fateOfS = Syntax.ArgumentStructure.Alternation.ParticipantFate.denucleativized

S-denucleativization completes the paradigm: all three target different TR-roles.

Bridge: Reflexivization/Reciprocalization ↔ existing data

§8.3.3: reflexivization and reciprocalization cumulate two participant roles (A and P) into a single participant (S). They differ in whether S refers to a single individual (reflexive) or a group whose members mutually fill both roles (reciprocal).

Both are classified as valency-decreasing in Creissels' framework — the derived construction has fewer core terms. The existing WALS Ch 106 data in Typology.lean captures the cross-linguistic formal relationship between reflexive and reciprocal markers.

theorem Creissels2025.refl_recip_same_structure : Syntax.ArgumentStructure.Alternation.reflexivization.fateOfA = Syntax.ArgumentStructure.Alternation.reciprocalization.fateOfA ∧ Syntax.ArgumentStructure.Alternation.reflexivization.fateOfP = Syntax.ArgumentStructure.Alternation.reciprocalization.fateOfP ∧ Syntax.ArgumentStructure.Alternation.reflexivization.involvesCumulation = true ∧ Syntax.ArgumentStructure.Alternation.reciprocalization.involvesCumulation = true

Reflexivization and reciprocalization have identical structural effects on core terms — they differ only in the semantic interpretation of cumulation (individual vs. group).

Voice Marker Stacking (§8.4)

§8.4: voice markers can be stacked compositionally. Example from Tswana (§8.4.1, ex. 38):

• write-CAUS-APPL: causativize then applicativize
• write-APPL-PASS: applicativize then passivize
• write-CAUS-PASS: causativize then passivize
• write-CAUS-APPL-PASS: all three composed

The compositional stacking means we can model multi-marker verb forms as sequential application of ValencyAlternation operations.

@[reducible, inline]

abbrev Creissels2025.VoiceStack : Type

A stacked voice derivation: a sequence of alternations applied in order.

Equations

• Creissels2025.VoiceStack = List Syntax.ArgumentStructure.Alternation.ValencyAlternation

def Creissels2025.tswana_caus_appl : VoiceStack

Example Tswana stacking patterns (§8.4.1).

Equations

• Creissels2025.tswana_caus_appl = [Syntax.ArgumentStructure.Alternation.causativization, Syntax.ArgumentStructure.Alternation.pApplicativization]

def Creissels2025.tswana_appl_pass : VoiceStack

Equations

• Creissels2025.tswana_appl_pass = [Syntax.ArgumentStructure.Alternation.pApplicativization, Syntax.ArgumentStructure.Alternation.passivization]

def Creissels2025.tswana_caus_pass : VoiceStack

Equations

• Creissels2025.tswana_caus_pass = [Syntax.ArgumentStructure.Alternation.causativization, Syntax.ArgumentStructure.Alternation.passivization]

def Creissels2025.tswana_caus_appl_pass : VoiceStack

Equations

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

Portative Derivation (§8.3.7)

§8.3.7 identifies portative derivation as a distinct voice alternation type that cannot be reduced to either causativization or applicativization, although it shares features with both:

• Like causativization: the derived construction has a prototypical agent in A
• Like applicativization: a new participant is introduced as P
• Unlike either: the A of the derived construction corresponds to the S of the initial construction (not a new causer), and the new P is the carried entity

Example: Caddo Ci-ʔa=d(ih)-ʔaʔ 'I will go' → Ci-ni-ʔa=d(ih)-ʔaʔ 'I will take it' (§8.3.7, ex. 33).

theorem Creissels2025.portative_distinct_from_causativization : Syntax.ArgumentStructure.Alternation.portativeDerivation.isValencyIncreasing = true ∧ Syntax.ArgumentStructure.Alternation.portativeDerivation.initialTransitive = some false ∧ Syntax.ArgumentStructure.Alternation.causativization.newParticipant = some Syntax.ArgumentStructure.Alternation.TRRole.A ∧ Syntax.ArgumentStructure.Alternation.portativeDerivation.newParticipant = some Syntax.ArgumentStructure.Alternation.TRRole.P

Portative derivation is valency-increasing but structurally distinct from both causativization and applicativization.

Alignment Profiles (§1.3.4)

§1.3.4.2: most languages have a clear preference for either A-alignment (S codes like A) or P-alignment (S codes like P). Some languages (e.g., Basque, Georgian) show split-S patterns.

def Creissels2025.russian : Syntax.ArgumentStructure.Alternation.ObligatoryCodingProfile

Equations

• Creissels2025.russian = { language := "Russian", defaultAlignment := Syntax.ArgumentStructure.Alternation.Alignment.A_alignment }

def Creissels2025.avar : Syntax.ArgumentStructure.Alternation.ObligatoryCodingProfile

Equations

• Creissels2025.avar = { language := "Avar", defaultAlignment := Syntax.ArgumentStructure.Alternation.Alignment.P_alignment }

def Creissels2025.basque : Syntax.ArgumentStructure.Alternation.ObligatoryCodingProfile

Equations

• Creissels2025.basque = { language := "Basque", defaultAlignment := Syntax.ArgumentStructure.Alternation.Alignment.P_alignment, violationsExist := true, splitS := true }

def Creissels2025.mandinka : Syntax.ArgumentStructure.Alternation.ObligatoryCodingProfile

Equations

• Creissels2025.mandinka = { language := "Mandinka", defaultAlignment := Syntax.ArgumentStructure.Alternation.Alignment.A_alignment, violationsExist := true }

Russian -sja polysemy (§1.2, ex. 8)

The Russian verbal suffix -sja / -s' is a paradigmatic example of voice marker polysemy. It marks at least four different voice alternation types:

(8a) reflexivization: Ivan mo-et-sja 'Ivan washes (himself)' (8b) reciprocalization: Paren' i devuška celuj-ut-sja 'The boy and the girl were kissing' (8c) passivization: Lekcija čita-et-sja professor-om 'The course is delivered by the professor' (8d) antipassivization: Sobaka kusa-et-sja 'The dog bites (people)'

def Creissels2025.russian_sja : Syntax.ArgumentStructure.Alternation.VoiceMarkerProfile

Equations

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

theorem Creissels2025.russian_sja_polysemy : russian_sja.alternations.length = 4

Russian -sja is polysemous across four voice alternation types.

Tswana -el polysemy (§8.2)

The Tswana voice suffix -el (traditionally called "applicative") marks both P-nucleativization (applicativization) and A-nucleativization of obliques (non-causative A/S-nucleativization). Example:

(12) Ki-tłàà-kwál-él-á Kítsó lò-kwâːlɔ̀ 'I'll write the letter to/for Kitso' (P-nucleativization of recipient) (13b) Nàmà í-ʃáb-él-à bò-χɔ́ːbɛ̀ 'Meat gives flavor to the porridge' (A-nucleativization of instrument → A)

def Creissels2025.tswana_el : Syntax.ArgumentStructure.Alternation.VoiceMarkerProfile

Equations

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

Causativizability and Voice Alternations

Ch 12 discusses restrictions on causativization. [Kre12]'s hierarchy (already formalized in MorphologicalCausation.lean) describes which verb classes can be causativized: unaccusatives > middles/ingestives > unergatives > simple transitives. This hierarchy predicts that causativization of transitive verbs (§12.3.5) often requires antipassivization to create an intransitive base first.

def Creissels2025.causativization_via_antipassive : VoiceStack

Causativization of transitives may require prior antipassivization to create an intransitive base (§12.3.5). This is an instance of compositional voice marker stacking.

Equations

• Creissels2025.causativization_via_antipassive = [Syntax.ArgumentStructure.Alternation.antipassivization, Syntax.ArgumentStructure.Alternation.causativization]

Cross-linguistic voice distribution (Bahrt 2021)

§8.3.8 reports [Bah21]'s survey of synthetic voice marking across 222 languages from all genera.

structure Creissels2025.VoiceDistribution : Type

Cross-linguistic prevalence of a voice alternation type: the share of languages with synthetic marking for it.

• alternation : Syntax.ArgumentStructure.Alternation.ValencyAlternation
• share : ℚ

  Fraction of languages with synthetic marking for this alternation.

def Creissels2025.instReprVoiceDistribution.repr : VoiceDistribution → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Creissels2025.instReprVoiceDistribution : Repr VoiceDistribution

Equations

• Creissels2025.instReprVoiceDistribution = { reprPrec := Creissels2025.instReprVoiceDistribution.repr }

def Creissels2025.bahrt2021Distribution : List VoiceDistribution

[Bah21] distribution data, cited in §8.3.8: the fraction of the 222 languages (all genera) with synthetic marking for each voice alternation type. Note (§8.3.8): Bahrt's "applicativization" conflates applicativization with non-causative A/S-nucleativization, so that row is broader than Creissels's pApplicativization.

Equations

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

theorem Creissels2025.causativization_most_common : Option.map (fun (x : VoiceDistribution) => x.alternation.name) bahrt2021Distribution.head? = some "causativization"

Causativization is the most common voice alternation type cross-linguistically ([Bah21]).

Compositional denotation of voice stacking (§8.4)

§8.4: voice markers stack, and a combination "operates on its valency properties exactly as it could operate on the valency of an underived verb form" — compositional stacking (§8.4.1). We model an alternation as a word over atomic coding-frame edits (the nucleativization/denucleativization atoms of §8.1.3), composition as the free-monoid product, and meaning as a denotation into partial transformations of coding frames. Two MonoidHoms — denote and valencyDelta — make stacking and the valency grading hold by construction.

End-roles (the S→P of causativization, P→S of passivization) are derived by normalizeFrame from the construction's transitivity, not stipulated — faithful to §8.1.3 (whose only atoms are nucleativization/denucleativization; the role changes are coding consequences, cf. footnote 5 §8.3.2.1).

This layer currently has a single consumer (this study), so per the project's graduation discipline it lives here; the FrameMap partial-transformation monoid (a Kleisli/Function.End analogue) and the denote/valencyDelta apparatus would hoist to Core/ and Alternation.lean once a second study consumes them.

inductive Creissels2025.Stacking.Coding : Type

A term's coding status in a construction (a state; ParticipantFate is the transition, derived below via fateOf).

• core (r : Syntax.ArgumentStructure.Alternation.TRRole) : Coding
• oblique : Coding
• suppressed : Coding

@[implicit_reducible]

instance Creissels2025.Stacking.instDecidableEqCoding : DecidableEq Coding

Equations

• Creissels2025.Stacking.instDecidableEqCoding = Creissels2025.Stacking.instDecidableEqCoding.decEq

def Creissels2025.Stacking.instDecidableEqCoding.decEq (x✝ x✝¹ : Coding) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Creissels2025.Stacking.instDecidableEqCoding.decEq (Creissels2025.Stacking.Coding.core a) (Creissels2025.Stacking.Coding.core b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Creissels2025.Stacking.instDecidableEqCoding.decEq (Creissels2025.Stacking.Coding.core r) Creissels2025.Stacking.Coding.oblique = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqCoding.decEq (Creissels2025.Stacking.Coding.core r) Creissels2025.Stacking.Coding.suppressed = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqCoding.decEq Creissels2025.Stacking.Coding.oblique (Creissels2025.Stacking.Coding.core r) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqCoding.decEq Creissels2025.Stacking.Coding.oblique Creissels2025.Stacking.Coding.oblique = isTrue ⋯
• Creissels2025.Stacking.instDecidableEqCoding.decEq Creissels2025.Stacking.Coding.suppressed (Creissels2025.Stacking.Coding.core r) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqCoding.decEq Creissels2025.Stacking.Coding.suppressed Creissels2025.Stacking.Coding.suppressed = isTrue ⋯

structure Creissels2025.Stacking.CodedTerm : Type

A coding-frame entry: a stable identity (tracked through a derivation) and its current status.

• id : ℕ
• coding : Coding

def Creissels2025.Stacking.instDecidableEqCodedTerm.decEq (x✝ x✝¹ : CodedTerm) : Decidable (x✝ = x✝¹)

Equations

• Creissels2025.Stacking.instDecidableEqCodedTerm.decEq { id := a, coding := a_1 } { id := b, coding := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Creissels2025.Stacking.instDecidableEqCodedTerm : DecidableEq CodedTerm

Equations

• Creissels2025.Stacking.instDecidableEqCodedTerm = Creissels2025.Stacking.instDecidableEqCodedTerm.decEq

@[reducible, inline]

abbrev Creissels2025.Stacking.CodingFrame : Type

A coding frame (§1.3.3): the participants and their statuses.

Equations

• Creissels2025.Stacking.CodingFrame = List Creissels2025.Stacking.CodedTerm

def Creissels2025.Stacking.coreCount (f : CodingFrame) : ℕ

Equations

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

def Creissels2025.Stacking.rerole (cc : ℕ) : Coding → Coding

Recompute a term's role from transitivity: the sole core term is S; a core S alongside other cores becomes P (a transitive clause has A and P, an intransitive clause has S).

Equations

• One or more equations did not get rendered due to their size.
• Creissels2025.Stacking.rerole cc x✝ = x✝

def Creissels2025.Stacking.normalizeFrame (f : CodingFrame) : CodingFrame

Normalize end-roles after an edit — this derives the S↔P relabellings a relabel atom would otherwise stipulate.

Equations

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

def Creissels2025.Stacking.freshId (f : CodingFrame) : ℕ

Equations

• Creissels2025.Stacking.freshId f = List.foldl (fun (m : ℕ) (t : Creissels2025.Stacking.CodedTerm) => m.max (t.id + 1)) 0 f

def Creissels2025.Stacking.setFirstCore (r : Syntax.ArgumentStructure.Alternation.TRRole) (c : Coding) : CodingFrame → Option CodingFrame

Equations

• One or more equations did not get rendered due to their size.
• Creissels2025.Stacking.setFirstCore r c [] = none

def Creissels2025.Stacking.removeFirstCore (r : Syntax.ArgumentStructure.Alternation.TRRole) : CodingFrame → Option CodingFrame

Equations

• One or more equations did not get rendered due to their size.
• Creissels2025.Stacking.removeFirstCore r [] = none

def Creissels2025.Stacking.HasCore (r : Syntax.ArgumentStructure.Alternation.TRRole) (f : CodingFrame) : Prop

Some core term in the frame bears role r.

Equations

• Creissels2025.Stacking.HasCore r f = ∃ t ∈ f, t.coding = Creissels2025.Stacking.Coding.core r

@[implicit_reducible]

instance Creissels2025.Stacking.instDecidableHasCore (r : Syntax.ArgumentStructure.Alternation.TRRole) (f : CodingFrame) : Decidable (HasCore r f)

Equations

• Creissels2025.Stacking.instDecidableHasCore r f = Creissels2025.Stacking.instDecidableHasCore._aux_1 r f

inductive Creissels2025.Stacking.Atom : Type

The atomic voice operations: Creissels's nucleativization / denucleativization (§8.1.3) plus cumulation (reflexivization, §8.3.3).

• nucleativize (target : Syntax.ArgumentStructure.Alternation.TRRole) : Atom
• denucleativize (role : Syntax.ArgumentStructure.Alternation.TRRole) : Atom
• suppress (role : Syntax.ArgumentStructure.Alternation.TRRole) : Atom
• cumulate (r1 r2 : Syntax.ArgumentStructure.Alternation.TRRole) : Atom

def Creissels2025.Stacking.instDecidableEqAtom.decEq (x✝ x✝¹ : Atom) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.nucleativize a) (Creissels2025.Stacking.Atom.nucleativize b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.nucleativize target) (Creissels2025.Stacking.Atom.denucleativize role) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.nucleativize target) (Creissels2025.Stacking.Atom.suppress role) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.nucleativize target) (Creissels2025.Stacking.Atom.cumulate r1 r2) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.denucleativize role) (Creissels2025.Stacking.Atom.nucleativize target) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.denucleativize a) (Creissels2025.Stacking.Atom.denucleativize b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.denucleativize role) (Creissels2025.Stacking.Atom.suppress role_1) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.denucleativize role) (Creissels2025.Stacking.Atom.cumulate r1 r2) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.suppress role) (Creissels2025.Stacking.Atom.nucleativize target) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.suppress role) (Creissels2025.Stacking.Atom.denucleativize role_1) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.suppress a) (Creissels2025.Stacking.Atom.suppress b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.suppress role) (Creissels2025.Stacking.Atom.cumulate r1 r2) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.cumulate r1 r2) (Creissels2025.Stacking.Atom.nucleativize target) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.cumulate r1 r2) (Creissels2025.Stacking.Atom.denucleativize role) = isFalse ⋯
• Creissels2025.Stacking.instDecidableEqAtom.decEq (Creissels2025.Stacking.Atom.cumulate r1 r2) (Creissels2025.Stacking.Atom.suppress role) = isFalse ⋯

@[implicit_reducible]

instance Creissels2025.Stacking.instDecidableEqAtom : DecidableEq Atom

Equations

• Creissels2025.Stacking.instDecidableEqAtom = Creissels2025.Stacking.instDecidableEqAtom.decEq

@[reducible, inline]

abbrev Creissels2025.Stacking.Word : Type

An alternation as a word over atoms; composition = the free-monoid product (= voice-marker stacking, §8.4).

Equations

• Creissels2025.Stacking.Word = FreeMonoid Creissels2025.Stacking.Atom

def Creissels2025.Stacking.FrameMap : Type

Partial transformations of coding frames under Kleisli composition; f * g is "apply f then g" (the MulOpposite of Function.End-style order). Kept a def (not abbrev) so this Monoid is keyed on FrameMap and does not leak to bare _ → Option _. Not PFun: Part ≠ Option, and the demos below rely on Option's decidability.

Equations

• Creissels2025.Stacking.FrameMap = (Creissels2025.Stacking.CodingFrame → Option Creissels2025.Stacking.CodingFrame)

@[implicit_reducible]

instance Creissels2025.Stacking.instMonoidFrameMap : Monoid FrameMap

Equations

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

def Creissels2025.Stacking.atomDenote : Atom → FrameMap

Equations

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

def Creissels2025.Stacking.atomDelta : Atom → ℤ

Equations

• Creissels2025.Stacking.atomDelta (Creissels2025.Stacking.Atom.nucleativize target) = 1
• Creissels2025.Stacking.atomDelta (Creissels2025.Stacking.Atom.denucleativize role) = -1
• Creissels2025.Stacking.atomDelta (Creissels2025.Stacking.Atom.suppress role) = -1
• Creissels2025.Stacking.atomDelta (Creissels2025.Stacking.Atom.cumulate r1 r2) = -1

def Creissels2025.Stacking.denote : Word →* FrameMap

Denotation of a word as a partial coding-frame transformation. A MonoidHom, so map_mul gives compositional stacking (§8.4.1).

Equations

• Creissels2025.Stacking.denote = FreeMonoid.lift Creissels2025.Stacking.atomDenote

def Creissels2025.Stacking.valencyDelta : Word →* Multiplicative ℤ

The valency grading: net change in number of core terms. A MonoidHom into Multiplicative ℤ, so stacking adds deltas.

Equations

• Creissels2025.Stacking.valencyDelta = FreeMonoid.lift fun (a : Creissels2025.Stacking.Atom) => Multiplicative.ofAdd (Creissels2025.Stacking.atomDelta a)

def Creissels2025.Stacking.netValency (w : Word) : ℤ

Equations

• Creissels2025.Stacking.netValency w = Multiplicative.toAdd (Creissels2025.Stacking.valencyDelta w)

@[simp]

theorem Creissels2025.Stacking.denote_of (a : Atom) : denote (FreeMonoid.of a) = atomDenote a

@[simp]

theorem Creissels2025.Stacking.valencyDelta_of (a : Atom) : valencyDelta (FreeMonoid.of a) = Multiplicative.ofAdd (atomDelta a)

theorem Creissels2025.Stacking.netValency_mul (x y : Word) : netValency (x * y) = netValency x + netValency y

def Creissels2025.Stacking.fateOf : Coding → Coding → Syntax.ArgumentStructure.Alternation.ParticipantFate

The substrate ParticipantFate, derived from a status transition — reusing the comparative-concept enum rather than forking a new one.

Equations

• Creissels2025.Stacking.fateOf (Creissels2025.Stacking.Coding.core r) (Creissels2025.Stacking.Coding.core r_1) = Syntax.ArgumentStructure.Alternation.ParticipantFate.maintained
• Creissels2025.Stacking.fateOf (Creissels2025.Stacking.Coding.core r) Creissels2025.Stacking.Coding.oblique = Syntax.ArgumentStructure.Alternation.ParticipantFate.denucleativized
• Creissels2025.Stacking.fateOf (Creissels2025.Stacking.Coding.core r) Creissels2025.Stacking.Coding.suppressed = Syntax.ArgumentStructure.Alternation.ParticipantFate.suppressed
• Creissels2025.Stacking.fateOf x✝ (Creissels2025.Stacking.Coding.core t) = Syntax.ArgumentStructure.Alternation.ParticipantFate.nucleativized t
• Creissels2025.Stacking.fateOf x✝¹ x✝ = Syntax.ArgumentStructure.Alternation.ParticipantFate.maintained

def Creissels2025.Stacking.roleHolder (r : Syntax.ArgumentStructure.Alternation.TRRole) : CodingFrame → Option ℕ

Id of the participant currently in core role r (frame-relative).

Equations

• Creissels2025.Stacking.roleHolder r [] = none
• Creissels2025.Stacking.roleHolder r (t :: ts) = if t.coding = Creissels2025.Stacking.Coding.core r then some t.id else Creissels2025.Stacking.roleHolder r ts

Named alternations as words (roles fall out of normalizeFrame)

def Creissels2025.Stacking.Word.causativization : Word

Equations

• Creissels2025.Stacking.Word.causativization = FreeMonoid.of (Creissels2025.Stacking.Atom.nucleativize Syntax.ArgumentStructure.Alternation.TRRole.A)

def Creissels2025.Stacking.Word.passivization : Word

Equations

• Creissels2025.Stacking.Word.passivization = FreeMonoid.of (Creissels2025.Stacking.Atom.denucleativize Syntax.ArgumentStructure.Alternation.TRRole.A)

def Creissels2025.Stacking.Word.decausativization : Word

Equations

• Creissels2025.Stacking.Word.decausativization = FreeMonoid.of (Creissels2025.Stacking.Atom.suppress Syntax.ArgumentStructure.Alternation.TRRole.A)

def Creissels2025.Stacking.Word.antipassivization : Word

Equations

• Creissels2025.Stacking.Word.antipassivization = FreeMonoid.of (Creissels2025.Stacking.Atom.denucleativize Syntax.ArgumentStructure.Alternation.TRRole.P)

def Creissels2025.Stacking.Word.applicativization : Word

Equations

• Creissels2025.Stacking.Word.applicativization = FreeMonoid.of (Creissels2025.Stacking.Atom.nucleativize Syntax.ArgumentStructure.Alternation.TRRole.P)

def Creissels2025.Stacking.Word.reflexivization : Word

Equations

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

def Creissels2025.Stacking.Word.causativizationViaAntipassive : Word

§12.3.5: causativizing a transitive verb requires antipassivizing first to create an intransitive base.

Equations

• Creissels2025.Stacking.Word.causativizationViaAntipassive = Creissels2025.Stacking.Word.antipassivization * Creissels2025.Stacking.Word.causativization

Forward bridges: the denotation reproduces the comparative-concept records

These prove the word denotations agree with the schema-level ValencyAlternation records (Alternation.lean) where both are defined — the legitimate direction, not a redefinition of the schema.

theorem Creissels2025.Stacking.netValency_causativization : netValency Word.causativization = 1

theorem Creissels2025.Stacking.netValency_passivization : netValency Word.passivization = -1

theorem Creissels2025.Stacking.causativization_record_increases : Syntax.ArgumentStructure.Alternation.causativization.isValencyIncreasing = true

theorem Creissels2025.Stacking.passivization_record_decreases : Syntax.ArgumentStructure.Alternation.passivization.isValencyDecreasing = true

theorem Creissels2025.Stacking.denote_passivization : denote Word.passivization [{ id := 0, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.A }, { id := 1, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.P }] = some [{ id := 0, coding := Coding.oblique }, { id := 1, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.S }]

Passivization obliquifies the initial A (kept in participant structure); P becomes S by normalization.

theorem Creissels2025.Stacking.denote_decausativization : denote Word.decausativization [{ id := 0, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.A }, { id := 1, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.P }] = some [{ id := 0, coding := Coding.suppressed }, { id := 1, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.S }]

Decausativization suppresses the initial A (removed). Same net valency as passive, different A-fate — the headline §8.3.1.2 / §8.3.2.1 distinction.

theorem Creissels2025.Stacking.fate_passivization_agrees : fateOf (Coding.core Syntax.ArgumentStructure.Alternation.TRRole.A) Coding.oblique = Syntax.ArgumentStructure.Alternation.passivization.fateOfA

theorem Creissels2025.Stacking.fate_decausativization_agrees : fateOf (Coding.core Syntax.ArgumentStructure.Alternation.TRRole.A) Coding.suppressed = Syntax.ArgumentStructure.Alternation.decausativization.fateOfA

theorem Creissels2025.Stacking.denote_applicativization : denote Word.applicativization [{ id := 0, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.A }, { id := 1, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.P }] = some [{ id := 0, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.A }, { id := 1, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.P }, { id := 2, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.P }]

Applicativization adds a new core P; on a transitive base this yields a double-P construction (§8.1.8) — no role relabelling required.

theorem Creissels2025.Stacking.denote_reflexivization : denote Word.reflexivization [{ id := 0, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.A }, { id := 1, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.P }] = some [{ id := 0, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.S }]

Reflexivization cumulates A and P into a single core term, which normalizes to S (§8.3.3).

Real composition for voice stacking (§8.4)

theorem Creissels2025.Stacking.denote_stack (x y : Word) (f : CodingFrame) : denote (x * y) f = (denote x f).bind (denote y)

Stacking is genuine composition: a word product denotes the Kleisli composite of its parts (§8.4.1). This gives the denotational counterpart of the record-level, semantics-free causativization_via_antipassive (§13).

theorem Creissels2025.Stacking.caus_A_holder_is_causer : (denote Word.causativization [{ id := 0, coding := Coding.core Syntax.ArgumentStructure.Alternation.TRRole.S }]).bind (roleHolder Syntax.ArgumentStructure.Alternation.TRRole.A) = some 1

Under stacking, "the A" is frame-relative: after causativization of an intransitive, the participant in role A is the new causer (id 1), not the original (id 0, now P). So a fate must be read off the current frame's role-holder, not a frozen "initial A".

theorem Creissels2025.Stacking.netValency_causativizationViaAntipassive : netValency Word.causativizationViaAntipassive = 0

§12.3.5: causativization via prior antipassivization is valency-neutral (antipassive −1 then causative +1), composed as one transformation.