function definition noncomputable

Stream: new members

[Belisarius Cawl]

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.

[Kenny Lau]

just turn def into noncomputable def

[Belisarius Cawl]

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

[Belisarius Cawl]

Because for naturals it works.

[Belisarius Cawl]

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.

[Sebastien Gouezel]

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

[Belisarius Cawl]

haha ok :D

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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

[Belisarius Cawl]

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

[Anne Baanen]

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

[Belisarius Cawl]

hm, why not?

[Anne Baanen]

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.

[Anne Baanen]

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.

[Anne Baanen]

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.

[Kevin Buzzard]

A computer can't figure out whether the completely well-defined real number $\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.

[Belisarius Cawl]

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...

[Kevin Buzzard]

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.

[Anne Baanen]

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.

[Kevin Buzzard]

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

[Belisarius Cawl]

alright, understood. Thanks!

[Anne Baanen]

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

[Belisarius Cawl]

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

[Belisarius Cawl]

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

[Anne Baanen]

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.

[Scott Morrison]

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

[Belisarius Cawl]

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

[Belisarius Cawl]

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

[Belisarius Cawl]

(because fundamentalism has been disproven)

[Belisarius Cawl]

but yeah computability is definitely useful

[Belisarius Cawl]

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

[Mario Carneiro]

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

[Mario Carneiro]

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 $\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 $2^{-n}$ over all $n$ such that turing machine $M$ halts in at most $n$ steps, where $M$ 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

[Mario Carneiro]

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

[Damiano Testa]

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?

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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.

[Greg Price]

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 $2^{-n}$ over all $n$ such that turing machine $M$ halts in at most $n$ steps, where $M$ 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 $\delta > 0$. I have a feeling that's not a coincidence.

[Kevin Buzzard]

The reals are uncountable, the naturals are countable.

[Kevin Buzzard]

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.

[Greg Price]

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.

[Greg Price]

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

[Kevin Buzzard]

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

[Mario Carneiro]

@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

[Mario Carneiro]

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

[Mario Carneiro]

Here's one way to formalize the claim about uncountable sets: Suppose an algorithm is given elements $x,y$ in an uncountable set $X$, and it is permitted to ask questions of the form $x\in A?$ or $y\in A?$ where $A$ is some subset of $X$ 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/2^n,b/2^n)$.) The task is to determine if $x=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)$.

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=y$. But the diagonal itself is uncountable, so there must be two distinct points $x,y$ such that the program says $x=x$ and $y=y$ using exactly the same queries from start to end. But then $x$ and $y$ are indistinguishable to the algorithm, so it will also answer $x=y$, a contradiction.

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

[Greg Price]

That makes a lot of sense, thanks!

[Damiano Testa]

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 $n_P$ to be

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

As a mathematician, I would say that the value of $n_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?

[Mario Carneiro]

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 $n_P$ denotes.

[Mario Carneiro]

That is, the computation of $n_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.

[Damiano Testa]

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!

[Mario Carneiro]

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)!

[Damiano Testa]

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!

[Damiano Testa]

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.

[Damiano Testa]

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:

[Mario Carneiro]

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)

[Damiano Testa]

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

[Mario Carneiro]

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

[Damiano Testa]

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!

[Damiano Testa]

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