Handling potentially infinite loop?

Stream: lean4

[Josh]

As a beginner to Lean, I've seen that functions on natural numbers must be defined in a way that they do not infinitely recurse when given a finite input. I've vaguely come across some stuff about how Lean can do general programming as well. I was wondering then how an IO that performs "read a number from the console until it's less than 10" would be legal under Lean's constraints?

[Josh]

I assume that I'm missing some nuance of the actual requirements that makes this situation expressible.

[Josh]

Actually, not sure if this is the right place. I've mostly heard of general programming in conjunction with Lean 4, but does Lean 3 have similar general programming features?

[Johan Commelin]

@Josh Such "exceptions" to the rule of purity are handled by keywords such as meta

[Johan Commelin]

Which lift this "algorithms need to terminate" barrier from certain functions. But it acts like a "virus". If something is tagged meta, then everything that calls it also has to be meta.

[Mario Carneiro]

Both lean 3 and lean 4 have an io.forever primitive that is intended specifically for the use case of servers and the like, which runs an IO action in an infinite loop. This is without any use of meta. It can be justified in the case where the server takes at most finitely many steps between any external IO action like reading the next line of input; this is called "productivity" and you can formalize it using coinductive types

[Josh]

(deleted)

[Josh]

Is it then impossible to write a function computing the steps to reach 1 in the 3x+1 problem without using meta or IO given that no one has found a way to prove it always reaches 1?

[Kevin Buzzard]

What should such a function return given an input which turns out not ever to reach one? If you can answer that then I can write your function, it won't be meta, but it won't be computable either (at least in Lean 3), because it will have to branch on "exists n such that n'th iteration is 1" which is not a decidable statement.

[Josh]

Wouldn't you never be able to detect that case, since you would have to try infinite times before concluding that the number never reaches 1?

[Kevin Buzzard]

If you're coming from a CS background then you just write meta code and if I feed in my secret counterexample to the 3x+1 problem then your function doesn't terminate. With my noncomputable non-meta function I can reason about it, and if I were to formalise my proof that my secret counterexample is an actual counterexample then we'll be able to prove that my function returns the value which you want it to return on such inputs.

[Kevin Buzzard]

When I say "it's not decidable" I mean precisely what you just said

[Kevin Buzzard]

however mathematicians can sometimes prove theorems of the form "even though your naive approach goes into an infinite loop, this more mathematical approach proves your function goes into an infinite loop". That is what separates Lean from Haskell.

[Josh]

Ah, ok.
Let's say it returns an optional value with none if 1 can't be reached. What would the code for that roughly look like?

[Kevin Buzzard]

import tactic

/-- The function which applies one step of the 3x+1 problem. -/
def step (x : ℕ) := if x % 2 = 0 then x / 2 else 3 * x + 1

/-- The function which applies n steps of the 3x+1 problem.
Defined recursively. -/
def iterate_step (x : ℕ) : ℕ → ℕ
| 0 := x
| (n+1) := step (iterate_step n)

/-- The predicate which says iteration terminates in finite time. -/
def terminates (x : ℕ) := ∃ n : ℕ, iterate_step x n = 1

open_locale classical -- need to apply an "if" statement to an undecidable function

/-- The noncomputable function which returns how many iterations it takes
to get to 1. -/
noncomputable def termination_time (x : ℕ) : option ℕ :=
if h : terminates x then some (nat.find h) else none

(this is Lean 3, but it looks essentially the same in Lean 4)

[Kevin Buzzard]

I cannot run this function, but I can prove theorems about it. The meta version of the function I can run, but I cannot reason with.

[Kevin Buzzard]

theorem collatz (x : ℕ) : 0 < x → ∃ n, termination_time x = some n :=
begin
  -- solve this level of a puzzle game to become famous
  sorry
end

[Kevin Buzzard]

Note that just because I cannot run the function, it doesn't stop me proving theorems about the function, for example I could prove that termination_time 4 = some 2.

[Josh]

Huh, okay! If I understand correctly, you could call this function by giving a proof that there exists some number of iterations that reaches one, which due to Lean's constructive approach, requires finding exactly how many iterations that would take! And then you can reason about it by saying "if you can construct such a value..." without having to do any kind of infinite looping. That's really cool.
Also I like your comment lol.

[Kevin Buzzard]

theorem terminates_one : terminates 1 := ⟨0, rfl⟩
theorem terminates_one' : terminates 1 := ⟨3, rfl⟩ -- alternative proof
theorem terminates_two : terminates 2 := ⟨1, rfl⟩
theorem terminates_four : terminates 4 := ⟨2, rfl⟩

[Josh]

Thanks for your help!