[Agda] termination proofs

[Altenkirch Thorsten]

The set of Turing machines is countable but we were talking about
*functions*.

The standard proof by diagonalisation that the set of functions from Nat
to Nat is uncountable can be carried out in Agda - this has nothing to do
with being classical.

Assuming that we can find out how a function can be computed (Church's
thesis + choice) is fishy both from a classical and constructive
perspective.

What is difficult to understand about constructive logic? I am having more
trouble with classical logic. Bool = Prop seems a strange idea.

Thorsten

On 25/09/2012 17:33, "Serge D. Mechveliani" <mechvel at botik.ru> wrote:

>On Tue, Sep 25, 2012 at 05:12:01PM +0100, Peter Hancock wrote:
>>
>>> The countability grounds is not relevant here, because I asked about an
>>> _algorithmic_ map in  Nat -> Nat.
>>
>> For me, a function just *is* an algorithmic map which we can recognise
>>as total.
>> The normal Cantor diagonalisation argument shows that Nat->Nat is
>>uncountable.
>>
>> I admit, this will seem strange at first, because there are only
>>countably
>> many Turing machines, and the total ones will be a subset of these.  But
>> the notion of a cardinal is a bit strange constructively.  There are
>> arbitrarily many subsets of a singleton, constructively.  I suggest that
>> this argument is worth a bit more of your attention.
>>
>> (I also admit I am sweeping some subtle points under the carpet.)
>
>I meant classical mathematics and classical logic. According to them,
>the set of total Tuering machines is countable.
>I try now to imagine many subsets of a singleton. And it comes out that
>there are as many as  2^1  of them, that is  2.
>
>I like Agda, despite that understand nothing in a non-classical logic.
>So far I, studied only that proofs are build as members of a dependent
>type, and that negation for T is represented as  T -> \bottom
>(if I do not confuse anything).
>
>Regards,
>
>------
>Sergei
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda

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.