{-# OPTIONS --cubical --safe #-}
module Partiality-monad.Inductive.Fixpoints where
open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (⊥)
open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Monad equality-with-J hiding (sequence)
open import Univalence-axiom equality-with-J
open import Partiality-algebra using (Partiality-algebra)
import Partiality-algebra.Fixpoints as PAF
open import Partiality-algebra.Monotone
open import Partiality-algebra.Omega-continuous
open import Partiality-algebra.Pi as Pi hiding (at)
open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Monad
open import Partiality-monad.Inductive.Monotone using ([_⊥→_⊥]⊑)
open import Partiality-monad.Inductive.Omega-continuous
module _ {a} {A : Type a} where
open PAF.Fix {P = partiality-algebra A} public
open [_⊥→_⊥]
fix′ : (A → A ⊥) → A ⊥
fix′ f = fix (monotone-function (f ∗))
fix′-is-fixpoint-combinator :
(f : A → A ⊥) →
fix′ f ≡ fix′ f >>= f
fix′-is-fixpoint-combinator f =
fix′ f ≡⟨⟩
fix (monotone-function (f ∗)) ≡⟨ fix-is-fixpoint-combinator (f ∗) ⟩∎
fix (monotone-function (f ∗)) >>= f ∎
fix′-is-least :
(f : A → A ⊥) →
(x : A ⊥) → x >>= f ⊑ x → fix′ f ⊑ x
fix′-is-least f = fix-is-least (monotone-function (f ∗))
fix′-∘ : (f : A → A ⊥) → fix′ (λ x → f x >>= f) ≡ fix′ f
fix′-∘ f =
fix′ (λ x → f x >>= f) ≡⟨⟩
fix (monotone-function ((λ x → f x >>= f) ∗)) ≡⟨ cong fix (_↔_.to equality-characterisation-monotone λ (x : A ⊥) →
(x >>= λ y → f y >>= f) ≡⟨ associativity x f f ⟩∎
x >>= f >>= f ∎) ⟩
fix (monotone-function (f ∗) ∘⊑ monotone-function (f ∗)) ≡⟨ fix-∘ (monotone-function (f ∗)) ⟩∎
fix′ f ∎
fix′-induction₁ :
∀ {p}
(P : A ⊥ → Type p)
(P⊥ : P never)
(P⨆ : ∀ s → (∀ n → P (s [ n ])) → P (⨆ s))
(f : A → A ⊥) →
(∀ x → P x → P (x >>= f)) →
P (fix′ f)
fix′-induction₁ P P⊥ P⨆ f =
fix-induction₁ P P⊥ P⨆ ([_⊥→_⊥].monotone-function (f ∗))
module _ {a p} n
(As : Fin n → Type a)
(P : (∀ i → As i ⊥) → Type p)
(P⊥ : P (λ _ → never))
(P⨆ : ∀ ss → (∀ n → P (λ i → ss i [ n ])) → P (⨆ ∘ ss))
where
open PAF.N-ary n As (λ i → partiality-algebra (As i)) P P⊥ P⨆ public
fix′-induction :
(fs : ∀ i → As i → As i ⊥) →
(∀ xs → P xs → P (λ i → xs i >>= fs i)) →
P (fix′ ∘ fs)
fix′-induction fs =
fix-induction (λ i → [_⊥→_⊥].monotone-function (fs i ∗))
module _ {a b} (A : Type a) (B : A → Type b) where
Trans : Type (a ⊔ b)
Trans = ((x : A) → B x ⊥) → ((x : A) → B x ⊥)
Pi : Partiality-algebra (a ⊔ b) (a ⊔ b) ((x : A) → B x)
Pi = Π A (partiality-algebra ∘ B)
Trans-⊑ : Type (a ⊔ b)
Trans-⊑ = [ Pi ⟶ Pi ]⊑
private
sanity-check : Trans-⊑ → Trans
sanity-check = [_⟶_]⊑.function
Trans-ω : Type (a ⊔ b)
Trans-ω = [ Pi ⟶ Pi ]
module _ {a b} {A : Type a} {B : A → Type b} where
module Trans-⊑ = [_⟶_]⊑ {P₁ = Pi A B} {P₂ = Pi A B}
module Trans-ω = [_⟶_] {P₁ = Pi A B} {P₂ = Pi A B}
private
module F = PAF.Fix {P = Pi A B}
at :
(∃ λ (f : ℕ → (x : A) → B x ⊥) → ∀ n x → f n x ⊑ f (suc n) x) →
(x : A) → ∃ λ (f : ℕ → B x ⊥) → ∀ n → f n ⊑ f (suc n)
at = Pi.at (partiality-algebra ∘ B)
app→ : Trans-⊑ A B → ℕ → ((x : A) → B x ⊥)
app→ = F.app
fix→-sequence : Trans-⊑ A B →
Partiality-algebra.Increasing-sequence (Pi A B)
fix→-sequence = F.fix-sequence
fix→ : Trans-⊑ A B → ((x : A) → B x ⊥)
fix→ = F.fix
fix→-is-fixpoint-combinator :
(f : Trans-ω A B) →
fix→ (Trans-ω.monotone-function f) ≡
Trans-ω.function f (fix→ (Trans-ω.monotone-function f))
fix→-is-fixpoint-combinator = F.fix-is-fixpoint-combinator
fix→-is-least :
(f : Trans-⊑ A B) →
∀ g → (∀ x → Trans-⊑.function f g x ⊑ g x) →
∀ x → fix→ f x ⊑ g x
fix→-is-least = F.fix-is-least
fix→-∘ : (f : Trans-⊑ A B) → fix→ (f ∘⊑ f) ≡ fix→ f
fix→-∘ = F.fix-∘
module _
{a b p} n
(As : Fin n → Type a)
(Bs : (i : Fin n) → As i → Type b)
(P : (∀ i → (x : As i) → Bs i x ⊥) → Type p)
(P⊥ : P (λ _ _ → never))
(P⨆ : (ss : ∀ i (x : As i) → Increasing-sequence (Bs i x)) →
(∀ n → P (λ i xs → ss i xs [ n ])) →
P (λ i xs → ⨆ (ss i xs)))
(fs : ∀ i → Trans-⊑ (As i) (Bs i)) where
private
module N = PAF.N-ary n
(λ i → (x : As i) → Bs i x)
(λ i → Π (As i) (partiality-algebra ∘ Bs i))
P
P⊥
(λ _ → P⨆ _)
fs
fix→-induction′ :
(∀ n → P (λ i → app→ (fs i) n) →
P (λ i → app→ (fs i) (suc n))) →
P (λ i → fix→ (fs i))
fix→-induction′ = N.fix-induction′
fix→-induction :
((gs : ∀ i (x : As i) → Bs i x ⊥) →
P gs → P (λ i → Trans-⊑.function (fs i) (gs i))) →
P (λ i → fix→ (fs i))
fix→-induction = N.fix-induction
fix→-induction₁ :
∀ {a b p} {A : Type a} {B : A → Type b}
(P : ((x : A) → B x ⊥) → Type p) →
P (λ _ → never) →
((s : (x : A) → Increasing-sequence (B x)) →
(∀ n → P (λ x → s x [ n ])) →
P (λ x → ⨆ (s x))) →
(f : Trans-⊑ A B) →
(∀ g → P g → P (Trans-⊑.function f g)) →
P (fix→ f)
fix→-induction₁ P P⊥ P⨆ = PAF.fix-induction₁ P P⊥ (λ _ → P⨆ _)
record Partial
{a b c}
(A : Type a) (B : A → Type b) (C : Type c) :
Type (a ⊔ b ⊔ lsuc c) where
field
function : ((x : A) → B x ⊥) → C ⊥
monotone : ∀ {rec₁ rec₂} →
(∀ x → rec₁ x ⊑ rec₂ x) →
function rec₁ ⊑ function rec₂
sequence : ((x : A) → Increasing-sequence (B x)) →
Increasing-sequence C
sequence recs =
(λ n → function (λ x → recs x [ n ]))
, (λ n → monotone (λ x → increasing (recs x) n))
field
ω-continuous : (recs : (x : A) → Increasing-sequence (B x)) →
function (⨆ ∘ recs) ≡ ⨆ (sequence recs)
rec : ∀ {a b} {A : Type a} {B : A → Type b} →
(x : A) → Partial A B (B x)
rec x = record
{ function = _$ x
; monotone = _$ x
; ω-continuous = λ _ → refl
}
transformer : ∀ {a b} {A : Type a} {B : A → Type b} →
((x : A) → Partial A B (B x)) → Trans-⊑ A B
transformer f = record
{ function = λ g x → function (f x) g
; monotone = λ g₁⊑g₂ x → monotone (f x) g₁⊑g₂
}
where
open Partial
transformer-ω : ∀ {a b} {A : Type a} {B : A → Type b} →
((x : A) → Partial A B (B x)) → Trans-ω A B
transformer-ω f = record
{ monotone-function = transformer f
; ω-continuous = λ _ → ⟨ext⟩ λ x → ω-continuous (f x) _
}
where
open Partial
fixP : ∀ {a b} {A : Type a} {B : A → Type b} →
((x : A) → Partial A B (B x)) → ((x : A) → B x ⊥)
fixP {A = A} {B} =
((x : A) → Partial A B (B x)) ↝⟨ transformer ⟩
Trans-⊑ A B ↝⟨ fix→ ⟩□
((x : A) → B x ⊥) □
fixP-is-fixpoint-combinator :
∀ {a b} {A : Type a} {B : A → Type b} →
(f : (x : A) → Partial A B (B x)) →
fixP f ≡ flip (Partial.function ∘ f) (fixP f)
fixP-is-fixpoint-combinator =
fix→-is-fixpoint-combinator ∘ transformer-ω
fixP-is-least :
∀ {a b} {A : Type a} {B : A → Type b}
(f : (x : A) → Partial A B (B x)) →
∀ g → (∀ x → Partial.function (f x) g ⊑ g x) →
∀ x → fixP f x ⊑ g x
fixP-is-least = fix→-is-least ∘ transformer
infixr 40 _∘P_
_∘P_ :
∀ {a b} {A : Type a} {B : A → Type b} →
((x : A) → Partial A B (B x)) →
((x : A) → Partial A B (B x)) →
((x : A) → Partial A B (B x))
Partial.function ((f ∘P g) x) = λ h →
Partial.function (f x) λ y →
Partial.function (g y) h
Partial.monotone ((f ∘P g) x) = λ hyp →
Partial.monotone (f x) λ y →
Partial.monotone (g y) hyp
Partial.ω-continuous ((f ∘P g) x) = λ recs →
function (f x) (λ y → function (g y) (⨆ ∘ recs)) ≡⟨ cong (function (f x)) (⟨ext⟩ λ y → ω-continuous (g y) recs) ⟩
function (f x) (λ y → ⨆ (sequence (g y) recs)) ≡⟨ ω-continuous (f x) (λ y → sequence (g y) recs) ⟩∎
⨆ (sequence (f x) λ y → sequence (g y) recs) ∎
where
open Partial
fixP-∘ : ∀ {a b} {A : Type a} {B : A → Type b}
(f : (x : A) → Partial A B (B x)) →
fixP (f ∘P f) ≡ fixP f
fixP-∘ f =
fix→ (transformer (f ∘P f)) ≡⟨⟩
fix→ (transformer f ∘⊑ transformer f) ≡⟨ fix→-∘ (transformer f) ⟩∎
fix→ (transformer f) ∎
module _
{a b p} n
(As : Fin n → Type a)
(Bs : (i : Fin n) → As i → Type b)
(P : (∀ i (x : As i) → Bs i x ⊥) → Type p)
(P⊥ : P (λ _ _ → never))
(P⨆ : (ss : ∀ i (x : As i) → Increasing-sequence (Bs i x)) →
(∀ n → P (λ i xs → ss i xs [ n ])) →
P (λ i xs → ⨆ (ss i xs)))
(fs : ∀ i (x : As i) → Partial (As i) (Bs i) (Bs i x)) where
fixP-induction′ :
(∀ n → P (λ i → app→ (transformer (fs i)) n) →
P (λ i → app→ (transformer (fs i)) (suc n))) →
P (λ i → fixP (fs i))
fixP-induction′ =
fix→-induction′ n As Bs P P⊥ P⨆ (transformer ∘ fs)
fixP-induction :
((gs : ∀ i (x : As i) → Bs i x ⊥) →
P gs → P (λ i xs → Partial.function (fs i xs) (gs i))) →
P (λ i → fixP (fs i))
fixP-induction =
fix→-induction n As Bs P P⊥ P⨆ (transformer ∘ fs)
fixP-induction₁ :
∀ {a b p} {A : Type a} {B : A → Type b}
(P : ((x : A) → B x ⊥) → Type p) →
P (λ _ → never) →
((s : (x : A) → Increasing-sequence (B x)) →
(∀ n → P (λ x → s x [ n ])) →
P (λ x → ⨆ (s x))) →
(f : (x : A) → Partial A B (B x)) →
(∀ g → P g → P (λ x → Partial.function (f x) g)) →
P (fixP f)
fixP-induction₁ P P⊥ P⨆ f =
fix→-induction₁ P P⊥ P⨆ (transformer f)
equality-characterisation-Partial :
∀ {a b c} {A : Type a} {B : A → Type b} {C : Type c}
{f g : Partial A B C} →
(∀ rec → Partial.function f rec ≡ Partial.function g rec) ↔
f ≡ g
equality-characterisation-Partial {f = f} {g} =
(∀ rec → function f rec ≡ function g rec) ↔⟨ Eq.extensionality-isomorphism ext ⟩
function f ≡ function g ↝⟨ ignore-propositional-component
(Σ-closure 1
(implicit-Π-closure ext 1 λ _ →
implicit-Π-closure ext 1 λ _ →
Π-closure ext 1 λ _ →
⊑-propositional) λ _ →
Π-closure ext 1 λ _ →
⊥-is-set) ⟩
(function f , _) ≡ (function g , _) ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ lemma) ⟩□
f ≡ g □
where
open Partial
lemma :
Partial _ _ _
↔
∃ λ f →
∃ λ (_ : ∀ {rec₁ rec₂} → (∀ x → rec₁ x ⊑ _) → f rec₁ ⊑ _) → _
lemma = record
{ surjection = record
{ logical-equivalence = record
{ to = λ x → function x , monotone x , ω-continuous x
; from = λ { (f , m , ω) → record
{ function = f
; monotone = λ {rec₁ rec₂} → m {rec₁ = rec₁} {rec₂ = rec₂}
; ω-continuous = ω
} }
}
; right-inverse-of = λ _ → refl
}
; left-inverse-of = λ _ → refl
}
non-recursive :
∀ {a b c} {A : Type a} {B : A → Type b} {C : Type c} →
C ⊥ → Partial A B C
non-recursive x = record
{ function = const x
; monotone = const (x ■)
; ω-continuous = λ _ →
x ≡⟨ sym ⨆-const ⟩∎
⨆ (constˢ x) ∎
}
instance
partial-raw-monad : ∀ {a b c} {A : Type a} {B : A → Type b} →
Raw-monad (Partial {c = c} A B)
Raw-monad.return partial-raw-monad x = non-recursive (return x)
Raw-monad._>>=_ partial-raw-monad x f = record
{ function = λ rec →
function x rec >>=′ λ y →
function (f y) rec
; monotone = λ rec⊑rec →
monotone x rec⊑rec >>=-mono λ y →
monotone (f y) rec⊑rec
; ω-continuous = λ recs →
(function x (⨆ ∘ recs) >>=′ λ y → function (f y) (⨆ ∘ recs)) ≡⟨ cong₂ _>>=′_ (ω-continuous x recs)
(⟨ext⟩ λ y → ω-continuous (f y) recs) ⟩
(⨆ (sequence x recs) >>=′ λ y → ⨆ (sequence (f y) recs)) ≡⟨ ⨆->>= ⟩
⨆ ( (λ n →
function x (λ z → recs z [ n ]) >>=′ λ y →
⨆ (sequence (f y) recs))
, _
) ≡⟨ ⨆>>=⨆≡⨆>>= (sequence x recs)
(λ y → sequence (f y) recs) ⟩∎
⨆ ( (λ n → function x (λ z → recs z [ n ]) >>=′ λ y →
function (f y) (λ z → recs z [ n ]))
, _
) ∎
}
where
open Partial
partial-monad : ∀ {a b c} {A : Type a} {B : A → Type b} →
Monad (Partial {c = c} A B)
Monad.raw-monad partial-monad = partial-raw-monad
Monad.left-identity partial-monad _ f =
_↔_.to equality-characterisation-Partial
(λ h → left-identity _ (λ y → Partial.function (f y) h))
Monad.right-identity partial-monad _ =
_↔_.to equality-characterisation-Partial
(λ _ → right-identity _)
Monad.associativity partial-monad x _ _ =
_↔_.to equality-characterisation-Partial
(λ h → associativity (Partial.function x h) _ _)