Bobaljik 2000: the ins and outs of contextual allomorphy

[Bob00] argues from Itelmen agreement that Vocabulary Insertion is cyclic from the root outward and rewrites a morpheme's features as it discharges them, so that conditioning is asymmetric: an inner morpheme may look outward at the syntactic features of morphemes not yet realized, but an outer morpheme cannot look inward at features already discharged. The Class II marker between the root and object agreement is conditioned by the class of the root inside it and by the person of both arguments outside it, object agreement by the subject outside it, and the subject prefix — last to be inserted — by nothing inside. This file runs that derivation over the complex head with hierarchical locality and rewriting, and shows the asymmetry as a consequence: with non-deletion, the inner agreement features would still be visible to the prefix.

Main results

• itelmen_rows: the four forms (9)–(10) from one Vocabulary.
• prefix_sees_no_agreement: at the subject prefix, the rewritten object agreement is invisible; nondeletion_exposes that only rewriting hides it.
• outward_features_only: the Class II marker conditioned by both arguments sees their features, not exponents.

References

[Bob00], [HM93].

inductive Bobaljik2000.Feature : Type

• root (s : String) : Feature
• classII : Feature
• tense : Feature
• classMarker : Feature
• agrO : Feature
• agrS : Feature
• obj3 : Feature
• first : Feature
• second : Feature
• sg : Feature
• pl : Feature

@[instance_reducible]

instance Bobaljik2000.instDecidableEqFeature : DecidableEq Feature

Equations

• Bobaljik2000.instDecidableEqFeature = Bobaljik2000.instDecidableEqFeature.decEq

def Bobaljik2000.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Bobaljik2000.instReprFeature : Repr Feature

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Bobaljik2000.instReprFeature.repr Bobaljik2000.Feature.agrO prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bobaljik2000.Feature.agrO")).group prec✝
• Bobaljik2000.instReprFeature.repr Bobaljik2000.Feature.agrS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bobaljik2000.Feature.agrS")).group prec✝
• Bobaljik2000.instReprFeature.repr Bobaljik2000.Feature.obj3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bobaljik2000.Feature.obj3")).group prec✝
• Bobaljik2000.instReprFeature.repr Bobaljik2000.Feature.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bobaljik2000.Feature.sg")).group prec✝
• Bobaljik2000.instReprFeature.repr Bobaljik2000.Feature.pl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bobaljik2000.Feature.pl")).group prec✝

def Bobaljik2000.vocab : List (DistributedMorphology.VocabularyItem Feature String)

Present -s; the Class II marker -ki- under a first-person subject acting on a third-person object and -c- under a second-singular one; object agreement -cen under a first-person subject and -in under a second-singular; the subject prefix t- for first singular, null for second singular.

Equations

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

def Bobaljik2000.word (r : String) (classII? : Bool) (subj obj : List Feature) : DistributedMorphology.ComplexHead Feature String

√-T-(II)-AgrO-AgrS, the Class II marker present for a Class II root.

Equations

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

def Bobaljik2000.insert (dis : DistributedMorphology.ComplexHead.Discharge) (w : DistributedMorphology.ComplexHead Feature String) : DistributedMorphology.ComplexHead Feature String

Equations

• Bobaljik2000.insert dis w = w.insertAll (fun (x : String) => x = "") Bobaljik2000.vocab DistributedMorphology.ComplexHead.Locality.hierarchical (fun (x : String) => []) dis

def Bobaljik2000.morphs (w : DistributedMorphology.ComplexHead Feature String) : List String

Equations

• Bobaljik2000.morphs w = List.filter (fun (x : String) => decide (x ≠ "")) (Bobaljik2000.insert DistributedMorphology.ComplexHead.Discharge.rewriting w).exponents

def Bobaljik2000.parseArg : String → Option (List Feature)

Equations

• Bobaljik2000.parseArg "1sg" = some [Bobaljik2000.Feature.first, Bobaljik2000.Feature.sg]
• Bobaljik2000.parseArg "2sg" = some [Bobaljik2000.Feature.second, Bobaljik2000.Feature.sg]
• Bobaljik2000.parseArg "3sg" = some [Bobaljik2000.Feature.obj3, Bobaljik2000.Feature.sg]
• Bobaljik2000.parseArg "3pl" = some [Bobaljik2000.Feature.obj3, Bobaljik2000.Feature.pl]
• Bobaljik2000.parseArg x✝ = none

def Bobaljik2000.ofRow (ex : Data.Examples.LinguisticExample) : Option (DistributedMorphology.ComplexHead Feature String × List String)

Equations

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

def Bobaljik2000.rows : List (DistributedMorphology.ComplexHead Feature String × List String)

Equations

• Bobaljik2000.rows = List.filterMap Bobaljik2000.ofRow Bobaljik2000.Examples.all

theorem Bobaljik2000.itelmen_rows (r : DistributedMorphology.ComplexHead Feature String × List String) : r ∈ rows → morphs r.1 = r.2

The forms (9)–(10).

def Bobaljik2000.bring : DistributedMorphology.ComplexHead Feature String

(9b): t-t-s-ki-cen.

Equations

• Bobaljik2000.bring = Bobaljik2000.word "t" true [Bobaljik2000.Feature.first, Bobaljik2000.Feature.sg] [Bobaljik2000.Feature.obj3, Bobaljik2000.Feature.pl]

theorem Bobaljik2000.prefix_sees_no_agreement : Feature.agrO ∉ (((insert DistributedMorphology.ComplexHead.Discharge.rewriting bring).insertUpTo (fun (x : String) => x = "") vocab DistributedMorphology.ComplexHead.Locality.hierarchical (fun (x : String) => []) DistributedMorphology.ComplexHead.Discharge.rewriting 3).contextAt (fun (x : String) => x = "") DistributedMorphology.ComplexHead.Locality.hierarchical (fun (x : String) => []) 3).leftCtx.flatten

When the subject prefix is reached under rewriting, the object agreement inside it has discharged its features: nothing of agrO remains to condition the prefix, the asymmetry of (12).

theorem Bobaljik2000.nondeletion_exposes : Feature.agrO ∈ ((bring.insertUpTo (fun (x : String) => x = "") vocab DistributedMorphology.ComplexHead.Locality.hierarchical (fun (x : String) => []) DistributedMorphology.ComplexHead.Discharge.nondeletion 3).contextAt (fun (x : String) => x = "") DistributedMorphology.ComplexHead.Locality.hierarchical (fun (x : String) => []) 3).leftCtx.flatten

Under non-deletion the same context carries agrO: symmetric conditioning, as in [HM93], would let the prefix see inward.

theorem Bobaljik2000.outward_features_only : ((bring.insertUpTo (fun (x : String) => x = "") vocab DistributedMorphology.ComplexHead.Locality.hierarchical (fun (x : String) => []) DistributedMorphology.ComplexHead.Discharge.rewriting 1).contextAt (fun (x : String) => x = "") DistributedMorphology.ComplexHead.Locality.hierarchical (fun (x : String) => []) 1).rightCtx = [[Feature.agrO, Feature.obj3, Feature.pl], [Feature.agrS, Feature.first, Feature.sg]]

The Class II marker, second to be inserted, sees both agreement morphemes outside it bare: their features, at hierarchical distance one and two.