Can we prove the Lean type checker is undecidable in lean?

Stream: lean4

[Eric Vergo]

Hey all,

While working on an unrelated project about Turing machines, I realized that Lean 4 may have all the pieces in place to do something cool: prove that the Lean 4 type checker is undecidable, using Lean 4.

The pieces:

• Lean 4 is bootstrapped, so the type checker exists as actual Lean code
• Mathlib contains core computability theorems, including Rice's theorem and the halting problem
• Type checking in Lean requires termination checking for recursive definitions, which is essentially the halting problem

Could we connect these pieces to formally prove that type checking Lean code is undecidable in general? Has anyone explored this direction before? Any thoughts on feasibility or which parts of the compiler would be most amenable to this approach?

[Henrik Böving]

The core type checker of Lean is written in C++. Though you might have some luck with Lean4lean

[Henrik Böving]

Also type checking in lean, at least for the core calculus, does not require termination checking, they are desugared long before the kernel checks the term, type checking is undecidable for other reasons

[Martin Dvořák]

@Mario Carneiro

[Mario Carneiro]

Type checking in lean is undecidable, but for the "wrong" reasons; very similar systems like Rocq have decidable type checking. The termination checker underapproximates the halting problem, which is to say there are some definitions which are terminating but the checker doesn't know how to prove it. When this happens, lean rejects your definition and requires you to prove it terminating. But once you've done that, the termination checking problem becomes easy, it's just regular proof checking and no infinite search is required because the proof is right there handed to you.

[Eric Vergo]

Thank you for the responses; this is very interesting! Is it fair to say that the reason you have to underapproximate the halting problem is because of implementation practicalities similar to recursion depth limits?

It seems like a few of my assumptions were incorrect, sorry. I’m still getting my feet wet with theoretical computer science and will spend some time checking out lean4lean.

[Kenny Lau]

Mario Carneiro said:

the termination checking problem becomes easy

From a document you sent me some time ago (I think it's called "ttt"?) it talked about how in a contradictory context one can make non-terminating functions when unfolded (e.g. recursing upwards on Nat). Does that have an impact here?

[Mario Carneiro]

Eric Vergo said:

Thank you for the responses; this is very interesting! Is it fair to say that the reason you have to underapproximate the halting problem is because of implementation practicalities similar to recursion depth limits?

No. It is the nature of any type system that it allows some underapproximation of semantic correctness. To take a simple example, using simply typed functions, the expression if true then "hi" else 1 : String will generally not be well typed, even though it is semantically correct. That's a tradeoff we make to make type checking not just practical but also easy for a user to predict so they can use the system effectively. In this case we would say that we are deliberately not considering the value of the condition when typechecking, so we can just say "one side is a String and the other is a Nat, that's not well typed" and the user can learn. The point is to get the user to write manifestly correct expressions.

When you increase the complexity of the type system you can typecheck more things that are semantically correct, so that's closing the gap a bit. With dependent types you can actually typecheck that if statement because it will have type if true then String else Nat and the system evaluates that expression to String. But the fundamental tradeoff is still unchanged. An example that would not be accepted is if RiemannHypothesis then "hi" else 1 : String, not just because we don't know how to prove riemann's hypothesis, but because the system won't even try to prove it in this situation - it doesn't compute to true and that's reason enough to reject it.

So to come back to the original question, this underapproximation is really a fundamental property of decidable type systems, and has nothing to do with implementation limits.

[Mario Carneiro]

Kenny Lau said:

Mario Carneiro said:

the termination checking problem becomes easy

From a document you sent me some time ago (I think it's called "ttt"?) it talked about how in a contradictory context one can make non-terminating functions when unfolded (e.g. recursing upwards on Nat). Does that have an impact here?

(You are thinking of #leantt.) This is what I am referring to with

Type checking in lean is undecidable, but for the "wrong" reasons

and Henrik's

type checking is undecidable for other reasons

Most of my post would apply (and indeed it's easier to make the point) if Lean's type theory was decidable.

But to the OP question as stated, this "technicality" is actually very relevant.

Could we connect these pieces to formally prove that type checking Lean code is undecidable in general?

Yes we can: the construction in #leantt is not too hard to formalize, the hard part would be proving formally that you can embed decidable programs like turing machine evaluation for k steps in the definitional equality relation. My paper kind of handwaves that part (in true CS fashion); you would have to connect it up to Mathlib.Computability.HaltingProblem and show that primitive recursive function evaluation works as expected. There might also be more handwaving to show that in the non-halting case the definitional equality doesn't hold, because that requires you to know that the definitional equality relation is not degenerate and this is a very hard theorem.

[Eric Vergo]

Mario Carneiro said:

No. It is the nature of any type system that it allows some underapproximation of semantic correctness ... The point is to get the user to write manifestly correct expressions.

Wow, I was unaware of this subtlety and am not sure I have my head totally wrapped around it. Do you know where I might be able to read more about this specifically?

Mario Carneiro said:

Yes we can: the construction in #leantt is not too hard to formalize, the hard part would be proving formally that you can embed decidable programs like turing machine evaluation for k steps in the definitional equality relation. My paper kind of handwaves that part (in true CS fashion); you would have to connect it up to Mathlib.Computability.HaltingProblem and show that primitive recursive function evaluation works as expected. There might also be more handwaving to show that in the non-halting case the definitional equality doesn't hold, because that requires you to know that the definitional equality relation is not degenerate and this is a very hard theorem.

Cool. It's over my head but I'm going to take a crack at. Is it ok if I come back with some naive attempts and questions?