[Agda] termination by contradiction

[Peter Hancock]

On 01/07/2014 16:19, Altenkirch Thorsten wrote:
> Yes, this is true.

Er, what exactly do you think 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.

I think you are saying that Markov's *rule* is admissible (in any sane
formal system embodying some formal fragment of constructivity, like HA etc).

That at least is true.

To me, acceptance of Markov's axiom/principle has always seemed
a sufficient criterion for distinguishing those people who understand
constructivity platonistically from those who actually understand it
computationally.

Hank

> From: Dmytro Starosud
> <d.starosud at gmail.com<mailto:d.starosud at gmail.com>> Date: Tue, 1 Jul
> 2014 15:19:34 +0100 To: Sergei Meshveliani
> <mechvel at botik.ru<mailto:mechvel at botik.ru>> Cc: Agda mailing list
> <agda at lists.chalmers.se<mailto: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.
>
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________ Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>