Documentation

Linglib.Core.Alternation

Valency Alternation Typology #

@cite{creissels-2025}

A unified framework for describing valency alternations cross-linguistically, following @cite{creissels-2025}'s framework for transitivity, valency, and voice. This file provides the core vocabulary that subsumes both @cite{levin-1993}'s English-specific diathesis alternations and @cite{creissels-2025}'s cross-linguistic voice alternation typology.

TR-roles #

@cite{creissels-2025} §1.3.3 defines Transitivity-Related roles (A, P, S, X) as constructional properties of nominal terms, not semantic roles. A is "the nominal term whose coding matches the agent of a prototypical transitive verb" — it's defined by coding (flagging, indexation, order), anchored to semantic prototypes. These are already captured by Prominence.ArgumentRole (S, A, P, R, T). This file adds X (oblique) as a TRRole that extends ArgumentRole with the non-core case.

Nucleativization and Denucleativization #

The two fundamental operations on coding frames (§8.1.3):

Nucleativization: a non-nuclear participant becomes a core term (A, P, or S) in the derived construction.
Denucleativization: a core term of the initial construction becomes oblique or unexpressed in the derived construction.

All voice alternations are defined by specifying which participants are nucleativized or denucleativized, and what TR-roles they acquire.

Unification with Levin alternations #

@cite{levin-1993}'s DiathesisAlternation captures English-specific alternation patterns. Each maps to a ValencyAlternation that specifies the structural effect. The key distinction: Levin alternations are often uncoded (flexivalency — no verbal morphology marks the alternation), while @cite{creissels-2025}'s voice alternations are coded (marked by verbal morphology). The marking field captures this.

inductive Core.Alternation.TRRole :

Transitivity-Related role including obliques.

Extends Prominence.ArgumentRole (S, A, P, R, T) with X for obliques. §1.3.3: "OBLIQUE NOMINAL TERMS (or simply OBLIQUES), symbolized as X, are defined as nominal terms of verbal clauses that do not meet the definition of either A, P, or S."

S : TRRole
A : TRRole
P : TRRole
X : TRRole

Instances For

instance Core.Alternation.instDecidableEqTRRole :

DecidableEq TRRole

Equations

Core.Alternation.instDecidableEqTRRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Alternation.instBEqTRRole.beq :

TRRole → TRRole → Bool

Equations

Core.Alternation.instBEqTRRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Alternation.instBEqTRRole :

Equations

Core.Alternation.instBEqTRRole = { beq := Core.Alternation.instBEqTRRole.beq }

instance Core.Alternation.instReprTRRole :

Equations

Core.Alternation.instReprTRRole = { reprPrec := Core.Alternation.instReprTRRole.repr }

def Core.Alternation.instReprTRRole.repr :

TRRole → Nat → Std.Format

Equations

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

Instances For

def Core.Alternation.TRRole.ofArgumentRole :

Prominence.ArgumentRole → TRRole

