Shieber (1986): An Introduction to Unification-Based Approaches to Grammar

This file formalizes the information ordering of §3.2 on the token feature bundle Morphology.Features, the depth-one, reentrancy-free fragment of the book's feature structures. Every feature there is atomic-valued, so paths are single features and the reentrancy clause of subsumption is vacuous: the definition of §3.2.2, that D subsumes D′ when D(l) subsumes D′(l) for every feature l of D, an atom neither subsuming nor subsumed by a different one and the variable subsuming everything, is the product of the flat orders, the bundle's ≤, with the variable [ ] as ⊥. Unification (§3.2.3) is the most general structure both inputs subsume, failing on conflict: it succeeds exactly on pairs bounded above and its value is their least upper bound, from which the book's example laws follow, that unification adds information, is idempotent, has the variable as its identity, is commutative, associative with failure propagating, and monotone. Generalization, the most specific structure subsumed by both inputs, is total, the meet.

Implementation notes

• The order, the partial join and the meet are the pointwise instances of Core/Order/Flat.lean and Core/Order/PartialUnify.lean, so each law is the generic lemma at Features. The subsumption lattice is not distributive: a feature with three values is the diamond, modular but not distributive, as [Car92] notes of feature-structure orders in general. Phrasal combination and reentrant structures are not formalized.

References

• [Shi86]
• [Car92]

theorem Shieber1986.le_iff {f g : Morphology.Features} : f ≤ g ↔ ∀ (t : Morphology.Feature), f t ≤ g t

Subsumption is featurewise: the variable is below everything and distinct atoms are incomparable.

theorem Shieber1986.bot_le (f : Morphology.Features) : ⊥ ≤ f

The variable subsumes every structure.

theorem Shieber1986.unify_ne_top_iff {f g : Morphology.Features} : PartialUnify.unify f g ≠ ⊤ ↔ Compat f g

Unification succeeds exactly on structures with a common upper bound.

theorem Shieber1986.unify_eq_coe_iff_isLUB {f g u : Morphology.Features} : PartialUnify.unify f g = ↑u ↔ IsLUB {f, g} u

Unification is the least upper bound: the most general structure both inputs subsume.

theorem Shieber1986.le_of_unify_eq_coe {f g u : Morphology.Features} (hu : PartialUnify.unify f g = ↑u) : f ≤ u ∧ g ≤ u

Unification adds information: each input subsumes the result.

theorem Shieber1986.unify_self (f : Morphology.Features) : PartialUnify.unify f f = ↑f

Unification is idempotent.

theorem Shieber1986.bot_unify (f : Morphology.Features) : PartialUnify.unify ⊥ f = ↑f

The variable is the identity of unification.

theorem Shieber1986.unify_bot (f : Morphology.Features) : PartialUnify.unify f ⊥ = ↑f

theorem Shieber1986.unify_comm (f g : Morphology.Features) : PartialUnify.unify f g = PartialUnify.unify g f

Unification is commutative.

theorem Shieber1986.unify_assoc (f g h : Morphology.Features) : PartialUnify.unify f g ⊔ ↑h = ↑f ⊔ PartialUnify.unify g h

Unification is associative, failure propagating, so a set of structures unifies in any order.

theorem Shieber1986.unify_mono {f g u f' g' : Morphology.Features} (hf : f ≤ f') (hg : g ≤ g') (hu : PartialUnify.unify f' g' = ↑u) : ∃ (v : Morphology.Features), PartialUnify.unify f g = ↑v ∧ v ≤ u

Unification is monotone: more general inputs unify to a more general result.

theorem Shieber1986.le_inf_iff {f g h : Morphology.Features} : h ≤ f ⊓ g ↔ h ≤ f ∧ h ≤ g

Generalization is the meet, the most specific structure both inputs subsume, and is total.

theorem Shieber1986.unify_examples : PartialUnify.unify (Morphology.Features.of (some Person.third)) (Morphology.Features.of none (some Number.singular)) = ↑(Morphology.Features.of (some Person.third) (some Number.singular)) ∧ PartialUnify.unify (Morphology.Features.of none none none none none none none false none (some UD.Tense.Past)) (Morphology.Features.of none none none none none none none false none (some UD.Tense.Pres)) = ⊤

A third-person structure and a singular one unify to the third-person singular, and two tenses fail to unify.