Hyman and Mchombo 1992: morphotactic constraints in the Chichewa verb stem

Hyman and Mchombo study the orders in which the Chichewa verbal suffixes combine on a root such as mang- 'tie': the causative -its-, the applicative -ir-, the reciprocal -an-, the passive -idw- and the intensive -ITS-. Spell-out is cyclic and follows scope, but before a feature is spelled out a final morph may be marked off, circumscribed, and restored after the new one: -ir- and -idw- within the scope of the causative or the intensive, -an- optionally within that of the applicative and, by the later rule (36), of the causative or the intensive. The Repeated Morph Constraint (RMC) blocks two successive features spelled out by one morph, an applicative on a reciprocal base spells -an- a second time, and the reciprocal and the passive never combine, since a transitive verb is detransitivized only once. Circumscription makes the negative filters (10) redundant (filtered_of_mem_spellOut). The authors close with (34), which the cyclic account cannot exclude, and conclude that the causative is spelled out first.

Main definitions

• Feature, Input, Stem: the suffixal features, an input in order of scope, and a stem in surface order.
• RMC: the Repeated Morph Constraint, the OCP on the morph tier.
• rules₀, rules: the circumscriptions (15) and (22), and with them (36).
• splits, cycle, spellOut: the cyclic spell-out.
• Feature.valency, Input.valency: the valency each feature's voice derives.
• Role, Feature.target?, Role.passiveScopes: the thematic hierarchy (31) and its uses.

Main results

• filtered_of_mem_spellOut: no spelled-out stem violates the filters (10).
• rmc_of_mem_spellOut, mem_iff_of_mem_spellOut: every spelled-out stem satisfies the RMC and spells out exactly the features of its input.
• detransitivized_once: (4a).
• ambiguity_needs_late_rule: (35), (36).
• rank_lt_of_rules_ne_none: (33), circumscription respects the hierarchy.
• rows_spellOut, rows_cyclicFailures, rows_passive, rows_form: the paper's examples.

Implementation notes

• A feature's valency effect is that of the voice the fragment assigns it: it adds what the voice's derived frame adds to its initial frame or removes what it removes, and a voice that removes a core argument applies only to a base with at least the valency of its initial frame. The paper's one valency claim, (4a), is stated of mang-; the intensive, an adverbial, has no voice.
• The intensive is spelled out by the causative morph with a high tone (5b), so the RMC treats the two alike; the tone is written in capitals and the intensive reduplicates before another suffix (5a).
• The causative marks off one morph after another (18) and the intensive at most one (fn. 16); the applicative's only rule (22) marks off a single -an-. A cycle leaving an obligatory circumscription undone has no output. The respelled -an- (24) is added when the applicative is spelled out on a base containing a reciprocal and the base's own -an- was not marked off (22); the rule block's respelling of -ir- on a reciprocal cycle, which the paper shows blocked by the RMC, is omitted.
• The passive subjects of (27)–(30) are recorded on the rows and not derived, since the paper states only the order of the applicative and the passive. Rows marked ? or ?* carry no claim.

TODO

• (25): the paper suggests that the degraded triple applicatives violate the RMC if respelled morphs are invisible, OCP.IsCleanOn on the tier without them; this needs stems that record which -an- is respelled.
• The Cibemba data (20) and the phonological case for cyclic spell-out.

References

• [HM92]
• [Cre24]

Features and their morphs

inductive HymanMchombo1992.Feature : Type

The morphosyntactic features the verbal suffixes spell out (1).

• causative : Feature
• applicative : Feature
• reciprocal : Feature
• passive : Feature
• intensive : Feature

@[instance_reducible]

instance HymanMchombo1992.instDecidableEqFeature : DecidableEq Feature

Equations

• HymanMchombo1992.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HymanMchombo1992.instReprFeature : Repr Feature

Equations

• HymanMchombo1992.instReprFeature = { reprPrec := HymanMchombo1992.instReprFeature.repr }

def HymanMchombo1992.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HymanMchombo1992.instFintypeFeature : Fintype Feature

Equations

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

@[reducible, inline]

abbrev HymanMchombo1992.Input : Type

An input lists the features in order of scope, innermost first (2).

Equations

• HymanMchombo1992.Input = List HymanMchombo1992.Feature

@[reducible, inline]

abbrev HymanMchombo1992.Stem : Type

