Lean metatheory: what is the statement "f is noncomputable"?

Stream: general

[nrs]

I'm trying to find an adequate way to state whether or not a function or an operation is computable. Does anyone have suggestions?

[nrs]

Is it possible to state this internally in Lean?

[Eric Wieser]

Do not mean "not computable" in the CS sense, or noncomputable in the "does lean actually compile it" sense?

[nrs]

Eric Wieser said:

Do not mean "not computable" in the CS sense, or noncomputable in the "does lean actually compile it" sense?

I am not sure, do these two have any sort of relationship to one another?

[Eric Wieser]

Not really; neither is a subset of the other

[Siddhartha Gadgil]

Eric Wieser said:

Not really; neither is a subset of the other

If a function is not computable in the CS sense, shouldn't it have to be a noncomputable def in Lean?

[Max Nowak 🐉]

noncomputable is really a practical keyword. For example functions implemented directly using recursors need to be marked as noncomputable, even though recursors have a perfectly fine theoretical interpretation of computation. But using them directly leads to inefficient code being generated (so I've been told at least), hence the need to be marked as noncomputable.

[Eric Wieser]

Siddhartha Gadgil said:

If a function is not computable in the CS sense, shouldn't it have to be a noncomputable def in Lean?

No, see this thread

[Eric Wieser]

Max Nowak 🐉 said:

For example functions implemented directly using recursors need to be marked as noncomputable

Unless you use compile_inductive% first.

[Siddhartha Gadgil]

Eric Wieser said:

Siddhartha Gadgil said:

If a function is not computable in the CS sense, shouldn't it have to be a noncomputable def in Lean?

No, see this thread

I did not think of partial def. And if a regular def calls a partial def then it can be noncomputable. I understand now. Thanks.

[Max Nowak 🐉]

What does compile_inductive% do?

[Eric Wieser]

Makes the recursors computable

[Henrik Böving]

(Notably by accepting the badly generated code)

[Eric Wieser]

In some cases the generated code is optimal though, I think? Such as:

def unpack (u : ULift Nat) : Nat := u.rec id

Certainly it's non-optimal on types with more than one constructor.

[Henrik Böving]

Whats the IR thats generated by this?

[Henrik Böving]

But yeah this could be fine. Its generally an issue if actual recursion is involved

[Henrik Böving]

Its also a fixable issue by adding more optimizations

[Giacomo Stevanato]

Eric Wieser said:

Siddhartha Gadgil said:

If a function is not computable in the CS sense, shouldn't it have to be a noncomputable def in Lean?

No, see this thread

Doesn't this mean that either:

• there are functions marked not with noncomputable that will not actually be compiled by Lean (I feel like that noncomputable kinda lose its meaning then)
• haltingFunction compiles but at runtime behaves differently than what the haltingFunction_not_computable assumes (but wouldn't this be unsound?)

[Daniel Weber]

The runtime behavior is just running in an infinite loop

[Giacomo Stevanato]

Daniel Weber said:

The runtime behavior is just running in an infinite loop

Then why is it that haltingFunction is considered to be the halting function? To actually be the halting function it should not loop infinitely.

[Mario Carneiro]

Henrik Böving said:

Its also a fixable issue by adding more optimizations

I've generally found this issue to be overblown. Lean already switches to a partial call-by-need evaluation strategy for compiling casesOn, and it could do so for recOn too. It's really just adding a single additional case to handle recOn in the code generator, I looked into it maybe a year ago. But the code generator is frozen :shrug:

[Violeta Hernández]

I'm interested about the compile_inductive think, what exactly is the issue it solves?

[Violeta Hernández]

(maybe this should be a separate thread...)

[Mario Carneiro]

If you attempt to use T.rec directly in a definition, lean complains that it is noncomputable because the code generator doesn't know how to handle primitive recursors.

def foo : List Nat → Nat :=
  List.rec 0 (fun _ _ _ => 1)
-- code generator does not support recursor 'List.rec' yet, consider using 'match ... with' and/or structural recursion

Using the compile_inductive% command generates code for the recursors so that it works:

import Mathlib.Util.CompileInductive

def foo : List Nat → Nat :=
  List.rec 0 (fun _ _ _ => 1)

[Alex Meiburg]

What does the code generator handle then? I think of recursors as the "basic" terms from which all other functions are built. Like if statements are the recursor for Decidable, addition of nats is a recursor on nat...

Is it just a fixed list of operations which are supported?

[Mario Carneiro]

The code generator uses different primitive functions than the kernel. To the code generator, the primitive is casesOn and/or projections for getting data out and constructors for putting data in, plus unguarded recursion. In other words, the code generator thinks in terms of match and fix rather than recursors