Lean, unlike e.g. Haskell, makes you prove that recursive definitions of functions will eventually terminate, if the compiler can't do it by using structural recursion, by using decreasing_by or termination_by. Do there exist computable functions which can't be defined in Lean because of this restriction? In other words, are there total functions which are possible to define using the partial keyword but not possible without it?
$\begingroup$
$\endgroup$
0
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
4
Since Lean programs always terminate, it cannot be Turing-complete. In particular, one specific computable-but-not-Lean-computable problem is the problem of evaluating computable Lean expressions (i.e. given the representation of an expression of type nat, output the natural number corresponding to the evaluation of the expression).
You cannot write a Lean function that interprets Lean, assuming Lean is consistent, because then using standard diagonalization techniques (e.g. see the halting problem), we could write a Lean program that checks what it is supposed to output itself and outputs something different.
Another point of view: If you tried to write this program, you would eventually run into a termination_by goal that you couldn't prove. Proving this goal amounts to proving the consistency of Lean. By Godel's second incompleteness theorem, this is impossible.
This is not specific to Lean, but holds for any theorem prover under mild conditions.
-
1$\begingroup$ Your first sentence is slightly inaccurate. Simply-typed lambda calculus with intersection types contains exactly the strongly normalizing terms of untyped lambda calculus, and thus can decide any decidable set, thus is Turing complete. $\endgroup$– Trebor ♦Nov 14, 2022 at 7:01
-
2$\begingroup$ Of course, it is actually not very defined what "Turing complete" means for anything that is not a Turing machine. For these things we need to agree on an encoding beforehand, otherwise we can hide all the work in the encoding function and cheat. $\endgroup$– Trebor ♦Nov 14, 2022 at 7:09
-
$\begingroup$ @Trebor: I belive the exact statement is that a programming language with semidecidable set of valid expressions denoting only total functions $\mathbb{N} \to \mathbb{N}$ does not denote all of them. Which of these assumptions is broken by the $\lambda$-calculus with intersection types? I worry that $(\lambda x . x x)$ can be typed with intersection types. $\endgroup$ Nov 15, 2022 at 7:29
-
$\begingroup$ $\lambda x.xx : \sigma \cap (\sigma \to \tau) \to \tau$ can be typed alright. Intersection type breaks decidability (but I don't think it is not semidecidable: Given that the input is strongly normalizing the type is computable). $\endgroup$– Trebor ♦Nov 15, 2022 at 8:24
$\begingroup$
$\endgroup$
6
Yes. This is always going to be the case because of the halting problem: The set of functions accepted by lean is computable (because lean computes it), so if all halting functions are in the set then the halting problem is computable.
So we know there is a gap, but how big is it? One way to quantify this is to ask how fast the lean-definable functions from nat -> nat grow, by comparison to the busy beaver function which grows faster than every computable function. The answer is that the lean-definable functions grow according to the fast-growing hierarchy up to the proof-theoretic ordinal of ZFC with countably many universes, which is... really big. This is one of those stupendously large countable ordinals which defy all attempts to describe it.
As a result, constructing a counterexample is extremely difficult, other than the ones supplied already by the halting problem. A lean typechecker would be one such example: it is a computable function but lean cannot prove it always halts. On the flip side, this is one way to show that the worst-case asymptotic complexity of lean typechecking is stupendously large.
-
1$\begingroup$ The "idealized" Lean has undecidable type-checking, though, so the halting problem doesn't apply. Do we know if we can get more from this fact? $\endgroup$ Nov 14, 2022 at 7:34
-
$\begingroup$ Small nitpick: I think this is slightly closer to Rice’s theorem than the halting problem. A specialized version of Rice’s theorem states that the set of total computable functions (say from Nat to Nat) is not computable. (Of course all these results are connected and derivable from the others, and it isn’t clear what you mean by “all halting functions”.) $\endgroup$ Nov 14, 2022 at 12:12
-
$\begingroup$ @Pierre-MariePédrot Pick any sound Lean-like formal system which can prove certain functions are total. (For concreteness, consider functions from Nat to Nat, but this generalizes). This gives a computable enumeration of all provably total functions in your formal system. (If type checking loops, or times out depending on the specific formal system, then that code for that function will not be enumerated.) It is known that you cannot enumerate all total computable functions, so there must be some total functions which are not provably total in such a formal system. $\endgroup$ Nov 14, 2022 at 12:31
-
$\begingroup$ Edit: my last sentence should state there are “some total computable functions which are not provably total”. $\endgroup$ Nov 14, 2022 at 12:40
-
$\begingroup$ @JasonRute you're assuming that type-checking is RE for this, but is it really the case? (It seems reasonable to believe so, but maybe Idealized Lean is more powerful than I thought.) $\endgroup$ Nov 14, 2022 at 14:54
$\begingroup$
$\endgroup$
There are a few subtleties that should be clarified. Lean is both a theorem prover and a programming language. As a theorem prover, it is accepted in Lean to use the axiom of choice. If one uses the axiom of choice, then one can actually define every total computable function in Lean:
Prove there are countably many total computable functions and there is an enumeration of them. Then one can define nth_total_computable_function (n : Nat) : Nat -> Nat using the axiom of choice and define any particular total computable function via nth_total_computable_function.
Of course these definitions are not executable in Lean, and Lean won't let you run them. So you likely mean to ask about the functions which Lean marks as computable (which should be any function not defined using axioms, as well as some which use axioms, but only to prove propositions). For that, the other answers give you the basic flavor.
answered Nov 15, 2022 at 3:37