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.

[jsodd]

Is there a reason why I could want some of my definitions to be computable? I cannot come up with an example (within the context of proving theorems) where that could be useful.

[Eric Wieser]

Some possible reasons:

• You want to be able to quickly evaluate the definition with #eval to check it on small examples, without having to build a large library of lemmas first
• You actually want to write a program using the operations you just proved were correct (and perhaps don't care about their efficiency)
• You don't actually care about "computability", but the correlated concept of "kernel-reducibility". If your definition is kernel-reducible, then the decide tactic can often prove things about it for you.

[Kyle Miller]

noncomputable can serve as a proxy for "will this fail to be kernel reducible", but that's not what it's for, and there are both false positives and false negatives with that.

[Henrik Böving]

What do you mean by fail to be kernel reducible? Fail to reduce to a canonical term?

[Eric Wieser]

A nice example of that is Nat.sqrt:

import Mathlib

#eval ∀ n < 2, n ^ 2 < 16  -- true (computable)
example : ∀ n < 2, n ^ 2 < 16 := by decide -- succeeds (kernel-reducible)

#eval ∀ n < 2, n < Nat.sqrt 16 -- true (computable)
example : ∀ n < 2, n < Nat.sqrt 16 := by decide -- fails (not kernel-reducible)

[Eric Wieser]

@Kyle Miller, can you construct the converse: something non-computable but kernel-reducible?

[Kyle Miller]

@Henrik Böving One example is Eq.rec that depends on reducing types (pops up frequently from people defining Decidable instances using rw). It's perfectly fine as a computable algorithm, but fails to reduce.

[Kyle Miller]

@Eric Wieser I was thinking about for example having a let with a noncomputable value that's only used inside a proof, but here's another example:

noncomputable def n : Nat := Classical.choice inferInstance

noncomputable def m : Nat := n * 0

#reduce m
-- 0

[jsodd]

Are computability and decidability the same thing?

[Eric Wieser]

instance : Decidable P is a way of providing an algorithm to decide P, but nothing forces the algorithm you provide to be computable (if not, #eval fails) or kernel-reducible (if not, decide fails)

[Kyle Miller]

No @jsodd. Computability in the noncomputable sense is just whether the compiler is able to take your definition and translate it to C. Decidable is a framework for lifting individual terms of Prop to Bool.

[Kyle Miller]

They're related in that, hopefully, these Bool computations are computable in both the kernel reducibility and the noncomputable sense to support both decide and anyone who wants to use the proposition in if statements in programs. (And it's not actually Bool, but some proof-carrying version of Bool, but that's just a detail)

[jsodd]

So computability implies decidability, while for noncomputable we either prove decidability somehow or go classical?

[Kyle Miller]

It doesn't make sense to say computability implies decidability on the face of it. A particular expression describing a natural number can be turned into a computer program or not, but in what sense is a natural number decidable?

[jsodd]

Understood. But if we only speak of Prop? Then both concepts make sense, right?

[Eric Wieser]

A Prop is always computable, because it has no runtime representation

[Eric Wieser]

The computable operation is the conversion to Boo1, but that's not a Prop any more!

[Kyle Miller]

A proposition is decidable if there is a computable Bool-valued algorithm that evaluates to or reduces to true iff the proposition is true. It's not the proposition itself that's computable, but this auxiliary algorithm.

[jsodd]

Without any restrictions on how long this algorithm may run?

[jsodd]

I am trying to ask whether I'd need to supplement such algorithm with some kind of proof that it terminates within finite time to make something computable

[Kyle Miller]

If you're able to define the function at all in Lean, then it terminates (unless you opt out using partial, but partial definitions are not useful for math). Lots of times the "equation compiler" is able to construct the definition for you and fill in the necessary arguments, but sometimes you need a termination_by clause to help it out.

[Kyle Miller]

This part isn't about noncomputable — there are strong restrictions on what definitions can do to prevent paradoxes. (It ends up preventing you from writing Y combinators for example. You can use it to "construct" terms of any type by instead doing an infinite loop.)

[Kyle Miller]

In fact, you're allowed to have "computable" functions that never return:

partial def f (x : Nat) : Nat := f x + 1

but you can see that if you remove partial it's rejected.

[jsodd]

Okay, I understand it better now. Thank you very much! But getting back to my original question, what's the "guideline"? It feels as though there's little reason to even try making computable definitions, and the examples above suggest (to me) that the only benefit of keeping things computable (or kernel-reducible) is that sometimes lean can close some goals by computing the thing directly... This is not convincing enough

[jsodd]

Anyway, I understand that it all depends on the purposes for which one uses lean. I'm just trying to see what can be gained from computable definitions. If nothing except for direct computational proofs, then I can relax again :smile:

[Kyle Miller]

There are different opinions here, but I think that for most math it's not useful to worry about whether or not your definitions are noncomputable. It often causes difficulties for little (or no?) gain.

One big project is that for the last 2-3 years we've been switching from Fintype to Finite in a lot of theory in mathlib. The first has computational content, and the second doesn't. It saves needing to worry about properly handling DecidableEq and Fintype instances to avoid eq-but-not-defeq problems.

[jsodd]

Hmm... Should I use Finite then, if I don't care about computations in lean?

[Kyle Miller]

Yeah, though there's still some "impedance mismatch" when you're working with Finset, since a lot of that is in terms of Fintype.

[Eric Wieser]

One common example of where ignoring computability often makes things harder is when working with quotients: there is a temptation to use docs#Quotient.out to pick an arbitrary value under the quotient, and then work with that, but actually it often is less work in the long run to use the computable docs#Quotient.lift.

[Kyle Miller]

I think that example isn't about computability though, it's that it's "mathematically wrong" to use .out, since definitions are cleaner when you don't rely on choosing arbitrary representatives, instead relying on universal properties.

[Kyle Miller]

(Though being able to rely on the reduction rule for .lift is a nice benefit!)

[Eric Wieser]

I mention that example since most early run-ins with computability are around Exists.some and Quotient.out, and as a warning that "I don't care about computability" isn't always a sufficient reason to use these.