Church-Turing thesis for Lean computability

Stream: new members

[Stepan Nesterov]

Let us call a function $f : \mathbb{N} \to \mathbb{N}$ computable in Lean, if there exists some compiling Lean code which I can put after

def f : Nat -> Nat :=

Without having to say noncomputable def, such that for any natural number n, f n equals to the right number by rfl.
I apologize for the imprecision of this definition. I’m not an expert in logic, so there might be some subtleties which I’m missing. For example, I do not want to talk about whether we can prove in Lean whether two functions f and g are actually equal, just that for some set-theoretic function there exists a Lean code computing it in some platonic sense.
My questions about this notion are:
1) Is it true that every function computable in Lean is a total recursive function?
2) Is it possible in principle to write a meta program which will automatically deduce that f is recursive from the fact that its definition is computable?

[Aaron Liu]

Stepan Nesterov said:

such that for any natural number n, f n equals to the right number by rfl.

This part seems like it could be problematic, since how do you determine what is the "right" number and also it's not possible to check statements about "any natural number n" in a finite amount of time

[Stepan Nesterov]

Ok let me try to explain how I would imagine a more precise definition would go.
I assume (but do not know a precise reference in the literature for) that there is a notion of a set-theoretic model of Lean, which is a tuple $\mathfrak{M}=(\mathrm{Type}_{\mathfrak{M}}, \mathrm{Term}_{\mathfrak{M}}, :_{\mathfrak{M}}, \equiv_{\mathfrak{M}}, \ldots)$ consisting of a set of terms, a set of types, a typing relation, a definitional equality relation, and some maps corresponding to constructing dependent product types, inductive types, quot types, function applications, abstractions, recursors, and quot makers.
For any model $\mathfrak{M}$ of Lean, there exists a distingushed element $\mathrm{Nat}_{\mathfrak{M}}$ -- the naturals of $\mathfrak{M}$, with two distinguished terms $\mathrm{zero}_{\mathfrak{M}} :_{\mathfrak{M}} \mathrm{Nat}_{\mathfrak{M}}$ and $\mathrm{succ}_{\mathfrak{M}} :_{\mathfrak{M}} \mathrm{Nat}_{\mathfrak{M}} \to_{\mathfrak{M}} \mathrm{Nat}_{\mathfrak{M}}$. This allows us to construct an embedding from $\mathbb{N}$ to the set of terms of type $\mathrm{Nat}_{\mathfrak{M}}$, the image of which I will call standard naturals.
Now, for any computable (which I assume means "does not have Classical.choice anywhere") term $F \in \mathrm{Term}_{\mathfrak{M}}$ of type $\mathrm{Nat}_{\mathfrak{M}} \to_{\mathfrak{M}} \mathrm{Nat}_{\mathfrak{M}}$. I can construct by application a function from the set of terms of type $\mathrm{Nat}_{\mathfrak{M}}$ to itself. Then one can ask the following questions:
a) Is it true that for any $F$ as above, the corresponding function preserves the set of standard naturals?
b) Let $F$ be a computable Lean term of type $\mathrm{Nat} \to \mathrm{Nat}$, such that for any model of Lean, the corresponding function preserves the set of standard naturals. Is it true that the restriction of $F$ to the set of standard naturals is independent of the model?
c) Let $F$ be a computable Lean term of type $\mathrm{Nat} \to \mathrm{Nat}$, such that for any model of Lean, the corresponding function preserves the set of standard naturals, and the restriction to standard naturals is independent of the model. Is it true that this restriction is a total recursive function?

[Aaron Liu]

Stepan Nesterov said:

a) Is it true that for any $F$ as above, the corresponding function preserves the set of standard naturals?

I'm assuming you mean up to definitional equality? (the answer is no)

[Aaron Liu]

This is assuming you're allowed axioms docs#propext and docs#Quot.sound even though choice is banned

[Stepan Nesterov]

Aaron Liu said:

This is assuming you're allowed axioms docs#propext and docs#Quot.sound even though choice is banned

Can I use these axioms without having to mark the definition as noncomputable?

[Aaron Liu]

yes

[Stepan Nesterov]

Aaron Liu said:

Stepan Nesterov said:

a) Is it true that for any $F$ as above, the corresponding function preserves the set of standard naturals?

I'm assuming you mean up to definitional equality? (the answer is no)

So my assumption was that when I write computable definitions in Lean, then I really write a program and when I try to use rfl, Lean runs this program and see whether the results are the same. Like that’s how 2+2=4 ends up being rfl

[Aaron Liu]

you can also use docs#Classical.choice without having to mark it noncomputable

[Stepan Nesterov]

If my assumption is false, and the answer to a) is false, I’m happy to relax to propositional equality

[Aaron Liu]

it does become some sort of program

[Aaron Liu]

and you can still #eval it and get a number

[Aaron Liu]

but defeq gets stuck sometimes

[Stepan Nesterov]

Here is one issue that I assume arises:
If $f$ is a total recursive function which is not provably total in Lean, is it possible that I can computably define such an $f$?

[Stepan Nesterov]

I would assume no

[Aaron Liu]

probably not

