[Agda] termination by contradiction

[Dmytro Starosud]

Hello,

You are definitelly able to add new axioms to constructive logic if you are
sure (you have an evidence in theory or in meta-theory) it will not lead to
inconsistency.
And from that point of view Markov axiom is Ok.
The only problem is that people didn't find nice (non-adhoc) way to put
this axiom in theory (if I am not mistaking).

NB You can add this axiom only for types like Nat or "similar" (probably
"similar" here means сardinality).
For example adding such axiom for Float will lead to infinite loop.

Best regards,
Dmytro



2014-07-01 12:47 GMT+03:00 Sergei Meshveliani <mechvel at botik.ru>:

> 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
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140701/15726b2b/attachment.html