Zulip Chat Archive

Stream: new members

Topic: Is it possible to implement infinite loop in lean?


Rui Liu (Dec 09 2020 at 16:31):

Is it possible to define such a function: def find_first_true: (N -> bool) -> N, which will find the first value of natural number that's true for a function?

Yakov Pechersky (Dec 09 2020 at 16:31):

docs#nat.find might be related

Mario Carneiro (Dec 09 2020 at 16:32):

This is nat.find, but note the precondition: it needs to be not always false!

Rui Liu (Dec 09 2020 at 16:33):

Is it possible that this call runs forever?

Mario Carneiro (Dec 09 2020 at 16:33):

all lean programs terminate

Mario Carneiro (Dec 09 2020 at 16:33):

halting problem solved :)

Rui Liu (Dec 09 2020 at 16:34):

so in lean, it's not possible to have infinite loop? lean cannot be used as general programming language?

Kevin Buzzard (Dec 09 2020 at 16:34):

you can write meta code and then it's just like Haskell

Kevin Buzzard (Dec 09 2020 at 16:35):

but if it's not meta, the kernel checks that it terminates

Mario Carneiro (Dec 09 2020 at 16:35):

there are caveats, of course. But for non-meta functions it would break the logic (make it inconsistent) to have nonterminating functions

Rui Liu (Dec 09 2020 at 16:36):

OK...

Mario Carneiro (Dec 09 2020 at 16:37):

consider that if you could write find_first_true in lean, you should be able to refine it to the signature \all f : N -> bool, {n | f n = tt}, and this is plainly false

Mario Carneiro (Dec 09 2020 at 16:39):

however if you don't care about computation or garbage values and just want a function with that signature, you can write

noncomputable def nat.maybe_find (f :   bool) :  :=
by classical; exact
if h :  n, f n = tt then nat.find h else 37

Last updated: Dec 20 2023 at 11:08 UTC