Jabłońska (2004): When the Prefixes Meet the Suffixes

This file formalizes [Jab04], the account of the readings of the Polish prefix po- as a function of the verbalizer it attaches to. The verbalizer classes of Table 1 and Table 2 (Verbalizer) each carry an Aktionsart profile (Verbalizer.profile) and a continuum for po- to measure along, (40): the run time of a process, the scale of a gradable property, (16), or a path, (55). A derivation stacks the four prefix positions of (41) and the Secondary Imperfective as layers (Layer) over a stem, each merging only when its selectional requirement is met (Layer.merge), and well-formedness (WellFormed) and perfectivity (Perfective) are read off the resulting profile. The seven shapes of a well-formed derivation (wellFormed_iff) yield the paper's generalizations: stacking is contingent on the Secondary Imperfective (si_of_asp3), a purely perfectivizing prefix stacks with nothing (eq_of_perf), only the interval-denoting classes form Secondary Imperfectives (denotesInterval_of_si), and the stacking generalization of [Sve04] follows (wellStacked). The readings of po- follow from the continuum and the boundaries of the stem (Asp1Reading, Asp3Reading) and reproduce Table 2 (asp1Reading_iff_table2). The attested forms are analysed (attested) and the starred ones excluded (starred_not_wellFormed).

Implementation notes

• The Aktionsart profile of a bare stem is atelic throughout, the paper's unbounded bare stem; the semelfactive is the punctual class and the stative the non-dynamic one. The continuum, the telos and the adjectival base are the paper's own parameters.
• The semelfactive suffix values [uPerf] against Asp1, (47): a bare semelfactive is perfective, and a purely perfectivizing prefix over it is a vacuous viewpoint shift, (70), which Table 2 hedges as "yes ???" (wellFormed_perf_iff). A lexical prefix on a semelfactive stays possible in principle, (79a) and fn. 20.
• With directed motion stems the purely perfectivizing position is filled by do- or przy-, Table 2 fn. c; the model records these stems as lacking a telos of their own.
• The "considerable change" reading is confined to -ej- stems: fn. 22 records that inchoative -n- stems lack it without deriving the gap. The inceptive za- of (53) reads an -ej- stem as a state and is recorded as a row only.

References

• [Jab04]
• [Sve04]
• [DUE00]
• [Rot04]

Verbalizers

inductive Jablonska2004.Verbalizer : Type

The verbalizer classes of Table 1 and Table 2.

• processual : Verbalizer

  The high processual verbalizers -i/y- and -aj-, with root insertion inside ν.

• semelfactive : Verbalizer

  The high instantaneous verbalizer, semelfactive -n-.

• degree : Verbalizer

  The low verbalizer -ej-: a degree achievement over an adjectival base, (2b).

• inchoative : Verbalizer

  The low inchoative verbalizer -n-, (2a).

• directedMotion : Verbalizer

  A directed-motion stem, measuring movement along a path, (55).

• nonDirectedMotion : Verbalizer

  A non-directed-motion stem, a high processual verbalizer, (49).

• stative : Verbalizer

  A stative stem.

@[instance_reducible]

instance Jablonska2004.instDecidableEqVerbalizer : DecidableEq Verbalizer

Equations

• Jablonska2004.instDecidableEqVerbalizer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Jablonska2004.Continuum : Type

The continuum along which po- measures development, (40).

• temporal : Continuum
• degree : Continuum
• path : Continuum

@[instance_reducible]

instance Jablonska2004.instDecidableEqContinuum : DecidableEq Continuum

Equations

• Jablonska2004.instDecidableEqContinuum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jablonska2004.Verbalizer.profile : Verbalizer → Aspect.VendlerClass

The Aktionsart profile of a bare stem: atelic, lacking a right boundary, Section 2.3; punctual for the semelfactive, Section 2.3.1; stative for the statives, which lack a left boundary, Section 5.

Equations

• Jablonska2004.Verbalizer.semelfactive.profile = Aspect.VendlerClass.semelfactive
• Jablonska2004.Verbalizer.stative.profile = Aspect.VendlerClass.state
• x✝.profile = Aspect.VendlerClass.activity

def Jablonska2004.Verbalizer.continuum : Verbalizer → Option Continuum

The continuum a verbalizer supplies; a semelfactive is a point and supplies none.

Equations

