Muñoz Pérez (2026): Stylistic Applicatives

This file formalizes Muñoz Pérez's analysis of the stylistic applicative of Chilean Spanish. A marked anticausative with an affected dative surfaces in General Spanish with the cluster se me. Chilean Spanish also has me le and se me le, with an invariable le that refers to nothing, and the three are synonymous. The alternation is confined to first and second person singular datives and to predicates that take the anticausative marker.

The paper takes the dative clitic to realize an applicative head and se to be an expletive in the specifier of a Voice head that introduces no argument and has no meaning. A fission rule splits an applicative head that is [+PART, +SING] into two exponents when the predicate is inchoative: a clitic with the person and number of the head, and the inflectionless dative le. At PF the Voice projection must be overtly marked by a reflexive clitic, and every head must be pronounced. The first exponent of a fissioned head is syncretic with a reflexive, so it can mark Voice while le pronounces the applicative head. This is why se is optional exactly where fission applies, and since the three clusters spell out one clause under a meaningless Voice head, they do not differ in meaning.

Main declarations

• Clause, Clause.site, marked, unmarked: a clause by its Voice head, its verbal heads and the bundle of its applicative head, with the site of that head; the clauses of marked and unmarked anticausatives.
• IsFissionApplicable, applExponents: the fission rule and the exponents it gives the applicative head.
• Converges: the two PF conditions on the clitics of a clause.
• clusters: the clitic clusters a clause surfaces with.

Main results

• isFissionApplicable_iff: fission applies to the speaker and the addressee alone.
• clusters_marked, clusters_unmarked: the typology of realizations. A marked anticausative has the marker with a plain dative and, where fission applies, the fissioned dative with and without the marker; an unmarked one has the plain dative alone.
• marker_optional_iff: the marker can be absent exactly where fission applies.
• converges_of_fission, not_converges_singleton: fission rescues a clause without the marker because the dative is syncretic with the reflexive outside the third person, and an unfissioned dative cannot, since it would leave the applicative head unpronounced.
• anticausative_rows, other_rows: the judgments on the paper's clitic clusters.
• causer_reading_rows: the unintentional causer reading arises only from the marked clause.
• isLicit_me_iff_nos: no person case constraint separates me le from nos le.

Implementation notes

The verbal heads of a marked anticausative are a change and a result state and those of an unmarked one a change alone, after the structures the paper adopts from Cuervo; the applicative head merges as low as the structure allows, taking the result state as its complement where there is one, Cuervo's affected applicative, and the theme otherwise (Clause.site); the context of the fission rule, the change head over the applicative over the state head, is that the site is affected. The paper leaves the structure of unmarked anticausatives open; all that matters here is that they lack the result state and a Voice head that asks for a marker. The optionality of the marker in the syntax, which the paper derives from a principle that lets an unchecked feature fail, is built into markers. The clauses given to quejarse and to impersonal dar say only that they are not inchoative.

TODO

The paper's comparison with the two-flavour Voice of Martin, Schäfer and Kastner is not formalized.

References

• M. C. Cuervo, Datives at Large (2003)
• A. Koontz-Garboden, Anticausativization (2009)
• C. Muñoz Pérez, Stylistic applicatives: A lens into the nature of anticausative SE (2026)

Clauses

structure MunozPerez2026.Clause : Type

A clause as the clitic system sees it.

• voice : Minimalist.Voice.Head

  The Voice head.

• heads : List Minimalist.LittleV

  The verbal heads below Voice, highest first.

• appl : Option Person.Category

  The bundle of the high applicative head, if the clause has an affected dative.

def MunozPerez2026.Clause.site (k : Clause) : Minimalist.ApplSite

The applicative head takes as its complement the result state where there is one, the affected applicative of [Cue03] the paper adopts for marked anticausatives, and the theme otherwise, as under an unmarked anticausative, which lacks the state.

Equations

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

def MunozPerez2026.marked (a : Option Person.Category) : Clause

A marked anticausative is a change and its result state under a Voice head that introduces no argument and asks for a specifier.

Equations

• MunozPerez2026.marked a = { voice := Minimalist.Voice.anticausative, heads := [Minimalist.LittleV.vGO, Minimalist.LittleV.vBE], appl := a }

