{-# OPTIONS --without-K --safe #-}
module Unbounded-space where
open import Colist
open import Conat hiding (pred) renaming (_+_ to _⊕_)
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Omniscience
open import Prelude
open import Tactic.By
open import Function-universe equality-with-J as F hiding (_∘_)
open import Nat equality-with-J as Nat using (_≤_; _≤↑_; pred)
open import Only-allocation
open import Upper-bounds
modify : Stmt → ℕ → ℕ
modify alloc = suc
modify dealloc = pred
mutual
⟦_⟧ : ∀ {i} → Program i → ℕ → Colist ℕ i
⟦ p ⟧ h = h ∷ ⟦ p ⟧′ h
⟦_⟧′ : ∀ {i} → Program i → ℕ → Colist′ ℕ i
⟦ [] ⟧′ h .force = []
⟦ s ∷ p ⟧′ h .force = ⟦ p .force ⟧ (modify s h)
Heap-usage : Program ∞ → Conat ∞ → Set
Heap-usage p n = LUB (⟦ p ⟧ 0) n
Heap-usage′ : Program ∞ → Conat ∞ → Set
Heap-usage′ p n =
(∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝)
×
(∀ n′ → (∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n′ ⊕ ⌜ h ⌝) → [ ∞ ] n ≤ n′)
∀⟦⟧⊑⇔⟦⟧⊑ :
∀ {p n i} →
[ i ] ⟦ p ⟧ 0 ⊑ n ⇔ (∀ h → [ i ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝)
∀⟦⟧⊑⇔⟦⟧⊑ {p} {n} {i} = record
{ to = to p
; from = (∀ h → [ i ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝) ↝⟨ _$ 0 ⟩
[ i ] ⟦ p ⟧ 0 ⊑ n ⊕ ⌜ 0 ⌝ ↝⟨ flip transitive-⊑≤ (∼→≤ (+-right-identity _)) ⟩□
[ i ] ⟦ p ⟧ 0 ⊑ n □
}
where
+⊕-cong :
∀ {m₁ m₂ n i} → [ i ] ⌜ m₁ ⌝ ≤ m₂ → [ i ] ⌜ m₁ + n ⌝ ≤ m₂ ⊕ ⌜ n ⌝
+⊕-cong {m₁} {m₂} {n} {i} =
[ i ] ⌜ m₁ ⌝ ≤ m₂ ↝⟨ _+-mono reflexive-≤ _ ⟩
[ i ] ⌜ m₁ ⌝ ⊕ ⌜ n ⌝ ≤ m₂ ⊕ ⌜ n ⌝ ↝⟨ transitive-≤ (∼→≤ (⌜⌝-+ m₁)) ⟩□
[ i ] ⌜ m₁ + n ⌝ ≤ m₂ ⊕ ⌜ n ⌝ □
to : ∀ {m i} p →
[ i ] ⟦ p ⟧ m ⊑ n → ∀ h → [ i ] ⟦ p ⟧ (m + h) ⊑ n ⊕ ⌜ h ⌝
to [] (m≤n ∷ _) _ = +⊕-cong m≤n ∷ λ { .force → [] }
to (s ∷ p) (m≤n ∷ p⊑) h = +⊕-cong m≤n ∷ λ { .force →
to′ _ s (force p⊑) }
where
to′ : ∀ {i} m s →
[ i ] ⟦ force p ⟧ (modify s m) ⊑ n →
[ i ] ⟦ force p ⟧ (modify s (m + h)) ⊑ n ⊕ ⌜ h ⌝
to′ _ alloc p⊑ = to (force p) p⊑ h
to′ (suc m) dealloc p⊑ = to (force p) p⊑ h
to′ zero dealloc p⊑ = transitive-⊑≤ (to (force p) p⊑ (pred h))
(reflexive-≤ n
+-mono
⌜⌝-mono (Nat.pred≤ _))
Heap-usage⇔Heap-usage′ :
∀ p n → Heap-usage p n ⇔ Heap-usage′ p n
Heap-usage⇔Heap-usage′ p n =
([ ∞ ] ⟦ p ⟧ 0 ⊑ n ↝⟨ ∀⟦⟧⊑⇔⟦⟧⊑ ⟩□
(∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n ⊕ ⌜ h ⌝) □)
×-cong
((∀ n′ → [ ∞ ] ⟦ p ⟧ 0 ⊑ n′ → [ ∞ ] n ≤ n′) ↝⟨ ∀-cong _ (λ _ → →-cong _ ∀⟦⟧⊑⇔⟦⟧⊑ F.id) ⟩□
(∀ n′ → (∀ h → [ ∞ ] ⟦ p ⟧ h ⊑ n′ ⊕ ⌜ h ⌝) → [ ∞ ] n ≤ n′) □)
max-unique :
∀ {p m n i} →
Heap-usage p m → Heap-usage p n → Conat.[ i ] m ∼ n
max-unique = lub-unique
max-respects-∼ :
∀ {p q m n} →
Colist.[ ∞ ] ⟦ p ⟧ 0 ∼ ⟦ q ⟧ 0 →
Conat.[ ∞ ] m ∼ n →
Heap-usage p m → Heap-usage q n
max-respects-∼ {p} {q} {m} {n} p∼q m∼n = Σ-map
([ ∞ ] ⟦ p ⟧ 0 ⊑ m ↝⟨ (λ hyp → transitive-⊑≤ (□-∼ p∼q hyp) (∼→≤ m∼n)) ⟩□
[ ∞ ] ⟦ q ⟧ 0 ⊑ n □)
((∀ o → [ ∞ ] ⟦ p ⟧ 0 ⊑ o → [ ∞ ] m ≤ o) ↝⟨ (λ hyp₁ o hyp₂ → transitive-≤ (∼→≤ (Conat.symmetric-∼ m∼n))
(hyp₁ o (□-∼ (Colist.symmetric-∼ p∼q) hyp₂))) ⟩□
(∀ o → [ ∞ ] ⟦ q ⟧ 0 ⊑ o → [ ∞ ] n ≤ o) □)
no-finite-max→infinite-max :
∀ p → (∀ n → ¬ [ ∞ ] ⟦ p ⟧ 0 ⊑ ⌜ n ⌝) → Heap-usage p infinity
no-finite-max→infinite-max p hyp =
(⟦ p ⟧ 0 ⊑infinity)
, λ n′ →
[ ∞ ] ⟦ p ⟧ 0 ⊑ n′ ↝⟨ no-finite→infinite hyp ⟩
Conat.[ ∞ ] n′ ∼ infinity ↝⟨ ∼→≤ ∘ Conat.symmetric-∼ ⟩□
[ ∞ ] infinity ≤ n′ □
max→wlpo : (∀ p → ∃ λ n → Heap-usage p n) → WLPO
max→wlpo find-max = λ f → case find-max (p f) of λ where
(zero , max-0) → inj₁ (_⇔_.to 0⇔≡false max-0)
(suc _ , max-+) → inj₂ (+→≢false max-+)
where
p : ∀ {i} → (ℕ → Bool) → Program i
p f = helper (f 0)
module P where
helper =
if_then alloc ∷′ []
else dealloc ∷ λ { .force → p (λ n → f (1 + n)) }
0⇔≡false :
∀ {f} → Heap-usage (p f) ⌜ 0 ⌝ ⇔ (∀ n → f n ≡ false)
0⇔≡false = record
{ to = →≡false _ ∘ proj₁
; from = λ ≡false →
≡false→ _ ≡false Nat.≤-refl
, (λ _ _ → zero)
}
where
→≡false : ∀ f → [ ∞ ] ⟦ p f ⟧ 0 ⊑ ⌜ 0 ⌝ → ∀ n → f n ≡ false
→≡false f ⟦pf⟧0⊑0 _ = helper _ _ refl ⟦pf⟧0⊑0
where
helper : ∀ b n →
f 0 ≡ b →
[ ∞ ] ⟦ P.helper f b ⟧ 0 ⊑ ⌜ 0 ⌝ →
f n ≡ false
helper false zero f0≡false = λ _ → f0≡false
helper false (suc n) _ =
[ ∞ ] ⟦ P.helper f false ⟧ 0 ⊑ ⌜ 0 ⌝ ↝⟨ □-tail ⟩
[ ∞ ] ⟦ p (f ∘ suc) ⟧ 0 ⊑ ⌜ 0 ⌝ ↝⟨ (λ hyp → →≡false (f ∘ suc) hyp n) ⟩□
(f ∘ suc) n ≡ false □
helper true n _ =
[ ∞ ] ⟦ P.helper f true ⟧ 0 ⊑ ⌜ 0 ⌝ ↝⟨ □-head ∘ □-tail ⟩
([ ∞ ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝) ↝⟨ ⌜⌝-mono⁻¹ ⟩
1 ≤ 0 ↝⟨ Nat.+≮ 0 ⟩
⊥ ↝⟨ ⊥-elim ⟩□
f n ≡ false □
≡false→ :
∀ {m n i} f →
(∀ n → f n ≡ false) →
m ≤ n → [ i ] ⟦ p f ⟧ m ⊑ ⌜ n ⌝
≡false→ {m} {n} f ≡false m≤n with f 0 | ≡false 0
... | true | ()
... | false | _ =
zero +-mono ⌜⌝-mono m≤n ∷ λ { .force →
≡false→ (f ∘ suc) (≡false ∘ suc) (
pred m Nat.≤⟨ Nat.pred≤ _ ⟩
m Nat.≤⟨ m≤n ⟩∎
n ∎≤) }
+→≢false :
∀ {f n} → Heap-usage (p f) (suc n) → ¬ (∀ n → f n ≡ false)
+→≢false {f} {n} =
Heap-usage (p f) (suc n) ↝⟨ (λ max-+ →
Heap-usage (p f) ⌜ 0 ⌝ ↝⟨ max-unique max-+ ⟩
Conat.[ ∞ ] suc n ∼ ⌜ 0 ⌝ ↝⟨ (λ ()) ⟩□
⊥ □) ⟩
¬ Heap-usage (p f) ⌜ 0 ⌝ ↝⟨ (λ hyp ≡false → hyp (_⇔_.from 0⇔≡false ≡false)) ⟩□
¬ (∀ n → f n ≡ false) □
wlpo⇔max : WLPO ⇔ (∀ p → ∃ λ n → Heap-usage p n)
wlpo⇔max = record
{ to = λ wlpo p → wlpo→lub wlpo (⟦ p ⟧ 0)
; from = max→wlpo
}
wlpo⇔lub : WLPO ⇔ (∀ ms → ∃ λ n → LUB ms n)
wlpo⇔lub = record
{ to = wlpo→lub
; from = λ find-lub → max→wlpo (λ p → find-lub (⟦ p ⟧ 0))
}
bounded-loops :
∀ {i n} → Conat.[ i ] length (⟦ bounded ⟧ n) ∼ infinity
bounded-loops =
suc λ { .force →
suc λ { .force →
bounded-loops }}
bounded₂-loops :
∀ {i n} → Conat.[ i ] length (⟦ bounded₂ ⟧ n) ∼ infinity
bounded₂-loops =
suc λ { .force →
suc λ { .force →
suc λ { .force →
suc λ { .force →
bounded₂-loops }}}}
unbounded-loops :
∀ {i n} → Conat.[ i ] length (⟦ unbounded ⟧ n) ∼ infinity
unbounded-loops =
suc λ { .force →
unbounded-loops }
⟦bounded⟧⋢0 : ¬ [ ∞ ] ⟦ bounded ⟧ 0 ⊑ ⌜ 0 ⌝
⟦bounded⟧⋢0 =
[ ∞ ] ⟦ bounded ⟧ 0 ⊑ ⌜ 0 ⌝ ↝⟨ □-head ∘ □-tail ⟩
[ ∞ ] ⌜ 1 ⌝ ≤ ⌜ 0 ⌝ ↝⟨ ⌜⌝-mono⁻¹ ⟩
(1 ≤ 0) ↝⟨ Nat.+≮ 0 ⟩□
⊥ □
⟦bounded⟧⊑1 :
∀ {i} → [ i ] ⟦ bounded ⟧ 0 ⊑ ⌜ 1 ⌝
⟦bounded⟧⊑1 =
≤suc ∷ λ { .force →
reflexive-≤ _ ∷ λ { .force →
⟦bounded⟧⊑1 }}
max-bounded-1 : Heap-usage bounded ⌜ 1 ⌝
max-bounded-1 =
⟦bounded⟧⊑1
, λ n′ →
[ ∞ ] ⟦ bounded ⟧ 0 ⊑ n′ ↝⟨ □-head ∘ □-tail ⟩□
[ ∞ ] ⌜ 1 ⌝ ≤ n′ □
⟦bounded₂⟧⊑2 :
∀ {i} → [ i ] ⟦ bounded₂ ⟧ 0 ⊑ ⌜ 2 ⌝
⟦bounded₂⟧⊑2 =
zero ∷ λ { .force →
suc (λ { .force → zero }) ∷ λ { .force →
reflexive-≤ _ ∷ λ { .force →
suc (λ { .force → zero }) ∷ λ { .force →
⟦bounded₂⟧⊑2 }}}}
max-bounded₂-2 : Heap-usage bounded₂ ⌜ 2 ⌝
max-bounded₂-2 =
⟦bounded₂⟧⊑2
, λ n′ →
[ ∞ ] ⟦ bounded₂ ⟧ 0 ⊑ n′ ↝⟨ □-head ∘ □-tail ∘ □-tail ⟩□
[ ∞ ] ⌜ 2 ⌝ ≤ n′ □
⟦unbounded⟧⋢⌜⌝ :
∀ {n} → ¬ [ ∞ ] ⟦ unbounded ⟧ 0 ⊑ ⌜ n ⌝
⟦unbounded⟧⋢⌜⌝ {n} = helper (Nat.≤→≤↑ (Nat.zero≤ _))
where
helper :
∀ {h} → h ≤↑ 1 + n → ¬ [ ∞ ] ⟦ unbounded ⟧ h ⊑ ⌜ n ⌝
helper (Nat.≤↑-refl refl) =
[ ∞ ] ⟦ unbounded ⟧ (1 + n) ⊑ ⌜ n ⌝ ↝⟨ □-head ⟩
[ ∞ ] ⌜ 1 + n ⌝ ≤ ⌜ n ⌝ ↝⟨ ⌜⌝-mono⁻¹ ⟩
(1 + n ≤ n) ↝⟨ Nat.+≮ 0 ⟩□
⊥ □
helper {h} (Nat.≤↑-step 1+h≤1+n) =
[ ∞ ] ⟦ unbounded ⟧ h ⊑ ⌜ n ⌝ ↝⟨ □-tail ⟩
[ ∞ ] ⟦ unbounded ⟧ (1 + h) ⊑ ⌜ n ⌝ ↝⟨ helper 1+h≤1+n ⟩□
⊥ □
max-unbounded-∞ : Heap-usage unbounded infinity
max-unbounded-∞ =
no-finite-max→infinite-max unbounded λ _ → ⟦unbounded⟧⋢⌜⌝
opt : ∀ {i} → Program ∞ → Program i
opt [] = []
opt (dealloc ∷ p) = dealloc ∷ λ { .force → opt (p .force) }
opt {i} (alloc ∷ p) = opt₁ (p .force)
module Opt where
default : Program i
default = alloc ∷ λ { .force → opt (p .force) }
opt₂ : Program ∞ → Program i
opt₂ (dealloc ∷ p″) = alloc ∷ λ { .force → opt (p″ .force) }
opt₂ _ = default
opt₁ : Program ∞ → Program i
opt₁ (alloc ∷ p′) = opt₂ (p′ .force)
opt₁ _ = default
opt-bounded₂∼bounded :
∀ {i n} →
Colist.[ i ] ⟦ opt bounded₂ ⟧ n ∼ ⟦ bounded ⟧ n
opt-bounded₂∼bounded =
refl ∷ λ { .force →
refl ∷ λ { .force →
opt-bounded₂∼bounded }}
opt-improves :
∃ λ p → Heap-usage p ⌜ 2 ⌝ × Heap-usage (opt p) ⌜ 1 ⌝
opt-improves =
bounded₂
, max-bounded₂-2
, max-respects-∼
(Colist.symmetric-∼ opt-bounded₂∼bounded)
(_ ∎∼)
max-bounded-1
mutual
opt-correct :
∀ {i m n} p →
Heap-usage (opt p) m → Heap-usage p n → [ i ] m ≤ n
opt-correct p max₁ max₂ =
_⇔_.to (≲⇔least-upper-bounds-≤ max₁ max₂) (opt-correct-≲ p)
opt-correct-≲ : ∀ {h i} p → [ i ] ⟦ opt p ⟧ h ≲ ⟦ p ⟧ h
opt-correct-≲ {h} [] =
⟦ opt [] ⟧ h ∼⟨ ∷∼∷′ ⟩≲
h ∷′ [] ∼⟨ Colist.symmetric-∼ ∷∼∷′ ⟩□≲
⟦ [] ⟧ h
opt-correct-≲ {h} (dealloc ∷ p) =
⟦ opt (dealloc ∷ p) ⟧ h ∼⟨ ∷∼∷′ ⟩≲
h ∷′ ⟦ opt (p .force) ⟧ (pred h) ≲⟨ (cons′-≲ λ { hyp .force → opt-correct-≲ (p .force) hyp }) ⟩
h ∷′ ⟦ p .force ⟧ (pred h) ∼⟨ Colist.symmetric-∼ ∷∼∷′ ⟩□≲
⟦ dealloc ∷ p ⟧ h
opt-correct-≲ {h} (alloc ∷ p) =
⟦ opt (alloc ∷ p) ⟧ h ≡⟨⟩≲
⟦ Opt.opt₁ p (p .force) ⟧ h ≲⟨ opt-correct₁ _ refl ⟩
h ∷′ ⟦ p .force ⟧ (1 + h) ∼⟨ Colist.symmetric-∼ ∷∼∷′ ⟩□≲
⟦ alloc ∷ p ⟧ h
where
default-correct :
∀ {p′ i} →
p′ ≡ p .force →
[ i ] ⟦ Opt.default p ⟧ h ≲ h ∷′ ⟦ p′ ⟧ (1 + h)
default-correct refl =
⟦ Opt.default p ⟧ h ∼⟨ ∷∼∷′ ⟩≲
h ∷′ ⟦ opt (p .force) ⟧ (1 + h) ≲⟨ (cons′-≲ λ { hyp .force → opt-correct-≲ (p .force) hyp }) ⟩□
h ∷′ ⟦ p .force ⟧ (1 + h)
opt-correct₁ :
∀ {i} p′ →
p′ ≡ p .force →
[ i ] ⟦ Opt.opt₁ p p′ ⟧ h ≲ h ∷′ ⟦ p′ ⟧ (1 + h)
opt-correct₁ [] []≡ = default-correct []≡
opt-correct₁ (dealloc ∷ p′) d∷≡ = default-correct d∷≡
opt-correct₁ (alloc ∷ p′) a∷≡ =
⟦ Opt.opt₂ p (p′ .force) ⟧ h ≲⟨ opt-correct₂ (p′ .force) refl ⟩
h ∷′ 1 + h ∷′ ⟦ p′ .force ⟧ (2 + h) ∼⟨ (refl ∷ λ { .force → Colist.symmetric-∼ ∷∼∷′ }) ⟩□≲
h ∷′ ⟦ alloc ∷ p′ ⟧ (1 + h)
where
default-correct′ :
∀ {i p″} →
p″ ≡ p′ .force →
[ i ] ⟦ Opt.default p ⟧ h ≲ h ∷′ 1 + h ∷′ ⟦ p″ ⟧ (2 + h)
default-correct′ refl =
⟦ Opt.default p ⟧ h ≲⟨ default-correct refl ⟩
h ∷′ ⟦ p .force ⟧ (1 + h) ≡⟨ by a∷≡ ⟩≲
h ∷′ ⟦ alloc ∷ p′ ⟧ (1 + h) ∼⟨ (refl ∷ λ { .force → ∷∼∷′ }) ⟩□≲
h ∷′ 1 + h ∷′ ⟦ p′ .force ⟧ (2 + h)
opt-correct₂ :
∀ {i} p″ →
p″ ≡ p′ .force →
[ i ] ⟦ Opt.opt₂ p p″ ⟧ h ≲ h ∷′ 1 + h ∷′ ⟦ p″ ⟧ (2 + h)
opt-correct₂ [] []≡ = default-correct′ []≡
opt-correct₂ (alloc ∷ p″) a∷≡ = default-correct′ a∷≡
opt-correct₂ (dealloc ∷ p″) _ =
⟦ Opt.opt₂ p (dealloc ∷ p″) ⟧ h ∼⟨ ∷∼∷′ ⟩≲
h ∷′ ⟦ opt (p″ .force) ⟧ (1 + h) ≲⟨ (cons′-≲ λ { hyp .force → opt-correct-≲ (p″ .force) hyp }) ⟩
h ∷′ ⟦ p″ .force ⟧ (1 + h) ≲⟨ (cons′-≲ λ { hyp .force → consʳ-≲ (consʳ-≲ (_ □≲)) hyp }) ⟩
h ∷′ 1 + h ∷′ 2 + h ∷′ ⟦ p″ .force ⟧ (1 + h) ∼⟨ (refl ∷ λ { .force → refl ∷ λ { .force → Colist.symmetric-∼ ∷∼∷′ } }) ⟩□≲
h ∷′ 1 + h ∷′ ⟦ dealloc ∷ p″ ⟧ (2 + h)