Zulip Chat Archive

Stream: new members

Topic: function definition noncomputable


view this post on Zulip Belisarius Cawl (Mar 26 2021 at 09:53):

import data.real.basic
import analysis.special_functions.pow

def value (a t o1 o2 A T O1 O2 N : ) (N > 0) := A^a * T^t * O1^o1 * O2^o2 / N^(a + t + o1 + o2)

gives definition 'value' is noncomputable, it depends on 'real.division_ring'

Am at a loss here.

view this post on Zulip Kenny Lau (Mar 26 2021 at 09:53):

just turn def into noncomputable def

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 09:54):

Ok have not seen that before, thanks. What does it mean, though? both the error and the modifier.

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 09:54):

Because for naturals it works.

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 09:55):

My guess would be that I need to import the right stuff first but given the imports already in place I don't know what.

view this post on Zulip Sebastien Gouezel (Mar 26 2021 at 09:56):

The short answer is: you don't want to know, just add noncomputable.

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 09:56):

haha ok :D

view this post on Zulip Sebastien Gouezel (Mar 26 2021 at 09:57):

The long answer is that Lean is also a programming language, so you might want to write functions in Lean, and then compile it to executable code on your machine. Then Lean needs to know a recipe to compute the function. But this is not possible with real numbers, so Lean complains.

view this post on Zulip Sebastien Gouezel (Mar 26 2021 at 09:58):

noncomputable says: I will never use this function in executable code, so I don't care.

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 09:59):

that makes sense. Why is it not possible, though?

view this post on Zulip Anne Baanen (Mar 26 2021 at 09:59):

To divide by a real number, you need to check if it is equal to 0. But you cannot do that computably.

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:00):

hm, why not?

view this post on Zulip Anne Baanen (Mar 26 2021 at 10:01):

The standard example goes something like: define a real number ρ_99 as follows: the ith decimal of ρ_99 is 1 if the i .. i+99th decimals of π are all 9, 0 otherwise.

view this post on Zulip Anne Baanen (Mar 26 2021 at 10:02):

Then this number is exactly equal to 0 iff π has no block of 99 nines in its decimal expansion. Since we don't know whether this block of decimals exists, you cannot know whether ρ_99 is 0.

view this post on Zulip Anne Baanen (Mar 26 2021 at 10:04):

Computable means "computable in finite time" here, so just going through all the decimals of π and stopping at a block of 99 nines wouldn't work, if the block does not exist your computation would never finish.

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:05):

A computer can't figure out whether the completely well-defined real number π2/6n1n2\pi^2/6-\sum_{n\geq1}n^{-2} is zero or not, it needs to be told a theorem of Euler first. Nobody knows whether the well-defined number "sup of real parts of zeros of the zeta function" - 1/2 is zero or not.

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:06):

sure sure. And I guess it is proven that we can't know the thing about π.

But in any case I defined N to be nonzero...

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:07):

The point is that mathematicians manipulate real numbers in a different way to computers. We do non-computable things and it's no big deal.

view this post on Zulip Anne Baanen (Mar 26 2021 at 10:07):

In that case you could define a new division operator that doesn't need this check. However, in mathlib we tend not to care too much about computability, which is why the advice is to just put noncomputable in front of definitions where Lean asks you to.

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:07):

In Lean the reals are non-computable because everyone is happy with this state of affairs

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:08):

alright, understood. Thanks!

view this post on Zulip Anne Baanen (Mar 26 2021 at 10:09):

I care more about computability than the average mathlib user, but I know I will not win those discussions :)

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:11):

Well I guess it depends on your goals. Hard to argue about those

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:13):

but even if you care about computability having noncomputable stuff can be useful, not the other way around.

view this post on Zulip Anne Baanen (Mar 26 2021 at 10:15):

Indeed! And "computable in finite time" does not mean "computable before the end of the universe", and I tend to care more about the latter than the former.

view this post on Zulip Scott Morrison (Mar 26 2021 at 10:36):

Very-low-degree-P or don't bother!

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:37):

Wouldn't a physicist say the universe will last forever? Maybe you mean "before the universe reaches a stable state" ;)

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:38):

As an inverse fundamentalist I believe by the way the universe will exist for only 6000 more years

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:38):

(because fundamentalism has been disproven)

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:39):

but yeah computability is definitely useful

view this post on Zulip Belisarius Cawl (Mar 26 2021 at 10:40):

If not for practical reasons then because it approximates them, and also because the question is there

view this post on Zulip Mario Carneiro (Mar 26 2021 at 16:19):

Belisarius Cawl said:

Wouldn't a physicist say the universe will last forever? Maybe you mean "before the universe reaches a stable state" ;)

Well "before the computer falls apart" seems like a reasonable limitation