def MunozPerez2026.unmarked (a : Option Person.Category) : Clause

An unmarked anticausative is a change alone, under a Voice head that asks for nothing.

Equations

• MunozPerez2026.unmarked a = { voice := Minimalist.Voice.middle, heads := [Minimalist.LittleV.vGO], appl := a }

theorem MunozPerez2026.site_marked_unmarked (a : Option Person.Category) : (marked a).site.Affected ∧ (unmarked a).site.Low

The applicative of a marked anticausative is affected, between the change and the state; that of an unmarked one is low, the rule's context failing.

theorem MunozPerez2026.not_hasSemantics (a : Option Person.Category) : ¬(marked a).voice.IsThematic ∧ ¬(unmarked a).voice.IsThematic

The Voice head of an anticausative has no meaning, marked or not, so the clitics that spell a clause out cannot change what it means.

The fission rule

def MunozPerez2026.IsFissionApplicable (c : Person.Category) : Prop

The bundle condition of the fission rule holds of an applicative head that is [+PART, +SING].

Equations

• MunozPerez2026.IsFissionApplicable c = (Person.Feature.participant ∈ c.toFeatures ∧ c.IsSingular)

@[instance_reducible]

instance MunozPerez2026.instDecidablePredCategoryIsFissionApplicable : DecidablePred IsFissionApplicable

Equations

• MunozPerez2026.instDecidablePredCategoryIsFissionApplicable x✝ = { decide := decide (Person.Feature.participant ∈ x✝.toFeatures) && decide x✝.IsSingular, reflects_decide := ⋯ }

theorem MunozPerez2026.isFissionApplicable_iff (c : Person.Category) : IsFissionApplicable c ↔ c = Person.Category.speaker ∨ c = Person.Category.addressee

The bundle condition singles out the speaker and the addressee, since a third person lacks [+PART] and a group lacks [+SING].

def MunozPerez2026.datives : Person.Category → Finset String

The dative clitics of a category. The form se that a third-person dative takes before an accusative clitic is left out, no accusative clitic being present.

Equations

• MunozPerez2026.datives = PersonalPronoun.paradigm (Spanish.Clitics.dative.erase Spanish.Clitics.se_dat)

def MunozPerez2026.applExponents (k : Clause) : Finset (List String)

The exponents of the applicative head. It is pronounced as a dative clitic of its category, and when the head sits between the change and the result state and is [+PART, +SING] it may instead split into that clitic and the inflectionless dative le.

Equations

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

The conditions at PF

def MunozPerez2026.IsReflexiveForm (f : String) : Prop

A form counts as a reflexive clitic at PF when the reflexive series has it, syncretic elements being indistinguishable there.

Equations

• MunozPerez2026.IsReflexiveForm f = ∃ p ∈ Spanish.Clitics.reflexive, p.form = f

@[instance_reducible]

instance MunozPerez2026.instDecidablePredStringIsReflexiveForm : DecidablePred IsReflexiveForm

Equations

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

def MunozPerez2026.RequiresMarker (v : Minimalist.Voice.Head) : Prop

A Voice head must be marked at PF when it introduces no argument and asks for a specifier.

Equations

• MunozPerez2026.RequiresMarker v = (¬v.IsThematic ∧ v.HasD)

@[instance_reducible]

instance MunozPerez2026.instDecidablePredHeadRequiresMarker : DecidablePred RequiresMarker

Equations

• MunozPerez2026.instDecidablePredHeadRequiresMarker x✝ = { decide := decide ¬x✝.IsThematic && decide x✝.HasD, reflects_decide := ⋯ }

def MunozPerez2026.markers (k : Clause) : Finset (Option String)

The markers the syntax may supply. A Voice head that asks for a specifier gets a reflexive or nothing, the feature being free to fail.

Equations

• MunozPerez2026.markers k = if MunozPerez2026.RequiresMarker k.voice then {none, some Spanish.Clitics.se.form} else {none}

def MunozPerez2026.Converges (marker : Option String) (appl : List String) : Prop

The clitics of a clause converge when Voice is marked by a reflexive clitic and the applicative head is pronounced. Without a marker from the syntax, an exponent of the applicative head that has the form of a reflexive can mark Voice, provided another exponent is left to pronounce the head.