[Stepan Nesterov]

But if yes, then my questions do kind of break down

[Aaron Liu]

since defining it would amount to a proof that it's total

[Stepan Nesterov]

But then I really asked for a blanket statement of the type “is every computably definable function recursive”

[Stepan Nesterov]

That could still be true

[Aaron Liu]

well I don't see why not

[Stepan Nesterov]

But you are saying that if the program is sufficiently complicated, then rfl just gives up and doesn’t reduce the term fully?

[Aaron Liu]

well it does do that sometimes but that's not what I'm saying

[Henrik Böving]

noncomputable has no theoretically relevant meaning, it just tells the compiler not to generate code for your function, either because you don't want to or because it can't for whatever reason. These reasons can be manifold and also arbitrary limitations of the current algorithm.

[Niels Voss]

Related thread: #maths > (Partial) Church's thesis. This thread seems to imply that the answer to your question 1) is no and 2) is yes for some large subset of the definable functions (although no one has actually implemented such a metaprogram).

[Aaron Liu]

here we are

def f : Nat → Nat := fun n =>
  @Eq.rec (@Quot Nat fun _ _ => True)
    (@Quot.mk Nat (fun _ _ => True) Nat.zero)
    (fun _ _ => Nat) n
    (@Quot.mk Nat (fun _ _ => True) n)
    (@Quot.sound Nat (fun _ _ => True) Nat.zero n True.intro)

example : f 0 = 0 := by rfl -- works
example : f 1 = 1 := by rfl -- fails

#eval f 0 -- 0
#eval f 1 -- 1

#reduce f 0 -- 0
#reduce f 1 -- ⋯ ▸ 1

[Niels Voss]

If $f$ is a total recursive function which is not provably total in Lean, is it possible that I can computably define such an $f$?

Not sure if this is what you are asking, but you might be interested in https://proofassistants.stackexchange.com/q/1840/6046

[James E Hanson]

Stepan Nesterov said:

If $f$ is a total recursive function which is not provably total in Lean, is it possible that I can computably define such an $f$?

What do you mean by 'computably define'?

[James E Hanson]

The standard way to do something like this would be to write w program that enumerates all of the functions from $\mathbb{N}$ to $\mathbb{N}$ that Lean proves are total and then diagonalize against them.

[Stepan Nesterov]

James E Hanson said:

Stepan Nesterov said:

If $f$ is a total recursive function which is not provably total in Lean, is it possible that I can computably define such an $f$?

What do you mean by 'computably define'?

being able to write some code
def f : Nat -> Nat := ...
without having to mark it as "noncomputable"

[James E Hanson]

You wouldn't be able to do this within Lean itself, no.

[James E Hanson]

You should, however, be able to do it in Lean together with an axiom asserting that Lean is arithmetically sound.

[James E Hanson]

James E Hanson said:

You wouldn't be able to do this within Lean itself, no.

Well okay, this depends on what you mean by certain words.

[James E Hanson]

You can write two computer programs A and B which compute the same function from $\mathbb{N}$ to $\mathbb{N}$ such that Lean proves A computes a total function but Lean does not prove B computes a total function.

[James E Hanson]

I'm not sure if that's the kind of thing you're looking for.

[Stepan Nesterov]

All of these are subtleties which I'm really trying to avoid for the purposes of my main question:
is it possible in principle to write a metaprogram which proves automatically that any function from $\mathbb{N} \to \mathbb{N}$ whose definition does not involve the axiom of choice is recursive?

[James E Hanson]

What do you mean by 'doesn't involve the axiom of choice'? Do you mean 'is definable in Lean without Classical.choice?

[Stepan Nesterov]

James E Hanson said:

What do you mean by 'doesn't involve the axiom of choice'? Do you mean 'is definable in Lean without Classical.choice?

Something like that yes

[James E Hanson]

And what do you mean by your metaprogram 'proving' that these things are are recursive?

[Stepan Nesterov]

Are there other things that trigger the error message "consider marking the definition is noncomputable", besides using choice?

[James E Hanson]

Are you saying you want a program that takes a Lean definition of a function and produces a Lean proof that that function agrees with some specific Turing machine?

[Stepan Nesterov]

James E Hanson said:

Are you saying you want a program that takes a Lean definition of a function and produces a Lean proof that that function agrees with some specific Turing machine?

Yes

[James E Hanson]

Ah okay. The core theory of Lean is a fairly basic constructive type theory, so this should be possible by a pretty standard realizability argument.

[Stepan Nesterov]

Aaron Liu said:

This is assuming you're allowed axioms docs#propext and docs#Quot.sound even though choice is banned

So is it true that propext and Quot.sound might break recursiveness in some way or are they subsumed by a realizability argument?

[James E Hanson]

I do not think those will keep these functions from being computable.

[James E Hanson]

There's a more direct argument for this but basically my thinking is that the standard construction of a model of MLTT/CIC with universes in IZF + universes will cover Lean with propositional extensionality and the quotient soundness axiom.

[James E Hanson]

And then IZF + universes has a realizer interpretation.

[James E Hanson]

And at the level of finitely many universes, this should all be internalizable in Lean.

