Hyman 2003: suffix ordering in Bantu

[Hym03] argues that the order of the Bantu verbal extensions, causative, applicative, reciprocal and passive, is driven by a Pan-Bantu default template, CARP (5), not by semantic scope or by [Bak85]'s Mirror Principle: Chichewa realizes both scopes of causative and applicative as -its-il- (3), a reciprocal inside a causative surfaces in the templatic order -its-an- as well as the mirror order -an-its- while the mirror order has only the compositional reading (2), a reciprocal inside an applicative surfaces as templatic -il-an- or with the reciprocal doubled, -an-il-an-, never as -an-il- (13), and no extension repeats (18). The two pressures, TEMPLATE, which licenses a sequence in the template's order, and the suffix-specific MIRROR constraints, which license a sequence in the order of scope, are ranked, violably and sometimes freely, as in Optimality Theory: a candidate succeeds at the first licensor down the ranking by which every sequence and every doubling in it is licensed, and a doubled suffix must be a mirror override repaired by a templatic sequence, licensed by the conjunction of the two (16). Chimwiini ranks only the template (19), and the syntax of Chichewa passives (22)–(23) shows the order of syntactic operations varying under one fixed affix order, so the Mirror Principle holds, if at all, as a violable constraint (§3).

Main definitions

• Ext, carp, templatic: the extensions, the CARP template and an input's templatic realization.
• Licensor, Licensor.licenses, LicensedBy: TEMPLATE, MIRROR and their conjunction, what each licenses of a candidate, and full licensing by a set of them.
• candidates, tableau, Grammar, Grammar.outputs: the candidates of an input, Hyman's evaluation under a ranking as an OT tableau, a partially ordered set of licensors, and the outputs across its linear extensions.
• chichewa, chimwiini, passiveGrammar: the grammars of §2, §3 and (12).

Main results

• licensedBy_iff_templatic, chimwiini_outputs: the template alone licenses exactly the templatic realization, the only output of a template-only grammar (19).
• outputs_isChain_ne, doubling_licensed: no output repeats a suffix, and a doubled suffix is a mirror override the template repairs.
• asymmetric_compositionality, causative_applicative, applicative_reciprocal, passive: (2), (3) with (7), (13) with (16), and (12).
• three_suffixes: the appendix's table for three extensions.
• scope_not_recoverable, mirror_predicts_distinct_words, rows_passive: one affix order for two syntactic derivations (§3), which [Bak85]'s architecture would keep apart and whose passives his rules derive from scope.
• rows_outputs: the paper's forms.

Implementation notes

• Hyman's tableaux mark the sequences a licensor licenses rather than violations; the evaluation, a candidate winning at the first rank by which all its sequences are licensed, is the lexicographic minimization of the profile whose k-th entry says whether the top k + 1 licensors fail to license the candidate, so it is a substrate Tableau.
• The conjunction MIRROR (x, y) & TEMPLATE licenses an adjacent x y followed by x, the templatic repair of a mirror override, and the doubling of x in any x … y x. This follows §2's generalization that doubling yields A-B-A only when A-B is a mirror override; the appendix's tableaux (48c, e) also mark mang-an-its-il-an successful, licensing its doubled -an- without the conjunction, which the model does not derive.
• Chichewa's licensors are TEMPLATE, MIRROR (R, C) and the conjunction for (R, A), freely ranked, as the appendix ranks them; MIRROR (A, C) is not activated and MIRROR (R, A) alone is dominated by TEMPLATE, so neither ever licenses an output.
• [Bak85]'s rules run on Chichewa with the Chamorro-type causative and the passive of the first object, the asymmetric-object setting of (22)–(23).

TODO

• Table (48) diverges from the model on two forms (three_suffixes): the paper's licensing of non-adjacent sequences, invoked for -an- … -il-an-, is not defined and would settle both.
• The elaborated template CARCP (28) with the short causative, and the phonological templatic requirements of §5.

References

• [Hym03]
• [HM92]
• [Als99]
• [Aba78]
• [Bak85]
• [Ant97]

The template

inductive Hyman2003.Ext : Type

The Proto-Bantu verbal extensions of the template (5): causative, applicative, reciprocal, passive.

• C : Ext
• A : Ext
• R : Ext
• P : Ext

@[instance_reducible]

instance Hyman2003.instDecidableEqExt : DecidableEq Ext

Equations

• Hyman2003.instDecidableEqExt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hyman2003.instReprExt : Repr Ext

Equations

• Hyman2003.instReprExt = { reprPrec := Hyman2003.instReprExt.repr }

def Hyman2003.instReprExt.repr : Ext → ℕ → Std.Format

Equations

• Hyman2003.instReprExt.repr Hyman2003.Ext.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2003.Ext.C")).group prec✝
• Hyman2003.instReprExt.repr Hyman2003.Ext.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2003.Ext.A")).group prec✝
• Hyman2003.instReprExt.repr Hyman2003.Ext.R prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2003.Ext.R")).group prec✝
• Hyman2003.instReprExt.repr Hyman2003.Ext.P prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hyman2003.Ext.P")).group prec✝

@[instance_reducible]

instance Hyman2003.instFintypeExt : Fintype Ext

Equations

• Hyman2003.instFintypeExt = { elems := { val := ↑Hyman2003.Ext.enumList, nodup := Hyman2003.Ext.enumList_nodup }, complete := Hyman2003.instFintypeExt._proof_1 }

def Hyman2003.carp : Morphology.AffixTemplate Ext

The Pan-Bantu default template (5), CARP: the extensions as suffix slots in the order Causative-Applicative-Reciprocal-Passive.

Equations

• Hyman2003.carp = { suffixSlots := [Hyman2003.Ext.C, Hyman2003.Ext.A, Hyman2003.Ext.R, Hyman2003.Ext.P] }

def Hyman2003.Ext.slot (x : Ext) : ℕ

An extension's position in the template.

Equations

• x.slot = List.idxOf x Hyman2003.carp.suffixSlots

theorem Hyman2003.slot_injective : Function.Injective Ext.slot

theorem Hyman2003.carp_pairwise_slot : List.Pairwise (fun (x y : Ext) => x.slot < y.slot) carp.suffixSlots

@[reducible, inline]

abbrev Hyman2003.Input : Type

A morphosyntactic input: the extensions in order of scope, innermost first, the bracketing [[[V] x] y].

Equations

• Hyman2003.Input = List Hyman2003.Ext

def Hyman2003.Input.Inside (i : Input) (x y : Ext) : Prop

In the input, x is within the scope of y.

Equations

• i.Inside x y = (x ∈ i ∧ y ∈ i ∧ List.idxOf x i < List.idxOf y i)

@[instance_reducible]

instance Hyman2003.instDecidableInside (i : Input) (x y : Ext) : Decidable (i.Inside x y)

Equations

• Hyman2003.instDecidableInside i x y = { decide := decide (x ∈ i) && decide (y ∈ i ∧ List.idxOf x i < List.idxOf y i), reflects_decide := ⋯ }

@[reducible, inline]

abbrev Hyman2003.Candidate : Type

A candidate output: the suffixes in surface order, innermost first.

Equations

• Hyman2003.Candidate = List Hyman2003.Ext

def Hyman2003.templatic (i : Input) : Candidate

The templatic realization of an input: the template's slots filled by its extensions.

Equations

• Hyman2003.templatic i = List.filter (fun (x : Hyman2003.Ext) => decide (x ∈ i)) Hyman2003.carp.suffixSlots

theorem Hyman2003.templatic_nodup (i : Input) : List.Nodup (templatic i)

theorem Hyman2003.templatic_pairwise (i : Input) : List.Pairwise (fun (x y : Ext) => x.slot < y.slot) (templatic i)

theorem Hyman2003.mem_templatic {i : Input} {x : Ext} : x ∈ templatic i ↔ x ∈ i