Equations

• MunozPerez2026.Converges marker appl = (marker.isSome = true ∨ ∃ f ∈ appl, MunozPerez2026.IsReflexiveForm f ∧ appl.erase f ≠ [])

@[instance_reducible]

instance MunozPerez2026.instDecidableConverges (marker : Option String) (appl : List String) : Decidable (Converges marker appl)

Equations

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

def MunozPerez2026.clusters (k : Clause) : Finset (List String)

The clitic clusters a clause surfaces with.

Equations

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

The typology of realizations

theorem MunozPerez2026.clusters_marked (c : Person.Category) : clusters (marked (some c)) = Finset.image (fun (x : String) => ["se", x]) (datives c) ∪ if IsFissionApplicable c then Finset.image (fun (x : String) => ["se", x, "le"]) (datives c) ∪ Finset.image (fun (x : String) => [x, "le"]) (datives c) else ∅

A marked anticausative always has the marker with the plain dative. Where fission applies it also has the fissioned dative, with the marker and without it.

theorem MunozPerez2026.clusters_unmarked (c : Person.Category) : clusters (unmarked (some c)) = Finset.image (fun (x : String) => [x]) (datives c)

An unmarked anticausative has the plain dative alone.

theorem MunozPerez2026.clusters_none : clusters (marked none) = {["se"]} ∧ clusters (unmarked none) = {[]}

Without a dative, a marked anticausative has the marker and an unmarked one has nothing.

theorem MunozPerez2026.clusters_marked_speaker : clusters (marked (some Person.Category.speaker)) = {["se", "me"], ["se", "me", "le"], ["me", "le"]}

The three clusters of a first person singular dative.

theorem MunozPerez2026.marker_optional_iff (c : Person.Category) : (∃ l ∈ clusters (marked (some c)), "se" ∉ l) ↔ IsFissionApplicable c

The marker can be absent from a marked anticausative exactly where fission applies.

Why fission rescues the clause

theorem MunozPerez2026.isReflexiveForm_of_mem_datives {c : Person.Category} (hc : c.person ≠ Person.third) {f : String} (hf : f ∈ datives c) : IsReflexiveForm f

Outside the third person every dative clitic is a reflexive form, by the syncretism of the two series.

theorem MunozPerez2026.converges_of_fission {c : Person.Category} (hc : IsFissionApplicable c) {f : String} (hf : f ∈ datives c) : Converges none [f, Spanish.Clitics.le.form]

A fissioned head converges without a marker, since its first exponent marks Voice and le pronounces the head.

theorem MunozPerez2026.not_converges_singleton (f : String) : ¬Converges none [f]

An unfissioned dative does not converge without a marker, whatever its form. Taken as the marker of Voice it leaves the applicative head unpronounced.

theorem MunozPerez2026.not_isReflexiveForm_le : ¬IsReflexiveForm Spanish.Clitics.le.form

The second exponent le is not a reflexive form, so the marking comes from the first.

theorem MunozPerez2026.syncretic_not_isFissionApplicable : (∀ f ∈ datives Person.Category.speakerOthers, IsReflexiveForm f) ∧ ¬IsFissionApplicable Person.Category.speakerOthers

Syncretism with the reflexive does not suffice for a stylistic clitic. The first person plural nos is syncretic, and fission still skips it for want of [+SING].

The examples

def MunozPerez2026.verb? (e : Datum) : Option Spanish.Verbs.SpanishVerbEntry

The verb of an example, from the Fragment.

Equations

• MunozPerez2026.verb? e = (e.feature? "verb").bind fun (f : String) => List.find? (fun (x : Spanish.Verbs.SpanishVerbEntry) => decide (x.form = f)) Spanish.Verbs.allVerbs

def MunozPerez2026.appl? (e : Datum) : Option (Option Person.Category)

The bundle of the dative of an example, none where it has no dative.

Equations

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

def MunozPerez2026.clauses (a : Option Person.Category) : Spanish.Verbs.AnticausativeMarking → List Clause

The clauses a verb's intransitive has, by its marking.

Equations