• Jablonska2004.Verbalizer.processual.continuum = some Jablonska2004.Continuum.temporal
• Jablonska2004.Verbalizer.nonDirectedMotion.continuum = some Jablonska2004.Continuum.temporal
• Jablonska2004.Verbalizer.stative.continuum = some Jablonska2004.Continuum.temporal
• Jablonska2004.Verbalizer.degree.continuum = some Jablonska2004.Continuum.degree
• Jablonska2004.Verbalizer.inchoative.continuum = some Jablonska2004.Continuum.degree
• Jablonska2004.Verbalizer.directedMotion.continuum = some Jablonska2004.Continuum.path
• Jablonska2004.Verbalizer.semelfactive.continuum = none

def Jablonska2004.Verbalizer.IsPunctual (v : Verbalizer) : Prop

Punctual: no continuum to measure along, (45).

Equations

• v.IsPunctual = (v.profile.duration = Aspect.Duration.punctual)

@[instance_reducible]

instance Jablonska2004.Verbalizer.instDecidablePredIsPunctual : DecidablePred IsPunctual

Equations

• v.instDecidablePredIsPunctual = Jablonska2004.Verbalizer.instDecidablePredIsPunctual._aux_1 v

def Jablonska2004.Verbalizer.HasLeftBoundary (v : Verbalizer) : Prop

Dynamic eventualities come with a left boundary, the preceding state at which the event does not hold, Section 2.3; states do not.

Equations

• v.HasLeftBoundary = (v.profile.dynamicity = Aspect.Dynamicity.dynamic)

@[instance_reducible]

instance Jablonska2004.Verbalizer.instDecidablePredHasLeftBoundary : DecidablePred HasLeftBoundary

Equations

• v.instDecidablePredHasLeftBoundary = Jablonska2004.Verbalizer.instDecidablePredHasLeftBoundary._aux_1 v

def Jablonska2004.Verbalizer.HasTelos (v : Verbalizer) : Prop

A natural telos for a purely perfectivizing prefix to coincide with, (10): the end of the scale of a gradable property, or the change of state of the affected object of a processual verb, Section 2.2.

Equations

• v.HasTelos = (v = Jablonska2004.Verbalizer.processual ∨ v = Jablonska2004.Verbalizer.degree ∨ v = Jablonska2004.Verbalizer.inchoative)

@[instance_reducible]

instance Jablonska2004.Verbalizer.instDecidablePredHasTelos : DecidablePred HasTelos

Equations

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

def Jablonska2004.Verbalizer.IsAdjectival (v : Verbalizer) : Prop

An adjectival base in the derivational history, (2b) and (72): no Result phrase.

Equations

• v.IsAdjectival = (v = Jablonska2004.Verbalizer.degree)

@[instance_reducible]

instance Jablonska2004.Verbalizer.instDecidablePredIsAdjectival : DecidablePred IsAdjectival

Equations

• v.instDecidablePredIsAdjectival = Jablonska2004.Verbalizer.instDecidablePredIsAdjectival._aux_1 v

def Jablonska2004.Verbalizer.DenotesInterval (v : Verbalizer) : Prop

Denotes a delimitable interval, the selectional requirement of the Secondary Imperfective, (66): a temporal continuum and a left boundary.

Equations

• v.DenotesInterval = (v.continuum = some Jablonska2004.Continuum.temporal ∧ v.HasLeftBoundary)

@[instance_reducible]

instance Jablonska2004.Verbalizer.instDecidablePredDenotesInterval : DecidablePred DenotesInterval

Equations

• v.instDecidablePredDenotesInterval = { decide := decide (v.continuum = some Jablonska2004.Continuum.temporal) && decide v.HasLeftBoundary, reflects_decide := ⋯ }

@[simp]

theorem Jablonska2004.Verbalizer.isPunctual_iff (v : Verbalizer) : v.IsPunctual ↔ v = semelfactive

@[simp]

theorem Jablonska2004.Verbalizer.hasLeftBoundary_iff (v : Verbalizer) : v.HasLeftBoundary ↔ v ≠ stative

@[simp]

theorem Jablonska2004.Verbalizer.isAdjectival_iff (v : Verbalizer) : v.IsAdjectival ↔ v = degree

@[simp]

theorem Jablonska2004.Verbalizer.hasTelos_iff (v : Verbalizer) : v.HasTelos ↔ v = processual ∨ v = degree ∨ v = inchoative

@[simp]

