Complexity Theory in CSLib

Stream: CSLib

[Bolton Bailey]

I recently made an effort to put a formalization of the P vs NP conjecture in the Deepmind formal-conjectures repository. In the course of that, I did a short formalization of the relevant complexity classes.

It's nice for formal-conjectures to have a famous conjecture like this, but ultimately, I think it would be better if the development of complexity theory could happen in CSLib, for a few reasons

• It would be nice to develop other classes (PSPACE, EXP, the Polynomial Hierarchy, various probabilistic classes), which would start to balloon the portion of formal-conjectures this would take up.
• Rather than just stating open questions, it would be nice to actually prove known relationships between these classes. (In particular, to validate that there's nothing wrong with the definitions).
• Based on the name, I feel like I would be more likely to expect CSLib to have these concepts than Mathlib or formal-conjectures.

So, does this seem like the sort of thing that would make sense to put in CSLib? I know there is a plan for CSLib to have its own language, so perhaps a Turing-machine based formulation of complexity classes doesn't belong for that reason, but I'd be interested in the opinion of anyone who's more actively involved.

[Shreyas Srinivas]

There is a way to formalise complexity theory in a word ram model and Emanuelle Viola is writing such a book. Nevertheless it can’t hurt to have the TM version of these classes either.

[Frederick Pu]

i think in order to be able to pratically construct reductions for all of the problems in the NP complete class, we need a way of constructing quoted functions in very natural way. Like some sort of embedding of simply typed lambda caluculus and the corresponding formalization of complexity theory for it

[Frederick Pu]

that way when you do correctness proof you can interpret the embedded lambda function as a normal lean function and use all of the monadic verification tools to verify the correctness about the reduction program

[Tudor]

I know there is a plan for CSLib to have its own language, so perhaps a
Turing-machine based formulation of complexity classes doesn't belong for
that reason

Just curious, what are the advantages of this language over Lean?

[Bolton Bailey]

For reference, the language is "Boole", you can search Zulip for it, I think the idea is that it will be a procedural language and that it will be easier to reason about time complexity in an embedded DSL rather than native Lean, where it is unclear how we would count the number of steps a function takes to execute.

[Frederick Pu]

i think if the language is defined as a type that doesnt contain ani Pi or functions types you define the complexity by interpretting the recursors in some sort of execution model

[Frederick Pu]

and then there would prbably be some composition rules for computational complexity