[James E Hanson]

Again though, that's not going to be the right way to actually write such a program.

[James E Hanson]

That's just an argument that it should be possible.

[Stepan Nesterov]

How do universes affect which functions are definable in Lean?

[Stepan Nesterov]

I mean functions from $\mathbb{N}$ to $\mathbb{N}$ specifically

[James E Hanson]

Well each universe increases the consistency strength of Lean considerably and leads to more provably total computable functions.

[James E Hanson]

Basically, Lean with $n+1$ universes can take the list of computable functions that Lean with $n$ universes can prove are total and uniformly prove that they're all computable.

[Stepan Nesterov]

So is it true that a function is definable in Lean using
def f : Nat -> Nat := ...
iff it is recursive and provably total in Lean?

[James E Hanson]

There might be a slight subtlety with Markov's principle. I'm not completely sure, but this is probably true.

[James E Hanson]

Well okay, regarding Markov's principle, it's going to depend on what you mean by 'provably total', I guess. But with the strongest interpretation of that, the answer is going to be yes.

[Stepan Nesterov]

Ok then this answers my questions in the strongest possible form :+1:

[James E Hanson]

The strongest interpretation being the most direct: We say that Lean proves that the program A is total if it proves that for every n : Nat, there is a stage s : Nat at which A halts on input n.

[Stepan Nesterov]

James E Hanson said:

Well okay, regarding Markov's principle, it's going to depend on what you mean by 'provably total', I guess. But with the strongest interpretation of that, the answer is going to be yes.

I want to say $f : \mathbb{N} \to \mathbb{N}$ is provably total if there exists an $e \in \mathbb{N}$ such that $U_e$ computes $f$ and Lean proves that $\forall n \in \mathbb{N}, U_e(n) \downarrow$

[James E Hanson]

Yes that's basically what I'm saying.

[Jean Abou Samra]

@Stepan Nesterov Regarding your second message in this thread: you really have two questions there, the first being "will a Lean term ℕ → ℕ applied to a numeral compute to a numeral, perhaps up to propositional equality", and the other is "is every Lean-definable function $ℕ → ℕ$" computable. IUUC, you're trying to use a positive answer to the first question in other to define what it even means to be Lean-definable for the second question to make sense, by saying that $f : ℕ → ℕ$ is Lean-definable when there exists a Lean term f_impl : ℕ → ℕ such that f_impl applied to a numeral $⌈n⌉$ (i.e., succ (succ (... zero )) with $n$ applications of succ) is the numeral $⌈f(n)⌉$ up to either definitional or propositional equality. But you don't need this. You can just interpret a Lean term of type ℕ → ℕ into the standard model (aka set model or metacircular interpretation) of type theory and that gives you a bonafide function $ℕ → ℕ$.

So you can say that $f : ℕ → ℕ$ is Lean-definable-without-choice iff there exists a Lean term f_impl : ℕ → ℕ not containing Classical.choice whose interpretation in the standard model is $f$. And then it's indeed true, by standard realizability arguments, that if $f$ is Lean-definable-without-choice then it is computable, and the proof of this is constructive so from a Lean term ℕ → ℕ without choice you can compute a Turing machine that computes the associated function $ℕ → ℕ$.

[Jean Abou Samra]

However, I do not see that it easily follows that for every Lean-without-choice term f_impl : ℕ → ℕ, calling $f : ℕ → ℕ$ the associated function, there is a Turing machine $U$ such that Lean-without-choice proves that ∀ n, turing_machine_halts_on_input_and_returns_output U n (f n) (this is what I understand from what you're saying about a "meta program"). In other words, @James E Hanson I don't see how you get "And at the level of finitely many universes, this should all be internalizable in Lean" (unless I misunderstood what you mean by that).

[Jean Abou Samra]

(It is a statement of the same flavor as propositional canonicity, which would be "every closed term of type ℕ in Lean-without-choice is propositionally equal to a numeral" (although I don't actually see how to deduce propositional canonicity from your statement). Both have the form "for every internal thing, there is a concrete external thing and an internal proof that they agree". And propositional canonicity is hard to prove in general.)

[James E Hanson]

Jean Abou Samra said:

However, I do not see that it easily follows that for every Lean-without-choice term f_impl : ℕ → ℕ, calling $f : ℕ → ℕ$ the associated function, there is a Turing machine $U$ such that Lean-without-choice proves that ∀ n, turing_machine_halts_on_input_and_returns_output U n (f n) (this is what I understand from what you're saying about a "meta program"). In other words, James E Hanson I don't see how you get "And at the level of finitely many universes, this should all be internalizable in Lean" (unless I misunderstood what you mean by that).

It depends on what you mean by 'internalizable in Lean'. There is no function you can define from $\mathbb{N} \to \mathbb{N}$ to $\mathbb{N}$ that will give you a Turing index of a program that computes a given function from $\mathbb{N}$ to $\mathbb{N}$, but for a fixed universe level u you should be able to write a function that takes a syntactic representation of a term t that only uses universes up to u and produces the corresponding actual term t, a Turing index e, and a proof that the function computed by e is equal to t.