Partial unification: computable pairwise least upper bounds

PartialUnify α equips a partial order with a computable partial join: unify a b returns the least upper bound of {a, b} when the pair is bounded above, and none otherwise. This is the pairwise face of bounded completeness — [Car92]'s setting for unification domains (Definition 2.1: an inheritance hierarchy is a finite bounded complete partial order), with the join taken as primitive because "joins correspond to unifications" (p. 13). Carpenter notes the equivalence this file exploits: "a finite BCPO is nothing more nor less than a finite meet semilattice", presented through its joins.

The laws of unification — idempotence, commutativity, associativity-with-failure, ⊥ as identity, guarded monotonicity — are proved here once, from least-upper-bound uniqueness; carriers (feature slots, bundles, attribute-value records) supply only unify and the two axioms.

Adjoining a top element to make the join total is a derived presentation ([Car92] p. 16 attributes it to Aït-Kaci and Smolka), not the primitive; this file deliberately does not take it.

Main declarations

• PartialUnify — the class
• PartialUnify.unify_eq_some_iff_isLUB, PartialUnify.isSome_unify_iff_bddAbove — characterizations
• PartialUnify.unify_comm, unify_assoc, unify_self, bot_unify, unify_mono — the unification laws
• the Pi instance: pointwise unification over a Fintype index

class PartialUnify (α : Type u_1) [PartialOrder α] : Type u_1

A computable partial join on a partial order: unify a b is some of the least upper bound of {a, b} when the pair is bounded above, and none otherwise — the pairwise face of [Car92]'s bounded completeness, with the join as the primitive operation.

• unify : α → α → Option α

  The partial join.

• isLUB_of_unify_eq_some {a b c : α} : unify a b = some c → IsLUB {a, b} c

  A successful unification is a least upper bound.

• isSome_unify_of_bddAbove {a b : α} : BddAbove {a, b} → (unify a b).isSome = true

  Unification succeeds on bounded-above pairs.

theorem PartialUnify.mem_upperBounds_pair {α : Type u_1} [Preorder α] {u a b : α} : u ∈ upperBounds {a, b} ↔ a ≤ u ∧ b ≤ u

theorem PartialUnify.isSome_unify_iff_bddAbove {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b : α} : (unify a b).isSome = true ↔ BddAbove {a, b}

theorem PartialUnify.unify_eq_some_iff_isLUB {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b c : α} : unify a b = some c ↔ IsLUB {a, b} c

theorem PartialUnify.unify_eq_none_iff {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b : α} : unify a b = none ↔ ¬BddAbove {a, b}

theorem PartialUnify.unify_comm {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b : α) : unify a b = unify b a

@[simp]

theorem PartialUnify.unify_self {α : Type u_1} [PartialOrder α] [PartialUnify α] (a : α) : unify a a = some a

@[simp]

theorem PartialUnify.bot_unify {α : Type u_1} [PartialOrder α] [PartialUnify α] [OrderBot α] (a : α) : unify ⊥ a = some a

@[simp]

theorem PartialUnify.unify_bot {α : Type u_1} [PartialOrder α] [PartialUnify α] [OrderBot α] (a : α) : unify a ⊥ = some a

theorem PartialUnify.isLUB_pair_step {α : Type u_1} [PartialOrder α] {a b c v u : α} (hv : IsLUB {a, b} v) : IsLUB {v, c} u ↔ IsLUB {a, b, c} u

Glueing pairwise LUBs: if v is the LUB of {a, b}, then LUBs of {v, c} are exactly LUBs of {a, b, c}.

theorem PartialUnify.bind_unify_left_eq_some_iff {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b c u : α} : ((unify a b).bind fun (x : α) => unify x c) = some u ↔ IsLUB {a, b, c} u

theorem PartialUnify.unify_assoc {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b c : α) : ((unify a b).bind fun (x : α) => unify x c) = (unify b c).bind fun (x : α) => unify a x

Unification is associative, with failure propagating: both associations compute the least upper bound of all three elements.

theorem PartialUnify.unify_mono {α : Type u_1} [PartialOrder α] [PartialUnify α] {a₁ a₂ b₁ b₂ u₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) (h₂ : unify a₂ b₂ = some u₂) : ∃ (u₁ : α), unify a₁ b₁ = some u₁ ∧ u₁ ≤ u₂

Unification is monotone where defined: shrinking both inputs preserves success and shrinks the output.

Pointwise unification on Pi types

@[implicit_reducible]

instance PartialUnify.instForall {F : Type u_2} {S : F → Type u_3} [(t : F) → PartialOrder (S t)] [(t : F) → PartialUnify (S t)] [Fintype F] : PartialUnify ((t : F) → S t)

Equations

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

Compatibility

The consistency relation of unification: two elements are compatible when they have a common upper bound — equivalently (compat_iff_isSome_unify), when they unify. On feature carriers this is the agreement relation ([Car92]; [Shi86]'s "compatible").

@[reducible, inline]

abbrev Compat {α : Type u_1} [Preorder α] (a b : α) : Prop

Two elements are compatible: bounded above — the consistency relation of unification. An abbrev so the BddAbove API applies directly.

Equations

• Compat a b = BddAbove {a, b}

theorem Compat.of_le {α : Type u_1} [Preorder α] {a b u : α} (ha : a ≤ u) (hb : b ≤ u) : Compat a b

A common upper bound witnesses compatibility.

theorem Compat.symm {α : Type u_1} [Preorder α] {a b : α} (h : Compat a b) : Compat b a

theorem compat_self {α : Type u_1} [Preorder α] (a : α) : Compat a a

theorem bot_compat {α : Type u_1} [Preorder α] [OrderBot α] (a : α) : Compat ⊥ a

⊥ is a wildcard: compatible with everything.

theorem compat_bot {α : Type u_1} [Preorder α] [OrderBot α] (a : α) : Compat a ⊥

theorem Monotone.compat {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) {a b : α} (h : Compat a b) : Compat (f a) (f b)

Monotone maps preserve compatibility.

theorem compat_iff_isSome_unify {α : Type u_1} [PartialOrder α] [PartialUnify α] {a b : α} : Compat a b ↔ (PartialUnify.unify a b).isSome = true

Compatibility is decided by unification.

@[implicit_reducible]

instance instDecidableCompatOfPartialUnify {α : Type u_1} [PartialOrder α] [PartialUnify α] (a b : α) : Decidable (Compat a b)

Equations

• instDecidableCompatOfPartialUnify a b = decidable_of_iff ((PartialUnify.unify a b).isSome = true) ⋯