# Zulip Chat Archive

## Stream: new members

### Topic: function definition noncomputable

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

#### Kenny Lau (Mar 26 2021 at 09:53):

just turn `def`

into `noncomputable def`

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

#### Belisarius Cawl (Mar 26 2021 at 09:54):

Because for naturals it works.

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

#### Sebastien Gouezel (Mar 26 2021 at 09:56):

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

.

#### Belisarius Cawl (Mar 26 2021 at 09:56):

haha ok :D

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

#### Sebastien Gouezel (Mar 26 2021 at 09:58):

`noncomputable`

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

#### Belisarius Cawl (Mar 26 2021 at 09:59):

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

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

#### Belisarius Cawl (Mar 26 2021 at 10:00):

hm, why not?

#### Anne Baanen (Mar 26 2021 at 10:01):

The standard example goes something like: define a real number `ρ_99`

as follows: the `i`

th decimal of `ρ_99`

is 1 if the `i .. i+99`

th decimals of π are all 9, 0 otherwise.

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

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

#### Kevin Buzzard (Mar 26 2021 at 10:05):

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

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

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

#### Kevin Buzzard (Mar 26 2021 at 10:07):

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

#### Belisarius Cawl (Mar 26 2021 at 10:08):

alright, understood. Thanks!

#### 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 :)

#### Belisarius Cawl (Mar 26 2021 at 10:11):

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

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

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

#### Scott Morrison (Mar 26 2021 at 10:36):

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

#### 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" ;)

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

#### Belisarius Cawl (Mar 26 2021 at 10:38):

(because fundamentalism has been disproven)

#### Belisarius Cawl (Mar 26 2021 at 10:39):

but yeah computability is definitely useful

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

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

#### 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 $\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 (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

#### 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?

#### Eric Wieser (Mar 26 2021 at 22:21):

You can't write the `if`

in that definition because that requires decidability too

#### Damiano Testa (Mar 26 2021 at 22:23):

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

#### Eric Wieser (Mar 26 2021 at 22:51):

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

#### 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`

.

#### Yury G. Kudryashov (Mar 26 2021 at 23:01):

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

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

#### 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 $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 (Mar 27 2021 at 00:45):

The reals are uncountable, the naturals are countable.

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

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

#### Greg Price (Mar 27 2021 at 00:50):

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

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

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

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

#### 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,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 (Mar 27 2021 at 05:08):

That makes a lot of sense, thanks!

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

#### Mario Carneiro (Mar 27 2021 at 06:18):

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

#### 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`

)!

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

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

#### 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:

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

#### Damiano Testa (Mar 27 2021 at 06:43):

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

#### Mario Carneiro (Mar 27 2021 at 06:44):

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

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

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