Existence of a TM (or other) for computable lean functions

Stream: Is there code for X?

[Andrew Carter]

Is it possible to make use of the fact the a definition is computable in lean somehow? Like can we say this definition is computable therefore there is Turing Machine (or otherwise) that models the lean function? I'll admit I'm not 100% sure what this question even means to a certain extent - since the keyword is actually the inverse i.e. "noncomputable" whereas things like "decidable" are actually built using lean primitives rather than as a keyword. But I'd imagine I'd be thinking of something like:

instance inhabited_tm2_computable {α β: Type*} (f: α → β) [fc: computable f] (αen) (βen):
  inhabited (turing.tm2_computable αen βen f) :=
sorry

where computable would be a typeclass that indicates f is computable as far as lean is concerned (and probably comes bundled with some fin_encoding on its input and output in some way - rather than picking any such existence).

Does something like this even make sense in lean as a statement? If so, how might one approach it?

[Kyle Miller]

"Lean computable" means that Lean's able to take the definition and evaluate it using it's VM (though without any guarantee that this evaluation is in any way correct). It does this by way of a compiler that creates some bytecode representation. It would be cool if there were a certified compiler and a formal model of the VM, along with something that automatically creates a computable instance with the compiled bytecode and a proof that it correctly computes the function.

This doesn't exist, but it seems plausible.

[Andrew Carter]

Is it possible to access that bytecode representation within the lean language itself?

[Andrew Carter]

And can you access whether a function is computable through the proof language in anyway (outside of the noncomputable keyword)

[Kyle Miller]

No, noncomputable is a metatheoretic concept. It would take something like having Lean define a computable instance for you to get access to that something is computable.

[Kyle Miller]

The bytecode representation is available to meta code I believe. At least it's available to the C++ side of things, and it could be made available to the Lean side if it's not already.

[Andrew Carter]

Would one be able to define a computable type class that has a lean representation of the byte code, and then use something like derive to generate it, or would I have to generate them on a case by case basis with a tactic?

[Kyle Miller]

I'm not sure really what having the bytecode would help you do, since the VM compiler isn't formally verified.

[Andrew Carter]

Oh, so the byte code doesn’t come with a correctness proof?

[Kyle Miller]

No, not at all, that's what I meant in my first message's first sentence.

[Kyle Miller]

Given your turing machine question, I think what you'd need is your own formally verified compiler to some formal evaluation model, then use attributes or something to get your compiler to generate these computable instances for you.

[Kyle Miller]

It would be really cool if someone did this -- it seems like a lot of work though!

[Andrew Carter]

Yeah, I was hoping there was already something so I could leverage it for complexity, which is even more work…
So if I’m understanding your suggested direction, we would create a new @computable attribute, and in theory this attribute could be applied to any non-noncomputable function. But if you needed it, then you would have to derive it (or use a tactic) for each function?

[Kyle Miller]

Attributes are sort of weird in Lean is that they both act as tags but also as a hook to execute any code you want for metaprogramming purposes. I was thinking computable could be how you say "I believe this is computable, so derive a computable instance for me"

[Kyle Miller]

(For example, you could define a decidable attribute for Prop-valued functions that would try to derive a decidable instance for them.)

[Andrew Carter]

Ok, i think I understand (@simp complains sometime so I think I’ve seen that behavior, although does a decidable attribute already exist, I don’t think I’ve seen it used). But the end result might be that slowly all computable functions in mathlib get marked with this attribute as we want them in computability/complexity theory?

[Kyle Miller]

There's no decidable attribute yet, but it might be helpful if there were one.

Some complicated metaprograms that use attributes as their hook are simps and to_additive.

[Andrew Carter]

Ok, I’ll chew on that then

[Kyle Miller]

And regarding whether to mark everything with the attribute, I suppose so, but I imagine you wouldn't need to tag every computable function. (Potentially also the compiler could recursively create instances whenever it reaches a definition it hasn't compiled yet.)

[Kyle Miller]

It looks like you're using Lean 3, but this will all be easier if you're using Lean 4 (though to be clear, this project seems difficult :smile:)

[Kyle Miller]

I imagine others have already thought about how to do this in the dependent type theory world, and I've heard it go under the name "program extraction," if you want to look to see if there are any provably correct systems.

[Andrew Carter]

