Vocabularies over containment hierarchies: rules and specificity

The carrier for the realizational engine of [Bob12]'s comparative-suppletion generalizations, over an arbitrary n-grade containment hierarchy. An SpanRule realizes the initial span [0, spans] of the hierarchy, optionally conditioned on a higher head. One carrier carries two Exponence.Rule views: the Subset reading (SpanRule, applicability is threshold containment) is DM Elsewhere insertion; the Superset reading (SupersetRule, applicability is constituent containment) is nanosyntax spellout, dual à la OrderDual.

Main declarations

• SpanRule — exponent, exponed span [0, spans], optional conditioning head
• SpanRule.threshold, AppliesAt, MoreSpecific — Subset applicability and its moreSpecific_iff_threshold_le reflection
• SpanRule.Matches, SupersetRule — Superset applicability and its matches_imp_iff_spans_le reflection
• Terminal, Adjacent, Antihomophonous, Grounded, ContextFree — well-formedness conditions on vocabularies

Rules of exponence and derived specificity

structure Morphology.Containment.SpanRule (n : ℕ) (F : Type u_2) : Type u_2

A rule of exponence ([Bob12]) over an n-grade containment hierarchy. The rule realizes the initial span [0, spans] — the bare root when spans = 0, a root+heads portmanteau when spans > 0 — and applies only when its optional conditioning head context is present. Latin ([Bob12] (204)): bon is ⟨bon, 0, none⟩, mel- is ⟨mel, 0, some 1⟩, the portmanteau opt- is ⟨opt, 1, some 2⟩.

• exponent : F

  The phonological exponent inserted for the span.

• spans : Fin n

  Upper end of the exponed initial span [0, spans].

• context : Option (Fin n)

  Head whose presence conditions the rule, if any.

@[implicit_reducible]

instance Morphology.Containment.instDecidableEqSpanRule {n✝ : ℕ} {F✝ : Type u_2} [DecidableEq F✝] : DecidableEq (SpanRule n✝ F✝)

Equations

• Morphology.Containment.instDecidableEqSpanRule = Morphology.Containment.instDecidableEqSpanRule.decEq

def Morphology.Containment.instDecidableEqSpanRule.decEq {n✝ : ℕ} {F✝ : Type u_2} [DecidableEq F✝] (x✝ x✝¹ : SpanRule n✝ F✝) : Decidable (x✝ = x✝¹)

Equations

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

def Morphology.Containment.instReprSpanRule.repr {n✝ : ℕ} {F✝ : Type u_2} [Repr F✝] : SpanRule n✝ F✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Containment.instReprSpanRule {n✝ : ℕ} {F✝ : Type u_2} [Repr F✝] : Repr (SpanRule n✝ F✝)

Equations

• Morphology.Containment.instReprSpanRule = { reprPrec := Morphology.Containment.instReprSpanRule.repr }

def Morphology.Containment.SpanRule.threshold {n : ℕ} {F : Type u_1} (it : SpanRule n F) : Fin n

The least grade at which the rule is applicable: everything the rule mentions — exponed span and conditioning context — must be contained in the structure.

Equations

• it.threshold = max it.spans (it.context.getD it.spans)

def Morphology.Containment.SpanRule.AppliesAt {n : ℕ} {F : Type u_1} (it : SpanRule n F) (g : Fin n) : Prop

A rule applies at grade g when grade g's structure contains everything the rule mentions.

Equations

• it.AppliesAt g = (it.threshold ≤ g)

@[implicit_reducible]

instance Morphology.Containment.SpanRule.instDecidableAppliesAt {n : ℕ} {F : Type u_1} (it : SpanRule n F) (g : Fin n) : Decidable (it.AppliesAt g)

Equations

• it.instDecidableAppliesAt g = Morphology.Containment.SpanRule.instDecidableAppliesAt._aux_1 it g

def Morphology.Containment.SpanRule.MoreSpecific {n : ℕ} {F : Type u_1} (it jt : SpanRule n F) : Prop

A rule it is at least as specific as jt when it applies in a subset of the contexts jt applies in (Pāṇinian specificity).

Equations

• it.MoreSpecific jt = ∀ ⦃g : Fin n⦄, it.AppliesAt g → jt.AppliesAt g

theorem Morphology.Containment.SpanRule.moreSpecific_iff_threshold_le {n : ℕ} {F : Type u_1} {it jt : SpanRule n F} : it.MoreSpecific jt ↔ jt.threshold ≤ it.threshold

Over a linear containment hierarchy, applicability sets are nested upward sets, so derived specificity is threshold comparison — the Elsewhere ordering ([Kip73]) is total.

