[Agda] termination by contradiction

[Frédéric Blanqui]

Hi.

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).

Best regards,

Frédéric.

Le 30/06/2014 11:52, Sergei Meshveliani a écrit :
> People,
>
> 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.
>
> Consider the following attempt.
> For a recursive function        f : Nat -> Nat,
> define
>         g : Nat -> Nat -> State,
>
> such that   g x n  is the `state' of the computation of  f x
> at the step  n.
> Then the type
>                (n : Nat) ->  \neg (isFinalState (g x n))          (NT)
>
> expresses a non-termination at x, and
>
>            ((n : Nat) ->  \neg (isFinalState (g x n)))  ->  \bottom
>
> will express termination by (M).
> Right?
>
> How to express this in Agda ?  Needs it to be expressed?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda