Dalrymple & Kaplan 2000: Feature Indeterminacy and Feature Resolution

[DK00a]

Set-valued syntactic features, against atomic-value-plus-equality. Two phenomena, one representational move (§4, eq. 25: "Sets encode indeterminate feature possibilities"):

• Indeterminacy (distributive features: case, noun class, vform): a syncretic form bears a set of atomic values — German was {NOM, ACC} — and contextual requirements are membership assertions (ACC ∈ (↑ OBJ CASE)), not equalities. The paper refutes the two obvious alternatives: disjunctive specification DNF-collapses into a homophone listing (§3.1), and underspecification both derives NOM = ACC by transitivity of equality and overgenerates dative contexts (§3.2).
• Resolution (nondistributive features: person, gender): a coordinate phrase's person/gender is the union of its conjuncts' marker sets (§6, §7) — person values are subsets of {S, H} ({S} 1exc, {S,H} 1inc, {H} 2nd, {} 3rd), and the union analysis predicts the full Fula paradigm (87–88), the collapsed English/Spanish/Slovak system (91–92), and the gender tables of Hindi (112), Icelandic (120), and Slovene with the conjunction contributing F (126–127).

The deliberate sharp line (§8): resolving features are never indeterminate — Hindi wah is masc-or-fem by wide-scope disjunction (ambiguity), not by a set value, which is why *wah arrived.MASC and arrived.FEM fails (128).

This is the flagship counterexample to treating the flat information order (the subsumption/unification substrate at the end of this file) as linguistically definitional: indeterminate agreement is an annotation-level phenomenon demanding non-flat (set-valued) slots. toIndet below certifies the relationship — the flat order embeds into the (superset-ordered) indeterminacy lattice as the determinate fragment, with ⊥ (no information) mapping to the universal set.

Formal highlights replicated as theorems: the German/Polish contrast set ((17)/(28) vs (32); (40) vs (41)), the §3 refutations, verb-side indeterminacy (Xhosa (56), Chicheŵa (59), German kaufen (62)), the resolution tables, the minimal-model derivation of José y tu (96–97), the Sag-et-al intersection refutation (§6.5, (100)–(101) vs Fula), and the De Morgan duality (102–103) — which is mathlib's Finset.compl_union. The person-marker sets also project onto the binary person decomposition of Features/Person.lean, with the inclusive/exclusive collapse made explicit.

§4: indeterminate values are sets; checking is membership

@[reducible, inline]

abbrev DalrympleKaplan2000.IndetVal (α : Type u_1) : Type u_1

An indeterminate feature value: the set of atomic values the form can realize (eq. 25). Singleton = determinate.

Equations

• DalrympleKaplan2000.IndetVal α = Finset α

@[reducible, inline]

abbrev DalrympleKaplan2000.requires {α : Type u_1} [DecidableEq α] (c : α) (v : IndetVal α) : Prop

Contextual requirement (eq. 27): the required atom is a member of the value set.

Equations

• DalrympleKaplan2000.requires c v = (c ∈ v)

def DalrympleKaplan2000.wer : IndetVal Case

German relative pronouns (26): wer nominative, was syncretic, wem dative.

Equations

• DalrympleKaplan2000.wer = {Case.nom}

def DalrympleKaplan2000.was : IndetVal Case

Equations

• DalrympleKaplan2000.was = {Case.nom, Case.acc}

def DalrympleKaplan2000.wem : IndetVal Case

Equations

• DalrympleKaplan2000.wem = {Case.dat}

theorem DalrympleKaplan2000.was_satisfies_both : requires Case.acc was ∧ requires Case.nom was

(17)/(28): Ich habe gegessen was übrig war — was satisfies the matrix verb's accusative requirement and the relative clause's nominative requirement at once.

theorem DalrympleKaplan2000.wem_fails_matrix : requires Case.dat wem ∧ ¬requires Case.nom wem

(32): *Wem du vertraust muss klug sein — wem {DAT} satisfies vertraut but not the matrix NOM ∈ requirement.

def DalrympleKaplan2000.kogo : IndetVal Case

Polish (40)/(41): kogo {ACC, GEN} survives coordination of an ACC-taking and a GEN-taking verb; co {NOM, ACC} does not.

Equations

• DalrympleKaplan2000.kogo = {Case.acc, Case.gen}

def DalrympleKaplan2000.co : IndetVal Case

Equations

• DalrympleKaplan2000.co = {Case.nom, Case.acc}

theorem DalrympleKaplan2000.kogo_grammatical : requires Case.acc kogo ∧ requires Case.gen kogo

theorem DalrympleKaplan2000.co_ungrammatical : requires Case.acc co ∧ ¬requires Case.gen co

§3: why the rival accounts fail

def DalrympleKaplan2000.atomicSatisfies (x : Case) (reqs : List Case) : Prop

An atomic-value account: one case value checked by equality against every requirement.

