Put the fixed point algorithm code into its own file
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
cbebe599b2
commit
e3b8cc39f1
|
|
@ -6,7 +6,7 @@ module Chain {a} {A : Set a}
|
||||||
(_R_ : 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
|
(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.Nat.Properties using (+-comm; m+1+n≰m)
|
||||||
open import Data.Product using (_×_; Σ; _,_)
|
open import Data.Product using (_×_; Σ; _,_)
|
||||||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
|
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
|
||||||
|
|
|
||||||
81
Fixedpoint.agda
Normal file
81
Fixedpoint.agda
Normal file
|
|
@ -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 ⊥ᴬ))
|
||||||
95
Lattice.agda
95
Lattice.agda
|
|
@ -442,98 +442,3 @@ module IsFiniteHeightLatticeInstances where
|
||||||
(proj₂ (IsFiniteHeightLattice.fixedHeight lB) b₁b₂))
|
(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 ⊥ᴬ))
|
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user