• MunozPerez2026.clauses a Spanish.Verbs.AnticausativeMarking.marked = [MunozPerez2026.marked a]
• MunozPerez2026.clauses a Spanish.Verbs.AnticausativeMarking.unmarked = [MunozPerez2026.unmarked a]
• MunozPerez2026.clauses a Spanish.Verbs.AnticausativeMarking.optional = [MunozPerez2026.marked a, MunozPerez2026.unmarked a]

theorem MunozPerez2026.anticausative_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "anticausative" → ∃ v ∈ verb? e, ∃ a ∈ appl? e, ∃ s ∈ e.feature? "cluster", Judgment.marginal ≤ e.judgment ↔ ∃ m ∈ v.anticausativeMarking, ∃ k ∈ clauses a m, ∃ l ∈ clusters k, " ".intercalate l = s

An anticausative example is accepted exactly when its clitic cluster is one that a clause of its verb surfaces with. This covers the three synonymous clusters, the restriction to first and second person singular datives, the invariability of le, the ban on stylistic le with unmarked anticausatives, and the marking of anticausatives without a dative.

def MunozPerez2026.otherClause? (e : Datum) : Option Clause

The clause of an example that is not anticausative. Quejarse has an external argument and impersonal dar is an activity under an impersonal Voice head.

Equations

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

theorem MunozPerez2026.other_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "inherent" ∨ e.feature? "construction" = some "impersonal" → ∃ k ∈ otherClause? e, ∃ s ∈ e.feature? "cluster", Judgment.marginal ≤ e.judgment ↔ ∃ l ∈ applExponents k, " ".intercalate ("se" :: l) = s

Where se has another source and the clause is not inchoative, the applicative head has its plain exponent alone, so stylistic le is out.

theorem MunozPerez2026.causer_reading_rows (e : Datum) : e ∈ Examples.all → List.lookup "unintentional causer" e.readings = some Judgment.acceptable → ∃ a ∈ appl? e, ∃ s ∈ e.feature? "cluster", ∃ l ∈ clusters (marked a), " ".intercalate l = s

An example with the unintentional causer reading has a cluster of the marked clause. The cluster me le of hervir has the reading although it lacks se, since only the marked clause fissions.

Against a constraint on clitic clusters

theorem MunozPerez2026.isLicit_me_iff_nos (g : PCC.Grammar) : (∃ io ∈ Spanish.Clitics.le.person, ∃ do_ ∈ Spanish.Clitics.me_acc.person, PCC.IsLicit g { high := io, low := do_ }) ↔ ∃ io ∈ Spanish.Clitics.le.person, ∃ do_ ∈ Spanish.Clitics.nos_acc.person, PCC.IsLicit g { high := io, low := do_ }

A person case constraint sees the persons of the two clitics, and me and nos have the same person, so no such constraint separates me le from nos le.

theorem MunozPerez2026.weak_pcc_bans : ∃ io ∈ Spanish.Clitics.le.person, ∃ do_ ∈ Spanish.Clitics.me_acc.person, ¬PCC.IsLicit PCC.weakGrammar { high := io, low := do_ }

The weak constraint bans a third-person dative over a first-person accusative, as in the ditransitive examples, so it would ban stylistic me le as well.

theorem MunozPerez2026.fission_separates : IsFissionApplicable Person.Category.speaker ∧ ¬IsFissionApplicable Person.Category.speakerOthers

The fission rule does separate the two.

Against a null reflexive

On the reflexivization analysis of [KG09] extended with a null reflexive, every alternating verb has a reflexive in its anticausative, overt or silent, and an overt one is always possible.

def MunozPerez2026.seMarkedIfAlternating (v : Spanish.Verbs.SpanishVerbEntry) : Prop

The null-reflexive extension predicts that if a verb alternates, its intransitive can take the clitic.

Equations

• MunozPerez2026.seMarkedIfAlternating v = (v.Alternates → v.anticausativeMarking ≠ some Spanish.Verbs.AnticausativeMarking.unmarked)

theorem MunozPerez2026.not_seMarkedIfAlternating_mejorar : ¬seMarkedIfAlternating Spanish.Verbs.mejorar

mejorar alternates and rejects the clitic, against the prediction.