McCarthy 91 function using partial_fixpoint

Stream: lean4

[Joachim Breitner]

@Bhavik Mehta asked me if the new partial_fixpoint feature can help to define the **McCarthy 91 function**, which is known to be a tricky case for termination proofs.

A naive definition like

def f91 (n : Nat) : Nat :=
  if n > 100
  then n - 10
  else f91 (f91 (n + 11))

does not work; lean is not able to prove termination of this functions.

Moreover, trying to use well-founded recursion with an explicit measure (e.g. termination_by 101 - n) is also doomed, because we’d have to prove something about the function we are defining (namely $f91 n = f91 101 = 91$ for $90 ≤ n ≤ 100$) and use that result in the termination proof. (The Wikipedia page spells the proof out.)

We can make well-founded recursion work if we change the signature and use a subtype on the result to prove the necessary properties while we are defining the function (Lean by Example shows how to do it), but for larger examples this can be hard or tedious.

With partial_fixpoint, we can define the function as a partial function without worrying about termination. This changes the type to return an Option Nat, using Option.none as the logical value for potential non-termination:

def f91 (n : Nat) : Option Nat :=
  if n > 100
    then pure (n - 10)
    else f91 (n + 11) >>= f91
partial_fixpoint

This function definition compiles and runs just fine:

/-- info: some 91 -/
#guard_msgs in
#eval f91 42

But the crucial question is: Can we prove anything about this? In particular, can we prove that this function is actually total?

Turns out we can. Since we have the f91 function defined, we can start proving auxillary theorems, using whatever induction schemes we need. In particular we can prove that f91 is total and always returns 91 for $n <= 100$:

theorem f91_spec_high (n : Nat) (h : 100 < n) : f91 n = some (n - 10) := by
  unfold f91; simp [*]

theorem f91_spec_low (n : Nat) (h₂ : n ≤ 100) : f91 n = some 91 := by
  unfold f91
  rw [if_neg (by omega)]
  by_cases n < 90
  · rw [f91_spec_low (n + 11) (by omega)]
    simp only [Option.bind_eq_bind, Option.some_bind]
    rw [f91_spec_low 91 (by omega)]
  · rw [f91_spec_high (n + 11) (by omega)]
    simp only [Nat.reduceSubDiff, Option.some_bind]
    by_cases h : n = 100
    · simp [f91, *]
    · exact f91_spec_low (n + 1) (by omega)

theorem f91_spec (n : Nat) : f91 n =  some (if n ≤ 100 then 91 else n - 10) := by
  by_cases h100 : n ≤ 100
  · simp [f91_spec_low, *]
  · simp [f91_spec_high, Nat.lt_of_not_le ‹_›, *]

-- Generic totality theorem
theorem f91_total (n : Nat) : (f91 n).isSome := by simp [f91_spec]

(Note that theorem f91_spec_low is itself recursive in a somewhat non-trivial way, but Lean can figure that out. Use termination_by? if you are curious.)

This is pretty good already!

But what if we want a function of type f91! (n : Nat) : Nat, without the Option? We can derive that from the partial variant, as that turned out to not be partial:

def f91! (n : Nat) : Nat  := (f91 n).get (f91_total n)

We can prove the original defining equation for that function. In order to do so, we need to add some lemmas about Option.get that (maybe) should be part of the standard library:

-- Generic setup for pushing `Option.get` inside

theorem Option.of_isSome_bind_left {o : Option α} {f : α → Option β} (h : (o >>= f).isSome) :
    o.isSome := by
  cases o <;> simp_all

theorem Option.of_isSome_bind_right {o : Option α} {f : α → Option β} (h : (o >>= f).isSome) :
    (f (o.get (Option.of_isSome_bind_left h))).isSome := by
  cases o <;> simp [h] at h |-

@[simp] theorem Option.get_bind (o : Option α) (f : α → Option β) (h : (o >>= f).isSome) :
    (o >>= f).get h = (f (o.get (Option.of_isSome_bind_left h))).get (Option.of_isSome_bind_right h) := by
  cases o <;> simp at h |-

With this setup, we can define the original equation for the f91 function:

def f91'_eq (n : Nat) : f91! n = if n > 100 then n - 10 else f91! (f91! (n + 11)) := by
  conv => lhs; unfold f91! f91
  split <;> simp [← f91!.eq_def, - Option.bind_eq_bind]

This “totalization“ construction could presumably be even automated – maybe one day.

[Markus Himmel]

Joachim Breitner said:

Maybe it's possible if we return a subtype that encodes some information about the result, but it won’t be pretty.

FWIW, Lean By Example contains a pretty short proof of termination using this approach:

def Mc91 (n : Nat) : Nat :=
  (M n).val
where
  M (n : Nat) : { m : Nat // m ≥ n - 10 } :=
    if h : n > 100 then
      ⟨n - 10, by omega⟩
    else
      have : n + 11 - 10 ≤ M (n + 11) := (M (n + 11)).property
      have lem : n - 10 ≤ M (M (n + 11)) := calc
        _ ≤ (n + 11) - 10 - 10 := by omega
        _ ≤ (M (n + 11)) - 10 := by omega
        _ ≤ M (M (n + 11)) := (M (M (n + 11)).val).property

      ⟨M (M (n + 11)), lem⟩
  termination_by 101 - n

Sadly, #check Mc91.M.induct runs for a while and then prints (deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached.

[Joachim Breitner]

Thanks for the pointer! I’ll update my choice of wording :-)

[Edward van de Meent]

Joachim Breitner said:

Moreover, trying to use well-founded recursion with an explicit measure (e.g. termination_by 101 - n) is also doomed, because we’d have to prove something about the function we are defining (namely $f91 n = f91 101 = 91$ for $90 ≤ n ≤ 100$) and use that result in the termination proof. (The Wikipedia page spells the proof out.)

It’s possible to combine the definition of the function with a proof of the properties we need for termination (see for example Lean by Example, but for larger examples this can be hard or tedious.

So which is it, is using an explicit measure doomed or not?

[Joachim Breitner]

I think it’s doomed without changing the function signature. If you use subtypes in the return type, it can work. I clarified, thanks!