Equations

• DalrympleKaplan2000.atomicSatisfies x reqs = ∀ r ∈ reqs, x = r

theorem DalrympleKaplan2000.underspecification_fails : ¬∃ (x : Case), atomicSatisfies x [Case.acc, Case.nom]

§3.2 (eq. 24): no single atomic value satisfies both verbs of (17) — transitivity of equality would force NOM = ACC.

theorem DalrympleKaplan2000.disjunction_collapses (x : Case) : x ∈ was → ¬atomicSatisfies x [Case.acc, Case.nom]

§3.1 (18)–(21): disjunctive specification means choosing one disjunct per utterance — and every choice from {NOM, ACC} fails one of the two requirements. The set-based account (was_satisfies_both) succeeds where every disjunctive resolution fails: that contrast is the paper's argument.

§4.4: indeterminate requirements (verb-side sets)

theorem DalrympleKaplan2000.xhosa_zibomvu : 7 ∈ {7, 9} ∧ 9 ∈ {7, 9}

Xhosa (54)–(56): zibomvu requires its subject's noun class to be in {7/8, 9/10} (classes as their singular-class numbers), so class-7/8 izandla and class-9/10 neendlebe conjuncts each satisfy it.

def DalrympleKaplan2000.kaufenReq : IndetVal UD.Person

German (60)–(63): kaufen imposes (↑ SUBJ PERSON) ∈ {1, 3}; right-node raising over a 1-person and a 3-person subject satisfies the requirement in each conjunct.

Equations

• DalrympleKaplan2000.kaufenReq = {UD.Person.first, UD.Person.third}

theorem DalrympleKaplan2000.kaufen_rnr : requires UD.Person.first kaufenReq ∧ requires UD.Person.third kaufenReq ∧ ¬requires UD.Person.second kaufenReq

The refinement certificate: the flat order is the determinate fragment

