Martin Escardo | 27 Nov 22:56 2013
Picon
Picon

If all functions (N->N)->N are continuous, then 0=1.


   If all functions (N->N)->N are continuous, then 0=1.

Think of functions a : N -> N as sequences of natural numbers:

    a 0, a 1, a 2, a 3, ..., a n, ...

The "continuity axiom" for functions

     f : (N -> N) -> N,

that map sequences a : N -> N to numbers f(a), going back to Brouwer
in his intuitionistic mathematics in the early 20th century, says that
the value f(a) can depend only on a finite prefix of the infinite
argument a.

This makes sense computationally: there are no crystal balls in
computational processes, able to see and grasp the infinite input at
once. The input of f is computed bit-by-bit, in fact, often only when
f queries it.

After finitely many queries to its argument a : N -> N, the function f
is supposed to deliver its answer, if it's ever going to produce an
answer.

When this finiteness condition holds, we say that f is continuous
(never mind the reason for the terminology "continuous" in this message).

The link

(Continue reading)

Altenkirch Thorsten | 28 Nov 09:28 2013
Picon
Picon

Re: If all functions (N->N)->N are continuous, then 0=1.

I am puzzled again!

Clearly, this formulation of continuity is inconsistent with functional
extensionality because it makes it possible to observe an intensional
property of a function - its modulus of continuity. What is surprising is
that you manage to derive a contradiction w.o. using ext! So the wrong
formulation of continuity doesn't even work in vanilla intensional Type
Theory. 

Thorsten

On 27/11/2013 21:56, "Martin Escardo" <m.escardo@...> wrote:

>
>
>
>   If all functions (N->N)->N are continuous, then 0=1.

That is a bit of a lie. What you are saying is if for all functions we
know why they are continuous, then 0=1.

I mean "is continuous" does sound like a proposition, doesn't it?

>
>
>
>Think of functions a : N -> N as sequences of natural numbers:
>
>    a 0, a 1, a 2, a 3, ..., a n, ...
>
(Continue reading)

Martin Escardo | 28 Nov 10:52 2013
Picon
Picon

Re: If all functions (N->N)->N are continuous, then 0=1.


On 28/11/13 08:28, Altenkirch Thorsten wrote:
> Clearly, this formulation of continuity is inconsistent with functional
> extensionality because it makes it possible to observe an intensional
> property of a function - its modulus of continuity. What is surprising is
> that you manage to derive a contradiction w.o. using ext! So the wrong
> formulation of continuity doesn't even work in vanilla intensional Type
> Theory.

That's indeed one the points:

>> NB. Only the purest form of intensional Martin-Loef Type Theory is
>> used in the above Agda proof, and no universes are needed. No HoTT
>> axioms in particular.

(And no function extensionality in particular, as remarked in the
link.)

But the main point is that the interpretation Sigma of "exists" is not
always what we want (which is well known among a number of people).

Here is another (well known) example. If you define the image of a
function f : X -> Y to be

   im f = Sigma(y : Y).Sigma(x : X). f x = y,  (wrong),

then you get that im f is pointwise isomorphic to X. This is so even
if all elements of X are mapped to the same element y0 of Y. What one
needs is to hide some information, but not all:

(Continue reading)

Martin Escardo | 28 Nov 14:59 2013
Picon
Picon

Re: If all functions (N->N)->N are continuous, then 0=1.


On 28/11/13 08:28, Altenkirch Thorsten wrote:
> I am puzzled again!
>
> you manage to derive a contradiction w.o. using ext!

This has nothing to do with extensionality.

My one-sentence summary is this:

    Finding a continuity witness is a non-continuous operation.

No finite part of f:(N->N)->N is enough to find out which finite part
of a:N->N suffices to compute f(a).

The formulation of continuity, using Sigma, both

    (1) says that all functions are continuous, and
    (2) provides a continuity-witness-finder.

The proof of 0=1 works by defining a non-continuous function using the
hypothetical continuity-witness-finder (2), thus contradicting (1).

