Explaining noncomputable

Stream: new members

[Max Bobbin]

I noticed that a couple of Lean defs have the tag noncomputable, and recently Lean has given me a warning that my def needs the noncomputable tag because it depends on a noncomputable def. Can you explain what is meant by noncomputable? I noticed, for example, real.has_pow is noncomputable. Is that because Lean can't calculate the expression like e^e the same as it could calculate 2^2 = 4?

[Riccardo Brasca]

It means that it is not computable even if in principle, for example because something depends on the axiom of choice

[Riccardo Brasca]

The definition of real numbers as equivalence classes of something for example is not computable (I think)

[Kevin Buzzard]

What does "calculate the expression e^e" mean?

[Riccardo Brasca]

So there is no algorithm to say if s given real number is equal to zero

[Max Bobbin]

Kevin Buzzard said:

What does "calculate the expression e^e" mean?

I meant, as an example, you can say in Lean

example : (2 : ℝ) + 2 = 4 := by norm_num

but there is no way of saying

example : (real.exp 1)^(real.exp 1) = ? := by norm_num

[Kevin Buzzard]

docs#real.has_pow

[Junyan Xu]

Apparently it's docs#complex.cpow (which underlies docs#real.has_pow) that invokes decidability of equality.

[Kevin Buzzard]

I guess you can see that it must be noncomputable because 0^0=1 and 0^y=0 if y isn't 0, so the even the function 0^x isn't computable.

[Riccardo Brasca]

The difference is that in 2+2 = 4 (as natural numbers) you can unfold everything and then you see that both sides become succ succ succ succ 0. For reals you can not just do that. norm_num is a smart tactic, so sometimes it can prove stuff even if they're not computable I think (using simp)

[Riccardo Brasca]

But 2+2=4 can be also proved by refl, unfolding the definitions

[Max Bobbin]

Yea, I was running into problems where norm_num just returned false, which made sense due to the type casting. Does noncomputable make the math any different, or is it more just a tag that Lean needs?

[Riccardo Brasca]

If you add noncomputable theory at the beginning the math becomes more "standard"

[Max Bobbin]

Ok, I will give that a try, thank you!

[Kyle Miller]

noncomputable is a way that Lean keeps track of which definitions should be compiled (by the VM compiler) into a more efficient representation (for the VM). You should more or less only care about whether or not a definition is noncomputable if you care about evaluating it using #eval or evaluating it from within the implementation of some tactic.

[Riccardo Brasca]

In mathlib it's useful to try to be computable when possibile to prove stupid stuff. For example I once spent literally hours proving that the finite set {1, 3, 5, 15} has four elements and then someone told me refl can do it. It can because everything is computable so we can say to Lean "just look"

[Kyle Miller]

@Riccardo Brasca That example's not the same kind of computability as what noncomputable is about

[Riccardo Brasca]

Ops, I am sorry

[Kyle Miller]

There are at least three ways Lean can compute something, I think. One is the elaborator doing expression reduction (which honors things like the reducible/semireducible/irreducible attributes), another is the Lean kernel itself doing expression reduction (which doesn't honor these -- everything is essentially reducible I believe), and the third is the VM after VM compilation (which is not guaranteed to evaluate things correctly, but it sure tries)

[Riccardo Brasca]

Oh sure, this about decidability! I must be still jetlagged

[Kyle Miller]

(My understanding is that the original Lean evaluator was just the expression reducer, and noncomputable was used to keep track of which definitions could actually reduce all the way. From what I remember, one of the reasons for the VM besides speed is that it gets around the fact that eq.rec terms don't always reduce.)

[Riccardo Brasca]

@Max Bobbin in any case you can safely ignore this warning if you want to do standard mathematics

[Kyle Miller]

Oh right, and a fourth type of "evaluation" is decidable via dec_trivial, where you use the typeclass system to search for a proof using whatever instances happen to lie around.

[Max Bobbin]

Ok, cool. Thank you. This is helpful, I think my problems are more type casting related then. I just wanted to make sure noncomputable wasn't the problem

[Kyle Miller]

I guess a fifth type is norm_num (and simp) which pretty much doesn't care about whether something is noncomputable since it just operates on the terms themselves and applies rules ("norm_num plugins"). It evaluates terms more in the Mathematica or Sage sense, symbolically.