The flat slot order (this file's subsumption substrate below) embeds into the indeterminacy lattice: a determinate commitment ↑x is the singleton {x}, and no information (⊥) is the universal set (any realization possible). Information increases as sets shrink, so the embedding is order-reversing into ⊆ — i.e. an embedding into the superset order. Set-valued slots are a refinement of the flat layer, not a rival to it.

def DalrympleKaplan2000.toIndet : Flat Case → IndetVal Case

A flat slot as an indeterminate value: ⊥ = no commitment = anything goes.

Equations

• DalrympleKaplan2000.toIndet none = Finset.univ
• DalrympleKaplan2000.toIndet (some x_1) = {x_1}

theorem DalrympleKaplan2000.toIndet_injective : Function.Injective toIndet

theorem DalrympleKaplan2000.le_iff_toIndet_superset (a b : Flat Case) : a ≤ b ↔ toIndet b ⊆ toIndet a

The embedding certificate: flat subsumption is superset inclusion of realization sets. More committed = smaller set; ⊥ sits below everything because univ contains everything.

§§5–6: feature resolution — person as marker sets, resolution as union

inductive DalrympleKaplan2000.Marker : Type

The person markers (§6): S speaker, H hearer. §6.3 argues no third marker is attested (Sierra Popoluca's "limited inclusive" is an inclusive dual, per Noyer).

• S : Marker
• H : Marker

@[instance_reducible]

instance DalrympleKaplan2000.instDecidableEqMarker : DecidableEq Marker

Equations

• DalrympleKaplan2000.instDecidableEqMarker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DalrympleKaplan2000.instReprMarker : Repr Marker

Equations

• DalrympleKaplan2000.instReprMarker = { reprPrec := DalrympleKaplan2000.instReprMarker.repr }

def DalrympleKaplan2000.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DalrympleKaplan2000.instFintypeMarker : Fintype Marker

Equations

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

@[reducible, inline]

abbrev DalrympleKaplan2000.PersonSet : Type

Equations

• DalrympleKaplan2000.PersonSet = Finset DalrympleKaplan2000.Marker

def DalrympleKaplan2000.fula1exc : PersonSet

Fula's four-way system (87): full use of the marker inventory.

Equations

• DalrympleKaplan2000.fula1exc = {DalrympleKaplan2000.Marker.S}

def DalrympleKaplan2000.fula1inc : PersonSet

Equations

• DalrympleKaplan2000.fula1inc = {DalrympleKaplan2000.Marker.S, DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.fula2 : PersonSet

Equations

• DalrympleKaplan2000.fula2 = {DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.fula3 : PersonSet

Equations

• DalrympleKaplan2000.fula3 = ∅

def DalrympleKaplan2000.resolve (p q : PersonSet) : PersonSet

Resolution is union (77, 93): "the person feature of a coordinate structure is resolved to be the UNION of the person features of the conjuncts".

Equations

• DalrympleKaplan2000.resolve p q = p ∪ q

theorem DalrympleKaplan2000.fula_table : resolve fula1exc fula2 = fula1inc ∧ resolve (resolve fula1exc fula2) fula3 = fula1inc ∧ resolve fula1exc fula3 = fula1exc ∧ resolve fula2 fula3 = fula2 ∧ resolve fula3 fula3 = fula3

The Fula resolution table (78)/(88), in full.

def DalrympleKaplan2000.eng1 : PersonSet

English/Spanish/Slovak collapse the inclusive/exclusive distinction (§6.2): all first person is {S, H} — preserving only attested syntactic distinctions at the cost of the referential correlation (Aronoff's impersonal you, French on).

Equations

• DalrympleKaplan2000.eng1 = {DalrympleKaplan2000.Marker.S, DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.eng2 : PersonSet

Equations

• DalrympleKaplan2000.eng2 = {DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.eng3 : PersonSet

Equations

• DalrympleKaplan2000.eng3 = ∅

theorem DalrympleKaplan2000.english_table : resolve eng1 eng2 = eng1 ∧ resolve eng1 eng3 = eng1 ∧ resolve eng2 eng3 = eng2 ∧ resolve eng3 eng3 = eng3

The collapsed-system resolution table (91)/(92).

theorem DalrympleKaplan2000.jose_y_tu : resolve eng3 eng2 = eng2 ∧ resolve eng3 eng2 ≠ eng1

José y tu habláis (95)–(99): the resolved person of 3 ∪ 2 is {H} — the minimal model — so the 2PL verb's constraining equation =c {H} succeeds and the 1PL verb's =c {S,H} fails.

The substrate bridge: Person.resolve is marker-set union

def DalrympleKaplan2000.markerSetOf : Person → Option PersonSet

The marker sets of the canonical quadripartition values — the Fula encoding (87). Plain first underdetermines clusivity (their §6.2 English collapse picks {S, H} by stipulation), and zero is outside the system, so both map to none.

Equations

• DalrympleKaplan2000.markerSetOf Person.firstExclusive = some DalrympleKaplan2000.fula1exc
• DalrympleKaplan2000.markerSetOf Person.firstInclusive = some DalrympleKaplan2000.fula1inc
• DalrympleKaplan2000.markerSetOf Person.second = some DalrympleKaplan2000.fula2
• DalrympleKaplan2000.markerSetOf Person.third = some DalrympleKaplan2000.fula3
• DalrympleKaplan2000.markerSetOf x✝ = none

theorem DalrympleKaplan2000.person_resolve_is_union (p q : Person) (sp sq : PersonSet) : markerSetOf p = some sp → markerSetOf q = some sq → markerSetOf (p.resolve q) = some (resolve sp sq)

The substrate's canonical resolution is the paper's union (77)/(93): on the quadripartition, Person.resolve commutes with the marker encoding — the same grounding Person.resolve_profile states intrinsically, here in the paper's own vocabulary.

theorem DalrympleKaplan2000.two_markers_four_persons : Fintype.card PersonSet = 4

Two markers bound the system (§6.3): at most four person values are expressible, matching the maximally differentiated (Fula-type) inventory.

§6.5: union vs intersection — Sag et al. refuted, De Morgan vindicated

def DalrympleKaplan2000.sag1 : PersonSet

Sag et al. 1985's marker sets (100): first = {}, second = {XSP}, third = {XSP, THP}, resolution by intersection. Reusing our two markers for their two.

Equations

• DalrympleKaplan2000.sag1 = ∅

def DalrympleKaplan2000.sag2 : PersonSet

Equations

• DalrympleKaplan2000.sag2 = {DalrympleKaplan2000.Marker.S}

def DalrympleKaplan2000.sag3 : PersonSet

Equations

• DalrympleKaplan2000.sag3 = {DalrympleKaplan2000.Marker.S, DalrympleKaplan2000.Marker.H}

theorem DalrympleKaplan2000.sag_intersection_fails : sag1 ∩ sag2 = sag1 ∩ sag3 ∧ resolve fula1exc fula2 ≠ resolve fula1exc fula3

The refutation (§6.5): with first person as ∅, intersection makes you and I and Bill and I indistinguishable — "it is in principle impossible to distinguish different kinds of coordination involving a first person pronoun", so Fula's inclusive/exclusive contrast is underivable. Union keeps them apart.

theorem DalrympleKaplan2000.union_intersection_duality (p q : PersonSet) : (p ∪ q)ᶜ = pᶜ ∩ qᶜ

The De Morgan duality (102)–(103): any union analysis transforms into an equivalent intersection analysis over complement sets (markers reread as absences). The paper's observation is mathlib's Finset.compl_union.

§7: gender resolution by the same mechanism

inductive DalrympleKaplan2000.GMark : Type

Gender markers; per-language assignments below reuse one inventory.

• M : GMark
• F : GMark
• N : GMark

@[instance_reducible]

instance DalrympleKaplan2000.instDecidableEqGMark : DecidableEq GMark

Equations

• DalrympleKaplan2000.instDecidableEqGMark x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DalrympleKaplan2000.instReprGMark : Repr GMark

Equations

• DalrympleKaplan2000.instReprGMark = { reprPrec := DalrympleKaplan2000.instReprGMark.repr }

def DalrympleKaplan2000.instReprGMark.repr : GMark → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DalrympleKaplan2000.instFintypeGMark : Fintype GMark

Equations

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

@[reducible, inline]

abbrev DalrympleKaplan2000.GenderSet : Type

Equations

• DalrympleKaplan2000.GenderSet = Finset DalrympleKaplan2000.GMark

theorem DalrympleKaplan2000.hindi_table : {GMark.M} ∪ {GMark.M} = {GMark.M} ∧ {GMark.M} ∪ ∅ = {GMark.M} ∧ ∅ ∪ ∅ = ∅

Hindi (111): two genders, masculine {M}, feminine {} — mixed coordination resolves masculine (112).

theorem DalrympleKaplan2000.icelandic_mixed_is_neuter : {GMark.M} ∪ {GMark.F} = {GMark.M, GMark.F} ∧ {GMark.M} ∪ {GMark.M, GMark.F} = {GMark.M, GMark.F} ∧ {GMark.F} ∪ {GMark.M, GMark.F} = {GMark.M, GMark.F}

Icelandic (119): masc {M}, fem {F}, neut {M, F} — like genders preserved, any mixture resolves neuter (118/120).

def DalrympleKaplan2000.slovResolve (p q : GenderSet) : GenderSet

Slovene (122)/(126)–(127): masc {F, N}, fem {F}, neut {N}, and the conjunction itself contributes F ∈ (↑ GENDER) — deriving the surprising NEUT & NEUT = MASC (123)–(124).

Equations

• DalrympleKaplan2000.slovResolve p q = p ∪ q ∪ {DalrympleKaplan2000.GMark.F}

theorem DalrympleKaplan2000.slovene_neut_neut_is_masc : slovResolve {GMark.N} {GMark.N} = {GMark.F, GMark.N} ∧ slovResolve {GMark.F} {GMark.F} = {GMark.F}

Bridge: marker sets project onto the binary person decomposition

Features/Person.lean's two-boolean decomposition (hasAuthor, hasParticipant) is the image of the marker-set representation: S ∈ p is authorship, membership of either marker is participanthood. The map collapses exactly the inclusive/exclusive distinction — Fula's {S} and {S, H} land on the same binary value — which is the formal content of §6.2's "fewer pronominal distinctions".

def DalrympleKaplan2000.toBinary (p : PersonSet) : Person.Features

Project a marker set onto the binary decomposition.

Equations

• DalrympleKaplan2000.toBinary p = { hasParticipant := decide (DalrympleKaplan2000.Marker.S ∈ p ∨ DalrympleKaplan2000.Marker.H ∈ p), hasAuthor := decide (DalrympleKaplan2000.Marker.S ∈ p) }

theorem DalrympleKaplan2000.toBinary_values : toBinary fula1exc = Person.firstF ∧ toBinary fula1inc = Person.firstF ∧ toBinary fula2 = Person.secondF ∧ toBinary fula3 = Person.thirdF

theorem DalrympleKaplan2000.binary_collapses_clusivity : toBinary fula1exc = toBinary fula1inc ∧ fula1exc ≠ fula1inc

The inclusive/exclusive collapse, explicitly: the binary decomposition cannot separate Fula's two first persons.

BundleLike with Finset slots: the generic substrate accommodates indeterminacy

A multi-feature indeterminacy bundle is just a Pi type with Finset slots, ordered superset-first (more determinate = smaller set). BundleLike's slot type family S : F → Type* (parameter S carrying its own order) covers this case without any new generic machinery: S t := (Finset (V t))ᵒᵈ. The BundleLike.Subsumes order then reads, per slot, b₁ t ≤ b₂ t in the order dual — i.e. (b₂ t).1 ⊆ (b₁ t).1 — which is exactly the §4 (eq. 25) information-as-set-of-possibilities convention.

This is the structural payoff: a feature-space tweak (Finset slots instead of Flat slots), not a re-development of the lattice theory.

@[reducible, inline]

abbrev DalrympleKaplan2000.IndetBundle (F : Type u_1) (V : F → Type u_2) : Type (max u_1 u_2)

An indeterminacy bundle: each slot holds a Finset of possible atomic values, ordered superset-first via Finset's order dual.

Equations

• DalrympleKaplan2000.IndetBundle F V = ((t : F) → (Finset (V t))ᵒᵈ)

@[instance_reducible]

instance DalrympleKaplan2000.IndetBundle.instBundleLikeOrderDualFinset {F : Type u_1} {V : F → Type u_2} : BundleLike (IndetBundle F V) F fun (t : F) => (Finset (V t))ᵒᵈ

Equations

• DalrympleKaplan2000.IndetBundle.instBundleLikeOrderDualFinset = { val := fun (b : DalrympleKaplan2000.IndetBundle F V) => b }

instance DalrympleKaplan2000.IndetBundle.instLawfulBundleLikeOrderDualFinset {F : Type u_1} {V : F → Type u_2} : LawfulBundleLike (IndetBundle F V)

Concrete witness: a 1-feature Case-indeterminacy bundle. We exhibit two bundles — was {NOM, ACC} and wer {NOM} — and confirm that wer subsumes (is more determinate than) was, via the generic BundleLike.Subsumes.

@[reducible, inline]

abbrev DalrympleKaplan2000.CaseBundle : Type

A single-feature Case bundle.

Equations

• DalrympleKaplan2000.CaseBundle = DalrympleKaplan2000.IndetBundle Unit fun (x : Unit) => Case

def DalrympleKaplan2000.wasBundle : CaseBundle

Equations

• DalrympleKaplan2000.wasBundle x✝ = OrderDual.toDual DalrympleKaplan2000.was

def DalrympleKaplan2000.werBundle : CaseBundle

Equations

• DalrympleKaplan2000.werBundle x✝ = OrderDual.toDual DalrympleKaplan2000.wer

theorem DalrympleKaplan2000.wer_subsumes_was : BundleLike.Subsumes wasBundle werBundle

wer {NOM} is more determinate than was {NOM, ACC}: their subsumption in the generic BundleLike order matches set-superset on the slot.

Subsumption and unification on UD.MorphFeatures

[Shi86]

The information ordering of unification-based grammar ([Shi86] §3.2), on UD.MorphFeatures — the depth-1, reentrancy-free fragment of Shieber's feature structures. Every feature here is atomic-valued, so paths are single features, the reentrancy clause of subsumption is vacuous, and the definition (§3.2.2: D ⊑ D′ iff D(l) ⊑ D′(l) for all l ∈ dom(D); "an atomic feature structure neither subsumes nor is subsumed by a different atomic feature structure"; "variables subsume all other feature structures") reduces to the product of flat orders. Subsumption is registered as ≤ (Shieber's ⊑); the all-none bundle — Shieber's variable [ ] — is ⊥.

Unification (§3.2.3) is "the most general feature structure D such that D′ ⊑ D and D′′ ⊑ D", failing on conflict: MorphFeatures.unify returns some exactly on Compatible (= bounded above) inputs, and its result is the least upper bound (unify_isLUB). The example laws of §3.2.3 are theorems: unification is idempotent (unify_self), commutative (unify_comm), and variables are identity elements (bot_unify).

Main declarations

• instance : PartialOrder UD.MorphFeatures — subsumption ("only a partial order", §3.2.3), with decidable ≤.
• instance : OrderBot UD.MorphFeatures — the empty bundle is bottom.
• instance : SemilatticeInf UD.MorphFeatures — the meet is Shieber's generalization (anti-unification): total, unlike the join.
• UD.MorphFeatures.Compatible — boundedness above (BddAbove {f, g}), decidable via the Bool check (compatible_iff_bddAbove).
• unify_isLUB, unify_eq_some_iff_isLUB, unify_comm, unify_assoc, unify_self, bot_unify/unify_bot, unify_mono — the §3.2.3 laws plus associativity and guarded monotonicity.

Theory-neutrality boundary

Three strata with different statuses: the record is annotation consensus (Data/UD/Basic.lean); the order ≤ is shared substrate every framework consumes its own way (DM's matching clause, underspecification, syncretism down-sets); the operations ⊔/⊓ are commitments of the unification tradition — [Shi86] §3.1 states unification-as-sole-combinator as a design constraint, and rival frameworks combine differently (DM matches and competes; Minimalist Agree values asymmetrically). This file is not that tradition's headquarters: unification-based grammar (PATR, HPSG, LFG — reentrant feature structures, phrasal combination) is a syntax family whose substrate belongs in Syntax/ when consuming studies demand it. What lives here is only the tradition's morphological-bundle fragment — the algebra of one token's Feats column — which it shares with rivals: at the level of claims about morphological feature combination this file is a sibling of DistributedMorphology/ and Nanosyntax/, not a foundation beneath them.

Implementation notes

Morphology owns the bundle algebra: MorphFeatures is the token's morphology (UD's Feats column), and unification at the ms-word level is the morphology/syntax interface operation. The matching clause of DM's Subset Principle (an exponent is insertable iff exponent.features ≤ morpheme.features) could consume ≤ directly, but the existing Morphology/DistributedMorphology/VocabularyInsertion.lean matches by List-subset on [BEq F] rather than MorphFeatures.≤; bridging is left for a future PR. The competition clause — most-specified-wins — is separate argmax machinery already implemented in that same file. (Nanosyntax's Superset Principle is not a consumer: it matches by containment of syntactic trees, see Nanosyntax/TreeSpellout.lean's NanoTree.contains, not by an order on flat bundles.) Lives apart from Data/UD/Basic.lean so the (heavily imported) standard mirror stays mathlib-free — this file is the one that pays for Mathlib.Order — and it is the canonical home for order instances on UD.MorphFeatures.

The non-distributivity of the subsumption lattice is a documented obstruction (Flat.unify_distinct_eq_none): any ≥3-value slot (here, Case) makes the per-slot lattice the diamond Mₙ, modular but not distributive ([Car92] p. 15, eq. (4), notes this explicitly: "our partial orders are not required to be distributive (and in fact, are not even required to be modular)"). This matters for generalization-then-unification reorderings in paradigm-induction learners.

The flat order on one feature slot

The slot-level subsumption relation ([Shi86] §3.2.2: ⊥ below everything, distinct atoms incomparable) is the order of Flat (Linglib/Core/Order/Flat.lean), whose PartialOrder/OrderBot/SemilatticeInf/PartialUnify instances supply the per-slot steps of the bundle-level proofs below.

inductive UD.MorphFeatureType : Type

The 14-case feature-type index for MorphFeatures — the signature of UD's Feats column treated as a fixed finite type family.

• number : MorphFeatureType
• gender : MorphFeatureType
• case_ : MorphFeatureType
• definite : MorphFeatureType
• degree : MorphFeatureType
• pronType : MorphFeatureType
• reflex : MorphFeatureType
• person : MorphFeatureType
• verbForm : MorphFeatureType
• tense : MorphFeatureType
• aspect : MorphFeatureType
• mood : MorphFeatureType
• voice : MorphFeatureType
• polarity : MorphFeatureType

@[instance_reducible]

instance UD.instDecidableEqMorphFeatureType : DecidableEq MorphFeatureType

Equations

• UD.instDecidableEqMorphFeatureType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance UD.instReprMorphFeatureType : Repr MorphFeatureType

Equations

• UD.instReprMorphFeatureType = { reprPrec := UD.instReprMorphFeatureType.repr }

def UD.instReprMorphFeatureType.repr : MorphFeatureType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.number prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.number")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.gender prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.gender")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.case_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.case_")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.degree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.degree")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.reflex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.reflex")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.person prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.person")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.tense prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.tense")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.aspect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.aspect")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.mood prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.mood")).group prec✝
• UD.instReprMorphFeatureType.repr UD.MorphFeatureType.voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "UD.MorphFeatureType.voice")).group prec✝

