Svenonius (2004): Slavic Prefixes Inside and Outside VP

This file formalizes [Sve04]'s division of Slavic verbal prefixes into two classes by their place in a decomposed clause (2): a lexical prefix is the resultative R head inside the VP, like a Germanic verb particle ([dD95]), while a superlexical prefix is an Asp head above the VP with an adverbial, aspectual or quantificational meaning. The same prefix form serves either class, Russian za- spatial and idiomatic in (1a)–(1b) and inceptive in (1c), on the shared fragment morph. A prefix in a word is classified, PrefixClass, the superlexical case carrying its aspectual subtype, SuperlexicalSubtype, and an analysis pairs an attested example with its fragment stem and its classified prefix sequence, outermost first, Analysis, with the word-formation tree it determines, Analysis.tree. The structure is Structure: the Asp heads highest first and the optional R head over the stem, and a word's prefixes are its linearization, Structure.prefixes. Two generalizations follow from the structure. A superlexical prefix always appears outside a lexical one (4), WellStacked, Structure.wellStacked_prefixes, so the attested reversals (4b) and (4d) have no structure, reverse_4a_not_wellStacked, reverse_4c_not_wellStacked; and a VP has at most one lexical prefix, since it has one resultative position (4.4), Structure.lexicals_length_le_one. Together they characterize the linearizations: a prefix sequence is that of some structure exactly when it is well-stacked with at most one lexical prefix, Structure.exists_prefixes_eq_iff, and every analysis of the paper has one, analyses_structured. Among the diagnostics of superlexical prefixes (56), selection for an imperfective stem (56c) holds of the Russian analyses, superlexical_selects_imperfective; the Bulgarian stacks (3), from [Ist04], attach to the perfective razkaža.

Implementation notes

The subtypes are the glosses of (57)–(58) together with [Ist04]'s terminative and excessive, an open list. The secondary imperfective's scope (4.5), the argument-structure effects of lexical prefixes (4.3), and the phrasal-movement alternative of section 5 are not formalized; the classification of the examples is the paper's, and [Rom04] documents mismatches among the diagnostics.

References

• [Sve04]
• [Ist04]
• [dD95]
• [Rom04]

inductive Svenonius2004.SuperlexicalSubtype : Type

The aspectual subtypes of superlexical prefixes, the glosses of (57)–(58) with [Ist04]'s terminative and excessive.

• delimitative : SuperlexicalSubtype
• cumulative : SuperlexicalSubtype
• completive : SuperlexicalSubtype
• repetitive : SuperlexicalSubtype
• inceptive : SuperlexicalSubtype
• distributive : SuperlexicalSubtype
• attenuative : SuperlexicalSubtype
• terminative : SuperlexicalSubtype
• excessive : 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

The class of a prefix in a word: the R head or an Asp head with its subtype.

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

@[instance_reducible]

instance Svenonius2004.instDecidableEqPrefixClass : DecidableEq PrefixClass

Equations

• Svenonius2004.instDecidableEqPrefixClass = Svenonius2004.instDecidableEqPrefixClass.decEq

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 ⋯

def Svenonius2004.PrefixClass.IsSuperlexical : PrefixClass → Prop

A superlexical class.

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

theorem Svenonius2004.PrefixClass.not_isSuperlexical_iff (c : PrefixClass) : ¬c.IsSuperlexical ↔ c = lexical

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

A classified prefix sequence, outermost first, is well-stacked when no lexical prefix appears outside a superlexical one (4).

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

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

The lexical prefixes of a sequence.

Equations

• Svenonius2004.lexicals prefixes = List.filter (fun (x : Morphology.Morph × Svenonius2004.PrefixClass) => decide (x.2 = Svenonius2004.PrefixClass.lexical)) prefixes

The structure (2)

structure Svenonius2004.Structure : Type

The decomposed clause of (2): the superlexical prefixes are Asp heads above the VP, highest first, and a lexical prefix is the resultative R head below V, of which a VP has one position (4.4).

• outer : List (Morphology.Morph × SuperlexicalSubtype)

  The Asp heads, highest first.

• result : Option Morphology.Morph

  The R head.

• stem : Verb.Stem

  The verb.

def Svenonius2004.Structure.prefixes (s : Structure) : List (Morphology.Morph × PrefixClass)

The linearization: the Asp heads, then the R head, before the stem.

Equations

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

theorem Svenonius2004.Structure.wellStacked_prefixes (s : Structure) : WellStacked s.prefixes

The stacking generalization (4): a linearized structure is well-stacked.

theorem Svenonius2004.Structure.lexicals_length_le_one (s : Structure) : (lexicals s.prefixes).length ≤ 1

Structural uniqueness (4.4): a linearized structure has at most one lexical prefix.

theorem Svenonius2004.Structure.exists_prefixes_eq_iff (ps : List (Morphology.Morph × PrefixClass)) (st : Verb.Stem) : (∃ (s : Structure), s.stem = st ∧ s.prefixes = ps) ↔ WellStacked ps ∧ (lexicals ps).length ≤ 1

The linearizations of structures over a stem are exactly the well-stacked sequences with at most one lexical prefix.

structure Svenonius2004.Analysis : Type

An analysis of an attested example: the fragment stem it is built on and its classified prefix sequence, outermost first.

• ex : Datum

  The attested example.

• stem : Verb.Stem

  The fragment verb stem.

• prefixes : List (Morphology.Morph × PrefixClass)

  The 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.

The paper's analyses

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 (1a) 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) za-kuritj: superlexical inceptive za-.

Equations

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

def Svenonius2004.a58po : Analysis

(58) 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-.

Equations

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

def Svenonius2004.a3a : Analysis

(3a) po-na-razkaža, glossed 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, glossed CMPL-DSTR-CMLT-RPET, the deepest stack cited from [Ist04].

Equations

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

def Svenonius2004.analyses : List Analysis

The analyses.

Equations

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

Results

theorem Svenonius2004.analyses_structured (a : Analysis) (ha : a ∈ analyses) : ∃ (s : Structure), s.stem = a.stem ∧ s.prefixes = a.prefixes

Every analysis is well-stacked with at most one lexical prefix, so it is the linearization of a structure over its stem.

theorem Svenonius2004.reverse_4a_not_wellStacked : ¬WellStacked a4a.prefixes.reverse ∧ ¬∃ (s : Structure), s.stem = a4a.stem ∧ s.prefixes = a4a.prefixes.reverse

The attested reversal (4b) vy-po-brasyvatj, the ungrammatical alternative recorded with (4a), is not well-stacked, so no structure linearizes to it.

theorem Svenonius2004.reverse_4c_not_wellStacked : ¬WellStacked a4c.prefixes.reverse ∧ ¬∃ (s : Structure), s.stem = a4c.stem ∧ s.prefixes = 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 = Aspect.Perfectivity.imperfective

Diagnostic (56c) over the Russian analyses: a superlexically prefixed verb is built on an imperfective stem.