A stem lists the features whose morphs follow the root, in surface order; a respelled -an- is a second reciprocal.

Equations

• HymanMchombo1992.Stem = List HymanMchombo1992.Feature

def HymanMchombo1992.Feature.voice? : Feature → Option Voice

The voice a feature realizes; the intensive, an adverbial, realizes none.

Equations

• HymanMchombo1992.Feature.causative.voice? = some Chichewa.causative
• HymanMchombo1992.Feature.applicative.voice? = some Chichewa.applicative
• HymanMchombo1992.Feature.reciprocal.voice? = some Chichewa.reciprocal
• HymanMchombo1992.Feature.passive.voice? = some Chichewa.passive
• HymanMchombo1992.Feature.intensive.voice? = none

def HymanMchombo1992.Feature.morphs : Feature → List Morphology.Morph

The morphs that spell out a feature are its voice's marker, and for the intensive the causative's (5b).

Equations

• HymanMchombo1992.Feature.causative.morphs = Chichewa.causative.marker
• HymanMchombo1992.Feature.intensive.morphs = Chichewa.causative.marker
• HymanMchombo1992.Feature.applicative.morphs = Chichewa.applicative.marker
• HymanMchombo1992.Feature.reciprocal.morphs = Chichewa.reciprocal.marker
• HymanMchombo1992.Feature.passive.morphs = Chichewa.passive.marker

@[reducible, inline]

abbrev HymanMchombo1992.RMC (s : Stem) : Prop

The Repeated Morph Constraint bars two successive features spelled out by the same morphs (4b); it is the OCP on the morph tier.

Equations

• HymanMchombo1992.RMC s = OCP.IsClean (List.map HymanMchombo1992.Feature.morphs s)

Cyclic spell-out

inductive HymanMchombo1992.Circumscription : Type

Whether a circumscription must or may apply.

• obligatory : Circumscription
• optional : Circumscription

@[instance_reducible]

instance HymanMchombo1992.instDecidableEqCircumscription : DecidableEq Circumscription

Equations

• HymanMchombo1992.instDecidableEqCircumscription x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HymanMchombo1992.instReprCircumscription.repr : Circumscription → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HymanMchombo1992.instReprCircumscription : Repr Circumscription

Equations

• HymanMchombo1992.instReprCircumscription = { reprPrec := HymanMchombo1992.instReprCircumscription.repr }

@[reducible, inline]

abbrev HymanMchombo1992.Rules : Type

A set of circumscription rules says what the spell-out of f does to a base ending in the morph of g.

Equations

• HymanMchombo1992.Rules = (HymanMchombo1992.Feature → HymanMchombo1992.Feature → Option HymanMchombo1992.Circumscription)

def HymanMchombo1992.rules₀ : Rules

The rules (15) and (22) mark off -ir- and -idw- within the scope of the causative or the intensive, and may mark off -an- within the scope of the applicative.

Equations

• HymanMchombo1992.rules₀ HymanMchombo1992.Feature.causative HymanMchombo1992.Feature.applicative = some HymanMchombo1992.Circumscription.obligatory
• HymanMchombo1992.rules₀ HymanMchombo1992.Feature.causative HymanMchombo1992.Feature.passive = some HymanMchombo1992.Circumscription.obligatory
• HymanMchombo1992.rules₀ HymanMchombo1992.Feature.intensive HymanMchombo1992.Feature.applicative = some HymanMchombo1992.Circumscription.obligatory
• HymanMchombo1992.rules₀ HymanMchombo1992.Feature.intensive HymanMchombo1992.Feature.passive = some HymanMchombo1992.Circumscription.obligatory
• HymanMchombo1992.rules₀ HymanMchombo1992.Feature.applicative HymanMchombo1992.Feature.reciprocal = some HymanMchombo1992.Circumscription.optional
• HymanMchombo1992.rules₀ x✝¹ x✝ = none

def HymanMchombo1992.rules : Rules

With (36), the rules may also mark off -an- within the scope of the causative or the intensive.

Equations

• HymanMchombo1992.rules HymanMchombo1992.Feature.causative HymanMchombo1992.Feature.reciprocal = some HymanMchombo1992.Circumscription.optional
• HymanMchombo1992.rules HymanMchombo1992.Feature.intensive HymanMchombo1992.Feature.reciprocal = some HymanMchombo1992.Circumscription.optional
• HymanMchombo1992.rules x✝¹ x✝ = HymanMchombo1992.rules₀ x✝¹ x✝