@[instance_reducible]

instance UD.instFintypeMorphFeatureType : Fintype MorphFeatureType

Equations

• UD.instFintypeMorphFeatureType = { elems := { val := ↑UD.MorphFeatureType.enumList, nodup := UD.MorphFeatureType.enumList_nodup }, complete := UD.instFintypeMorphFeatureType._proof_1 }

def UD.MorphFeatureType.Val : MorphFeatureType → Type

Per-slot value space. The reflex slot is privative (Unit); all other slots take their concrete UD enum.

Equations

• UD.MorphFeatureType.number.Val = UD.Number
• UD.MorphFeatureType.gender.Val = UD.Gender
• UD.MorphFeatureType.case_.Val = UD.Case
• UD.MorphFeatureType.definite.Val = UD.Definite
• UD.MorphFeatureType.degree.Val = UD.Degree
• UD.MorphFeatureType.pronType.Val = UD.PronType
• UD.MorphFeatureType.reflex.Val = Unit
• UD.MorphFeatureType.person.Val = UD.Person
• UD.MorphFeatureType.verbForm.Val = UD.VerbForm
• UD.MorphFeatureType.tense.Val = UD.Tense
• UD.MorphFeatureType.aspect.Val = UD.Aspect
• UD.MorphFeatureType.mood.Val = UD.Mood
• UD.MorphFeatureType.voice.Val = UD.Voice
• UD.MorphFeatureType.polarity.Val = UD.Polarity