Okay, I’ll take a look, lean 3 had a lot more stuff already proved, but I’ve set up stuff in both, and it sounds like there isn’t much existing work.

Even if I don’t complete anything on the complexity side, hopefully I’d be able to move the ball forward a little bit

[Kyle Miller]

For complexity theory, there's also the question of being able to choose different cost models, which might be difficult when what you have is a general Lean compiler. Maybe it's better to have a mini-language that's not quite so dependently typed in which it's easy to write the sorts of programs you want to analyze, and with which it's easy to specify the model of computation? This mini-language could be represented using some inductive type along with some Lean 4 macros to make it convenient to write programs.

[Andrew Carter]

Yeah, I've played around with that using costed monads as sort of DSL, but then you either have to pay close attention to the implementation (which kind of defeats the purpose of using a theorem prover) or prove that the DSL has the same properties as a similar lean function with the same properties (which kind of defeats the purpose of the DSL in my opinion). I have mini-languages which are essentially models of computation (for example untyped lambda-calculus or turing machines ora novel ram-like model that uses hierarchical memory instead of a flat memory structure), but it'd be nice if the proof writer could avoid ever having to write any code in that underlying model IMO. Certainly on the complexity side the choice of model is very important, but on the computable side it shouldn't be important for the turing-complete class.

[Reid Barton]

Yes for computability this is something that doesn't exist yet in Lean, but people more or less understand how to do.

[Reid Barton]

For complexity it seems a lot harder. I find it hard to even imagine what the system would do and how the user would interact with it.

[Reid Barton]

In an algorithms paper you have to write proofs that the algorithms run in the stated complexity class, but you don't have to write proofs that the functions they compute are computable. So they are already different kinds of tasks.

[Andrew Carter]

Reid Barton said:

For complexity it seems a lot harder. I find it hard to even imagine what the system would do and how the user would interact with it.

So there is another thread in General with an ongoing conversation, but what I'm converging to is to have a model with referentially transparent constant time composition (this unfortunately throws a wrench in TMs, but lambda calculus and RAM-like models should both support this), and then lean can automatically generate a trace from a definition - based on this conversation maybe using attributes/hooks. This trace would include all calls it makes as well as all recursive usages, so for example inside of list.split it is plain to humans that if the input list matches to list.nil then it makes no calls, and if it pattern matches to (a::l) then it makes a recursive call with l. Assuming any function takes constant time locally, it would be relatively straightforward to show inductively that list.split is O(l.length).

Currently this is captured with
https://github.com/calcu16/lean_complexity/blob/main/src/hmem/encoding/list.lean

def split_trace
  (μ: Type*) [decidable_eq μ] [has_zero μ] [has_one μ] [ne_zero (1:μ)]
  {α: Type*} [complexity.has_encoding (runtime_model μ) α]: list α → hmem.trace μ
| [] := ⟨ encode (@list.nil α, @list.nil α), [tt], 2, [], [] ⟩
| (x::xs) := ⟨ encode (list.split (x::xs)), [ff], 4, [], [encode xs] ⟩

theorem split_has_trace {α: Type*} [complexity.has_encoding (runtime_model μ) α] (l : list α):
  (split μ).has_trace (encode l) (split_trace μ l) := ...

I intend to abstract this further, such that rather than dealing with the encoded values, the user would be able to interact with the lean types directly instead.

I leverage this trace to prove complexity here:
https://github.com/calcu16/lean_complexity/blob/main/src/hmem/encoding/list_complexity.lean
ideally this is also simplified by leveraging the Master Theorem, but that machinery doesn't seem to exist in lean yet either, but also should be straightforward.

From my vantage point getting from a computable lean function to some form of lean accessible bytecode (i.e. demonstrating computability) is much more difficult then going from computability to complexity

[Reid Barton]

The issue is that it is probably much easier to automate proofs of computability in ways that aren't helpful for analyzing complexity.

[Reid Barton]

First, in order to prove a certain function is computable, I don't actually have to produce a TM at all, I just have to prove that there (classically) exists one.

[Reid Barton]

That's probably not very relevant in practice, but also, I only have to produce a TM that the same automation knows how to reason about (as far as knowing what function it computes).

[Reid Barton]

I don't have to produce one that is pleasant in any way for manual reasoning about complexity, or one that is stable under changes to definitions, or one that has the right complexity class at all in the first place.