diff --git a/Lattice.agda b/Lattice.agda index 1ede49c..6f03d7f 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -237,13 +237,16 @@ record IsFiniteHeightLattice {a} (A : Set a) field {{fixedHeight}} : FixedHeight h + private + module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong + + open MyChain.Height fixedHeight using (⊥; ⊤) public + -- If the equality is decidable, we can prove that the top and bottom -- elements of the chain are least and greatest elements of the lattice module _ {{≈-Decidable : IsDecidable _≈_}} where open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec) - module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong - open MyChain.Height fixedHeight using (⊥; ⊤) public open MyChain.Height fixedHeight using (bounded; longestChain) ⊥≼ : ∀ (a : A) → ⊥ ≼ a diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 48a32ae..630d522 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -456,7 +456,7 @@ record Graph : Set where Total-⊓? : Dec Total-⊓ Total-⊓? = P-Total? Have-⊓? - module AssumeWellFormed (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where + module Basic (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where n₁→n₂×n₂→n₁⇒n₁≡n₂ : ∀ {n₁ n₂} → PathExists n₁ n₂ → PathExists n₂ n₁ → n₁ ≡ n₂ n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁→n₂ n₂→n₁ with n₁→n₂ | n₂→n₁ | noCycles (n₁→n₂ ++ n₂→n₁) @@ -606,3 +606,119 @@ record Graph : Set where { absorb-⊔-⊓ = absorb-⊔-⊓ ; absorb-⊓-⊔ = absorb-⊓-⊔ } + + module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set FiniteHeightLattice) where + open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc) + + Elem : Set + Elem = Σ Node λ n → (proj₁ (𝓛 n)) + + data _≈_ : Elem → Elem → Set where + ≈-lift : ∀ {n : Node} {l₁ l₂ : proj₁ (𝓛 n)} → + FiniteHeightLattice._≈_ (proj₂ (𝓛 n)) l₁ l₂ → + (n , l₁) ≈ (n , l₂) + + ≈-refl : ∀ {e : Elem} → e ≈ e + ≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) + + ≈-sym : ∀ {e₁ e₂ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₁ + ≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (proj₂ (𝓛 n₁)) l₁≈l₂) + + ≈-trans : ∀ {e₁ e₂ e₃ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃ + ≈-trans {n₁ , l₁} (≈-lift l₁≈l₂) (≈-lift l₂≈l₃) = ≈-lift (FiniteHeightLattice.≈-trans (proj₂ (𝓛 n₁)) l₁≈l₂ l₂≈l₃) + + _⊔_ : Elem → Elem → Elem + _⊔_ e₁ e₂ + using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂ + with n' ← n₁ ⊔ᵇ n₂ + with n' ≟ n₁ | n' ≟ n₂ + ... | yes refl | yes refl = (n' , FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) (proj₂ e₁) (proj₂ e₂)) + ... | yes refl | _ = (n' , proj₂ e₁) + ... | _ | yes refl = (n' , proj₂ e₂) + ... | no _ | no _ = (n' , FiniteHeightLattice.⊥ (proj₂ (𝓛 n'))) + + ⊔-idemp : ∀ e → (e ⊔ e) ≈ e + ⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n + with n ≟ n + ... | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (proj₂ (𝓛 n)) l) + ... | no n≢n = ⊥-elim (n≢n refl) + + ⊔-comm : ∀ (e₁ e₂ : Elem) → (e₁ ⊔ e₂) ≈ (e₂ ⊔ e₁) + ⊔-comm (n₁ , l₁) (n₂ , l₂) + rewrite ⊔ᵇ-comm n₁ n₂ + with n ← n₂ ⊔ᵇ n₁ + with n ≟ n₁ | n ≟ n₂ + ... | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (proj₂ (𝓛 n)) l₁ l₂) + ... | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) + ... | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) + ... | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) + + private + data Expr (A : Set) : Set where + `_ : A → Expr A + _⊔ᵉ_ : Expr A → Expr A → Expr A + + eval : ∀ {A} → (A → A → A) → Expr A → A + eval _ (` v) = v + eval f (e₁ ⊔ᵉ e₂) = f (eval f e₁) (eval f e₂) + + mapᵉ : ∀ {A B} → (A → B) → Expr A → Expr B + mapᵉ f (` a) = ` (f a) + mapᵉ f (e₁ ⊔ᵉ e₂) = (mapᵉ f e₁) ⊔ᵉ (mapᵉ f e₂) + + filterᵉ : ∀ (n : Node) → Expr Elem → Maybe (Expr (proj₁ (𝓛 n))) + filterᵉ n (` (n' , l')) + with n ≟ n' + ... | yes refl = just (` l') + ... | no _ = nothing + filterᵉ n (e₁ ⊔ᵉ e₂) + with filterᵉ n e₁ | filterᵉ n e₂ + ... | just e₁' | just e₂' = just (e₁' ⊔ᵉ e₂') + ... | just e₁' | nothing = just e₁' + ... | nothing | just e₂' = just e₂' + ... | nothing | nothing = nothing + + Node-homo : ∀ e → proj₁ (eval _⊔_ e) ≡ eval _⊔ᵇ_ (mapᵉ proj₁ e) + Node-homo (` _) = refl + Node-homo (e₁ ⊔ᵉ e₂) + with IH₁ ← Node-homo e₁ with IH₂ ← Node-homo e₂ + with (n₁ , l₁) ← eval _⊔_ e₁ with (n₂ , l₂) ← eval _⊔_ e₂ + with n ← n₁ ⊔ᵇ n₂ in p + with n ≟ n₁ | n ≟ n₂ + ... | yes refl | yes refl rewrite sym IH₁ rewrite sym IH₂ = sym (⊔ᵇ-idemp n) + ... | yes refl | no _ rewrite sym IH₁ rewrite sym IH₂ = sym p + ... | no _ | yes refl rewrite sym IH₁ rewrite sym IH₂ = sym p + ... | no _ | no _ rewrite sym IH₁ rewrite sym IH₂ = sym p + + -- A key simplifying property is that notionally, only the + -- "elements with the final tag" in the expression matter. All + -- others are subsubed. If none of the elments have the final tag, + -- we've found a better supremum and the second element will be ⊥. + Expr-final : ∀ e → let n = eval _⊔ᵇ_ (mapᵉ proj₁ e) + ⊥ⁿ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) + _⊔ⁿ_ = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) + in (eval _⊔_ e) ≈ (n , Maybe.maybe′ (eval _⊔ⁿ_) ⊥ⁿ (filterᵉ n e)) + Expr-final = {!!} + + ⊔-assoc : ∀ (e₁ e₂ e₃ : Elem) → ((e₁ ⊔ e₂) ⊔ e₃) ≈ (e₁ ⊔ (e₂ ⊔ e₃)) + ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃) + using exprˡ ← (((` e₁) ⊔ᵉ (` e₂)) ⊔ᵉ (` e₃)) + using exprʳ ← ((` e₁) ⊔ᵉ ((` e₂) ⊔ᵉ (` e₃))) + with nˡ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprˡ) in pˡ + with nʳ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprʳ) in pʳ + with final₁ ← Expr-final exprˡ + with final₂ ← Expr-final exprʳ + rewrite pˡ rewrite pʳ + rewrite ⊔ᵇ-assoc n₁ n₂ n₃ + rewrite trans (sym pˡ ) pʳ + with nʳ ≟ n₁ | nʳ ≟ n₂ | nʳ ≟ n₃ + ... | yes refl | yes refl | yes refl = + let l-assoc = FiniteHeightLattice.⊔-assoc (proj₂ (𝓛 n₁)) l₁ l₂ l₃ + in ≈-trans final₁ (≈-trans (≈-lift l-assoc) (≈-sym final₂)) + ... | yes refl | yes refl | no _ = ≈-trans final₁ (≈-sym final₂) + ... | yes refl | no _ | yes refl = ≈-trans final₁ (≈-sym final₂) + ... | yes refl | no _ | no _ = ≈-trans final₁ (≈-sym final₂) + ... | no _ | yes refl | yes refl = ≈-trans final₁ (≈-sym final₂) + ... | no _ | yes refl | no _ = ≈-trans final₁ (≈-sym final₂) + ... | no _ | no _ | yes refl = ≈-trans final₁ (≈-sym final₂) + ... | no _ | no _ | no _ = ≈-trans final₁ (≈-sym final₂)