[Agda] termination by contradiction

[Sergei Meshveliani]

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?


Frédéric Blanqui wrote on June 30
> [..]
> I think that you need some axioms (dependent choice and excluded 
> middle). See
http://color.inria.fr/doc/CoLoR.Util.Relation.NotSN_IS.html 
> and related files (SN, InfSeq, NotSN).
> [..]


I would like to add some comments and to ask some questions.

(1) (M) does not intend to introduce a total excluded `or', it is only 
    for termination.
But is this possible? Can this lead logically to a total excluded `or' ?

(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 `or' ?
Can (3) be replaced in Agda with something that avoids
NO_TERMINATION_CHECK and `postulate' ?

Thanks,

------
Sergei











> >
> > Thanks,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>