theorem Jablonska2004.Verbalizer.denotesInterval_iff (v : Verbalizer) : v.DenotesInterval ↔ v = processual ∨ v = nonDirectedMotion

Aspectual layers

inductive Jablonska2004.Level : Type

The aspectual level reached by a derivation, (41).

• root : Level
• asp1 : Level
• asp2 : Level
• asp3 : Level

@[instance_reducible]

instance Jablonska2004.instDecidableEqLevel : DecidableEq Level

Equations

• Jablonska2004.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Jablonska2004.Profile : Type

The aspectual profile of the predicate built so far: the highest projection merged; whether it is [+Perf], bounded by a Reference Time AFTER its Event Time; and whether its delimited subevents are changes of state of their participants, the contribution of a lexical prefix, (30), so that iterated subevents can overlap and be S-summed, (36) and (37).

• level : Level
• bounded : Bool
• resultative : Bool

@[instance_reducible]

instance Jablonska2004.instDecidableEqProfile : DecidableEq Profile

Equations

• Jablonska2004.instDecidableEqProfile = Jablonska2004.instDecidableEqProfile.decEq

def Jablonska2004.instDecidableEqProfile.decEq (x✝ x✝¹ : Profile) : Decidable (x✝ = x✝¹)

Equations

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

inductive Jablonska2004.Layer : Type

The four prefix positions of (41) and the Secondary Imperfective.

• lexical (m : Morphology.Morph) : Layer

  A lexical prefix in the complement of RP, valuing [uPerf] against Asp1.

• asp1 (m : Morphology.Morph) : Layer

  A superlexical prefix in Spec,Asp1P, a Reference Time AFTER the Event Time, (40).

• perf (m : Morphology.Morph) : Layer

  A purely perfectivizing prefix in Spec,Asp2P, (68).

• si : Layer

  The Secondary Imperfective, Asp2 with the semantics WITHIN or OUTSIDE, (66).

• asp3 (m : Morphology.Morph) : Layer

  po- in Spec,Asp3P, above the Secondary Imperfective, (26).

@[instance_reducible]

instance Jablonska2004.instDecidableEqLayer : DecidableEq Layer

Equations

• Jablonska2004.instDecidableEqLayer = Jablonska2004.instDecidableEqLayer.decEq

def Jablonska2004.instDecidableEqLayer.decEq (x✝ x✝¹ : Layer) : Decidable (x✝ = x✝¹)

Equations

• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.lexical a) (Jablonska2004.Layer.lexical b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.lexical m) (Jablonska2004.Layer.asp1 m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.lexical m) (Jablonska2004.Layer.perf m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.lexical m) Jablonska2004.Layer.si = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.lexical m) (Jablonska2004.Layer.asp3 m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp1 m) (Jablonska2004.Layer.lexical m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp1 a) (Jablonska2004.Layer.asp1 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp1 m) (Jablonska2004.Layer.perf m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp1 m) Jablonska2004.Layer.si = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp1 m) (Jablonska2004.Layer.asp3 m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.perf m) (Jablonska2004.Layer.lexical m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.perf m) (Jablonska2004.Layer.asp1 m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.perf a) (Jablonska2004.Layer.perf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.perf m) Jablonska2004.Layer.si = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.perf m) (Jablonska2004.Layer.asp3 m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq Jablonska2004.Layer.si (Jablonska2004.Layer.lexical m) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq Jablonska2004.Layer.si (Jablonska2004.Layer.asp1 m) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq Jablonska2004.Layer.si (Jablonska2004.Layer.perf m) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq Jablonska2004.Layer.si Jablonska2004.Layer.si = isTrue ⋯
• Jablonska2004.instDecidableEqLayer.decEq Jablonska2004.Layer.si (Jablonska2004.Layer.asp3 m) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp3 m) (Jablonska2004.Layer.lexical m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp3 m) (Jablonska2004.Layer.asp1 m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp3 m) (Jablonska2004.Layer.perf m_1) = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp3 m) Jablonska2004.Layer.si = isFalse ⋯
• Jablonska2004.instDecidableEqLayer.decEq (Jablonska2004.Layer.asp3 a) (Jablonska2004.Layer.asp3 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Jablonska2004.Layer.merge (v : Verbalizer) : Layer → Profile → Option Profile

Merging a layer over a bare stem of class v with profile p, when the layer's selectional requirement is met. A lexical prefix needs a Result phrase, (72); po- in Asp1 needs a continuum, (40); both value [uPerf] against Asp1 and cannot co-occur, (42). A purely perfectivizing prefix in Asp2 needs a telos and an unbounded predicate, since a second Reference Time AFTER the first is a vacuous viewpoint shift, (70), which also bars it from a semelfactive, (47). The Secondary Imperfective selects a delimited interval, (32) and (66), in the Asp2 slot, (68). po- in Asp3 selects a [-Perf] predicate, (25), whose iterated subevents are S-summable, (36), which requires each to be a change of state of its participant, (37) and (61).

Equations

• One or more equations did not get rendered due to their size.
• Jablonska2004.Layer.merge v x✝¹ x✝ = none

def Jablonska2004.Layer.prefix? : Layer → Option Morphology.Morph

The prefix morph of a layer.

Equations

• (Jablonska2004.Layer.lexical m).prefix? = some m
• (Jablonska2004.Layer.asp1 m).prefix? = some m
• (Jablonska2004.Layer.perf m).prefix? = some m
• (Jablonska2004.Layer.asp3 m).prefix? = some m
• Jablonska2004.Layer.si.prefix? = none

def Jablonska2004.Layer.IsLexical : Layer → Prop

A lexical prefix.

Equations

• (Jablonska2004.Layer.lexical m).IsLexical = True
• x✝.IsLexical = False

@[instance_reducible]

instance Jablonska2004.Layer.instDecidablePredIsLexical : DecidablePred IsLexical

Equations

• (Jablonska2004.Layer.lexical m).instDecidablePredIsLexical = isTrue trivial
• (Jablonska2004.Layer.asp1 m).instDecidablePredIsLexical = isFalse ⋯
• (Jablonska2004.Layer.perf m).instDecidablePredIsLexical = isFalse ⋯
• Jablonska2004.Layer.si.instDecidablePredIsLexical = isFalse Jablonska2004.Layer.instDecidablePredIsLexical._proof_3
• (Jablonska2004.Layer.asp3 m).instDecidablePredIsLexical = isFalse ⋯

Derivations

def Jablonska2004.profileFrom (v : Verbalizer) : Profile → List Layer → Option Profile

The profile after merging the layers ls, innermost first, over profile p.

Equations

• Jablonska2004.profileFrom v x✝ [] = some x✝
• Jablonska2004.profileFrom v x✝ (l :: ls) = (Jablonska2004.Layer.merge v l x✝).bind fun (x : Jablonska2004.Profile) => Jablonska2004.profileFrom v x ls

def Jablonska2004.profile (v : Verbalizer) (ls : List Layer) : Option Profile

The profile of a derivation over a bare stem of class v.

Equations

• Jablonska2004.profile v ls = Jablonska2004.profileFrom v { level := Jablonska2004.Level.root, bounded := false, resultative := false } ls

def Jablonska2004.WellFormed (v : Verbalizer) (ls : List Layer) : Prop

A derivation is well-formed when every layer's selectional requirement is met.

Equations

• Jablonska2004.WellFormed v ls = ((Jablonska2004.profile v ls).isSome = true)

@[instance_reducible]

instance Jablonska2004.instDecidableWellFormed (v : Verbalizer) (ls : List Layer) : Decidable (WellFormed v ls)

Equations

• Jablonska2004.instDecidableWellFormed v ls = Jablonska2004.instDecidableWellFormed._aux_1 v ls

def Jablonska2004.Perfective (v : Verbalizer) (ls : List Layer) : Prop

The derived predicate is [+Perf]: bounded by a Reference Time, or a bare semelfactive, whose suffix values [uPerf] against Asp1, (47). It is then no complement of a phasal verb and has no present-tense interpretation, the tests of Section 2.1.

Equations

• Jablonska2004.Perfective v ls = match Jablonska2004.profile v ls with | some p => p.bounded = true ∨ v.IsPunctual | none => False

@[instance_reducible]

instance Jablonska2004.instDecidablePerfective (v : Verbalizer) (ls : List Layer) : Decidable (Perfective v ls)

Equations

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

theorem Jablonska2004.wellFormed_iff {v : Verbalizer} {ls : List Layer} : WellFormed v ls ↔ ls = [] ∨ (∃ (m : Morphology.Morph), ls = [Layer.lexical m] ∧ ¬v.IsAdjectival) ∨ (∃ (m : Morphology.Morph), ls = [Layer.asp1 m] ∧ ¬v.IsPunctual) ∨ (∃ (m : Morphology.Morph), ls = [Layer.perf m] ∧ ¬v.IsPunctual ∧ v.HasTelos) ∨ (∃ (m : Morphology.Morph), ls = [Layer.lexical m, Layer.si] ∧ ¬v.IsAdjectival ∧ v.DenotesInterval) ∨ (∃ (m : Morphology.Morph), ls = [Layer.asp1 m, Layer.si] ∧ ¬v.IsPunctual ∧ v.DenotesInterval) ∨ ∃ (m : Morphology.Morph) (m' : Morphology.Morph), ls = [Layer.lexical m, Layer.si, Layer.asp3 m'] ∧ ¬v.IsAdjectival ∧ v.DenotesInterval

The seven shapes of a well-formed derivation: a bare stem; a lexical prefix, (30); po- in Asp1, (27); a purely perfectivizing prefix, (67); a lexically prefixed or Asp1-delimited stem under the Secondary Imperfective, (31a) and (56); and po- in Asp3 over a lexically prefixed Secondary Imperfective, (34).

The paper's generalizations

theorem Jablonska2004.perfective_nil_iff {v : Verbalizer} : Perfective v [] ↔ v.IsPunctual

A bare stem is perfective exactly when it is a semelfactive, (46).

theorem Jablonska2004.si_of_asp3 {v : Verbalizer} {ls : List Layer} {m : Morphology.Morph} (h : WellFormed v ls) (hm : Layer.asp3 m ∈ ls) : ∃ (m' : Morphology.Morph), ls = [Layer.lexical m', Layer.si, Layer.asp3 m]

Stacking is contingent on the Secondary Imperfective, Section 5: po- in Asp3 stacks only over a secondary imperfective, (24) and (42), and never over an attenuative-frequentative, (61).

theorem Jablonska2004.eq_of_perf {v : Verbalizer} {ls : List Layer} {m : Morphology.Morph} (h : WellFormed v ls) (hm : Layer.perf m ∈ ls) : ls = [Layer.perf m]

A purely perfectivizing prefix stacks on nothing and nothing stacks on it, (70): it is in complementary distribution with the Secondary Imperfective, (67), (69) and (68).

theorem Jablonska2004.denotesInterval_of_si {v : Verbalizer} {ls : List Layer} (h : WellFormed v ls) (hm : Layer.si ∈ ls) : v.DenotesInterval

Only the interval-denoting classes, the processual and the non-directed motion stems, form Secondary Imperfectives: not the degree achievements, (59) and (74), the inchoatives, (76), the semelfactives, (48) and (79b), the directed motion stems, (80), or the statives.

theorem Jablonska2004.not_lexical_and_asp1 {v : Verbalizer} {ls : List Layer} {m m' : Morphology.Morph} (h : WellFormed v ls) : ¬(Layer.lexical m ∈ ls ∧ Layer.asp1 m' ∈ ls)

A lexical prefix and po- in Asp1 both value [uPerf] against Asp1, so they do not co-occur, (42): no Multiple Agree.

theorem Jablonska2004.perfective_of_asp3 {v : Verbalizer} {ls : List Layer} {m : Morphology.Morph} (h : WellFormed v ls) (hm : Layer.asp3 m ∈ ls) : Perfective v ls

po- in Asp3 makes the derivation perfective, (33).

theorem Jablonska2004.not_perfective_of_getLast_si {v : Verbalizer} {ls : List Layer} (h : WellFormed v ls) (hl : ls.getLast? = some Layer.si) : ¬Perfective v ls

A derivation closed by the Secondary Imperfective is imperfective: the attenuative-frequentative forms, (56) and (64), are imperfectives, and Asp3 po- selects for [-Perf], (25).

theorem Jablonska2004.wellStacked {v : Verbalizer} {ls : List Layer} (h : WellFormed v ls) (f : Layer → Svenonius2004.PrefixClass) (hf : ∀ (l : Layer), (f l).IsSuperlexical ↔ ¬l.IsLexical) : Svenonius2004.WellStacked (List.filterMap (fun (l : Layer) => Option.map (fun (x : Morphology.Morph) => (x, f l)) l.prefix?) ls.reverse)

The prefix sequence of a derivation, outermost first, under any classification f that agrees with the lexical/superlexical split, is well-stacked in the sense of [Sve04]: the superlexical prefix is always outside the lexical one.

Table 2

theorem Jablonska2004.wellFormed_perf_iff (v : Verbalizer) (m : Morphology.Morph) : WellFormed v [Layer.perf m] ↔ v = Verbalizer.processual ∨ v = Verbalizer.degree ∨ v = Verbalizer.inchoative

Table 2, Asp2: a purely perfectivizing prefix needs a telos, (10) and (67), which the motion stems and the statives lack, and an unbounded stem, which the semelfactive is not, (47): the cell Table 2 hedges as "yes ???" is closed.

theorem Jablonska2004.wellFormed_lexical_si_iff (v : Verbalizer) (m : Morphology.Morph) : WellFormed v [Layer.lexical m, Layer.si] ↔ v = Verbalizer.processual ∨ v = Verbalizer.nonDirectedMotion

Table 2, the Secondary Imperfective: the processual and non-directed motion stems, which are also the classes on which po- stacks in Asp3, (43) and (83).

Readings

inductive Jablonska2004.Reading : Type

The readings of superlexical po-.

• delimitative : Reading

  'for a while': an arbitrary Reference Time, short of any telos, (12) and (27).

• considerableChange : Reading

  A degree of change short of the end of the scale, (11) and (22).

• centrifugal : Reading

  'away': ground covered along the path, (50).

• distributive : Reading

  A Reference Time after the last of the S-summed subevents, one per atom of the plural internal argument, each reaching its telos, (23) and (28).

• inceptive : Reading

  A Reference Time BEFORE the Event Time, fixing the missing left boundary of a state, (54).

@[instance_reducible]

instance Jablonska2004.instDecidableEqReading : DecidableEq Reading

Equations

• Jablonska2004.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jablonska2004.Asp1Reading (v : Verbalizer) (plural : Bool) : Reading → Prop

The readings of po- in Spec,Asp1P on a stem of class v, plural the plurality of the internal argument: the reading measures along the stem's continuum, (40); the distributive reading S-sums one subevent per atom of a plural internal argument, each with its telos, (36); and the inceptive reading fixes a left boundary the stem lacks, Section 2.4.

Equations

• Jablonska2004.Asp1Reading v plural Jablonska2004.Reading.delimitative = (v.continuum = some Jablonska2004.Continuum.temporal)
• Jablonska2004.Asp1Reading v plural Jablonska2004.Reading.considerableChange = (v = Jablonska2004.Verbalizer.degree)
• Jablonska2004.Asp1Reading v plural Jablonska2004.Reading.centrifugal = (v.continuum = some Jablonska2004.Continuum.path)
• Jablonska2004.Asp1Reading v plural Jablonska2004.Reading.distributive = (plural = true ∧ v.HasTelos)
• Jablonska2004.Asp1Reading v plural Jablonska2004.Reading.inceptive = ¬v.HasLeftBoundary

@[instance_reducible]

instance Jablonska2004.instDecidablePredReadingAsp1Reading (v : Verbalizer) (plural : Bool) : DecidablePred (Asp1Reading v plural)

Equations

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

def Jablonska2004.Asp3Reading (plural : Bool) : Reading → Prop

The readings of po- in Spec,Asp3P, (34): delimitative when the third Reference Time falls WITHIN the inherited first one, distributive when it follows the last iterated subevent, which needs a plural internal argument, (28e).

Equations

• Jablonska2004.Asp3Reading plural Jablonska2004.Reading.delimitative = True
• Jablonska2004.Asp3Reading plural Jablonska2004.Reading.distributive = (plural = true)
• Jablonska2004.Asp3Reading plural x✝ = False

@[instance_reducible]

instance Jablonska2004.instDecidablePredReadingAsp3Reading (plural : Bool) : DecidablePred (Asp3Reading plural)

Equations

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

def Jablonska2004.table2Asp1 : Verbalizer → List Reading

The Asp1 column of Table 2.

Equations

• Jablonska2004.table2Asp1 Jablonska2004.Verbalizer.processual = [Jablonska2004.Reading.delimitative, Jablonska2004.Reading.distributive]
• Jablonska2004.table2Asp1 Jablonska2004.Verbalizer.semelfactive = []
• Jablonska2004.table2Asp1 Jablonska2004.Verbalizer.degree = [Jablonska2004.Reading.distributive, Jablonska2004.Reading.considerableChange]
• Jablonska2004.table2Asp1 Jablonska2004.Verbalizer.inchoative = [Jablonska2004.Reading.distributive]
• Jablonska2004.table2Asp1 Jablonska2004.Verbalizer.directedMotion = [Jablonska2004.Reading.centrifugal]
• Jablonska2004.table2Asp1 Jablonska2004.Verbalizer.nonDirectedMotion = [Jablonska2004.Reading.delimitative]
• Jablonska2004.table2Asp1 Jablonska2004.Verbalizer.stative = [Jablonska2004.Reading.inceptive, Jablonska2004.Reading.delimitative]

theorem Jablonska2004.asp1Reading_iff_table2 (v : Verbalizer) (r : Reading) : Asp1Reading v true r ↔ r ∈ table2Asp1 v

The derived readings of po- in Asp1, with a plural internal argument, are those of Table 2: no delimitative reading with the change-of-state stems, Section 5, and the inceptive reading only with the statives, Section 2.4.

theorem Jablonska2004.not_asp1Reading_distributive (v : Verbalizer) : ¬Asp1Reading v false Reading.distributive

Without a plural internal argument the distributive reading is gone: (28c) has only the delimitative reading, the external argument being outside the scope of po-, (29).

The paper's analyses

structure Jablonska2004.Analysis : Type

An analysis of an attested form: the fragment stem, its verbalizer class, the layers innermost first, the plurality of the internal argument, and the paper's readings of the superlexical po-, if any.

• ex : Datum
• stem : Verb.Stem
• verbalizer : Verbalizer
• layers : List Layer
• plural : Bool
• readings : List Reading

def Jablonska2004.Analysis.Available (a : Analysis) (r : Reading) : Prop

The reading is available to the superlexical po- of the analysis, at Asp3 when the derivation is closed by po- there and at Asp1 otherwise.

Equations

• a.Available r = match a.layers.getLast? with | some (Jablonska2004.Layer.asp3 m) => Jablonska2004.Asp3Reading a.plural r | x => Jablonska2004.Asp1Reading a.verbalizer a.plural r

@[instance_reducible]

instance Jablonska2004.instDecidableAvailable (a : Analysis) (r : Reading) : Decidable (a.Available r)

Equations

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

def Jablonska2004.attested : List Analysis

The attested forms: the degree achievements of (10) and (23), the processual stems of (24), (27), (28), (30), (31), (34) and (43), the inchoatives of (39), the semelfactive of (46), the motion stems of (50), (51) and (80), the statives of (54) and fn. 21, the attenuative-frequentatives of (56) and (65), the purely perfectivized stems of (67), (69) and (75), the class shift of (77), the lexically prefixed semelfactive of (79) and the lexical po- of (81) to (83).

Equations

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

def Jablonska2004.starred : List Analysis

The starred forms: po- in Asp3 over a perfective, (24b) and (42); the Secondary Imperfective of a bare stem, (32), of a semelfactive, (48) and (79b), of a purely perfectivized stem, (67), (69), (73) and (78), of a degree achievement, (74), and of an inchoative, (76); po- on a semelfactive, (45) and (63b); and po- over an attenuative-frequentative, (61).

Equations

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

theorem Jablonska2004.attested_wellFormed (a : Analysis) : a ∈ attested → WellFormed a.verbalizer a.layers

Every attested form is a well-formed derivation.

theorem Jablonska2004.starred_not_wellFormed (a : Analysis) : a ∈ starred → ¬WellFormed a.verbalizer a.layers

Every starred form is excluded.

theorem Jablonska2004.attested_readings (a : Analysis) : a ∈ attested → ∀ r ∈ a.readings, a.Available r

The paper's readings of po- are the derived ones.

theorem Jablonska2004.attested_stem_perfectivity (a : Analysis) : a ∈ attested → (a.stem.perfectivity = Aspect.Perfectivity.perfective ↔ Perfective a.verbalizer [])

The fragment's dictionary aspect of each analysed stem is the bare-stem perfectivity the model derives: perfective for the semelfactives, imperfective otherwise, (46).

theorem Jablonska2004.attested_perfective (a : Analysis) : a ∈ attested → (Perfective a.verbalizer a.layers ↔ a.layers.getLast? ≠ some Layer.si)

The attested derivations closed by the Secondary Imperfective are imperfective and the rest perfective, by the tests of Section 2.1: (31a) and the attenuative-frequentatives pass the phasal-complement test, (33) and (46) fail it.