[Agda] termination by contradiction

[Sergei Meshveliani]

I am sorry for a typo in my last letter.

"excluded `or'"  needs to be  "excluded third"

everywhere in this letter
(otherwise the letter looks too stupid). 

I repeat it with improvement:


On Tue, 2014-07-01 at 13:47 +0400, Sergei Meshveliani wrote:
> To my  
> 
> > > [..]
> > > is it possible in Agda to prove termination of a function by programming
> > > a
> > >        negation of non-termination             -- call it  method  (M)
> > >
> > > (deriving an absurd from assuming an infinite work of the algorithm)
> > > ?
> > >
> > > A.A.Markov wrote that this provides a wider class of constructive
> > > objects, and that this is intuitive enough.
> > >
> > > My current termination proofs in Agda use only a simple approach by
> > > providing an upper bound for a certain counter. And I have an impression
> > > that (M) gives something wider.
> > > [..]
> > > [..]
> > > How to express this in Agda ?  Needs it to be expressed?
> 
> [..]

> I would like to add some comments and to ask some questions.
> 
> (1) (M) does not intend to introduce a total excluded third, it is only 
>     for termination.
> But is this possible? Can this lead logically to a total excluded third?
> 
> (2) Can anybody give a simple example of and algorithm for which there 
>   is a simple termination proof by (M) and it is difficult to provide a
> termination proof without using (M) ? 
> (I recall that there are many statements in classical mathematics for
> which it is difficult to provide a proof other than by assuming some
> particular infinite sequence and deriving a contradiction from this).
> 
> (3) What can be a axiom for (M) in an Agda program:
> 
>  {-# NO_TERMINATION_CHECK #-}
>  findNatByContra : 
>           (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P
> 
>  findNatByContra P P? _ =  findFrom 0
>    where
>    findFrom : ℕ → Σ ℕ P
>    findFrom n = case P? n of \ { (yes Pn) → (n , Pn)
>                                ; (no _)   → findFrom (suc n) }
> 
> I think that this occurrence of NO_TERMINATION_CHECK  expresses (M) for
> all predicates on  ℕ,
> and  findNatByContra  together with this occurrence of
> NO_TERMINATION_CHECK  present the needed axiom with respect to  ℕ.
> 
> Right?
> May this lead to a total excluded third?
> Can (3) be replaced in Agda with something that avoids
> NO_TERMINATION_CHECK and `postulate' ?
> 
> Thanks,
> 
> ------
> Sergei