@[instance_reducible]

instance UD.MorphFeatureType.instDecidableEqVal (t : MorphFeatureType) : DecidableEq t.Val

Equations

• UD.MorphFeatureType.number.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_1
• UD.MorphFeatureType.gender.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_3
• UD.MorphFeatureType.case_.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_5
• UD.MorphFeatureType.definite.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_7
• UD.MorphFeatureType.degree.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_9
• UD.MorphFeatureType.pronType.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_11
• UD.MorphFeatureType.reflex.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_13
• UD.MorphFeatureType.person.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_15
• UD.MorphFeatureType.verbForm.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_17
• UD.MorphFeatureType.tense.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_19
• UD.MorphFeatureType.aspect.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_21
• UD.MorphFeatureType.mood.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_23
• UD.MorphFeatureType.voice.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_25
• UD.MorphFeatureType.polarity.instDecidableEqVal = UD.MorphFeatureType.instDecidableEqVal._aux_27

Subsumption is a partial order with bottom

def UD.MorphFeatures.Subsumes (f g : MorphFeatures) : Prop

Subsumption ([Shi86] §3.2.2): f carries a subset of g's information — field-wise flat order on the option slots, implication on the reflex flag.

Equations

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

MorphFeatures as a feature bundle, and the derived order

MorphFeatures realizes BundleLike over the 14-case signature MorphFeatureType ([Car92]'s abstract feature structure): each slot projects to a Flat value, with the reflex flag normalized false ↦ none, true ↦ some () (the privative Unit case). The valuation is injective, so MorphFeatures is LawfulBundleLike, and the subsumption order is the per-slot Flat order pulled back along val (subsumes_iff_val_le) — the PartialOrder/OrderBot laws derive from the bundle embedding rather than being proved field by field.

def UD.MorphFeatures.val (f : MorphFeatures) (t : MorphFeatureType) : Flat t.Val

The valuation: project each slot as a Flat value, normalizing reflex : Bool to a privative Flat Unit.

Equations

• f.val UD.MorphFeatureType.number = f.number
• f.val UD.MorphFeatureType.gender = f.gender
• f.val UD.MorphFeatureType.case_ = f.case_
• f.val UD.MorphFeatureType.definite = f.definite
• f.val UD.MorphFeatureType.degree = f.degree
• f.val UD.MorphFeatureType.pronType = f.pronType
• f.val UD.MorphFeatureType.reflex = if f.reflex = true then ↑() else ⊥
• f.val UD.MorphFeatureType.person = f.person
• f.val UD.MorphFeatureType.verbForm = f.verbForm
• f.val UD.MorphFeatureType.tense = f.tense
• f.val UD.MorphFeatureType.aspect = f.aspect
• f.val UD.MorphFeatureType.mood = f.mood
• f.val UD.MorphFeatureType.voice = f.voice
• f.val UD.MorphFeatureType.polarity = f.polarity

@[instance_reducible]

instance UD.MorphFeatures.instBundleLikeMorphFeatureTypeFlatVal : BundleLike MorphFeatures MorphFeatureType fun (t : MorphFeatureType) => Flat t.Val

Equations

• UD.MorphFeatures.instBundleLikeMorphFeatureTypeFlatVal = { val := UD.MorphFeatures.val }

theorem UD.MorphFeatures.val_injective : Function.Injective val

The valuation is injective: a MorphFeatures bundle is determined by its per-slot assignments (with reflex reconstructed from Option Unit).

instance UD.MorphFeatures.instLawfulBundleLikeMorphFeatureTypeFlatVal : LawfulBundleLike MorphFeatures

theorem UD.MorphFeatures.subsumes_iff_val_le (f g : MorphFeatures) : f.Subsumes g ↔ f.val ≤ g.val

Subsumption is exactly the bundle order: the field-wise 14-conjunct form coincides with the per-slot Flat order on the valuation val.

@[instance_reducible]

instance UD.MorphFeatures.instPartialOrder : PartialOrder MorphFeatures

Equations

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

@[instance_reducible]

instance UD.MorphFeatures.instDecidableSubsumes (f g : MorphFeatures) : Decidable (f.Subsumes g)

Equations

• f.instDecidableSubsumes g = id inferInstance

@[instance_reducible]

instance UD.MorphFeatures.instDecidableLe (f g : MorphFeatures) : Decidable (f ≤ g)

Subsumption is decidable (each slot is).

Equations

• f.instDecidableLe g = f.instDecidableSubsumes g

@[instance_reducible]

instance UD.MorphFeatures.instOrderBot : OrderBot MorphFeatures

The empty bundle — Shieber's variable [ ] — is bottom: "variables subsume all other feature structures … they contain no information at all" (§3.2.2).

Equations

• UD.MorphFeatures.instOrderBot = { bot := { }, bot_le := UD.MorphFeatures.instOrderBot._proof_1 }

Compatibility is boundedness above; unification is the least upper bound

def UD.MorphFeatures.Compatible (f g : MorphFeatures) : Prop

Prop-native compatibility: the pair is bounded above in the subsumption order — mathlib's BddAbove, so the bounds API applies directly. Characterized by the executable compatible check via compatible_iff_bddAbove, which also makes it decidable.

Equations

• f.Compatible g = BddAbove {f, g}

theorem UD.MorphFeatures.le_merge_left (f g : MorphFeatures) : f ≤ f.merge g

The left input subsumes the merge.

theorem UD.MorphFeatures.le_merge_right {f g : MorphFeatures} (h : f.compatible g = true) : g ≤ f.merge g

The right input subsumes the merge — given compatibility (the doubly committed slots agree, so the left bias is harmless).

theorem UD.MorphFeatures.merge_le {f g u : MorphFeatures} (hf : f ≤ u) (hg : g ≤ u) : f.merge g ≤ u

The merge is below every common upper bound — minimality ("the most general feature structure", §3.2.3).

theorem UD.MorphFeatures.compatible_of_le {f g u : MorphFeatures} (hf : f ≤ u) (hg : g ≤ u) : f.compatible g = true

Bounded above implies the executable check passes.

theorem UD.MorphFeatures.compatible_iff_bddAbove (f g : MorphFeatures) : f.compatible g = true ↔ f.Compatible g

The Bool check is exactly boundedness above in the subsumption order: the order-theoretic identity of "compatible".

@[instance_reducible]

instance UD.MorphFeatures.instDecidableCompatible (f g : MorphFeatures) : Decidable (f.Compatible g)

Equations

• f.instDecidableCompatible g = decidable_of_iff (f.compatible g = true) ⋯

theorem UD.MorphFeatures.unify_eq_some_iff (f g : MorphFeatures) : (f.unify g).isSome = true ↔ f.Compatible g

Unification succeeds exactly on compatible inputs (§3.2.3: otherwise it "fails").

theorem UD.MorphFeatures.unify_isLUB {f g u : MorphFeatures} (h : f.unify g = some u) : IsLUB {f, g} u

Unification is the least upper bound ([Shi86] §3.2.3: "the most general feature structure D such that D′ ⊑ D and D′′ ⊑ D").

Generalization: the meet

Shieber's generalization (anti-unification): the most specific bundle subsumed by both inputs. Unlike unification it is total — the meet always exists — so MorphFeatures is a genuine SemilatticeInf with ⊥.

@[instance_reducible]

instance UD.MorphFeatures.instMin : Min MorphFeatures

Equations

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

@[instance_reducible]

instance UD.MorphFeatures.instSemilatticeInf : SemilatticeInf MorphFeatures

Equations

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

Unification computes least upper bounds — further laws

@[instance_reducible]

instance UD.MorphFeatures.instPartialUnify : PartialUnify MorphFeatures

MorphFeatures carries the pairwise-LUB structure of [Car92]'s bounded complete partial order: unify is the partial join, with unify_isLUB and compatible_iff_bddAbove supplying the two class axioms. The unification laws — commutativity, associativity (with failure propagating), ⊥-identity, idempotence, monotonicity — are inherited as one-line corollaries of the generic theorems in Core/Order/PartialUnify.lean.

Equations

• UD.MorphFeatures.instPartialUnify = { unify := UD.MorphFeatures.unify, isLUB_of_unify_eq_some := ⋯, isSome_unify_of_bddAbove := @UD.MorphFeatures.instPartialUnify._proof_1 }

@[simp]

theorem UD.MorphFeatures.unify_eq_partialUnify (f g : MorphFeatures) : PartialUnify.unify f g = f.unify g

The instance-projected unify is the same function as MorphFeatures.unify.

theorem UD.MorphFeatures.unify_eq_some_iff_isLUB {f g u : MorphFeatures} : f.unify g = some u ↔ IsLUB {f, g} u

Unification succeeds with value u exactly when u is the least upper bound.

theorem UD.MorphFeatures.unify_comm (f g : MorphFeatures) : f.unify g = g.unify f

Unification is commutative — a consequence of total compatibility: doubly committed slots agree, so the per-field left bias washes out.

@[simp]

theorem UD.MorphFeatures.unify_self (f : MorphFeatures) : f.unify f = some f

Unification is idempotent (§3.2.3's example law).

@[simp]

theorem UD.MorphFeatures.bot_unify (f : MorphFeatures) : ⊥.unify f = some f

Variables are unification identity elements (§3.2.3's example law): unifying with the empty bundle returns the other input.

theorem UD.MorphFeatures.unify_assoc (f g h : MorphFeatures) : ((f.unify g).bind fun (x : MorphFeatures) => x.unify h) = (g.unify h).bind fun (x : MorphFeatures) => f.unify x

Unification is associative, with failure propagating ([Shi86] §3.2.3's order-independence): both associations compute the lub of all three bundles.

@[simp]

theorem UD.MorphFeatures.unify_bot (f : MorphFeatures) : f.unify ⊥ = some f

The empty bundle is a right identity for unification.

theorem UD.MorphFeatures.unify_eq_none_iff (f g : MorphFeatures) : f.unify g = none ↔ ¬f.Compatible g

Unification fails exactly on incompatible inputs.

theorem UD.MorphFeatures.unify_mono {f₁ f₂ g₁ g₂ u₂ : MorphFeatures} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) (h2 : f₂.unify g₂ = some u₂) : ∃ (u₁ : MorphFeatures), f₁.unify g₁ = some u₁ ∧ u₁ ≤ u₂

Unification is monotone where defined: shrinking both inputs preserves success and shrinks the output. (Unguarded merge-monotonicity is false — the guard is needed.)