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_iff_insert {α : Type u_1} [PartialOrder α] {s : Set α} {a v u : α} (hv : IsLUB s v) : IsLUB {a, v} u ↔ IsLUB (insert a s) u

Glueing a LUB into a set: when v is a least upper bound of s, LUBs of {a, v} are exactly LUBs of insert a s.

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

@[instance_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.mono {α : Type u_1} [Preorder α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) (h : Compat b d) : Compat a c

Compatibility persists downward.

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.

@[instance_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) ⋯

Joining point sets

def Set.lubs {α : Type u_1} [PartialOrder α] (s t : Set α) : Set α

The least upper bounds of pairs drawn from two sets — the partial-join analogue of Set.sups, keeping exactly the bounded pairs: unification of description sets in [Car92]'s setting.

Equations

• s.lubs t = {c : α | ∃ a ∈ s, ∃ b ∈ t, IsLUB {a, b} c}

@[simp]

theorem Set.mem_lubs {α : Type u_1} [PartialOrder α] {s t : Set α} {c : α} : c ∈ s.lubs t ↔ ∃ a ∈ s, ∃ b ∈ t, IsLUB {a, b} c

theorem Set.lubs_comm {α : Type u_1} [PartialOrder α] (s t : Set α) : s.lubs t = t.lubs s

theorem Set.lubs_eq_left {α : Type u_1} [PartialOrder α] {s t : Set α} (h₁ : ∀ (a : α), ∃ b ∈ t, b ≤ a) (h₂ : ∀ (a b : α), b ∈ t → Compat a b → b ≤ a) : s.lubs t = s

A set of local units is a right identity for lubs: every element dominates a member of t, and members of t sit below anything they are compatible with — the set-level face of ⊥ as identity.

theorem Set.upperClosure_lubs {α : Type u_1} [PartialOrder α] (H : ∀ (a b : α), Compat a b → ∃ (c : α), IsLUB {a, b} c) (s t : Set α) : upperClosure (s.lubs t) = upperClosure s ⊔ upperClosure t

Under pairwise bounded completeness, upper closure sends lubs to the join: a point bounds a pairwise join iff it bounds a point of each set.

theorem Set.lubs_assoc {α : Type u_1} [PartialOrder α] (H : ∀ (a b : α), Compat a b → ∃ (c : α), IsLUB {a, b} c) (s t u : Set α) : (s.lubs t).lubs u = s.lubs (t.lubs u)

Under pairwise bounded completeness — every bounded pair has a join — joining point sets is associative.

List unification

def PartialUnify.unifyList {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] : List α → Option α

Unification of a finite list of elements: the least upper bound of its members (together with ⊥) when they are jointly bounded, none otherwise.

Equations

• PartialUnify.unifyList [] = some ⊥
• PartialUnify.unifyList (a :: l) = (PartialUnify.unifyList l).bind (PartialUnify.unify a)

@[simp]

theorem PartialUnify.unifyList_nil {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] : unifyList [] = some ⊥

theorem PartialUnify.unifyList_cons {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] (a : α) (l : List α) : unifyList (a :: l) = (unifyList l).bind (unify a)

theorem PartialUnify.isLUB_of_unifyList_eq_some {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] {l : List α} {u : α} (h : unifyList l = some u) : IsLUB (insert ⊥ {x : α | x ∈ l}) u

theorem PartialUnify.isSome_unifyList_of_bddAbove {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] {l : List α} (h : BddAbove {x : α | x ∈ l}) : (unifyList l).isSome = true

theorem PartialUnify.unifyList_eq_some_iff_isLUB {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] {l : List α} {u : α} : unifyList l = some u ↔ IsLUB (insert ⊥ {x : α | x ∈ l}) u

theorem PartialUnify.isSome_unifyList_iff_bddAbove {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] {l : List α} : (unifyList l).isSome = true ↔ BddAbove {x : α | x ∈ l}

theorem PartialUnify.unifyList_eq_none_iff {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] {l : List α} : unifyList l = none ↔ ¬BddAbove {x : α | x ∈ l}

@[simp]

theorem PartialUnify.unifyList_pair {α : Type u_1} [PartialOrder α] [OrderBot α] [PartialUnify α] (a b : α) : unifyList [a, b] = unify a b