[Agda] Re: Logical meaning of nontermination

[Dan Doel]

On Saturday 24 October 2009 3:24:14 pm Dan Doel wrote:
> You could, I suppose, write divergence as elements of (a) type (like):
> 
>   Diverges : ∀{A} → D A → Set
>   Diverges da = ∀{n} → ¬ Converges n da

Incidentally, this has a corresponding coalgebraic proof type:

---- snip ----

data ProofStream (P : ℕ → Set) : ℕ → Set where
  _::_ : ∀{m} → P m → ∞ (ProofStream P (suc m)) → ProofStream P m

from-∀ : ∀{m P} → (∀ n → P n) → ProofStream P m
from-∀ {m} p = p m :: (♯ from-∀ p)

add-l : ℕ → ℕ → ℕ
add-l zero    n = n
add-l (suc m) n = add-l m (suc n)

s≡s : ∀{m n} → m ≡ n → suc m ≡ suc n
s≡s refl = refl

lemma₀ : ∀{m n} → m + suc n ≡ suc m + n
lemma₀ {zero}  = refl
lemma₀ {suc m} = s≡s (lemma₀ {m})


lemma₁ : ∀{m n} → add-l m n ≡ m + n
lemma₁ {zero}      = refl
lemma₁ {suc m} {n} = begin
                       add-l m (suc n)
                     ≡⟨ lemma₁ {m} ⟩
                       m + suc n
                     ≡⟨ lemma₀ {m} {n} ⟩
                       suc m + n
                     ∎
                 
 where
 open EqReasoning setoid

lemma₂ : ∀{m} → m + 0 ≡ m
lemma₂ {zero}  = refl
lemma₂ {suc m} = s≡s lemma₂

ix : ∀{m P} → ProofStream P m → (n : ℕ) → P (add-l n m)
ix (Pm :: _)   zero    = Pm
ix (_  :: Psm) (suc n) = ix (♭ Psm) n

to-∀' : ∀{m P} → ProofStream P m → ∀ n → P (n + m)
to-∀' {m} {P} s n = subst P (lemma₁ {n} {m}) (ix s n)

to-∀ : ∀{P} → ProofStream P 0 → ∀ n → P n
to-∀ {P} s n = subst P lemma₂ (to-∀' s n)

---- snip ----

So:

  Diverges da = ProofStream (λ n → ¬ Converges n da) 0

-- Dan