Convert ArgumentRole to TRRole. R and T map to P (both are P-like in Creissels' binary core-term system).

Equations

Instances For

inductive Core.Alternation.ParticipantFate :

What happens to a participant's coding in a valency alternation.

Each alternation is defined by specifying the fate of each participant in the initial construction.

nucleativized (target : TRRole) : ParticipantFate
Participant is nucleativized: becomes a core term in the derived construction. The target specifies which TR-role it acquires.
denucleativized : ParticipantFate
Participant is denucleativized: demoted from core term to oblique or unexpressed, but MAINTAINED IN PARTICIPANT STRUCTURE. The participant is still semantically present and may appear as an oblique phrase. §8.3.2.1: "the referent of the initial A is denucleativized ... but is maintained in participant structure."
suppressed : ParticipantFate
Participant is suppressed: REMOVED FROM PARTICIPANT STRUCTURE entirely. The participant has no syntactic realization in the derived construction and is not semantically implied. §8.3.1.2: "Decausativization suppresses the referent of the initial A from participant structure."
maintained : ParticipantFate
Participant's coding is maintained unchanged.
cumulated : ParticipantFate
Two participants are cumulated into a single participant (reflexivization/reciprocalization).
na : ParticipantFate
Not applicable (participant does not exist in initial construction).

Instances For

def Core.Alternation.instDecidableEqParticipantFate.decEq (x✝ x✝¹ : ParticipantFate) :

Decidable (x✝ = x✝¹)

Equations

Instances For

instance Core.Alternation.instDecidableEqParticipantFate :

DecidableEq ParticipantFate

Equations

Core.Alternation.instDecidableEqParticipantFate = Core.Alternation.instDecidableEqParticipantFate.decEq

instance Core.Alternation.instBEqParticipantFate :

BEq ParticipantFate

Equations

Core.Alternation.instBEqParticipantFate = { beq := Core.Alternation.instBEqParticipantFate.beq }

def Core.Alternation.instBEqParticipantFate.beq :

ParticipantFate → ParticipantFate → Bool

Equations

Instances For

instance Core.Alternation.instReprParticipantFate :

Repr ParticipantFate

Equations

Core.Alternation.instReprParticipantFate = { reprPrec := Core.Alternation.instReprParticipantFate.repr }

def Core.Alternation.instReprParticipantFate.repr :

ParticipantFate → Nat → Std.Format

Equations

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

Instances For

inductive Core.Alternation.AlternationMarking :

Whether and how a valency alternation is morphologically coded.

§1.1.3: voice = coded alternation; flexivalency = uncoded alternation. The distinction is fundamental to his framework: same structural alternation, different morphosyntactic status.

synthetic : AlternationMarking
Coded by verbal morphology (affix, ablaut, tone, etc.) — this is VOICE in terminology.
analytic : AlternationMarking
Coded by an analytic construction (auxiliary + nonfinite form).
equipollent : AlternationMarking
Coded by equipollent marking (both forms equally complex).
uncoded : AlternationMarking
Uncoded — no morphological marking (FLEXIVALENCY).

Instances For

instance Core.Alternation.instDecidableEqAlternationMarking :

DecidableEq AlternationMarking

Equations

Core.Alternation.instDecidableEqAlternationMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Alternation.instBEqAlternationMarking.beq :

AlternationMarking → AlternationMarking → Bool

Equations

Core.Alternation.instBEqAlternationMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Alternation.instBEqAlternationMarking :

BEq AlternationMarking

Equations

Core.Alternation.instBEqAlternationMarking = { beq := Core.Alternation.instBEqAlternationMarking.beq }

instance Core.Alternation.instReprAlternationMarking :

Repr AlternationMarking

Equations

Core.Alternation.instReprAlternationMarking = { reprPrec := Core.Alternation.instReprAlternationMarking.repr }

def Core.Alternation.instReprAlternationMarking.repr :

AlternationMarking → Nat → Std.Format

Equations

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

Instances For

def Core.Alternation.AlternationMarking.isVoice :

AlternationMarking → Bool

Is this alternation an instance of voice (coded by verbal morphology)?

Equations

Instances For

structure Core.Alternation.ValencyAlternation :

A valency alternation defined by its structural effect on participants.

This is the unified type subsuming both @cite{levin-1993}'s English-specific diathesis alternations and cross-linguistic voice alternation types. Each alternation specifies:

What happens to each participant of the initial construction
Whether a new participant is introduced
How (if at all) the alternation is morphologically marked

name : String
Descriptive name
fateOfA : ParticipantFate
What happens to the initial A (if the initial construction is transitive)
fateOfP : ParticipantFate
What happens to the initial P (if the initial construction is transitive)
fateOfS : ParticipantFate
What happens to the initial S (if the initial construction is intransitive)
newParticipant : Option TRRole
Is a new participant introduced in the derived construction? If so, which TR-role does it receive?
initialTransitive : Option Bool
Is the initial construction transitive, intransitive, or either?
derivedTransitive : Option Bool
Is the derived construction transitive?

Instances For

instance Core.Alternation.instReprValencyAlternation :

Repr ValencyAlternation

Equations

Core.Alternation.instReprValencyAlternation = { reprPrec := Core.Alternation.instReprValencyAlternation.repr }

def Core.Alternation.instReprValencyAlternation.repr :

ValencyAlternation → Nat → Std.Format

Equations

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

Instances For

instance Core.Alternation.instBEqValencyAlternation :

BEq ValencyAlternation

Equations

Core.Alternation.instBEqValencyAlternation = { beq := Core.Alternation.instBEqValencyAlternation.beq }

def Core.Alternation.instBEqValencyAlternation.beq :

ValencyAlternation → ValencyAlternation → Bool

Equations

One or more equations did not get rendered due to their size.
Core.Alternation.instBEqValencyAlternation.beq x✝¹ x✝ = false

Instances For

def Core.Alternation.causativization :

ValencyAlternation

Causativization (§8.3.1.1): nucleativization of a causer in A role. Initial construction is intransitive; initial S becomes P in the derived transitive construction.

Equations

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

Instances For

def Core.Alternation.decausativization :

ValencyAlternation

Decausativization (§8.3.1.2): the initial A is SUPPRESSED FROM PARTICIPANT STRUCTURE; initial P becomes S of an intransitive construction. Called "anticausative" in most other frameworks; Creissels prefers "decausative" because the prefix de- transparently marks the removal of causation.

The critical difference from passivization: in decausativization, A is entirely removed from participant structure (.suppressed), whereas in passivization, A is denucleativized but remains in participant structure (.denucleativized).

Equations

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

Instances For

def Core.Alternation.passivization :

ValencyAlternation

Passivization (§8.3.2.1): A is denucleativized (oblique or unexpressed) but maintained in participant structure. No participant is nucleativized. P becomes S.

The key difference from decausativization: in passivization, the initial A is still semantically present (can appear as an oblique agent phrase). In decausativization, the initial A is removed from participant structure.

Equations

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

Instances For

def Core.Alternation.iPassivization :

ValencyAlternation

I-passivization (§8.3.2.2): impersonal variant of passivization. A is denucleativized, but P's coding is unchanged — the derived construction is impersonal (no S).

Equations

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

Instances For

def Core.Alternation.antipassivization :

ValencyAlternation

Antipassivization (§8.3.2.3): P is denucleativized (oblique or unexpressed); A becomes S of an intransitive construction.

Equations

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

Instances For

def Core.Alternation.sDenucleativization :

ValencyAlternation

S-denucleativization (§8.3.2.4): S of an intransitive construction is denucleativized, yielding an impersonal construction.

Equations

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

Instances For

def Core.Alternation.reflexivization :

ValencyAlternation

Reflexivization (§8.3.3): A and P are cumulated into S — a single participant fills both roles.

Equations

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

Instances For

def Core.Alternation.reciprocalization :

ValencyAlternation

Reciprocalization (§8.3.3): like reflexivization but with a group reading — participants mutually fill both roles.

Equations

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

Instances For

def Core.Alternation.pApplicativization :

ValencyAlternation

P-applicativization (§8.3.5, §14.1.1): a non-nuclear participant is nucleativized as P. The initial P may be denucleativized (demoted to oblique) or maintained in double-P constructions.

Equations

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

Instances For

def Core.Alternation.dApplicativization :

ValencyAlternation

D-applicativization (§14.1.3): a non-nuclear participant is nucleativized as a dative oblique (a special oblique type with core-term-like properties in many languages).

Equations

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

Instances For

def Core.Alternation.xApplicativization :

ValencyAlternation

X-applicativization (§14.1.4): a non-nuclear participant is nucleativized as an ordinary oblique.

Equations

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

Instances For

def Core.Alternation.asNucleativizationOfObliques :

ValencyAlternation

A/S-nucleativization of obliques (§8.3.4.1): an oblique participant (e.g., an instrument) takes over the A or S role in the derived construction. The nucleativized participant does NOT outrank the initial A/S in agentivity (distinguishing this from causativization).

Example: Laalaa (Cangin) Fetal-aa ap-ah-an paloom 'The gun will be used to kill antelopes' — instrument nucleativized as A.

Equations

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

Instances For

def Core.Alternation.concernativization :

ValencyAlternation

Concernativization (§8.3.4.2): nucleativization of a concernee (external possessor / adversely affected party) into the A role. The initial construction may be transitive or intransitive.

When initial is intransitive: S is maintained (becomes P-like), concernee becomes A, derived construction is transitive. When initial is transitive: A is maintained, P is maintained, concernee becomes an additional A-like participant.

Example: Central Alaskan Yupik Kit'-i-aqa kicaq 'I had the anchor sunk (me negatively affected)' — concernee as A.

Equations

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

Instances For

def Core.Alternation.portativeDerivation :

ValencyAlternation

Portative derivation (§8.3.7): converts a motion verb into a transitive 'A moves carrying P'. Distinguished from both causativization and applicativization.

Equations

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

Instances For

inductive Core.Alternation.Alignment :

Alignment between core terms of transitive and intransitive clauses.

§1.3.4.2: the central typological parameter is whether S patterns with A (A-alignment, traditionally "accusative") or with P (P-alignment, traditionally "ergative"). Creissels avoids the traditional case-based labels because A-alignment can occur without accusative case, and P-alignment without ergative case.

A_alignment : Alignment
S is coded like A — traditionally "nominative-accusative"
P_alignment : Alignment
S is coded like P — traditionally "absolutive-ergative"

Instances For

instance Core.Alternation.instDecidableEqAlignment :

DecidableEq Alignment

Equations

Core.Alternation.instDecidableEqAlignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Alternation.instBEqAlignment :

Equations

Core.Alternation.instBEqAlignment = { beq := Core.Alternation.instBEqAlignment.beq }

def Core.Alternation.instBEqAlignment.beq :

Alignment → Alignment → Bool

Equations

Core.Alternation.instBEqAlignment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Alternation.instReprAlignment :

Equations

Core.Alternation.instReprAlignment = { reprPrec := Core.Alternation.instReprAlignment.repr }

def Core.Alternation.instReprAlignment.repr :

Alignment → Nat → Std.Format

Equations

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

Instances For

structure Core.Alternation.ObligatoryCodingProfile :

The Obligatory Coding Principle (§1.3.4.4): in most languages, every verb assigns a particular type of participant coding to one of its participants, and this type coincides with either A coding or P coding. A language that fully complies has either obligatory A-coding or obligatory P-coding.

This is a reformulation of the accusative/ergative typology: obligatory A-coding = consistently accusative; obligatory P-coding = consistently ergative.

language : String
defaultAlignment : Alignment
Default alignment
violationsExist : Bool
Whether violations of the Obligatory Coding Principle exist
splitS : Bool
Whether the language is split-S (different S classes align differently)

Instances For

instance Core.Alternation.instReprObligatoryCodingProfile :

Repr ObligatoryCodingProfile

Equations

Core.Alternation.instReprObligatoryCodingProfile = { reprPrec := Core.Alternation.instReprObligatoryCodingProfile.repr }

def Core.Alternation.instReprObligatoryCodingProfile.repr :

ObligatoryCodingProfile → Nat → Std.Format

Equations

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

Instances For

instance Core.Alternation.instBEqObligatoryCodingProfile :

BEq ObligatoryCodingProfile

Equations

Core.Alternation.instBEqObligatoryCodingProfile = { beq := Core.Alternation.instBEqObligatoryCodingProfile.beq }

def Core.Alternation.instBEqObligatoryCodingProfile.beq :

ObligatoryCodingProfile → ObligatoryCodingProfile → Bool

Equations

One or more equations did not get rendered due to their size.
Core.Alternation.instBEqObligatoryCodingProfile.beq x✝¹ x✝ = false

Instances For

structure Core.Alternation.VoiceMarkerProfile :

A voice marker and the alternation types it can mark.

§8.2: cross-linguistically, voice markers are polysemous — the same morpheme may mark multiple voice alternation types. For example, Russian -sja marks reflexivization, reciprocalization, passivization, and antipassivization (§8.2, ex. 8).

language : String
Language name
marker : String
Morpheme form
alternations : List ValencyAlternation
Which alternation types this marker can encode

Instances For

instance Core.Alternation.instReprVoiceMarkerProfile :

Repr VoiceMarkerProfile

Equations

Core.Alternation.instReprVoiceMarkerProfile = { reprPrec := Core.Alternation.instReprVoiceMarkerProfile.repr }

def Core.Alternation.instReprVoiceMarkerProfile.repr :

VoiceMarkerProfile → Nat → Std.Format

Equations

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

Instances For

def Core.Alternation.instBEqVoiceMarkerProfile.beq :

VoiceMarkerProfile → VoiceMarkerProfile → Bool

Equations

One or more equations did not get rendered due to their size.
Core.Alternation.instBEqVoiceMarkerProfile.beq x✝¹ x✝ = false

Instances For

instance Core.Alternation.instBEqVoiceMarkerProfile :

BEq VoiceMarkerProfile

Equations

Core.Alternation.instBEqVoiceMarkerProfile = { beq := Core.Alternation.instBEqVoiceMarkerProfile.beq }

structure Core.Alternation.VoiceDistribution :

Cross-linguistic prevalence of voice alternation types.

§8.3.8, citing @cite{bahrt-2021}: distribution of synthetic voice marking across 222 languages from all genera.

alternation : ValencyAlternation
percentage : Float
Percentage of languages with synthetic marking for this alternation

Instances For

instance Core.Alternation.instReprVoiceDistribution :

Repr VoiceDistribution

Equations

Core.Alternation.instReprVoiceDistribution = { reprPrec := Core.Alternation.instReprVoiceDistribution.repr }

def Core.Alternation.instReprVoiceDistribution.repr :

VoiceDistribution → Nat → Std.Format

Equations

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

Instances For

def Core.Alternation.instBEqVoiceDistribution.beq :

VoiceDistribution → VoiceDistribution → Bool

Equations

Core.Alternation.instBEqVoiceDistribution.beq { alternation := a, percentage := a_1 } { alternation := b, percentage := b_1 } = (a == b && a_1 == b_1)
Core.Alternation.instBEqVoiceDistribution.beq x✝¹ x✝ = false

Instances For

instance Core.Alternation.instBEqVoiceDistribution :

BEq VoiceDistribution

Equations

Core.Alternation.instBEqVoiceDistribution = { beq := Core.Alternation.instBEqVoiceDistribution.beq }

def Core.Alternation.bahrt2021Distribution :

List VoiceDistribution

@cite{bahrt-2021} distribution data, cited in §8.3.8. Percentages represent languages (out of 222) with synthetic marking for each voice alternation type.

Equations

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

Instances For

theorem Core.Alternation.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 (@cite{bahrt-2021}).

def Core.Alternation.ValencyAlternation.involvesNucleativization (va : ValencyAlternation) :

Does this alternation involve nucleativization (adding a new core term)?

Equations

va.involvesNucleativization = va.newParticipant.isSome

Instances For

def Core.Alternation.ValencyAlternation.involvesDenucleativization (va : ValencyAlternation) :

Does this alternation involve denucleativization or suppression (removing a participant from core-term status)?

Equations

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

Instances For

def Core.Alternation.ValencyAlternation.isValencyIncreasing (va : ValencyAlternation) :

Is this a valency-increasing alternation?

Equations

va.isValencyIncreasing = (va.involvesNucleativization && !va.involvesDenucleativization)

Instances For

def Core.Alternation.ValencyAlternation.isValencyDecreasing (va : ValencyAlternation) :

Is this a valency-decreasing alternation?

Equations

va.isValencyDecreasing = (va.involvesDenucleativization && !va.involvesNucleativization)

Instances For

def Core.Alternation.ValencyAlternation.involvesCumulation (va : ValencyAlternation) :

Does this alternation involve cumulation (reflexivization/reciprocalization)?

Equations

va.involvesCumulation = (va.fateOfA == Core.Alternation.ParticipantFate.cumulated || va.fateOfP == Core.Alternation.ParticipantFate.cumulated)

Instances For

theorem Core.Alternation.causativization_increases :

causativization.isValencyIncreasing = true

theorem Core.Alternation.decausativization_decreases :

decausativization.isValencyDecreasing = true

theorem Core.Alternation.passivization_decreases :

passivization.isValencyDecreasing = true

theorem Core.Alternation.passivization_vs_decausativization :

passivization.fateOfA = ParticipantFate.denucleativized ∧ decausativization.fateOfA = ParticipantFate.suppressed

The central distinction of §8.3.2.1: passivization MAINTAINS A in participant structure (.denucleativized), while decausativization SUPPRESSES A from participant structure (.suppressed). These are structurally distinct operations.

theorem Core.Alternation.antipassivization_decreases :

antipassivization.isValencyDecreasing = true

theorem Core.Alternation.reflexivization_cumulates :

reflexivization.involvesCumulation = true

theorem Core.Alternation.reciprocalization_cumulates :

reciprocalization.involvesCumulation = true

theorem Core.Alternation.pApplicativization_increases :

pApplicativization.isValencyIncreasing = true

theorem Core.Alternation.as_nucleativization_increases :

asNucleativizationOfObliques.isValencyIncreasing = true

A/S-nucleativization of obliques is valency-increasing.

theorem Core.Alternation.portative_increases :

portativeDerivation.isValencyIncreasing = true

Portative derivation is valency-increasing, like causativization and applicativization, but cannot be reduced to either (§8.3.7).

def Core.Alternation.toValencyAlternation :

DiathesisAlternation → ValencyAlternation

Map @cite{levin-1993}'s English-specific diathesis alternations to cross-linguistic valency alternation types.

Key insight: most Levin alternations are UNCODED (flexivalency) in English — the structural effect is the same as the corresponding coded voice alternation, but without morphological marking. For example, English break (tr)/break (intr) has the same structural effect as Tswana -eχ decausativization, but English uses no verbal morphology.

Equations

One or more equations did not get rendered due to their size.
Core.Alternation.toValencyAlternation DiathesisAlternation.causativeInchoative = Core.Alternation.decausativization
Core.Alternation.toValencyAlternation DiathesisAlternation.inducedAction = Core.Alternation.causativization
Core.Alternation.toValencyAlternation DiathesisAlternation.verbalPassive = Core.Alternation.passivization

Instances For

theorem Core.Alternation.causativeInchoative_is_decausativization :

toValencyAlternation DiathesisAlternation.causativeInchoative = decausativization

The causative/inchoative alternation maps to decausativization (viewed from the transitive direction, the intransitive variant removes the causer).

theorem Core.Alternation.conative_is_antipassive_like :

(toValencyAlternation DiathesisAlternation.conative).involvesDenucleativization = true ∧ (toValencyAlternation DiathesisAlternation.conative).fateOfA = ParticipantFate.maintained

The conative alternation is structurally an antipassivization: A is maintained, P is denucleativized (demoted to oblique with at).

theorem Core.Alternation.bppa_is_applicative_like :

(toValencyAlternation DiathesisAlternation.bodyPartPossessorAscension).involvesNucleativization = true

Body-part possessor ascension is structurally a nucleativization (like applicativization): a possessor is promoted to core-term status.

theorem Core.Alternation.understoodReciprocal_cumulates :

(toValencyAlternation DiathesisAlternation.understoodReciprocalObject).involvesCumulation = true

The understood reciprocal object alternation involves cumulation, just like reflexivization and reciprocalization in.

theorem Core.Alternation.unspecifiedObject_decreases :

(toValencyAlternation DiathesisAlternation.unspecifiedObject).isValencyDecreasing = true

The unspecified object alternation is valency-decreasing: P is suppressed (removed from participant structure).

The instrument subject alternation involves both nucleativization (instrument → A) and denucleativization (original A demoted), so it is neither strictly valency-increasing nor valency-decreasing — it is a restructuring.

theorem Core.Alternation.inducedAction_is_causativization :

toValencyAlternation DiathesisAlternation.inducedAction = causativization

The induced action alternation maps to causativization: Bill ran → Bill ran the horse (intransitive S becomes P, new causer becomes A).

theorem Core.Alternation.verbalPassive_is_passivization :

toValencyAlternation DiathesisAlternation.verbalPassive = passivization

The verbal passive maps to passivization.

theorem Core.Alternation.understoodReflexive_cumulates :

(toValencyAlternation DiathesisAlternation.understoodReflexiveObject).involvesCumulation = true

The understood reflexive object alternation involves cumulation, like reflexivization in.

theorem Core.Alternation.cognateObject_increases :

(toValencyAlternation DiathesisAlternation.cognateObject).isValencyIncreasing = true

The cognate object alternation is valency-increasing: adds a P to an intransitive verb (she laughed → she laughed a bitter laugh).

theorem Core.Alternation.wayConstruction_increases :

(toValencyAlternation DiathesisAlternation.wayConstruction).isValencyIncreasing = true

The way construction is valency-increasing: adds a possessive P (she elbowed → she elbowed her way through).

theorem Core.Alternation.understoodBodyPartObject_decreases :

(toValencyAlternation DiathesisAlternation.understoodBodyPartObject).isValencyDecreasing = true

The understood body-part object alternation is valency-decreasing: P is suppressed (Bill waved his hand → Bill waved).

inductive Core.Alternation.AmbitransitivityType :

Types of ambitransitivity (uncoded transitivity alternation).

§15.2: a verb is ambitransitive when it can appear in both transitive and intransitive constructions without morphological marking. The five subtypes differ in what happens to the participants.

P_ambitransitivity : AmbitransitivityType
S of intransitive = P of transitive. The glass broke. / She broke the glass. Traditionally "anticausative" or "unaccusative" ambitransitivity.
A_ambitransitivity : AmbitransitivityType
S of intransitive = A of transitive. She ate. / She ate the cake. Traditionally "unergative" ambitransitivity.
reflexive : AmbitransitivityType
The intransitive is reflexive (A = P). She washed. = She washed herself.
reciprocal : AmbitransitivityType
The intransitive is reciprocal (A = P, group). They kissed.
unspecified : AmbitransitivityType
Ambiguous or underspecified.

Instances For

instance Core.Alternation.instDecidableEqAmbitransitivityType :

DecidableEq AmbitransitivityType

Equations

Core.Alternation.instDecidableEqAmbitransitivityType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Alternation.instBEqAmbitransitivityType.beq :

AmbitransitivityType → AmbitransitivityType → Bool

Equations

Core.Alternation.instBEqAmbitransitivityType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Alternation.instBEqAmbitransitivityType :

BEq AmbitransitivityType

Equations

Core.Alternation.instBEqAmbitransitivityType = { beq := Core.Alternation.instBEqAmbitransitivityType.beq }

instance Core.Alternation.instReprAmbitransitivityType :

Repr AmbitransitivityType

Equations

Core.Alternation.instReprAmbitransitivityType = { reprPrec := Core.Alternation.instReprAmbitransitivityType.repr }

def Core.Alternation.instReprAmbitransitivityType.repr :

AmbitransitivityType → Nat → Std.Format

Equations

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

Instances For

theorem Core.Alternation.p_ambi_is_uncoded_decausativization :

decausativization.involvesDenucleativization = true

P-ambitransitivity corresponds to uncoded decausativization.

theorem Core.Alternation.a_ambi_is_uncoded_antipassivization :

antipassivization.involvesDenucleativization = true

A-ambitransitivity corresponds to uncoded antipassivization.