1
$\begingroup$

I've heard that proof assistants like lean4 can formalize all the usual math.

I'm interested to see how they formalize the complexity estimates of algorithms, since they are not often discussed formally.

As a concrete example, can you give me an example of proving an upper bound on the computation time of Euclid's algorithm in lean4?


UPDATE: For example, the gcd function is defined to be recursive, but can we evaluate the number of recursive calls T when gcd a b is executed in terms of a and b, in Lean4?

Lean4 guarantees that Euclid's algorithm always stops at a finite number of times. Then I thought you might be able to estimate how many calls it would take to stop.

$\endgroup$
3
  • 1
    $\begingroup$ Does this answer your question? can proof assistants reason about complexity of programs? $\endgroup$
    – Jason Rute
    Aug 25, 2023 at 12:23
  • 1
    $\begingroup$ Thank you. I have read that question and I still have a question: $\endgroup$
    – Kitamado
    Aug 25, 2023 at 14:41
  • 2
    $\begingroup$ @Kitamado It would be great if you Edit your post to reflect that, instead of asking additional questions in comments. It helps other users of this site understand the question more quickly. $\endgroup$
    – Trebor
    Aug 29, 2023 at 9:30

1 Answer 1

3
$\begingroup$

One has to be careful. In Lean you can't naturally prove the that a specific implementation of gcd (say using Euclid's algorithm) is O(a+b) (or whatever it is). The quick reason is that using functional extensionality, Lean thinks all computations of gcd are the same. (And even without functional extensionality, beta reduction, would make enough versions of gcd the same to reduce any meaningful analysis.)

Instead, what you can do is either:

  1. Give a formal definition of best case complexity of a function from Nat -> Nat and then prove that the gcd function has a certain best case complexity.
  2. Model the semantics of a specific programming language (say x86 bytecode) in Lean and show under that for a certain piece of code (say a compiled version of Lean's gcd function) the complexity is such and such.
  3. (Update) You can instrument your function to keep track of information like the number of recursive calls, the number of basic arithmetic operations (like addition or multiplication operations), etc. Then you can use Lean to prove a bound on that number. I think you would have to modify your function explicitly and can't do it with an existing non-instrumented function, but you could make the instrumentation light weight with good engineering. If this interests you, maybe look into the thesis mentioned in this PA SE answer: https://proofassistants.stackexchange.com/a/2016/122 (Not Lean 4, but the ideas likely transfer.)

Neither of these approaches have been implemented yet in Lean as I'm aware. It is quite difficult.

See this question for more details and links: can proof assistants reason about complexity of programs?


Update: Here is an example of one possible way (of many) to do option (3) for Euclid's algorithm. I include a fuel parameter into the definition of gcd which counts down. If it gets to the answer before fuel is zero, then it returns a result (wrapped in an Option), else it returns none. One can formalize any upper bound on the the gcd calculation. Here I stub the theorems (without a proof) for two upper bounds I found on wikipedia. Note this just counts the recursive calls, which is also the number of mod operations. To measure the actual runtime, one needs to know the complexity of mod. (In Lean, % is defined mathematically with a horribly inefficient algorithm, but when run with #eval or when compiled, then it replaced with efficient C code.)

def gcd : (a : Nat) -> (b : Nat) -> (fuel : Nat) -> Option Nat
| _, _, 0 => none -- out of fuel
| a, 0, _ => some a
| a, b, (fuel+1) => gcd b (a % b) fuel

/--Reynaud's first runtime bound on the number of steps in Euclid's algorithm.--/
theorem gcd_runtime_bound_Reynaud
  (a b fuel : Nat)
  (h : b < fuel)
  : (gcd a b fuel).isSome :=
  -- The details are left as an exercise to the reader,
  -- but should be similar to other proofs about
  -- Euclid's algorithm using strong induction.
  sorry

/--Fink's runtime bound on the number of steps in Euclid's algorithm.--/
theorem gcd_runtime_bound_Fink
  (a b fuel : Nat)
  (h : 2 * Nat.log2 v + 1 < fuel)
  : (gcd a b fuel).isSome :=
  sorry
$\endgroup$
10
  • $\begingroup$ I think the general SE policy is to avoid answering questions you think should be closed (low-quality, duplicate, etc.) $\endgroup$
    – Trebor
    Aug 25, 2023 at 13:05
  • 1
    $\begingroup$ Yeah, I didn't really know how to handle this best. It think the answers in that other question better give a complete picture. While this question (which I don't think is low quality) is mostly a duplicate, I wanted to address anything that is more specific to their question about Lean or gcd. I view my answer as a long winded comment. :) (But maybe that means it isn't a true duplicate then.) $\endgroup$
    – Jason Rute
    Aug 25, 2023 at 13:11
  • $\begingroup$ Yeah, I meant low-quality or duplicate. I think it is best to wait for either a confirmation that the question is duplicate, or a clarification of exactly what part of the question is different, before writing an answer. That way we can avoid having information scattered over multiple question, as well as give more specific and helpful answers. $\endgroup$
    – Trebor
    Aug 25, 2023 at 13:39
  • $\begingroup$ For example, the gcd function is defined to be recursive, but can we evaluate the number of recursive calls T when gcd a b is executed in terms of a and b, in Lean4? $\endgroup$
    – Kitamado
    Aug 25, 2023 at 14:29
  • 1
    $\begingroup$ @Kitamado I added an example of how to do what you want in Lean 4 to my answer. $\endgroup$
    – Jason Rute
    Aug 26, 2023 at 4:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.