Absence of termination not detected with Id.run do

Stream: new members

[Sébastien Boisgérault]

Hi everyone!

I was pretty sure that Lean would blame me for not flagging the following function as partial but it doesn't.

def loop : Nat := Id.run do
  let mut n <- 0
  while true do
    n <- n + 1
  return n

Is there a simple explanation of why Lean "fails" to detect the absence of termination here?

Cheers!

Sébastien

[Aaron Liu]

You can include partial function inside other functions without having to mark the enclosing function as partial

[Sébastien Boisgérault]

Ah, interesting! Is there a way to detect all functions using partial functions then?

[Eric Wieser]

To elaborate on what Aaron said, while is always partial

[Robin Arnez]

#print opaques <your definition name> (import Batteries.Tactic.PrintOpaques) gives you a list of all opaque and partial definitions that a function depends on. Some of these might not be a opaque due to partial though (in particular e.g. IO operations) so if you want to know which of these are partials you can check whether <name>._unsafe_rec exists. Example:

import Batteries.Tactic.PrintOpaques

def loop : Nat := Id.run do
  let mut n <- 0
  while true do
    n <- n + 1
  return n

def testMe : IO Unit := do
  IO.println "hi"

/-- info: 'loop' depends on opaque or partial definitions: [Lean.Loop.forIn.loop] -/
#guard_msgs in
#print opaques loop

#print Lean.Loop.forIn.loop._unsafe_rec -- exists => is defined using `partial`

/-- info: 'testMe' depends on opaque or partial definitions: [IO.getStdout] -/
#guard_msgs in
#print opaques testMe

#print IO.getStdout._unsafe_rec -- doesn't exist => is opaque for other reasons

[Kyle Miller]

There's a tension between Lean as a system for mathematical reasoning and Lean as a programming language.

Currently while loops are mathematically opaque, but, when making executable code, the compiler will translate them into C that does the looping.

partial is a convenient way to create mathematically opaque definitions with a particular runtime specification. It doesn't really track whether functions terminate or not unfortunately.

Infinite loops in pure code are sort of an undefined behavior; the compiler is free to assume pure functions terminate, so for example the following #eval returns with 0.

def loop : Nat := Id.run do
  let mut n <- 0
  while true do
    n <- n + 1
  return n

def useloop : Nat :=
  let x := loop
  0

#eval useloop
-- 0

Interestingly, sometimes it's even possible to mathematically evaluate functions with while, provided they're sufficiently trivial:

def loop : Nat := Id.run do
  let mut n <- 0
  while true do
    n <- n + 1
  return n * 0

#reduce loop
-- 0

(The trick is that even though it looks like there's a data dependency, n * 0 is definitionally equal to 0, and then the whole thing can reduce to 0.)

[Sébastien Boisgérault]

Thanks all of you for your answers, that was very educational! :folded_hands: