[Agda] Re: Logical meaning of nontermination

[Dan Doel]

On Saturday 24 October 2009 1:39:16 pm Peter Hancock wrote:
> If I could throw another red herring into the pot, I wonder what
> people think of the idea of non-wellfounded proofs?  We might be
> reasonably comfortable with non-wellfounded data-structures, but
> I feel some reluctance to allow that *proofs* could be
> non-wellfounded in the same way. (Yes I am aware of Brotherston
> and Simpson, but that is something very specific and restricted.)
> It's like a proof has to be a wellfounded structure to carry
> conviction (from the premises to the conclusion).

Well, we have non-well-founded proofs in Agda, because proofs are data 
structures. Take, for instance, the partiality monad:

  data D (A : Set) : Set where
    now   : A → D A
    later : ∞ (D A) → D A

  ⊥ : ∀{A} → D A
  ⊥ = later (♯ ⊥)

Now, proofs of divergence are also codata:

  data Diverges {A : Set} : D A → Set where
    step : ∀{da} → ∞ (Diverges (♭ da)) → Diverges (later da)

  ⊥-diverges : ∀{A} → Diverges (⊥ {A})
  ⊥-diverges = step (♯ ⊥-diverges)

Proofs of bisimilarity of streams are in a similar boat. You could, I suppose, 
write divergence as elements of (a) type (like):

  Diverges : ∀{A} → D A → Set
  Diverges da = ∀{n} → ¬ Converges n da

But I don't really see a good reason to call the latter proofs and not the 
former.

-- Dan