Licensors

inductive Hyman2003.Licensor : Type

The licensors of suffix sequences: TEMPLATE licenses a sequence in the template's order (6a); MIRROR (x, y) licenses the sequence x y when x is within the scope of y (6b); their conjunction licenses a mirror override repaired by a templatic sequence, x y x (16).

• template : Licensor
• mirror (x y : Ext) : Licensor
• mirrorTemplate (x y : Ext) : Licensor

@[instance_reducible]

instance Hyman2003.instDecidableEqLicensor : DecidableEq Licensor

Equations

• Hyman2003.instDecidableEqLicensor = Hyman2003.instDecidableEqLicensor.decEq

def Hyman2003.instDecidableEqLicensor.decEq (x✝ x✝¹ : Licensor) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Hyman2003.instDecidableEqLicensor.decEq Hyman2003.Licensor.template Hyman2003.Licensor.template = isTrue ⋯
• Hyman2003.instDecidableEqLicensor.decEq Hyman2003.Licensor.template (Hyman2003.Licensor.mirror x_2 y) = isFalse ⋯
• Hyman2003.instDecidableEqLicensor.decEq Hyman2003.Licensor.template (Hyman2003.Licensor.mirrorTemplate x_2 y) = isFalse ⋯
• Hyman2003.instDecidableEqLicensor.decEq (Hyman2003.Licensor.mirror x_2 y) Hyman2003.Licensor.template = isFalse ⋯
• Hyman2003.instDecidableEqLicensor.decEq (Hyman2003.Licensor.mirror a a_1) (Hyman2003.Licensor.mirror b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Hyman2003.instDecidableEqLicensor.decEq (Hyman2003.Licensor.mirror x_2 y) (Hyman2003.Licensor.mirrorTemplate x_3 y_1) = isFalse ⋯
• Hyman2003.instDecidableEqLicensor.decEq (Hyman2003.Licensor.mirrorTemplate x_2 y) Hyman2003.Licensor.template = isFalse ⋯
• Hyman2003.instDecidableEqLicensor.decEq (Hyman2003.Licensor.mirrorTemplate x_2 y) (Hyman2003.Licensor.mirror x_3 y_1) = isFalse ⋯

def Hyman2003.instReprLicensor.repr : Licensor → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hyman2003.instReprLicensor : Repr Licensor

Equations

• Hyman2003.instReprLicensor = { reprPrec := Hyman2003.instReprLicensor.repr }

inductive Hyman2003.Demand : Type

What a candidate needs licensed: each adjacent pair, by the position of its first member, and each extension it doubles.

• pair (k : ℕ) : Demand
• doubling (x : Ext) : Demand

@[instance_reducible]

instance Hyman2003.instDecidableEqDemand : DecidableEq Demand

Equations

• Hyman2003.instDecidableEqDemand = Hyman2003.instDecidableEqDemand.decEq

def Hyman2003.instDecidableEqDemand.decEq (x✝ x✝¹ : Demand) : Decidable (x✝ = x✝¹)

Equations

• Hyman2003.instDecidableEqDemand.decEq (Hyman2003.Demand.pair a) (Hyman2003.Demand.pair b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hyman2003.instDecidableEqDemand.decEq (Hyman2003.Demand.pair k) (Hyman2003.Demand.doubling x_2) = isFalse ⋯
• Hyman2003.instDecidableEqDemand.decEq (Hyman2003.Demand.doubling x_2) (Hyman2003.Demand.pair k) = isFalse ⋯
• Hyman2003.instDecidableEqDemand.decEq (Hyman2003.Demand.doubling a) (Hyman2003.Demand.doubling b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hyman2003.instReprDemand : Repr Demand

Equations

• Hyman2003.instReprDemand = { reprPrec := Hyman2003.instReprDemand.repr }

def Hyman2003.instReprDemand.repr : Demand → ℕ → Std.Format

Equations

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

def Hyman2003.demands (c : Candidate) : List Demand

A candidate's demands.

Equations

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

def Hyman2003.Licensor.licenses (i : Input) (c : Candidate) : Licensor → Demand → Prop

A licensor meets a demand of a candidate for an input: TEMPLATE, a pair rising in the template; MIRROR (x, y), the pair x y with x inside y; the conjunction, either pair of an x y x with x inside y, and the doubling of x in any x … y x.

Equations

• One or more equations did not get rendered due to their size.
• Hyman2003.Licensor.licenses i c Hyman2003.Licensor.template (Hyman2003.Demand.pair k) = ∃ (x : Hyman2003.Ext) (y : Hyman2003.Ext), c[k]? = some x ∧ c[k + 1]? = some y ∧ x.slot < y.slot
• Hyman2003.Licensor.licenses i c (Hyman2003.Licensor.mirror x_2 y) (Hyman2003.Demand.pair k) = (i.Inside x_2 y ∧ c[k]? = some x_2 ∧ c[k + 1]? = some y)
• Hyman2003.Licensor.licenses i c Hyman2003.Licensor.template (Hyman2003.Demand.doubling x_2) = False
• Hyman2003.Licensor.licenses i c (Hyman2003.Licensor.mirror x_2 y) (Hyman2003.Demand.doubling x_3) = False

@[instance_reducible]

instance Hyman2003.instDecidableLicenses (i : Input) (c : Candidate) (l : Licensor) (d : Demand) : Decidable (Licensor.licenses i c l d)

Equations

• One or more equations did not get rendered due to their size.
• Hyman2003.instDecidableLicenses i c Hyman2003.Licensor.template (Hyman2003.Demand.doubling x_2) = { decide := false, reflects_decide := ⋯ }
• Hyman2003.instDecidableLicenses i c (Hyman2003.Licensor.mirror x_2 y) (Hyman2003.Demand.doubling x_3) = { decide := false, reflects_decide := ⋯ }

def Hyman2003.LicensedBy (i : Input) (S : List Licensor) (c : Candidate) : Prop

A candidate is licensed by a set of licensors when each of its demands is met by one.

Equations

• Hyman2003.LicensedBy i S c = ∀ d ∈ Hyman2003.demands c, ∃ l ∈ S, Hyman2003.Licensor.licenses i c l d

@[instance_reducible]

instance Hyman2003.instDecidableLicensedBy (i : Input) (S : List Licensor) (c : Candidate) : Decidable (LicensedBy i S c)

Equations

• Hyman2003.instDecidableLicensedBy i S c = Hyman2003.instDecidableLicensedBy._aux_1 i S c

theorem Hyman2003.LicensedBy.mono {i : Input} {S T : List Licensor} (h : S ⊆ T) {c : Candidate} (hc : LicensedBy i S c) : LicensedBy i T c

Evaluation

def Hyman2003.candidates (i : Input) : Finset Candidate

The candidates of an input: its templatic realization and every sequence over its extensions that realizes each of them, repeats none immediately and doubles at most one.

Equations

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

def Hyman2003.constraints (i : Input) (order : List Licensor) : OptimalityTheory.ConstraintSet Candidate (Fin order.length)

The constraint at rank k of a ranking of licensors: violated by a candidate the top k + 1 licensors do not license.

Equations

• Hyman2003.constraints i order k = OptimalityTheory.Constraint.binary fun (c : Hyman2003.Candidate) => ¬Hyman2003.LicensedBy i (List.take (↑k + 1) order) c

def Hyman2003.tableau (i : Input) (order : List Licensor) : OptimalityTheory.Tableau Candidate order.length

Hyman's evaluation under a ranking: a candidate succeeds at the first licensor down the ranking by which all of its demands are licensed, the lexicographic minimum of the cumulative profile.

Equations

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

structure Hyman2003.Grammar : Type

A grammar: licensors under a partial order ([Ant97]'s partially ordered constraints), evaluated under each linear extension; free ranking is the discrete order.

• n : ℕ

  The number of licensors.

• licensor : Fin self.n → Licensor

  The licensors.

• order : Fin self.n → Fin self.n → Prop

  The ranking, a partial order on the licensors.

• isPartialOrder : IsPartialOrder (Fin self.n) self.order
• decidableRel : DecidableRel self.order

def Hyman2003.Grammar.rankings (G : Grammar) : Finset (OptimalityTheory.Ranking (Fin G.n) G.n)

The linear extensions of the grammar's order.

Equations

• G.rankings = OptimalityTheory.consistentTotalOrders G.order

def Hyman2003.Grammar.ranked (G : Grammar) (σ : OptimalityTheory.Ranking (Fin G.n) G.n) : List Licensor

The licensors in the order of a ranking, most dominant first.

Equations

• G.ranked σ = List.map (fun (p : Fin G.n) => G.licensor (σ p)) (List.finRange G.n)

def Hyman2003.Grammar.outputs (G : Grammar) (i : Input) : Finset Candidate

The outputs of an input: the winners under some linear extension.

Equations

• G.outputs i = G.rankings.biUnion fun (σ : OptimalityTheory.Ranking (Fin G.n) G.n) => (Hyman2003.tableau i (G.ranked σ)).optimal

def Hyman2003.Grammar.free {n : ℕ} (licensor : Fin n → Licensor) : Grammar

A grammar of freely ranked licensors.

Equations

• Hyman2003.Grammar.free licensor = { n := n, licensor := licensor, order := fun (x1 x2 : Fin n) => x1 = x2, isPartialOrder := ⋯, decidableRel := instDecidableEqFin n }

def Hyman2003.Grammar.two (l₁ l₂ : Licensor) : Grammar

A grammar of two licensors, the first ranked above the second.

Equations

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

def Hyman2003.chichewa : Grammar

Chichewa (§2, appendix): TEMPLATE, MIRROR (R, C) and the conjunction for (R, A), freely ranked.

Equations

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

def Hyman2003.chimwiini : Grammar

Chimwiini (19): the template alone.

Equations

• Hyman2003.chimwiini = Hyman2003.Grammar.free ![Hyman2003.Licensor.template]

The template alone

The template licenses exactly the templatic realization: a candidate all of whose pairs rise in the template and which doubles nothing is the template's slots filled by its extensions.

theorem Hyman2003.mem_candidates {i : Input} {c : Candidate} : c ∈ candidates i ↔ c = templatic i ∨ ((List.length c = (List.dedup i).length ∨ List.length c = (List.dedup i).length + 1) ∧ ∀ x ∈ c, x ∈ i) ∧ (∀ x ∈ i, x ∈ c) ∧ List.IsChain (fun (x1 x2 : Ext) => x1 ≠ x2) c

theorem Hyman2003.templatic_mem_candidates (i : Input) : templatic i ∈ candidates i

theorem Hyman2003.licensedBy_template_templatic (i : Input) : LicensedBy i [Licensor.template] (templatic i)

The template licenses the templatic realization: its pairs rise in the template and it doubles nothing.

@[instance_reducible]

instance Hyman2003.instTransExtLtNatSlot : Trans (fun (x y : Ext) => x.slot < y.slot) (fun (x y : Ext) => x.slot < y.slot) fun (x y : Ext) => x.slot < y.slot

Equations

• Hyman2003.instTransExtLtNatSlot = { trans := @Hyman2003.instTransExtLtNatSlot._proof_1 }

theorem Hyman2003.licensedBy_iff_templatic {i : Input} {c : Candidate} (hc : c ∈ candidates i) : LicensedBy i [Licensor.template] c ↔ c = templatic i

A candidate the template alone licenses is the templatic realization.

theorem Hyman2003.chimwiini_outputs (i : Input) : chimwiini.outputs i = {templatic i}

Under a template-only grammar, every input has exactly its templatic realization: Chimwiini (19), where "it is not possible to put these extensions in any other order".

General properties of outputs

theorem Hyman2003.outputs_isChain_ne {G : Grammar} {i : Input} {c : Candidate} (hc : c ∈ G.outputs i) : List.IsChain (fun (x1 x2 : Ext) => x1 ≠ x2) c

theorem Hyman2003.licensedBy_of_mem_optimal {i : Input} {order : List Licensor} (hT : Licensor.template ∈ order) {c : Candidate} (hc : c ∈ (tableau i order).optimal) : LicensedBy i order c

Every output is licensed by the whole ranking that selects it: a candidate no rank licenses is beaten by the templatic realization, licensed once the template is reached.

theorem Hyman2003.doubling_licensed {G : Grammar} (hT : ∃ (p : Fin G.n), G.licensor p = Licensor.template) {i : Input} {c : Candidate} (hc : c ∈ G.outputs i) {x : Ext} (hx : 1 < List.count x c) : ∃ (y : Ext), (∃ (p : Fin G.n), G.licensor p = Licensor.mirrorTemplate x y) ∧ i.Inside x y

A doubled suffix in an output is a mirror override repaired by the template: some conjunction of the grammar licenses it, the generalization of §2 behind (16).

Chichewa (§2)

theorem Hyman2003.asymmetric_compositionality : chichewa.outputs [Ext.C, Ext.R] = {[Ext.C, Ext.R]} ∧ chichewa.outputs [Ext.R, Ext.C] = {[Ext.C, Ext.R], [Ext.R, Ext.C]}

(2), (10): asymmetric compositionality. A reciprocalized causative surfaces only in the templatic order -its-an-; a causativized reciprocal surfaces in the templatic order or in the mirror order -an-its-, so the templatic order is ambiguous and the mirror order is not.

theorem Hyman2003.causative_applicative : chichewa.outputs [Ext.C, Ext.A] = {[Ext.C, Ext.A]} ∧ chichewa.outputs [Ext.A, Ext.C] = {[Ext.C, Ext.A]}

(3), (7): both scopes of causative and applicative surface as -its-il-.

theorem Hyman2003.reciprocal_applicative_causative : [Ext.C, Ext.A, Ext.R] ∈ chichewa.outputs [Ext.R, Ext.A, Ext.C] ∧ [Ext.R, Ext.A, Ext.C] ∉ chichewa.outputs [Ext.R, Ext.A, Ext.C]

(8): a reciprocal inside an applicative inside a causative surfaces in the templatic order, with the causative two slots out of its compositional place; the compositional order is out.

theorem Hyman2003.applicative_reciprocal : chichewa.outputs [Ext.A, Ext.R] = {[Ext.A, Ext.R]} ∧ chichewa.outputs [Ext.R, Ext.A] = {[Ext.A, Ext.R], [Ext.R, Ext.A, Ext.R]}

(13), (14), (16), (17): a reciprocalized applicative surfaces as -il-an-; an applicativized reciprocal as -il-an- or with the reciprocal doubled, -an-il-an-, never as -an-il- or -il-an-il-.

theorem Hyman2003.repeated_morph (G : Grammar) (i : Input) (x : Ext) : [x, x] ∉ G.outputs i

(18): no output repeats an extension, Menn and MacWhinney's Repeated Morph Constraint.

theorem Hyman2003.three_suffixes : chichewa.outputs [Ext.C, Ext.A, Ext.R] = {[Ext.C, Ext.A, Ext.R]} ∧ chichewa.outputs [Ext.A, Ext.C, Ext.R] = {[Ext.C, Ext.A, Ext.R]} ∧ chichewa.outputs [Ext.C, Ext.R, Ext.A] = {[Ext.C, Ext.A, Ext.R], [Ext.C, Ext.R, Ext.A, Ext.R]} ∧ chichewa.outputs [Ext.A, Ext.R, Ext.C] = {[Ext.C, Ext.A, Ext.R], [Ext.A, Ext.R, Ext.C], [Ext.R, Ext.C, Ext.A]} ∧ chichewa.outputs [Ext.R, Ext.C, Ext.A] = {[Ext.R, Ext.A, Ext.R, Ext.C], [Ext.A, Ext.R, Ext.C], [Ext.C, Ext.A, Ext.R], [Ext.C, Ext.R, Ext.A, Ext.R], [Ext.R, Ext.C, Ext.A]} ∧ chichewa.outputs [Ext.R, Ext.A, Ext.C] = {[Ext.R, Ext.A, Ext.R, Ext.C], [Ext.A, Ext.R, Ext.C], [Ext.C, Ext.A, Ext.R], [Ext.C, Ext.R, Ext.A, Ext.R], [Ext.R, Ext.C, Ext.A]}

The appendix's table (48) of the six scopes of three extensions. The model derives every output Hyman lists but -an-its-il-an-, whose doubled reciprocal his tableaux license without the conjunction, and derives -an-its-il- for the scopes with the reciprocal inside the causative, which he stars: its pairs -an-its- and -its-il- are each licensed, and the paper states no constraint on the non-adjacent -an- … -il-.

Applicative and passive (11), (12)

inductive Hyman2003.Applicative : Type

What a Chichewa applicative licenses (11).

• benefactive : Applicative
• recipient : Applicative
• instrument : Applicative
• locative : Applicative
• circumstance : Applicative

@[instance_reducible]

instance Hyman2003.instDecidableEqApplicative : DecidableEq Applicative

Equations

• Hyman2003.instDecidableEqApplicative x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hyman2003.instReprApplicative : Repr Applicative

Equations

• Hyman2003.instReprApplicative = { reprPrec := Hyman2003.instReprApplicative.repr }

def Hyman2003.instReprApplicative.repr : Applicative → ℕ → Std.Format

Equations

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

def Hyman2003.passiveGrammar : Applicative → Grammar

(12): the ranking of MIRROR (P, A) against TEMPLATE by what the applicative licenses: below for a benefactive, recipient or instrument, free for a locative, above for a circumstance.

Equations

• Hyman2003.passiveGrammar Hyman2003.Applicative.locative = Hyman2003.Grammar.free ![Hyman2003.Licensor.template, Hyman2003.Licensor.mirror Hyman2003.Ext.P Hyman2003.Ext.A]
• Hyman2003.passiveGrammar Hyman2003.Applicative.circumstance = Hyman2003.Grammar.two (Hyman2003.Licensor.mirror Hyman2003.Ext.P Hyman2003.Ext.A) Hyman2003.Licensor.template
• Hyman2003.passiveGrammar x✝ = Hyman2003.Grammar.two Hyman2003.Licensor.template (Hyman2003.Licensor.mirror Hyman2003.Ext.P Hyman2003.Ext.A)

theorem Hyman2003.passive (a : Applicative) : (passiveGrammar a).outputs [Ext.P, Ext.A] = match a with | Applicative.locative => {[Ext.A, Ext.P], [Ext.P, Ext.A]} | Applicative.circumstance => {[Ext.P, Ext.A]} | x => {[Ext.A, Ext.P]}

(11): an applicative of a passive surfaces as -il-idw-, as -idw-il- too for a locative, and only as -idw-il- for a circumstance.

Template morphology and syntax (§3)

The two scopes of causative and applicative surface alike in Chichewa, so the affix order does not recover the syntactic derivation; the passives (22)–(23) show the derivations differ, the instrument becoming subject under one scope and the causee under the other. [Bak85]'s rules derive the subjects from the scope order, and his single-process architecture would have kept the two words apart.

theorem Hyman2003.scope_not_recoverable : chichewa.outputs [Ext.C, Ext.A, Ext.P] = {[Ext.C, Ext.A, Ext.P]} ∧ chichewa.outputs [Ext.A, Ext.C, Ext.P] = {[Ext.C, Ext.A, Ext.P]}

theorem Hyman2003.mirror_predicts_distinct_words : (Baker1985.word (Morphology.Morph.root "lim") [(Baker1985.Process.causative, Morphology.Morph.suff "its"), (Baker1985.Process.applicative, Morphology.Morph.suff "il"), (Baker1985.Process.passive, Morphology.Morph.suff "idw")]).toList ≠ (Baker1985.word (Morphology.Morph.root "lim") [(Baker1985.Process.applicative, Morphology.Morph.suff "il"), (Baker1985.Process.causative, Morphology.Morph.suff "its"), (Baker1985.Process.passive, Morphology.Morph.suff "idw")]).toList

Under the Mirror Principle the two derivations build different words, -its-il-idw- and -il-its-idw-.

def Hyman2003.Ext.toProcess : Ext → Baker1985.Process

[Bak85]'s process for an extension.

Equations

• Hyman2003.Ext.C.toProcess = Baker1985.Process.causative
• Hyman2003.Ext.A.toProcess = Baker1985.Process.applicative
• Hyman2003.Ext.R.toProcess = Baker1985.Process.reciprocal
• Hyman2003.Ext.P.toProcess = Baker1985.Process.passive

def Hyman2003.chichewaRules : Baker1985.Grammar

Chichewa under [Bak85]'s rules: the Chamorro-type causative, whose causee becomes the object, and the passive of the first object.

Equations

• Hyman2003.chichewaRules = { causative := Baker1985.CausativeType.chamorro }

The paper's examples

def Hyman2003.Ext.of? : Char → Option Ext

An extension by its letter in the template.

Equations

• Hyman2003.Ext.of? 'C' = some Hyman2003.Ext.C
• Hyman2003.Ext.of? 'A' = some Hyman2003.Ext.A
• Hyman2003.Ext.of? 'R' = some Hyman2003.Ext.R
• Hyman2003.Ext.of? 'P' = some Hyman2003.Ext.P
• Hyman2003.Ext.of? x✝ = none

def Hyman2003.exts? (r : Datum) (key : String) : Option (List Ext)

A row's feature as a sequence of extensions.

Equations

• Hyman2003.exts? r key = (r.feature? key).bind fun (s : String) => List.mapM Hyman2003.Ext.of? s.toList

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

A row's scope order, innermost first.

Equations

• Hyman2003.scope? r = Hyman2003.exts? r "scope"

def Hyman2003.suffixes? (r : Datum) : Option Candidate

A row's suffix order, innermost first.

Equations

• Hyman2003.suffixes? r = Hyman2003.exts? r "suffixes"

def Hyman2003.grammar? (r : Datum) : Option Grammar

A row's grammar.

Equations

• Hyman2003.grammar? r = match r.language with | "nyan1308" => some Hyman2003.chichewa | "chim1312" => some Hyman2003.chimwiini | x => none

def Hyman2003.subject? (r : Datum) : Option Baker1985.Arg

The passive subject a row reports.

Equations

• Hyman2003.subject? r = r.parse? "subject" [("instrument", Baker1985.Arg.applied), ("causee", Baker1985.Arg.agent)]

theorem Hyman2003.rows_outputs (r : Datum) : r ∈ Examples.all → subject? r = none → ∀ G ∈ grammar? r, ∀ i ∈ scope? r, ∀ c ∈ suffixes? r, r.judgment = Judgment.acceptable ↔ c ∈ G.outputs i

Every form the paper judges is acceptable exactly when it is an output of its scope.

theorem Hyman2003.rows_passive (r : Datum) : r ∈ Examples.all → ∀ i ∈ scope? r, ∀ a ∈ subject? r, (r.judgment = Judgment.acceptable ↔ ∃ st ∈ Baker1985.outcomes chichewaRules (List.map Ext.toProcess i) (Baker1985.initial false true), Voice.Stage.subjects st = [a]) ∧ ∀ c ∈ suffixes? r, c ∈ chichewa.outputs i

(22)–(23): a passive is acceptable exactly when [Bak85]'s rules, run in the order of scope, make the reported argument the subject; and its affix order is the one output of either scope.