Complexity Theory?

Stream: new members

[Ian Sweet]

I’m interested in looking at any/all formalizations in the domain of complexity theory. I saw that mathlib has a computability section with definitions for computable functions and Turing machines. Is there anything for e.g. polynomial time algorithms, Karp reductions, etc.?

Thanks in advance!!

[Yaël Dillies]

No, it's all missing. However, there seems to be a lot of people interested in formalising complexity theory recently, so I encourage you to type "complexity theory" in the Zulip search bar and see what comes up. I would do it for you but I'm on my phone!

[Ian Sweet]

Thanks! I took your advice to search Zulip but didn’t find anything else. I’m new to Zulip so I could be missing things unintentionally.

I’m interested in complexity theory as a foundation for asymptotic security in cryptography. I’ll keep looking around and see if I can find anything :)

Thanks again!!

[Yaël Dillies]

Hmm, hopefully @Shreyas Srinivas can point you to the relevant threads, or I arrive home and access my computer

[Daniel Weber]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Computational.20Complexity.20Theory

[Daniel Weber]

there's docs#Turing.TM2ComputableInPolyTime

[Ian Sweet]

Thanks so much @Daniel Weber , apologies for not finding it on my own.

This looks like a great place to start digging in.

[Daniel Weber]

I've wanted to work on complexity theory in Lean, but haven't found the time for that yet

[Daniel Weber]

Daniel Weber said:

there's docs#Turing.TM2ComputableInPolyTime

I believe this should suffice for defining a lot of cryptography, but writing code for reductions seems like it would be extremely challenging in the current state - I believe you'd have to manually create a Turing machine and all of its transitions

[Shreyas Srinivas]

About complexity theory in mathlib:

1. There is a computability part of mathlib which deals with Turing machines and partial recursive functions. There is also a notion of polytime computability, but there is no definition of the class NP. There was a #maths thread on defining complexity classes recently where someone suggested adding the certificate definition of NP.
2. In principle, someone who can devote sufficient time can formalise a number of results around Turing machines like time and space hierarchy theorems and such. In practice, TMs are a pain to work with, even with pen and paper proofs, where, after a point, textbooks get away with abstract descriptions of machines: Roughly you have something like M that compute some function f which takes inputs x : X on which a size : X -> Nat is defined, in time T (size x) many steps. You could try to encode this approach with some typeclasses. Then you could define Karp reductions using some notion of composition. By doing that properly, you might manage to narrow down the scope of your formalisation. Even then, to reiterate, the few TMs you define could be a pain to handle, because you need to take care of every little corner case. I suggest sticking to the binary alphabet if you take this approach, because you have a lot of good source material for nice binary encodings.

[Shreyas Srinivas]

All that being said, complexity is a vast topic, with many other areas.

[Shreyas Srinivas]

In particular circuit complexity is, despite its limitations, much neater to formalise upto a point. You need a notion of circuits which are DAGs. You could define them as trees with binders which point to a circuit in some context

[Shreyas Srinivas]

You can also define uniform circuit classes upto a point by parametrically generating a circuit from a computable lean function carrying a size parameter n. EDIT : I say "up to a point" because there does come a point where one needs to be explicit about the complexity of the function constructing the circuit: for e.g.: DLOGTIME uniform AC0.

[Shreyas Srinivas]

Stasys Jukna's book is a good place to start on this : https://web.vu.lt/mif/s.jukna/boolean/index.html

[Shreyas Srinivas]

The reason I recommend this over other areas is that once you have set up the relatively simple framework I described above for circuits, this area is mostly combinatorics. You can get a lot of help w.r.t combinatorics from mathlib and this zulipchat

[Shreyas Srinivas]

Hastad's switching lemma could be a good target to move towards

[Shreyas Srinivas]

If you are okay with doing more esoteric things that the practicing complexity theorist might probably not use, but is exciting nevertheless: there is this paper you could build on : https://drops.dagstuhl.de/storage/00lipics/lipics-vol193-itp2021/LIPIcs.ITP.2021.20/LIPIcs.ITP.2021.20.pdf

[Shreyas Srinivas]

One basic problem with moving too far into non conventional models is that you have to put in a lot of legwork to recover theorems which complexity theorists who work with TMs would prove using tricks like padding the input.

[Shreyas Srinivas]

another nice corner that is not strictly complexity theory, but still relevant, is boolean fourier transforms. It's a rather powerful technique that can recover several nice theorems from the CS theory literature : https://arxiv.org/abs/2105.10386

[Daniel Weber]

Shreyas Srinivas said:

another nice corner that is not strictly complexity theory, but still relevant, is boolean fourier transforms. It's a rather powerful technique that can recover several nice theorems from the CS theory literature : https://arxiv.org/abs/2105.10386

If you're interesting in that I did some of it in https://command-master.github.io/lean-bourgain/

[Shreyas Srinivas]

ooh that's cool. For others, what's nice about this framework is that you can get theorems like the correctness of BLR test, arrow's impossibility result, and goldreich levin very easily

[Shreyas Srinivas]

I'd say circuit complexity is at a sweet spot for formalisation because even though I used scary words like binders, I believe it is relatively simpler than the lambda calculus stuff, and once you have a working definition, it is mostly combinatorics. I don't know much about arithmetic circuits, but I assume that's similar stuff since you are essentially working with polynomials