view this post on Zulip Mario Carneiro (Mar 26 2021 at 16:23):

Belisarius Cawl said:

sure sure. And I guess it is proven that we can't know the thing about π.

Actually that is not a very good example because it is decidable whether π2/6n1n2\pi^2/6-\sum_{n\geq1}n^{-2} is zero or not: it is, thanks to a theorem of Euler. A better example is the sum of 2n2^{-n} over all nn such that turing machine MM halts in at most nn steps, where MM is a fixed turing machine that searches for a contradiction in lean and halts at the first proof of false. If lean is consistent then we can't prove or disprove that this real number is equal to zero

view this post on Zulip Mario Carneiro (Mar 26 2021 at 16:26):

If you could decide equality of real numbers, you could solve this problem, which is only possible if lean is inconsistent

view this post on Zulip Damiano Testa (Mar 26 2021 at 21:58):

These arguments always make me think that I can also define a natural number that is 0 if one of those weird reals is 0 and 1 otherwise.
This is also non-computable, right?
Aren't we now in a position where we do not know if an integer is 0 or 1?

view this post on Zulip Eric Wieser (Mar 26 2021 at 22:21):

You can't write the if in that definition because that requires decidability too

view this post on Zulip Damiano Testa (Mar 26 2021 at 22:23):

Can't I take the ceiling of those reals? Is that also not allowed?

view this post on Zulip Eric Wieser (Mar 26 2021 at 22:51):

I'd wager that's not computable / deicdable either

view this post on Zulip Yury G. Kudryashov (Mar 26 2021 at 23:00):

If you want to take Sup s, where s is a set of real numbers, then you need to be able to decide if a given number b is an upper bound for s.

view this post on Zulip Yury G. Kudryashov (Mar 26 2021 at 23:01):

(And you need to find out if your set is bounded from above).

view this post on Zulip Kevin Buzzard (Mar 27 2021 at 00:37):

You can't take the ceiling of the absolute value of the value at 1 of the second derivative of your favourite algebraic rank 4 elliptic curve over Q because even though it's 0.000000000000000 to 1000 decimal places we don't have the tools to prove that it's 0.

view this post on Zulip Greg Price (Mar 27 2021 at 00:45):

Damiano raises an interesting question, I think: what is it about the reals that this sort of argument is relying on, that's missing from the integers (or naturals)?

I don't understand this area well enough to put my finger on an answer, but one thing I notice in Mario's example:

Mario Carneiro said:

the sum of 2n2^{-n} over all nn such that turing machine MM halts in at most nn steps, where MM is a fixed turing machine that searches for a contradiction in lean and halts at the first proof of false. If lean is consistent then we can't prove or disprove that this real number is equal to zero

is that we can decide whether this real is different from 0 by more than δ \delta , for any δ>0 \delta > 0 . I have a feeling that's not a coincidence.

view this post on Zulip Kevin Buzzard (Mar 27 2021 at 00:45):

The reals are uncountable, the naturals are countable.

view this post on Zulip Kevin Buzzard (Mar 27 2021 at 00:48):

The example I gave (a value of a function which is conjectured (by Birch and Swinnerton-Dyer) to be zero but which we can't right now prove is zero) is the same -- you can evaluate it to as many decimal places as you like, you just get more zeros, thus giving you more and more accuracy, but no algorithm.

view this post on Zulip Greg Price (Mar 27 2021 at 00:48):

Hmm interesting, and I guess pinning the value of the given real down to within δ \delta amounts to pinning it down into one of countably many possibilities, which is compatible with that explanation.

view this post on Zulip Greg Price (Mar 27 2021 at 00:50):

How is it that the examples are using the reals' uncountability?

view this post on Zulip Kevin Buzzard (Mar 27 2021 at 00:56):

If you can constructively biject a set with the naturals then you have an algorithm to decide equality, because the naturals have decidable equality.

view this post on Zulip Mario Carneiro (Mar 27 2021 at 04:05):

@Greg Price The fact that you can approximate equality up to any fixed δ\delta reflects the fact that the reals have a computable countable basis

view this post on Zulip Mario Carneiro (Mar 27 2021 at 04:10):

While I'm not sure there is a direct relationship between uncountability and undecidability, there is a very strong analogy between Cantor's diagonal proof of the uncountability of the reals, and Turing's diagonal proof of the undecidability of the halting problem

view this post on Zulip Mario Carneiro (Mar 27 2021 at 04:32):

Here's one way to formalize the claim about uncountable sets: Suppose an algorithm is given elements x,yx,y in an uncountable set XX, and it is permitted to ask questions of the form xA?x\in A? or yA?y\in A? where AA is some subset of XX which may depend on all previous queries. (So for example if it queries bits then these sets are simple combinations of sets of the form [a/2n,b/2n)[a/2^n,b/2^n).) The task is to determine if x=yx=y. This can be seen as an infinite decision tree, where the nodes are points in the progress of the algorithm after asking some questions about (x,y)(x,y).

The entire decision tree is countable (the nodes, not the branches), since it is a subset of the complete infinite binary tree. Every answer must be delivered in finite time and so there are a finite number of yes answers, points in the decision tree where the program says that x=yx=y. But the diagonal itself is uncountable, so there must be two distinct points x,yx,y such that the program says x=xx=x and y=yy=y using exactly the same queries from start to end. But then xx and yy are indistinguishable to the algorithm, so it will also answer x=yx=y, a contradiction.

Thus no uncountable set XX can have a decision procedure for equality.

view this post on Zulip Greg Price (Mar 27 2021 at 05:08):

That makes a lot of sense, thanks!

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:01):

