Docs / Morphology / Exponence / Containment / Defs

Rule sets over containment hierarchies

import Linglib.Morphology.Exponence.Containment.Defs · namespace Morphology.Containment

The rules of the two realizational engines over an n-grade containment hierarchy, where grade g's structure contains every lower grade's. A SpanRule is a Distributed Morphology rule of exponence realizing the initial span [0, spans], optionally conditioned on a higher head; it applies, by the Subset Principle, at every grade containing all it mentions, the up-set of its threshold. A SupersetRule is a nanosyntax lexical entry storing the constituent [0, spans]; it applies, by the Superset Principle, at every grade its constituent contains, the down-set of spans. Specificity is threshold comparison for the first and span comparison for the second, in opposite directions.

Main definitions

SpanRule, SpanRule.threshold: a rule of exponence and the least grade it applies at.
SupersetRule: a lexical entry storing an initial span.
Terminal, Adjacent, Markedness, Grounded: well-formedness conditions on rule sets of span rules.

Main results

SpanRule.applySet_subset_iff: a rule is more specific than another iff its threshold is higher.
SupersetRule.applySet_subset_iff: an entry is more specific than another iff its span is smaller, the nanosyntax principle Minimize Junk.
markedness_iff_grounded: under adjacency the markedness condition is the downward closure of thresholds.

References

Bobaljik 2012, Universals in comparative morphology: Suppletion, superlatives, and the structure of words formalized
Caha 2009, The Nanosyntax of Case formalized
Kiparsky 1973, “Elsewhere” in Phonology
Starke 2009, Nanosyntax: A Short Primer to a New Approach to Language

The Subset reading: rules of exponence

A rule of exponence (Bobaljik 2012) over an n-grade containment hierarchy realizes the initial span [0, spans], the bare root when spans = 0 and a portmanteau when spans > 0, and applies only when its conditioning head context, if any, is present. In Latin bon is ⟨bon, 0, none⟩, mel- is ⟨mel, 0, some 1⟩ and the portmanteau opt- is ⟨opt, 1, some 2⟩.

structure SpanRule L53–64

(n : ℕ) (F : Type u_2) :

Type u_2

exponent : F
The exponent inserted for the span.
spans : Fin n
The upper end of the exponed initial span [0, spans].
context : Option (Fin n)
The head whose presence conditions the rule, if any.

Derives DecidableEq, Repr.

Used by SpanRule.threshold, instRuleSpanRuleFin, SpanRule.applies_iff, SpanRule.exponent_eq, SpanRule.applySet_subset_iff, SpanRule.applySet_ssubset_iff, Terminal, instDecidableTerminal, Adjacent, instDecidableAdjacent, Markedness, instDecidableMarkedness, Grounded, instDecidableGrounded, Grounded.markedness, markedness_iff_grounded

Used in Morphology/Exponence/Containment/Contiguity, Morphology/Exponence/Containment/Selection, Bobaljik2012, Graf2019, SmithMoskalEtAl2019

The least grade at which the rule applies, the least containing both the exponed span and the conditioning head.

def SpanRule.threshold L66–69

{n : ℕ} {F : Type u_1} (it : SpanRule n F) :

Fin n

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

Built from

Used by instRuleSpanRuleFin, instDecidableRelSpanRuleFinApplies, SpanRule.applies_iff, SpanRule.applySet_subset_iff, SpanRule.applySet_ssubset_iff

Used in Morphology/Exponence/Containment/Contiguity, Morphology/Exponence/Containment/Selection, Bobaljik2012, SmithMoskalEtAl2019

Over a linear hierarchy the applicability sets are nested, so specificity is the reverse of threshold order and the Elsewhere ordering (Kiparsky 1973) is total.

theorem SpanRule.applySet_subset_iff L86–89

{n : ℕ} {F : Type u_1} {it jt : SpanRule n F} :

Exponence.applySet it ⊆ Exponence.applySet jt ↔ jt.threshold ≤ it.threshold