Well-formedness conditions on vocabularies

Each generalization below hypothesizes exactly the conditions it needs; vocabularies violating a condition witness the corresponding unattested pattern (see the worked examples in Studies/Bobaljik2012.lean).

def Morphology.Containment.Terminal {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Prop

Every rule expones the bare root (no portmanteaux).

Equations

• Morphology.Containment.Terminal v = ∀ (it : Morphology.Containment.SpanRule n F), it ∈ v → ↑it.spans = 0

@[implicit_reducible]

instance Morphology.Containment.instDecidableTerminal {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Decidable (Terminal v)

Equations

• Morphology.Containment.instDecidableTerminal v = id inferInstance

def Morphology.Containment.Adjacent {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Prop

Conditioning heads are adjacent to the exponed span — [Bob12]'s (tentatively adopted) adjacency condition on contextual allomorphy.

Equations

• Morphology.Containment.Adjacent v = ∀ (it : Morphology.Containment.SpanRule n F), it ∈ v → ∀ (c : Fin n), it.context = some c → ↑c = ↑it.spans + 1

@[implicit_reducible]

instance Morphology.Containment.instDecidableAdjacent {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Decidable (Adjacent v)

Equations

• Morphology.Containment.instDecidableAdjacent v = id inferInstance

def Morphology.Containment.Antihomophonous {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Prop

Distinct rules carry distinct exponents — [Bob12]'s Antihomophony assumption (44), closing the loophole where a surface-ABA pattern is really an ABC with accidental A ≡ C homophony.

Equations

• Morphology.Containment.Antihomophonous v = ∀ (it : Morphology.Containment.SpanRule n F), it ∈ v → ∀ (jt : Morphology.Containment.SpanRule n F), jt ∈ v → it.exponent = jt.exponent → it = jt

@[implicit_reducible]

instance Morphology.Containment.instDecidableAntihomophonousOfDecidableEq {n : ℕ} {F : Type u_1} [DecidableEq F] (v : List (SpanRule n F)) : Decidable (Antihomophonous v)

Equations

• Morphology.Containment.instDecidableAntihomophonousOfDecidableEq v = id inferInstance

def Morphology.Containment.Grounded {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Prop

[Bob12]'s markedness condition (202): a context-sensitive rule of exponence involving a node requires a context-free rule involving that node. Under the threshold encoding, this is downward closure of the vocabulary's threshold set.

Equations

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

@[implicit_reducible]

instance Morphology.Containment.instDecidableGrounded {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Decidable (Grounded v)

Equations

• Morphology.Containment.instDecidableGrounded v = id inferInstance

def Morphology.Containment.ContextFree {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Prop

The nanosyntax restriction, in the pointer-free idealization of [Cah09]: entries store bare constituents, with no DM-style contextual environment.

Equations

• Morphology.Containment.ContextFree v = ∀ (it : Morphology.Containment.SpanRule n F), it ∈ v → it.context = none

@[implicit_reducible]

instance Morphology.Containment.instDecidableContextFree {n : ℕ} {F : Type u_1} (v : List (SpanRule n F)) : Decidable (ContextFree v)

Equations

• Morphology.Containment.instDecidableContextFree v = id inferInstance

The Subset reading: DM Elsewhere insertion

The containment engine implements Morphology.Exponence.Rule directly: applicability is threshold containment (the upper set Set.Ici threshold) and derived specificity is threshold comparison.

@[implicit_reducible]

instance Morphology.Containment.instRuleSpanRuleFin {n : ℕ} {F : Type u_1} : Exponence.Rule (SpanRule n F) (Fin n) F

Equations

• Morphology.Containment.instRuleSpanRuleFin = { exponent := Morphology.Containment.SpanRule.exponent, Applies := fun (it : Morphology.Containment.SpanRule n F) (i : Fin n) => it.threshold ≤ i }

@[implicit_reducible]

instance Morphology.Containment.instPreorderSpanRule {n : ℕ} {F : Type u_1} : Preorder (SpanRule n F)

Equations

• Morphology.Containment.instPreorderSpanRule = Morphology.Exponence.toPreorder

@[implicit_reducible]

instance Morphology.Containment.instDecidableRelSpanRuleFinApplies {n : ℕ} {F : Type u_1} : DecidableRel Exponence.Applies

Equations

• Morphology.Containment.instDecidableRelSpanRuleFinApplies it g = it.threshold.decLe g

@[simp]

theorem Morphology.Containment.SpanRule.applies_iff {n : ℕ} {F : Type u_1} {it : SpanRule n F} {g : Fin n} : Exponence.Applies it g ↔ it.threshold ≤ g

Subset applicability is threshold containment.

theorem Morphology.Containment.SpanRule.le_iff {n : ℕ} {F : Type u_1} {it jt : SpanRule n F} : it ≤ jt ↔ it.MoreSpecific jt

Containment specificity is the shared core's specificity order.

The Superset reading: nanosyntax spellout

One carrier, a dual view: the entry can spell out grade g when its stored constituent contains g (the down-set Set.Iic spans), and smallest-match selection is Pāṇinian specificity under superset matching. A distinct type synonym so the two readings carry different Exponence.Rule instances on one carrier, mirroring OrderDual.

def Morphology.Containment.SpanRule.Matches {n : ℕ} {F : Type u_1} (it : SpanRule n F) (g : Fin n) : Prop

The Superset Principle ([Sta09a]): an entry can spell out grade g when the constituent it stores contains grade g's structure. Anti-monotone in g, dually to AppliesAt.

Equations

• it.Matches g = (g ≤ it.spans)

@[implicit_reducible]

instance Morphology.Containment.instDecidableMatches {n : ℕ} {F : Type u_1} (it : SpanRule n F) (g : Fin n) : Decidable (it.Matches g)

Equations

• Morphology.Containment.instDecidableMatches it g = Morphology.Containment.instDecidableMatches._aux_1 it g

theorem Morphology.Containment.SpanRule.Matches.anti {n : ℕ} {F : Type u_1} {it : SpanRule n F} {g g' : Fin n} (h : it.Matches g') (hg : g ≤ g') : it.Matches g

theorem Morphology.Containment.SpanRule.matches_imp_iff_spans_le {n : ℕ} {F : Type u_1} {it jt : SpanRule n F} : (∀ ⦃g : Fin n⦄, it.Matches g → jt.Matches g) ↔ it.spans ≤ jt.spans

Minimize Junk derived, dually to SpanRule.moreSpecific_iff_threshold_le: an entry matches in a subset of the structures another matches in iff it stores the smaller constituent — smallest-match selection is Pāṇinian specificity under superset matching.

def Morphology.Containment.SupersetRule (n : ℕ) (F : Type u_2) : Type u_2

The Superset reading of an exponence rule: an entry spells out grade g when its stored constituent contains g (the down-set Set.Iic spans), dually to the Subset reading of SpanRule.

Equations

• Morphology.Containment.SupersetRule n F = Morphology.Containment.SpanRule n F

@[implicit_reducible]

instance Morphology.Containment.instRuleSupersetRuleFin {n : ℕ} {F : Type u_1} : Exponence.Rule (SupersetRule n F) (Fin n) F

Equations

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

@[implicit_reducible]

instance Morphology.Containment.instPreorderSupersetRule {n : ℕ} {F : Type u_1} : Preorder (SupersetRule n F)

Equations

• Morphology.Containment.instPreorderSupersetRule = Morphology.Exponence.toPreorder

@[implicit_reducible]

instance Morphology.Containment.instDecidableRelSupersetRuleFinApplies {n : ℕ} {F : Type u_1} : DecidableRel Exponence.Applies

Equations

• Morphology.Containment.instDecidableRelSupersetRuleFinApplies it g = g.decLe it.spans

def Morphology.Containment.SpanRule.superset {n : ℕ} {F : Type u_1} (it : SpanRule n F) : SupersetRule n F

Read an exponence rule under the Superset reading.

Equations

• it.superset = it

@[simp]

theorem Morphology.Containment.SupersetRule.applies_iff {n : ℕ} {F : Type u_1} {it : SupersetRule n F} {g : Fin n} : Exponence.Applies it g ↔ g ≤ it.spans

Superset applicability is constituent containment.

theorem Morphology.Containment.SupersetRule.le_iff {n : ℕ} {F : Type u_1} {it jt : SupersetRule n F} : it ≤ jt ↔ it.spans ≤ jt.spans

Minimize Junk is the Superset reading's specificity order: smaller span = more specific.

theorem Morphology.Containment.SpanRule.subset_le_iff_superset_le {n : ℕ} {F : Type u_1} {it jt : SpanRule n F} (hit : it.context = none) (hjt : jt.context = none) : it ≤ jt ↔ jt.superset ≤ it.superset

Subset/Superset duality over context-free vocabularies (the nanosyntax idealization): DM-style Subset specificity of it over jt is Superset specificity of jt over it. With contextual restrictions the Subset order compares thresholds, not spans, and the duality is only one-directional.