Thank you all for the explanations!

I find these decidability issues quite confusing. I am going to propose a further doubt that I have, in case you have not had enough of this thread!

Suppose that an oracle tells me that P is a proposition about the natural numbers and they tell me that it is algorithmically undecidable to find a counterexample to P. I define a natural number nPn_P to be

  • 0, if P has no counterexample;
  • 1, otherwise.

As a mathematician, I would say that the value of nPn_P is zero and move on with my life. However, with my abismal knowledge of computability, I would think that this natural number is non-computable.

Where is the fallacy in this argument?

view this post on Zulip Mario Carneiro (Mar 27 2021 at 06:17):

The natural number is noncomputable. The issue is that while natural numbers have decidable equality, this only means that given two values (i.e. numerals) of type nat we can determine in finite time if they are equal, and it extends to computable terms of type nat. The term you have given is of the form if P then 1 else 0 where P is not a decidable proposition, so it is not possible to compute the term that nPn_P denotes.

view this post on Zulip Mario Carneiro (Mar 27 2021 at 06:18):

That is, the computation of nPn_P involves first determining P as a boolean (true or false), which is to say, we need to decide P, which by supposition is impossible.

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:22):

Aahhh! I think that I am finally understanding! The representation in a computer of a natural/real number is via its digits. So "knowing" a number, means knowing it's digits. I was trying (and apparently succeeded) in making a single digit non-computable. The issue with the reals, though, is that you can even construct a real for which all the digits that you can compute turn out to be zero, but you will never know that, later on, there is a non-zero digit.

I hope that I got this right, now!

view this post on Zulip Mario Carneiro (Mar 27 2021 at 06:30):

By the way, there is a funny paradox in your oracle. Assume that P n is decidable for each n. The oracle claims that \exists n, P n is not decidable. If P n was true, then \exists n, P n would be decidable (because you can decide in finite time by finding the example), so therefore P n is always false. But then \exists n, P n is decidable, because it is false (and decided by the trivial algorithm return false)!

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:31):

This also aligns well with the "obvious" fact that you can prove that two real number are different, by finding that one of their digits is different, but that I would not look at the digits of two real numbers to check if they are equal!

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:35):

Mario, I think that your P is my not P. Apart from that, I also always find oracles confusing, precisely for reasons similar to your amusing paradox!

The fact that an unprovable proposition must not have counterexamples always stroke me as a very funny concept and essentially felt like the barber's paradox.

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:39):

In any case, I feel that I understand these decidability issues much better now, thank you all very much!

Also, I was using an oracle, since I find that the concrete examples with RH, BSD,... are always limited by the fact that I can always say that my algorithm for computing the various numbers, first enumerates possible proofs of the underlying conjecture, might find a proof, and eventually let me know the correct answer!

The oracle prevents this, at the potential cost of introducing an inconsistency. What's the problem with that? :wink:

view this post on Zulip Mario Carneiro (Mar 27 2021 at 06:42):

The oracle has the issue that it depends where the information is coming from, and it also makes it hard to distinguish "true" and "provable", the latter of which might have a finitistic import (i.e. you can search for a proof if it's provable)

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:43):

Technically, you also can search for a proof if it is not provable...

view this post on Zulip Mario Carneiro (Mar 27 2021 at 06:44):

more specifically you can search for a proof and know that your search will terminate

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:44):

Anyway, modulo oracle issues, I get the punchline now: knowing the digits of a real number is not a good way to decide if a number is zero or not. This seems the bottom line of the arguments. The same statement about integers is "clearly" ok!

view this post on Zulip Damiano Testa (Mar 27 2021 at 06:46):

Suddenly, "decidable equality" says exactly what it should and what I had failed to understand until now...


Last updated: May 08 2021 at 19:11 UTC