Martin
Andrea Vezzosi | 30 Nov 03:10 2013
Picon

Re: If all functions (N->N)->N are continuous, then 0=1.

On Thu, Nov 28, 2013 at 2:59 PM, Martin Escardo <m.escardo-dxBOTFGcEFw2EctHIo1CcQ@public.gmane.org> wrote:

My one-sentence summary is this:

   Finding a continuity witness is a non-continuous operation.

No finite part of f:(N->N)->N is enough to find out which finite part
of a:N->N suffices to compute f(a).


What would be an explicit definition of "finite part" for elements of (N -> N) -> N? Or, in other words, what's a good intuition for the topology of that type?


Andrea
 
The formulation of continuity, using Sigma, both

   (1) says that all functions are continuous, and
   (2) provides a continuity-witness-finder.

The proof of 0=1 works by defining a non-continuous function using the
hypothetical continuity-witness-finder (2), thus contradicting (1).


Martin
_______________________________________________
Agda mailing list
Agda-TrQ0NnR75ays1BDpvl8NfQ@public.gmane.orgmers.se
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Martin Escardo | 1 Dec 22:24 2013
Picon
Picon

Re: If all functions (N->N)->N are continuous, then 0=1.


On 30/11/13 02:10, Andrea Vezzosi wrote:
> On Thu, Nov 28, 2013 at 2:59 PM, Martin Escardo <m.escardo@...
> <mailto:m.escardo@...>> wrote:
>
>
>     My one-sentence summary is this:
>
>         Finding a continuity witness is a non-continuous operation.
>
>     No finite part of f:(N->N)->N is enough to find out which finite part
>     of a:N->N suffices to compute f(a).
>
>
> What would be an explicit definition of "finite part" for elements of (N
> -> N) -> N? Or, in other words, what's a good intuition for the topology
> of that type?

Sorry, I missed this question.

The topology of the type (N->N)->N is rather complicated in terms of
open sets. In terms of finiteness, an approach using domain theory is
natural, but requires a number of definitions and proofs before we can
say it.

Moreover, it is hard to formulate such things
constructively. Chuangjie Xu and I have done some work on this.

If you ignore constructivity, which can be useful for a rough (and
distorted) understanding, it is easier to think in terms of
convergent sequences. We say that a sequence f_i in (N->N)->N
converges to g if whenever a sequence a_i in N->N converges to b, then
the sequence f_i(a_i) converges to g(b).

So you still need to explain convergence in N->N. We say that a
sequence a_i in N->N convergers to b if for every n there is j such
that all a_i, for i>=j, agree with b in the first n positions.

Then the problem with the modulus-of-continuity functional is that it
doesn't preserve limits (it is not continuous).

If you want to know more, please feel free to ask. There are models of
type theory (classical and constructive) based on the above ideas. One
of them is Johnstone's topological topos. A closely related one,
studied by Chuangjie and myself, admits a constructive treatment.

Best,
Martin
Andrea Vezzosi | 4 Dec 07:22 2013
Picon

Re: If all functions (N->N)->N are continuous, then 0=1.

On Sun, Dec 1, 2013 at 10:24 PM, Martin Escardo <m.escardo-dxBOTFGcEFw2EctHIo1CcQ@public.gmane.org> wrote:
[...]
Then the problem with the modulus-of-continuity functional is that it
doesn't preserve limits (it is not continuous).

 
Does this mean that once we fix a modulus of continuity functional M we should be able to find a sequence f_i of continuous functions converging to g such that M f_i doesn't converge to M g? All without assuming M itself to be continuous?

It could be an interesting example.

 
If you want to know more, please feel free to ask. There are models of
type theory (classical and constructive) based on the above ideas. One
of them is Johnstone's topological topos. A closely related one,
studied by Chuangjie and myself, admits a constructive treatment.


What's a good article to start from for the constructive model?


-- Andrea
 
Best,

Martin

_______________________________________________
Agda mailing list
Agda-TrQ0NnR75ays1BDpvl8NfQ@public.gmane.orgmers.se
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda

Gmane