Built from ,

L91–92

Well-formedness conditions on rule sets

Each generalization hypothesizes exactly the conditions it needs, and rule sets violating a condition witness the corresponding unattested pattern.

Every rule expones the bare root, so the rule set has no portmanteaux.

def Terminal L101–103

{n : ℕ} {F : Type u_1} (v : Exponence.RuleSet (SpanRule n F)) :

Prop

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

Built from

Used by instDecidableTerminal

Used in Morphology/Exponence/Containment/Contiguity, Bobaljik2012, SmithMoskalEtAl2019

L105–106

Conditioning heads are adjacent to the exponed span, the adjacency condition on contextual allomorphy that Bobaljik 2012 tentatively adopts.

def Adjacent L108–111

{n : ℕ} {F : Type u_1} (v : Exponence.RuleSet (SpanRule n F)) :

Prop

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

Built from

Used by instDecidableAdjacent, markedness_iff_grounded

Used in Morphology/Exponence/Containment/Contiguity, Bobaljik2012, Graf2019, SmithMoskalEtAl2019

L113–114

Bobaljik 2012's markedness condition requires, for each context-sensitive rule involving a node, a context-free rule involving that node. A rule involves the nodes [0, k] of its span, context-sensitively below its threshold, and a context-free rule for [0, k] is one of threshold k, so every threshold below a rule's and within its span is some rule's.

def Markedness L116–121

{n : ℕ} {F : Type u_1} (v : Exponence.RuleSet (SpanRule n F)) :

Prop

The definition is too large to print here; read it in the source.

Built from

Used by instDecidableMarkedness, Grounded.markedness, markedness_iff_grounded

Used in Morphology/Exponence/Containment/Contiguity, Bobaljik2012, Graf2019, SmithMoskalEtAl2019

L123–124

A rule set is grounded when its thresholds are closed downward. This strengthens the markedness condition to the thresholds between a rule's span and its context, which adjacency leaves empty.

def Grounded L126–130

{n : ℕ} {F : Type u_1} (v : Exponence.RuleSet (SpanRule n F)) :

Prop

The definition is too large to print here; read it in the source.

Built from

Used by instDecidableGrounded, Grounded.markedness, markedness_iff_grounded

Used in Morphology/Exponence/Containment/Contiguity, Bobaljik2012, SmithMoskalEtAl2019

L132–133

L135–136

Under adjacency the markedness condition is the downward closure of thresholds.

theorem markedness_iff_grounded L138–151

{n : ℕ} {F : Type u_1} {v : Exponence.RuleSet (SpanRule n F)} (hA : Adjacent v) :

Markedness v ↔ Grounded v

Built from , , ,

The Superset reading: lexical entries

A nanosyntax lexical entry over an n-grade containment hierarchy stores the constituent [0, spans], with no contextual condition, in the pointer-free idealization of Caha 2009.

structure SupersetRule L155–162

(n : ℕ) (F : Type u_2) :

Type u_2

exponent : F
The exponent the entry spells out.
spans : Fin n
The upper end of the stored constituent [0, spans].

Derives DecidableEq, Repr.

Used by instRuleSupersetRuleFin, SupersetRule.applies_iff, SupersetRule.exponent_eq, SupersetRule.applySet_subset_iff, SupersetRule.applySet_ssubset_iff

Used in Morphology/Exponence/Containment/Contiguity, Morphology/Exponence/Containment/Selection, Morphology/Nanosyntax/Lexicalization, Morphology/Nanosyntax/TreeSpellout, Bobaljik2012 and 2 more

An entry is more specific than another iff it stores the smaller constituent, the nanosyntax principle Minimize Junk.

theorem SupersetRule.applySet_subset_iff L180–182

{n : ℕ} {F : Type u_1} {e e' : SupersetRule n F} :

Exponence.applySet e ⊆ Exponence.applySet e' ↔ e.spans ≤ e'.spans

Built from

L184