Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Semidecidability!
module Semidecidable where
open import Coinduction
open import Function
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary hiding (Rel)
import Relation.Binary.PropositionalEquality as PropEq
open import Category.Monad
open import Category.Monad.Partiality renaming (_⊥ to Partial)
open PropEq using (_≡_)
module M {f} = RawMonad (monad {f})
open Equivalence
data Terminates {a} {A : Set a} : Partial A → Set a where
now : (x : A) Terminates (now x)
later : {x} (t : Terminates (♭ x)) Terminates (later x)
get : {a} {A : Set a} {P : Partial A} Terminates P A
get (now x) = x
get (later t) = get t
data Loops {a} {A : Set a} : Partial A → Set a where
later : {x} (l : ∞ (Loops (♭ x))) Loops (later x)
module Respects {a ℓ} {A : Set a} (_∼_ : AASet ℓ) where
open Equality _∼_
terminates : {x y} k {eq : Equality k} Rel k x y Terminates x Terminates y
terminates k (Equality.now {y = y} x∼y) (now x) = now y
terminates ._ (Equality.laterʳ r) x = later (terminates _ r x)
terminates k {eq} (Equality.later x∼y) (later tx) = later (terminates k {eq} (♭ x∼y) tx)
terminates ._ {eq} (Equality.laterˡ r) (later tx) = terminates _ {eq} r tx
loops : {x y} k Rel k x y Loops x Loops y
loops k (Equality.later x∼y) (later l) = later (♯ (loops k (♭ x∼y) (♭ l)))
loops ._ (Equality.laterʳ r) (later l) = later (♯ (loops _ r (later l)))
loops ._ (Equality.laterˡ r) (later l) = loops _ r (♭ l)
>>=-terminates : {a} {A : Set a} {B : Set a}
{x : Partial A} (tx : Terminates x) {f : A Partial B} (tf : x Terminates (f x))
Terminates (x M.>>= f)
>>=-terminates (now x) tf = tf x
>>=-terminates {B = B} (later tx) tf = terminates (other weak) (Equality.laterʳ (refl PropEq.refl)) (>>=-terminates tx tf)
where open Respects {A = B} _≡_
record Semidecidable {A} (P : A → Set) : Set where
field
decide : x Partial (P x)
true-terminates : x P x Terminates (decide x)
-- Thanks to twanvl, benmachine, and the inhabitants of #Agda for pointing out that this didn't need to be a field of Semidecidable and
-- to twanvl in particular fo rwriting this implementation.
false-loops : {a} {A : Set a} (decider : Partial A) ¬ A Loops decider
false-loops (now x) ¬A = ⊥-elim (¬A x)
false-loops (later x) ¬A = later (♯ false-loops (♭ x) ¬A)
open import Data.Conat renaming (setoid to Coℕ-setoid)
data Finite : Coℕ → Set where
zero : Finite zero
suc : {n} (i : Finite (♭ n)) Finite (suc n)
finite : Semidecidable Finite
finite = record
{ decide = decide
; true-terminates = true-terminates
}
where
open Workaround
open Correct
mutual
decide-lemma : x (Finite x) ⊥P
decide-lemma x = later (♯ decide-helper x)
decide-helper : x (Finite x) ⊥P
decide-helper zero = now zero
decide-helper (suc n) = decide-lemma (♭ n) >>= (now ∘′ suc)
decide : x Partial (Finite x)
decide x = ⟦ decide-helper x ⟧P
true-terminates : x Finite x Terminates (decide x)
true-terminates zero zero = now zero
true-terminates (suc n) (suc f) =
terminates strong
(sym PropEq.sym _ (>>=-hom (decide-lemma (♭ n)) (now ∘′ suc)))
(later (>>=-terminates (true-terminates (♭ n) f) (λ x now (suc x))))
where open Respects {A = Finite (suc n)} _≡_
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.