Svenonius (2004): Slavic Prefixes Inside and Outside VP

[Sve04] splits Slavic verbal prefixes into two classes: lexical prefixes are R-heads inside VP (resultative, particle-like, connecting to [dD95]'s treatment of Germanic verb particles), while superlexical prefixes are Asp-heads outside VP (aspectual operators). The same prefix realises either class — his §1 exx. (1a)/(1c) use Russian za- both ways, on the shared fragment morph Russian.Verbs.za. The classification is contested rather than consensus: [Rom04] documents diagnostic mismatches, and Tatevosov's later work posits an intermediate class.

The syntactic height cut named here is the same one Minimalist.AspFlavor (outer vs inner aspect, Travis/Cinque) carries for Sinitic split-aspect; the types are kept separate because the commitments differ (lexical = resultative R-head, not merely inner-Asp host).

Data flow: attested examples live in Data.Examples.Svenonius2004 (generated from JSON); prefix morphs and stems are fragment entries; an Analysis pairs an example with a stem and a classified prefix sequence — the classification is this paper's analytical act, applied to shared data, never a fragment field.

Main definitions

• SuperlexicalSubtype, PrefixClass, PrefixClass.IsSuperlexical — a selection of superlexical Aktionsart subtypes (his §4, and [Ist04]'s taxonomy; not a closed set), and the two-way class.
• Analysis — an attested example, its fragment stem, and its classified prefix sequence (outermost first), with derived word-formation tree.
• WellStacked — no lexical prefix outside a superlexical one (§1: "the superlexical prefix always appears outside the lexical prefix").
• analyses — this paper's classified examples (Russian, one Polish, two Bulgarian stacks cited from [Ist04]).

Main results

• analyses_wellStacked / reverse_4a_not_wellStacked — the stacking generalization holds across the analyses, and the attested ungrammatical reversal (4b) vy-po-brasyvatj violates it.
• superlexical_selects_imperfective — diagnostic (56c) (§4.1) over the Russian analyses: superlexical prefixes select imperfective stems. (Russian-scoped: his Bulgarian stacks attach to the quantized perfective razkaža, per [Ist04].)
• analyses_match_segmentation — for citation-form examples, the paper's hyphen segmentation equals the analysis' prefix-stem decomposition.

inductive Svenonius2004.SuperlexicalSubtype : Type

Aspectual subtypes of the superlexical class — the labels recurring in [Sve04] §4 (his Bulgarian ordering (57)) and in [Ist04]'s prefix-by-prefix taxonomy. A selection, not a closed set: excessive, terminative, and perdurative also occur in the literature.

• delimitative : SuperlexicalSubtype
• cumulative : SuperlexicalSubtype
• completive : SuperlexicalSubtype
• repetitive : SuperlexicalSubtype
• inceptive : SuperlexicalSubtype
• distributive : SuperlexicalSubtype
• attenuative : SuperlexicalSubtype

@[instance_reducible]

instance Svenonius2004.instDecidableEqSuperlexicalSubtype : DecidableEq SuperlexicalSubtype

Equations

• Svenonius2004.instDecidableEqSuperlexicalSubtype x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Svenonius2004.PrefixClass : Type

[Sve04]'s lexical / superlexical split as a single ADT — the superlexical case carries its subtype.

• lexical : PrefixClass
• superlexical (subtype : SuperlexicalSubtype) : PrefixClass

def Svenonius2004.instDecidableEqPrefixClass.decEq (x✝ x✝¹ : PrefixClass) : Decidable (x✝ = x✝¹)

Equations

• Svenonius2004.instDecidableEqPrefixClass.decEq Svenonius2004.PrefixClass.lexical Svenonius2004.PrefixClass.lexical = isTrue ⋯
• Svenonius2004.instDecidableEqPrefixClass.decEq Svenonius2004.PrefixClass.lexical (Svenonius2004.PrefixClass.superlexical subtype) = isFalse ⋯
• Svenonius2004.instDecidableEqPrefixClass.decEq (Svenonius2004.PrefixClass.superlexical subtype) Svenonius2004.PrefixClass.lexical = isFalse ⋯
• Svenonius2004.instDecidableEqPrefixClass.decEq (Svenonius2004.PrefixClass.superlexical a) (Svenonius2004.PrefixClass.superlexical b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Svenonius2004.instDecidableEqPrefixClass : DecidableEq PrefixClass

Equations

• Svenonius2004.instDecidableEqPrefixClass = Svenonius2004.instDecidableEqPrefixClass.decEq

def Svenonius2004.PrefixClass.IsSuperlexical : PrefixClass → Prop

A PrefixClass is superlexical iff it is the superlexical _ case.

Equations

• Svenonius2004.PrefixClass.lexical.IsSuperlexical = False
• (Svenonius2004.PrefixClass.superlexical subtype).IsSuperlexical = True

@[instance_reducible]

instance Svenonius2004.PrefixClass.instDecidablePredIsSuperlexical : DecidablePred IsSuperlexical

Equations

• Svenonius2004.PrefixClass.lexical.instDecidablePredIsSuperlexical = isFalse Svenonius2004.PrefixClass.instDecidablePredIsSuperlexical._proof_1
• (Svenonius2004.PrefixClass.superlexical subtype).instDecidablePredIsSuperlexical = isTrue trivial

def Svenonius2004.WellStacked (prefixes : List (Morphology.Morph × PrefixClass)) : Prop

A classified prefix sequence (surface order, outermost first) is well-stacked when no lexical prefix appears outside a superlexical one — [Sve04] §1: "the superlexical prefix always appears outside the lexical prefix".

Equations

• Svenonius2004.WellStacked prefixes = List.Pairwise (fun (outer inner : Morphology.Morph × Svenonius2004.PrefixClass) => inner.2.IsSuperlexical → outer.2.IsSuperlexical) prefixes

@[instance_reducible]

instance Svenonius2004.instDecidablePredListProdMorphPrefixClassWellStacked : DecidablePred WellStacked

Equations

• Svenonius2004.instDecidablePredListProdMorphPrefixClassWellStacked prefixes = Svenonius2004.instDecidablePredListProdMorphPrefixClassWellStacked._aux_1 prefixes

structure Svenonius2004.Analysis : Type

An analysis of an attested example: the fragment stem it is built on and its prefix sequence (outermost first), each prefix a fragment morph paired with this paper's class assignment.

• ex : Data.Examples.LinguisticExample

  The attested example (from Data.Examples).

• stem : Verb.Stem

  The fragment verb-stem entry.

• prefixes : List (Morphology.Morph × PrefixClass)

  Classified fragment prefix morphs, outermost first.

def Svenonius2004.Analysis.tree (a : Analysis) : Morphology.Word.Tree Morphology.Morph

The word-formation tree: the prefix morphs folded, innermost-last, over the stem root.

Equations

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

theorem Svenonius2004.Analysis.tree_isConcatenative (a : Analysis) : a.tree.IsConcatenative

Every analysis tree is concatenative: prefixation only.

def Svenonius2004.Analysis.MatchesSegmentation (a : Analysis) : Prop

The example's hyphen-segmented text equals the analysis' decomposition into prefix forms plus stem. Applicable to citation-form examples (not sentence examples or inflected tokens).

Equations

• a.MatchesSegmentation = (a.ex.primaryText = "-".intercalate (List.map (fun (x : Morphology.Morph × Svenonius2004.PrefixClass) => x.1.form) a.prefixes ++ [a.stem.form]))

@[instance_reducible]

instance Svenonius2004.Analysis.instDecidablePredMatchesSegmentation : DecidablePred MatchesSegmentation

Equations

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

The paper's analyses

Russian from §1 and §4.1; the Polish (4c) and the Bulgarian stacks (3a), (3e) as he classifies them (for (3a) [Ist04]'s own finer taxonomy diverges — her attenuative po- — see Studies/Istratkova2004.lean).

def Svenonius2004.a1a : Analysis

(1a) za-brosil — lexical spatial za- on perfective brositj.

Equations

• Svenonius2004.a1a = { ex := Svenonius2004.Examples.ex_1a, stem := Russian.Verbs.brosit, prefixes := [(Russian.Verbs.za, Svenonius2004.PrefixClass.lexical)] }

def Svenonius2004.a1b : Analysis

(1b) za-brosil 'gave up' — the same lexical za-, idiomatic.

Equations

• Svenonius2004.a1b = { ex := Svenonius2004.Examples.ex_1b, stem := Russian.Verbs.brosit, prefixes := [(Russian.Verbs.za, Svenonius2004.PrefixClass.lexical)] }

def Svenonius2004.a1c : Analysis

(1c) za-brosal — superlexical inceptive za- on imperfective brosatj: the minimal pair with a1a on the same fragment morph.

Equations

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

def Svenonius2004.a4a : Analysis

(4a) po-vy-brasyvatj — superlexical distributive po- outside lexical vy- on the secondary-imperfective stem.

Equations

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

def Svenonius2004.a58za : Analysis

(58) discussion: za-kuritj — superlexical inceptive za-.

Equations

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

def Svenonius2004.a58po : Analysis

(58) discussion: po-čitatj — superlexical attenuative po-.

Equations

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

def Svenonius2004.russianAnalyses : List Analysis

The Russian analyses.

Equations

• Svenonius2004.russianAnalyses = [Svenonius2004.a1a, Svenonius2004.a1b, Svenonius2004.a1c, Svenonius2004.a4a, Svenonius2004.a58za, Svenonius2004.a58po]

def Svenonius2004.a4c : Analysis

(4c) po-w-chodzili — superlexical distributive po- outside lexical w- (Polish counterpart of a4a).

Equations

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

def Svenonius2004.a3a : Analysis

(3a) po-na-razkaža — his gloss DLMT-CMLT on perfective razkaža.

Equations

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

def Svenonius2004.a3e : Analysis

(3e) iz-po-na-pre-razkaža — his gloss CMPL-DSTR-CMLT-RPET, the deepest stack he cites from [Ist04].

Equations

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

def Svenonius2004.analyses : List Analysis

All analyses of this study.

Equations

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

Results

theorem Svenonius2004.analyses_wellStacked (a : Analysis) (ha : a ∈ analyses) : WellStacked a.prefixes

Every analysis is well-stacked.

theorem Svenonius2004.reverse_4a_not_wellStacked : ¬WellStacked a4a.prefixes.reverse

The attested ungrammatical reversal (4b) vy-po-brasyvatj (recorded as the alternatives of (4a)) violates well-stackedness: it would put the lexical prefix outside the superlexical one.

theorem Svenonius2004.reverse_4c_not_wellStacked : ¬WellStacked a4c.prefixes.reverse

Likewise the Polish reversal (4d) w-po-chodzili.

theorem Svenonius2004.superlexical_selects_imperfective (a : Analysis) (ha : a ∈ russianAnalyses) (hs : ∃ p ∈ a.prefixes, p.2.IsSuperlexical) : a.stem.perfectivity = Semantics.Aspect.Perfectivity.imperfective

Diagnostic (56c) (§4.1) over the Russian analyses: a superlexically prefixed verb is built on an imperfective stem. Russian-scoped: his Bulgarian stacks attach to the quantized perfective razkaža ([Ist04]), so (56c) is not a Bulgarian diagnostic.

theorem Svenonius2004.analyses_match_segmentation (a : Analysis) (ha : a ∈ [a4a, a58za, a58po, a3a, a3e]) : a.MatchesSegmentation

For the citation-form examples, the paper's hyphen segmentation equals the analysis' decomposition. (Sentence examples (1a)-(1c) and the inflected Polish token (4c) are excluded.)