From e3b8cc39f1eb0d8f0ab4cc1f074dbb91a770f0fb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 16 Sep 2023 13:39:35 -0700 Subject: [PATCH] Put the fixed point algorithm code into its own file Signed-off-by: Danila Fedorin --- Chain.agda | 2 +- Fixedpoint.agda | 81 +++++++++++++++++++++++++++++++++++++++++ Lattice.agda | 95 ------------------------------------------------- 3 files changed, 82 insertions(+), 96 deletions(-) create mode 100644 Fixedpoint.agda diff --git a/Chain.agda b/Chain.agda index 8aaf247..44c6bf7 100644 --- a/Chain.agda +++ b/Chain.agda @@ -6,7 +6,7 @@ module Chain {a} {A : Set a} (_R_ : A → A → Set a) (R-≈-cong : ∀ {a₁ a₁' a₂ a₂'} → a₁ ≈ a₁' → a₂ ≈ a₂' → a₁ R a₂ → a₁' R a₂') where -open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_) +open import Data.Nat using (ℕ; suc; _+_; _≤_) open import Data.Nat.Properties using (+-comm; m+1+n≰m) open import Data.Product using (_×_; Σ; _,_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) diff --git a/Fixedpoint.agda b/Fixedpoint.agda new file mode 100644 index 0000000..5fcf2ea --- /dev/null +++ b/Fixedpoint.agda @@ -0,0 +1,81 @@ +open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_) +open import Lattice + +module Fixedpoint {a} {A : Set a} + {h : ℕ} + {_≈_ : A → A → Set a} + {_⊔_ : A → A → A} {_⊓_ : A → A → A} + (decA : IsDecidable _≈_) + (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) + (f : A → A) + (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA) + (IsFiniteHeightLattice._≼_ flA) f) where + +open import Data.Nat.Properties using (+-suc; +-comm) +open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) +open import Relation.Binary.PropositionalEquality using (_≡_; sym) +open import Relation.Nullary using (Dec; ¬_; yes; no) + +import Chain +module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong + +open IsDecidable decA using () renaming (R-dec to ≈-dec) +open IsFiniteHeightLattice flA + +private + ⊥ᴬ : A + ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight)) + + ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a + ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ + ... | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a) + ... | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ) + ... | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))) + ... | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight)))) + where + ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ + ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _)) + + x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ + x≺⊥ᴬ = ((⊥ᴬ , ≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a))) , ⊥ᴬ⊓a̷≈⊥ᴬ) + + -- using 'g', for gas, here helps make sure the function terminates. + -- since A forms a fixed-height lattice, we must find a solution after + -- 'h' steps at most. Gas is set up such that as soon as it runs + -- out, we have exceeded h steps, which shouldn't be possible. + + doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a) + doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) + doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ) + with ≈-dec a₂ (f a₂) + ... | yes a₂≈fa₂ = (a₂ , a₂≈fa₂) + ... | no a₂̷≈fa₂ = doStep g' (suc hᶜ) a₁ (f a₂) c' g+hᶜ≡sh (Monotonicᶠ a₂≼fa₂) + where + a₂≺fa₂ : a₂ ≺ f a₂ + a₂≺fa₂ = (a₂≼fa₂ , a₂̷≈fa₂) + + c' : ChainA.Chain a₁ (f a₂) (suc hᶜ) + c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂}))) + + fix : Σ A (λ a → a ≈ f a) + fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ)) + +aᶠ : A +aᶠ = proj₁ fix + +aᶠ≈faᶠ : aᶠ ≈ f aᶠ +aᶠ≈faᶠ = proj₂ fix + +private + stepPreservesLess : ∀ (g hᶜ : ℕ) (a₁ a₂ a : A) (a≈fa : a ≈ f a) (a₂≼a : a₂ ≼ a) + (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) + (a₂≼fa₂ : a₂ ≼ f a₂) → + proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a + stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) + stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ) + with ≈-dec a₂ (f a₂) + ... | yes _ = a₂≼a + ... | no _ = stepPreservesLess g' _ _ _ a a≈fa (≼-cong ≈-refl (≈-sym a≈fa) (Monotonicᶠ a₂≼a)) _ _ _ + +aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a +aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ)) diff --git a/Lattice.agda b/Lattice.agda index a9c5ada..600da6d 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -442,98 +442,3 @@ module IsFiniteHeightLatticeInstances where (proj₂ (IsFiniteHeightLattice.fixedHeight lB) b₁b₂)) ) } - -module FixedHeightLatticeIsBounded {a} {A : Set a} {h : ℕ} - {_≈_ : A → A → Set a} - {_⊔_ : A → A → A} {_⊓_ : A → A → A} - (decA : IsDecidable _≈_) - (lA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) where - - open IsFiniteHeightLattice lA using (_≼_; _≺_; fixedHeight; ≈-equiv; ≈-refl; ≈-sym; ≈-trans; ≼-refl; ≼-cong; ≺-cong; ≈-⊔-cong; absorb-⊔-⊓; ⊔-comm; ⊓-comm) - open IsDecidable decA using () renaming (R-dec to ≈-dec) - open NatProps using (+-comm; m+1+n≰m) - - private - module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong - - A-BoundedBelow : Σ A (λ ⊥ᴬ → ∀ (a : A) → ⊥ᴬ ≼ a) - A-BoundedBelow = (⊥ᴬ , ⊥ᴬ≼) - where - ⊥ᴬ : A - ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight)) - - ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a - ⊥ᴬ≼ a - with ≈-dec a ⊥ᴬ - ... | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a) - ... | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ) - ... | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))) - ... | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight)))) - where - ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ - ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _)) - - x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ - x≺⊥ᴬ = ((⊥ᴬ , ≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a))) , ⊥ᴬ⊓a̷≈⊥ᴬ) - -module FixedPoint {a} {A : Set a} - (h : ℕ) - (_≈_ : A → A → Set a) (decA : IsDecidable _≈_) - (_⊔_ : A → A → A) (_⊓_ : A → A → A) - (isFiniteHeightLattice : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) - (f : A → A) (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ isFiniteHeightLattice) - (IsFiniteHeightLattice._≼_ isFiniteHeightLattice) f) where - open IsDecidable decA using () renaming (R-dec to ≈-dec) - open IsFiniteHeightLattice isFiniteHeightLattice - open FixedHeightLatticeIsBounded decA isFiniteHeightLattice - open NatProps using (+-suc; +-comm) - module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong - - private - ⊥ᴬ : A - ⊥ᴬ = proj₁ A-BoundedBelow - - ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a - ⊥ᴬ≼ = proj₂ A-BoundedBelow - - -- using 'g', for gas, here helps make sure the function terminates. - -- since A forms a fixed-height lattice, we must find a solution after - -- 'h' steps at most. Gas is set up such that as soon as it runs - -- out, we have exceeded h steps, which shouldn't be possible. - - doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a) - doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) - doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ) - with ≈-dec a₂ (f a₂) - ... | yes a₂≈fa₂ = (a₂ , a₂≈fa₂) - ... | no a₂̷≈fa₂ = doStep g' (suc hᶜ) a₁ (f a₂) c' g+hᶜ≡sh (Monotonicᶠ a₂≼fa₂) - where - a₂≺fa₂ : a₂ ≺ f a₂ - a₂≺fa₂ = (a₂≼fa₂ , a₂̷≈fa₂) - - c' : ChainA.Chain a₁ (f a₂) (suc hᶜ) - c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂}))) - - fix : Σ A (λ a → a ≈ f a) - fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ)) - - aᶠ : A - aᶠ = proj₁ fix - - aᶠ≈faᶠ : aᶠ ≈ f aᶠ - aᶠ≈faᶠ = proj₂ fix - - private - stepPreservesLess : ∀ (g hᶜ : ℕ) (a₁ a₂ a : A) (a≈fa : a ≈ f a) (a₂≼a : a₂ ≼ a) - (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) - (a₂≼fa₂ : a₂ ≼ f a₂) → - proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a - stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c) - stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ) - with ≈-dec a₂ (f a₂) - ... | yes _ = a₂≼a - ... | no _ = stepPreservesLess g' _ _ _ a a≈fa (≼-cong ≈-refl (≈-sym a≈fa) (Monotonicᶠ a₂≼a)) _ _ _ - - aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a - aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ)) -