[Agda] termination by contradiction

[Dmytro Starosud]

> What would be a good application of MP in programming?
It will extend the set of positively type-checked programs.
i.e. will decrease amount of first order errors, which in general is very
good.


2014-07-01 18:19 GMT+03:00 Altenkirch Thorsten <
psztxa at exmail.nottingham.ac.uk>:

> Yes, this is true.
>
> However, it is not clear how to do symbolic evaluation with MP. That is if
> we have a hypothetical classical proof of termination this doesn’t tell us
> wether we can partially execute our program.
> In the case of a constructive proof this is the case.
>
> We could say that we can run the program if the proof is closed but this
> seems a bit weird.
>
> What would be a good application of MP in programming?
>
> Cheers,
> Thorsten
>
>
> From: Dmytro Starosud <d.starosud at gmail.com>
> Date: Tue, 1 Jul 2014 15:19:34 +0100
> To: Sergei Meshveliani <mechvel at botik.ru>
> Cc: Agda mailing list <agda at lists.chalmers.se>
> Subject: Re: [Agda] termination by contradiction
>
> Markov axiom (for Nat) doesn't leed to a total excluded third.
> Constructive logic together with Markov axiom (for Nat) is still
> constructive.
> Here is really nice course
> <http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%2207756bb0-b872-4a4a-95b1-b77ad206dab3%22>
> (and book <http://homotopytypetheory.org/book/>) explaining in very deep
> details all that stuff with constructive vs classic vs whatever.
>
> Dmytro
>
> This message and any attachment are intended solely for the addressee and
> may contain confidential information. If you have received this message in
> error, please send it back to me, and immediately delete it.   Please do
> not use, copy or disclose the information contained in this message or in
> any attachment.  Any views or opinions expressed by the author of this
> email do not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140701/a7198804/attachment-0001.html