def HymanMchombo1992.splits (K : Rules) (f : Feature) : List Feature → Stem → List (Stem × Stem)

The ways the spell-out of f splits a stem, given in reverse, into the material it keeps and the material it marks off, which m accumulates. The causative marks off one morph after another (18) and every other feature at most one (fn. 16), and a split that leaves an obligatory circumscription undone is not one.

Equations

• One or more equations did not get rendered due to their size.
• HymanMchombo1992.splits K f [] x✝ = [([], x✝)]

def HymanMchombo1992.respelling (i : Input) (f : Feature) (m : Stem) : Stem

The -an- the applicative spells out again on a base containing a reciprocal (24), unless the base's own -an- was marked off (22).

Equations

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

def HymanMchombo1992.cycle (K : Rules) (i : Input) (f : Feature) (s : Stem) : List Stem

A cycle spells out f on a stem s of the input i by placing the new morph after the kept material and before the marked-off material; the RMC blocks a result that repeats a morph.

Equations

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

def HymanMchombo1992.spellOut (K : Rules) (i : Input) : Finset Stem

The stems the cyclic spell-out of an input derives.

Equations

• HymanMchombo1992.spellOut K i = HymanMchombo1992.spellOut.go K (List.reverse i)

def HymanMchombo1992.spellOut.go (K : Rules) : List Feature → Finset Stem

The stems of an input given in reverse.

Equations

• HymanMchombo1992.spellOut.go K [] = {[]}
• HymanMchombo1992.spellOut.go K (f :: rest) = (HymanMchombo1992.spellOut.go K rest).biUnion fun (s : HymanMchombo1992.Stem) => (HymanMchombo1992.cycle K rest.reverse f s).toFinset

theorem HymanMchombo1992.splits_spec {K : Rules} {f : Feature} {rev : List Feature} {acc : Stem} {km : Stem × Stem} : km ∈ splits K f rev acc → km.1 ++ km.2 = rev.reverse ++ acc ∧ (∀ x ∈ km.2, x ∈ acc ∨ K f x ≠ none) ∧ ∀ x ∈ List.getLast? km.1, K f x ≠ some Circumscription.obligatory

theorem HymanMchombo1992.mem_spellOut_go {K : Rules} {f : Feature} {rest : List Feature} {t : Stem} : t ∈ spellOut.go K (f :: rest) ↔ ∃ s ∈ spellOut.go K rest, t ∈ cycle K rest.reverse f s

theorem HymanMchombo1992.rmc_of_mem_spellOut {K : Rules} {i : Input} {s : Stem} (h : s ∈ spellOut K i) : RMC s

Every stem the cyclic spell-out derives satisfies the RMC.

theorem HymanMchombo1992.mem_iff_of_mem_spellOut {K : Rules} {i : Input} {s : Stem} (h : s ∈ spellOut K i) (x : Feature) : x ∈ s ↔ x ∈ i

Every stem the cyclic spell-out derives spells out exactly the features of its input.

The filters (10)

def HymanMchombo1992.Filtered (s : Stem) : Prop

A stem satisfies the negative filters (10b) when no applicative or passive immediately precedes a causative or an intensive.

Equations

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

theorem HymanMchombo1992.rules_eq_obligatory {f g : Feature} : rules f g = some Circumscription.obligatory ↔ g ∈ [Feature.applicative, Feature.passive] ∧ f ∈ [Feature.causative, Feature.intensive]

theorem HymanMchombo1992.not_mem_of_rules_ne_none {f x : Feature} (h : rules f x ≠ none) : x ∉ [Feature.causative, Feature.intensive]

theorem HymanMchombo1992.filtered_cons {f : Feature} {l : Stem} (hl : Filtered l) (h : ∀ y ∈ List.head? l, y ∉ [Feature.causative, Feature.intensive]) : Filtered (f :: l)

theorem HymanMchombo1992.Filtered.cycle {i : Input} {f : Feature} {s t : Stem} (hs : Filtered s) (ht : t ∈ HymanMchombo1992.cycle rules i f s) : Filtered t

theorem HymanMchombo1992.filtered_of_mem_spellOut {i : Input} {s : Stem} (h : s ∈ spellOut rules i) : Filtered s

The filters (10) follow from circumscription, since no stem the cyclic spell-out derives has an applicative or passive morph immediately before a causative or intensive one.

theorem HymanMchombo1992.ambiguity_needs_late_rule : spellOut rules₀ [Feature.reciprocal, Feature.causative] = {[Feature.reciprocal, Feature.causative]} ∧ spellOut rules [Feature.reciprocal, Feature.causative] = {[Feature.reciprocal, Feature.causative], [Feature.causative, Feature.reciprocal]}

A causativized reciprocal surfaces as -its-an- as well as -an-its- only by the circumscription (36), so without it -its-an- would spell out only a reciprocalized causative ((35), (36)).

Valency

def HymanMchombo1992.Feature.valency (f : Feature) (n : ℕ) : Option ℕ

A feature derives a valency from a base of valency n by adding what its voice's derived frame adds to its initial frame, or removing what it removes; a voice that removes a core argument applies only to a base with at least the valency of its initial frame.

Equations

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

def HymanMchombo1992.Input.valency (i : Input) (n : ℕ) : Option ℕ

The valency an input derives from a root of valency n, if every feature applies.

Equations

• i.valency n = List.foldlM (fun (n : ℕ) (f : HymanMchombo1992.Feature) => f.valency n) n i

theorem HymanMchombo1992.valency_reciprocal (n : ℕ) : Feature.reciprocal.valency n = if n < 2 then none else some (n - 1)

theorem HymanMchombo1992.valency_passive (n : ℕ) : Feature.passive.valency n = if n < 2 then none else some (n - 1)

theorem HymanMchombo1992.detransitivized_once {i : Input} {n : ℕ} : n ≤ 2 → Feature.causative ∉ i → Feature.applicative ∉ i → (i.valency n).isSome = true → (List.filter (fun (x : Feature) => decide (x ∈ [Feature.reciprocal, Feature.passive])) i).length ≤ n - 1

A transitive verb is detransitivized only once (4a). With no causative or applicative to add an argument, an input that a root of valency at most two survives has fewer reciprocals and passives than the root has arguments.

The thematic hierarchy

inductive HymanMchombo1992.Role : Type

The roles of the thematic hierarchy (31).

• agent : Role
• benefactive : Role
• goal : Role
• instrument : Role
• patient : Role
• locative : Role
• circumstantial : Role

@[instance_reducible]

instance HymanMchombo1992.instDecidableEqRole : DecidableEq Role

Equations

• HymanMchombo1992.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HymanMchombo1992.instReprRole : Repr Role

Equations

• HymanMchombo1992.instReprRole = { reprPrec := HymanMchombo1992.instReprRole.repr }

def HymanMchombo1992.instReprRole.repr : Role → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HymanMchombo1992.instFintypeRole : Fintype Role

Equations

• HymanMchombo1992.instFintypeRole = { elems := { val := ↑HymanMchombo1992.Role.enumList, nodup := HymanMchombo1992.Role.enumList_nodup }, complete := HymanMchombo1992.instFintypeRole._proof_1 }

def HymanMchombo1992.Role.rank : Role → ℕ

A role's place on the hierarchy (31), counted from the top.

Equations

• HymanMchombo1992.Role.agent.rank = 0
• HymanMchombo1992.Role.benefactive.rank = 1
• HymanMchombo1992.Role.goal.rank = 2
• HymanMchombo1992.Role.instrument.rank = 3
• HymanMchombo1992.Role.patient.rank = 4
• HymanMchombo1992.Role.locative.rank = 5
• HymanMchombo1992.Role.circumstantial.rank = 6

def HymanMchombo1992.Feature.target? : Feature → Option Role

The role a feature's suffix targets (33) is an agent for the causative, the prototypical benefactive for the applicative, and a patient for the reciprocal and the passive; the intensive, an adverbial, targets none.

Equations

• HymanMchombo1992.Feature.causative.target? = some HymanMchombo1992.Role.agent
• HymanMchombo1992.Feature.applicative.target? = some HymanMchombo1992.Role.benefactive
• HymanMchombo1992.Feature.reciprocal.target? = some HymanMchombo1992.Role.patient
• HymanMchombo1992.Feature.passive.target? = some HymanMchombo1992.Role.patient
• HymanMchombo1992.Feature.intensive.target? = none

