Converting Lean.Expr to untyped lambda calculus

Stream: Is there code for X?

[Jakub Nowak]

Is there maybe some code that does type erasure on Lean.Expr?

[Niels Voss]

I believe there is some type of intermediate language generated as part of the compiler pipeline, which is discussed in "Counting Immutable Beans", but I think it's still quite far from untyped lambda calculus.

What is the purpose of the translation to untyped lambda calculus? Does it need to be runnable?

[Jakub Nowak]

I want to create a framework where you can prove a statement like "REACHABILITY ∈ P" by implementing polynomial algorithm for REACHABILITY in Lean. The idea is to convert Lean.Expr to untyped lambda calculus and then to TM. The proof of TM implementation being polynomial can be obtained from untyped lambda calculus implementation being polynomial (with call-by-value computational model, see https://www.ps.uni-saarland.de/Publications/documents/ForsterSmolka_2017_L-Computability.pdf).

[Snir Broshi]

Are you following #CSLib > Proposal on Time Complexity and #CSLib > proofs with Std.Do?
Basically, are you doing this because you're not aware of existing solutions or because you believe a better solution exists?

[Jakub Nowak]

I haven't read through entire #CSLib > Proposal on Time Complexity, but I think it's a discussion about query model i.e. Cslib.Algorithms.Lean.TimeM. There are a few comments in this topic saying that it's possible to relate query model to computational models, but I don't think there is any existing solution atm. I'm trying a different approach.

[Jakub Nowak]

(deleted)

[Snir Broshi]

wdym, Boole and Std.Do are direct competitors to what you're suggesting IIUC

[Jakub Nowak]

Does Boole refers to https://github.com/Yu-Maryland/BoolE ? I also don't understand Std.Do very well. Isn't it for proving properties about monadic programs? And from what I read about BoolE, it's about automation for that. I fail to see where is computational model and time complexity in there? It's definitely useful for proving correctness and properties of time complexity in e.g. query model and any computational model with imperative style algorithms. What I suggested is a different model than query model. So I guess it is in some sense a competitor to Std.Do because it's not imperative? Though, it might be that Std.Do would also be useful for me, because it might be easier to reason about time complexity in weak call-by-value λ-calculus with it. Also, you said that there's existing solution, but I couldn't find any information about work for relating query model with any computational model.

[Snir Broshi]

Jakub Nowak said:

Does Boole refers to https://github.com/Yu-Maryland/BoolE ?

No, it's an upcoming solution by Amazon/CSLib for implementing and analyzing algorithms in Lean, probably with a DSL.
There aren't many details on it yet, and I'm not sure what the timeline on it is; they said August in multiple places but I guess that was postponed.

I might be missing some nuance as your message about different models goes over my head, but here's what I understand, correct me if I'm wrong:

You (and many other people, including myself) are looking for a way to prove statements in complexity theory / algorithms (such as REACHABILITY ∈ P that you mentioned), by implementing an algorithm and analyzing its complexity in Lean.
There are multiple existing solutions:

• cslib#165
• cslib#201
• Std.Do
• Waiting for Boole to be released

There might be differences in what they are counting exactly to analyze complexity, but they're trying to solve the same issue.
IIUC you're suggesting converting Lean code to a lambda calculus term or TM, which sounds pretty similar to how you can implement analyzable algorithms in Lean code using Std.Do

[Shreyas Srinivas]

I think he is describing Sebastian's solution

[Shreyas Srinivas]

Which is similar to cslib#201 upto a point

[Shreyas Srinivas]

Sebastian instead wants to tag a list of lean declarations whose calls are to be counted and then compile a lean function marked with a suitable attribute to TimeM

[Shreyas Srinivas]

I like the idea in principle but it will super hard in practice, especially if the costs of operations depend on the size of their inputs

[Jakub Nowak]

@Snir Broshi except for Boole, which I couldn't find any information about, I don't see how any of the existing solutions you mention can be directly used to prove anything in terms of Turing.TM2ComputableInPolyTime (this is mathlib's definition of f ∈ P).

[Shreyas Srinivas]

you prove that a given model can be simulated by a TM in polytime and then express f in that model

[Jakub Nowak]

Yeah, so what I want to do is to prove that Lean.Expr can be simulated in polytime, and then you can express f in Lean (which gets elaborated to Lean.Expr). And I think what Snir Broshi is speaking about are only tools for making models, yet, there isn't any high-level computational model implemented in Lean yet.

[Shreyas Srinivas]

Nope there isn’t. I am not sure it is worth doing it either. The recursive definition you write in lean goes through a compiler that will make a bazillion choices on how to evaluate a Lean.Expr. This includes beta/eta reduction strategies, tail call optimisation, reference counting and so on.

[Shreyas Srinivas]

You can try enforcing a simple execution cost model making simple assumptions on lean’s execution of Exprs but that might not give you this poly time simulation you are looking for

[Jakub Nowak]

But the computational model I'll define will be different from the one defined by the compiler. What compiler is doing doesn't matter.

[Jakub Nowak]

Ah, sorry, that's what you said in the second paragraph. I think, the simplified model is fine for stuff like polytime, but I might be wrong. I think all optimizations you mentioned doesn't even affect time complexity more than the linear factor in the sense of big O notation. Reference counting greatly affects size complexity though.

[Shreyas Srinivas]

What’s your beta reduction strategy?

[Shreyas Srinivas]

That’s going to make a huge difference

[Shreyas Srinivas]

And then you have to somehow avoid being able to rewrite with an equivalent function that reduces differently but is extensionally equal

[Jakub Nowak]

Ah yes, you would have to use Lean.Expr directly in complexity proofs for that reason. Which would require reimplementing many tactics to make it easier. Though I would hope that most proofs would get dispatched automatically.

[Jakub Nowak]

Shreyas Srinivas said:

What’s your beta reduction strategy?

Call-by-value, as described in this paper: https://www.ps.uni-saarland.de/Publications/documents/ForsterSmolka_2017_L-Computability.pdf