def HymanMchombo1992.Feature.rank (f : Feature) : WithBot ℕ

A feature's place on the hierarchy, an adverbial above every role.

Equations

• f.rank = Option.map HymanMchombo1992.Role.rank f.target?

theorem HymanMchombo1992.rank_lt_of_rules_ne_none {f g : Feature} (h : rules f g ≠ none) : f.rank < g.rank

Every circumscription marks off a suffix that targets a role lower on the hierarchy than the feature that marks it off (33). The paper notes that a locative or circumstantial applicative, below the patient, still precedes the reciprocal: the orders follow the affixes' prototypical functions.

def HymanMchombo1992.Role.IsArgument (r : Role) : Prop

An applied argument, a participant above the patient on the hierarchy (31).

Equations

• r.IsArgument = (r.rank < HymanMchombo1992.Role.patient.rank)

def HymanMchombo1992.Role.IsAdjunct (r : Role) : Prop

An applied adjunct, a setting at the foot of the hierarchy (31).

Equations

• r.IsAdjunct = ∀ (r' : HymanMchombo1992.Role), r'.rank ≤ r.rank

@[instance_reducible]

instance HymanMchombo1992.instDecidableIsArgument (r : Role) : Decidable r.IsArgument

Equations

• HymanMchombo1992.instDecidableIsArgument r = { decide := r.rank.succ.ble HymanMchombo1992.Role.patient.rank, reflects_decide := ⋯ }

@[instance_reducible]

instance HymanMchombo1992.instDecidableIsAdjunct (r : Role) : Decidable r.IsAdjunct

Equations

• HymanMchombo1992.instDecidableIsAdjunct r = { decide := decide (∀ a ∈ Finset.univ, (fun (x : HymanMchombo1992.Role) => x.rank ≤ r.rank) a), reflects_decide := ⋯ }

def HymanMchombo1992.Role.passiveScopes (r : Role) : List Input

The scopes an applicative of role r takes with the passive (31) put the applicative within the passive for an applied argument, the passive within the applicative for an applied adjunct, and either for a locative, which lies between them.

Equations

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

The paper's examples

def HymanMchombo1992.Feature.ofChar? : Char → Option Feature

A feature by its letter in the rows.

Equations

• HymanMchombo1992.Feature.ofChar? 'C' = some HymanMchombo1992.Feature.causative
• HymanMchombo1992.Feature.ofChar? 'A' = some HymanMchombo1992.Feature.applicative
• HymanMchombo1992.Feature.ofChar? 'R' = some HymanMchombo1992.Feature.reciprocal
• HymanMchombo1992.Feature.ofChar? 'P' = some HymanMchombo1992.Feature.passive
• HymanMchombo1992.Feature.ofChar? 'I' = some HymanMchombo1992.Feature.intensive
• HymanMchombo1992.Feature.ofChar? x✝ = none

def HymanMchombo1992.features? (r : Datum) (key : String) : Option (List Feature)

A row's feature as a sequence of features.

Equations

• HymanMchombo1992.features? r key = (r.feature? key).bind fun (s : String) => List.mapM HymanMchombo1992.Feature.ofChar? s.toList

def HymanMchombo1992.scope? (r : Datum) : Option Input

A row's scope, innermost first.

Equations

• HymanMchombo1992.scope? r = HymanMchombo1992.features? r "scope"

def HymanMchombo1992.suffixes? (r : Datum) : Option Stem

A row's suffixes, in surface order.

Equations

• HymanMchombo1992.suffixes? r = HymanMchombo1992.features? r "suffixes"

def HymanMchombo1992.root? (r : Datum) : Option Verb

A row's root.

Equations

• HymanMchombo1992.root? r = r.parse? "root" [("mang", Chichewa.Verbs.mang), ("uk", Chichewa.Verbs.uk)]

def HymanMchombo1992.role? (r : Datum) : Option Role

A row's applied role.

Equations

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

def HymanMchombo1992.Licensed (v : Verb) (i : Input) : Prop

A root survives an input when the valency of its frame suffices for each feature.

Equations

• HymanMchombo1992.Licensed v i = ∃ fr ∈ v.valency.frames.head?, (i.valency fr.valency).isSome = true

@[instance_reducible]

instance HymanMchombo1992.instDecidableLicensed (v : Verb) (i : Input) : Decidable (Licensed v i)

Equations

• HymanMchombo1992.instDecidableLicensed v i = HymanMchombo1992.instDecidableLicensed._aux_1 v i

def HymanMchombo1992.Feature.form (f : Feature) : String

The letters of a feature's morphs.

Equations

• f.form = List.foldr (fun (m : Morphology.Morph) (w : String) => m.form ++ w) "" f.morphs

def HymanMchombo1992.intensiveForm : String

The intensive suffix as the source writes it, in capitals for its high tone.

Equations

• HymanMchombo1992.intensiveForm = "ITS"

theorem HymanMchombo1992.intensiveForm_toList : intensiveForm.toList = List.map Char.toUpper Feature.causative.form.toList

The intensive suffix is the causative morph with a high tone (5b).

def HymanMchombo1992.spell : Stem → String

A stem in the source's spelling, each suffix after a hyphen, the intensive reduplicated before another suffix (5a).

Equations

• HymanMchombo1992.spell [] = ""
• HymanMchombo1992.spell [HymanMchombo1992.Feature.intensive] = "-" ++ HymanMchombo1992.intensiveForm
• HymanMchombo1992.spell (HymanMchombo1992.Feature.intensive :: s) = "-" ++ HymanMchombo1992.intensiveForm ++ HymanMchombo1992.intensiveForm ++ HymanMchombo1992.spell s
• HymanMchombo1992.spell (f :: s) = "-" ++ f.form ++ HymanMchombo1992.spell s

theorem HymanMchombo1992.rows_parse (r : Datum) : r ∈ Examples.all → (root? r).isSome = true ∧ (suffixes? r).isSome = true ∧ ((scope? r).isSome = true ∨ (role? r).isSome = true)

Every row names a root and its suffixes, and a scope or an applied role.

theorem HymanMchombo1992.rows_form (r : Datum) : r ∈ Examples.all → role? r = none → ∀ v ∈ root? r, ∀ s ∈ suffixes? r, r.primaryText = v.form ++ spell s ++ "-" ∨ r.primaryText = v.form ++ spell s ++ "-a"

Each stem row's form is its root followed by the spelling of its suffixes, as a bare stem or with the final vowel -a.

def HymanMchombo1992.cyclicFailures : List String

The rows the cyclic spell-out gets wrong are (34c), which it derives although the paper stars it, and the triple applicative of (25a), whose degradation the paper leaves open.

Equations

• HymanMchombo1992.cyclicFailures = ["hymanmchombo1992_34c", "hymanmchombo1992_25a_3"]

theorem HymanMchombo1992.rows_spellOut (r : Datum) : r ∈ Examples.all → ∀ v ∈ root? r, ∀ i ∈ scope? r, ∀ s ∈ suffixes? r, (r.judgment = Judgment.acceptable → Licensed v i ∧ s ∈ spellOut rules i) ∧ (r.judgment = Judgment.ungrammatical → r.id ∉ cyclicFailures → ¬(Licensed v i ∧ s ∈ spellOut rules i))

Every stem the paper accepts survives its root's valency and is spelled out from its scope; outside cyclicFailures, no stem it stars is.

theorem HymanMchombo1992.rows_cyclicFailures (r : Datum) : r ∈ Examples.all → r.id ∈ cyclicFailures → r.judgment = Judgment.ungrammatical ∧ ∀ v ∈ root? r, ∀ i ∈ scope? r, ∀ s ∈ suffixes? r, Licensed v i ∧ s ∈ spellOut rules i

The stems in cyclicFailures are starred, yet survive their root's valency and are spelled out from their scope ((34), (25)).

theorem HymanMchombo1992.rows_passive : (∀ r ∈ Examples.all, ∀ ρ ∈ role? r, ∀ s ∈ suffixes? r, r.judgment = Judgment.acceptable → ∃ i ∈ ρ.passiveScopes, s ∈ spellOut rules i) ∧ ∀ r ∈ Examples.all, ∀ ρ ∈ role? r, ∀ i ∈ ρ.passiveScopes, ∀ s ∈ spellOut rules i, ∃ r' ∈ Examples.all, role? r' = some ρ ∧ suffixes? r' = some s ∧ r'.judgment = Judgment.acceptable

Every order of applicative and passive the paper accepts is spelled out from a scope the applied role allows, and every order so spelled out is accepted in some sentence ((27)–(31)).