cook levin, np completeness of SAT

Stream: general

[TongKe Xue]

Is Cook-Levin, NP-completeness of SAT in MathLib ?

I found https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/TuringMachine.html for turing machines, but I can't find Cook-Levin / NP-Completeness of SAT.

I'm curious what the current state of Computational Complexity, with the respect of MathLib, i.e.

1. it is formalized, but I'm an idiot and not finding it
2. It is not formalized, and not intended to be formalized
3. It is not formalized, but there is a road map for it somewhere

[TongKe Xue]

In Lean4, is there a easy way to prove, under the "RAM Model" of computation, how long a Lean4 function runs?

Context: To prove a NP-completeness reduction, the typical structure is something like this:

1. We know language L1 is NP-complete.
2. We want to prove language L2 is complete.
3. We devise a polynomial time reduction P, s.t. x in L1 <-> P(x) in L2.

Then we can say: hypothetically, if you could solve L2 in polynomial time via some decision procedure D, then D(P(x)) solves x in L1 in polynomial time, and no one in the world knows how to decide L1 in polynomial time.

Now, the important part here is that P(x) must run in O(poly(size_of(x)) time. [Otherwise, we can run an exp time procedure to decide x, return one of two trivial elements known to belong / not-belong in L2].

To do this, we need to be able to argue "this lean function, under the RAM model, runs in time poly(number_of_bits(input))". Through both (1) the lean game server and (2) skimming the lean docs, I haven't seen any proofs of runtime of this form.

I am curious if there are pointers on how to do these "prove RAM model runtime of function" proofs in Lean.

Thanks!

[Mauricio Collares]

Maybe you can do a lot of metaprogramming to make it work, but it seems impossible to do analyze the complexity of Lean4 pure functions without it due to function extensionality. If you're not talking about pure functions, there is an open PR (#20924) for computing the number of "oracle operations" of a monadic function. See also this thread: #general > Formalization of Runtime Complexity of Sorting Algorithms @ 💬

[TongKe Xue]

1. I'm misunderstanding something very obvious. Why is "pure function" distinction important? (My interpretation of "pure function" is just a function w/o side effffects, i.e. no IO Monad).

2. Would it be correct to say there is currently almost no formalization of CLRS/Intro to Algorithms style running time proofs ? [It seems like most proofs are concerned with correctness / properties of outputs of functions, but not how long functions take.]

[Mirek Olšák]

I am a bit confused by the question as I see two independent ones

1. Could we measure computational complexity of Lean functions? For sure not directly, Lean functions should be thought of as mathematical -- not something "calculating" a value but rather as something that "has" a value for each input. This is deeply embedded into the logic through definitional equality and function extensionality. What is the computational complexity of sin? That some of them can be compiled into a code is a side-effect which cannot be exactly captured in the logic (unless we use metaprogramming, and look into the structure of the Lean expression rather than just the logical semantic representation). By the way, to my understanding, complexity of functional programming is a bit tricky -- are we counting the number of beta-reductions, or the time of a specific implementation performing them? In which order are we beta-reducing? So I am not really sure if this is a priority...
2. What is the status of the theory of computational complexity in Lean? To my understanding, not much of it is developed, I don't even see non-deterministic Turing machines in Mathlib (I can only see non-deterministic finite automata). Perhaps a NP could be defined by giving Turing.TM2.Stmt a hint in one of the stacks but I cannot find such definition. However, I am no expert in this, someone could correct me.

[TongKe Xue]

I don't have any answers. I just want to say that @Mirek Olšák 's question 1 is a great question that "crystallizes" things I've been thinking about, trying to formulate, but could not formulate. Thanks for capturing the "essence" of the issue.

In the spirit of increasing # of questions w/o increasing # of answers, some other hazy thoughts I've been thinking about with regards to NP-Completeness reductions. What do we use to express these NP-Completeness reductions? The three obvious choices seems to be:

1. Lean itself. This brings up the above issues of proving runtime of Lean 'functions'
2. Have a trivial https://en.wikipedia.org/wiki/MIPS_architecture interpreter defined in Lean. Except instead of 32 bit registers, we use log-n bit registers. Then 'reductions' becomes proofs of the form: we have a 3SAT instance encoded in memory; then our reduction (bunch of MIPs instrs) writes to a different part of RAM, with some encoding of Vertex Covering; and the "proof" becomes things like:
   2a. The memory encoding 3SAT is a satisfiable 3SAT, iff the memory coding the Vertex cover is a satisfiable Vertex Cover
   2b. We prove the MIPs interpreter runs in poly(n) time.

The downside of #2, of course, is that writing NP-completeness reductions in MIPs assembly is not the most pleasant experience in the world. So we might go for something like

3. Define a mini-OCaml interpreter in Lean; express the reduction in the mini-OCaml interpreter, and have some way to count the instrs of the mini-OCaml interpreter. Now, of course, "how do we count instrs" is annoying -- but not very important in the case of NP-completeness reductions, as we don't really about a poly(n) time here and a poly(n) term there. :-)

I have previously tried doing something like #2 in Coq; and failed. I have never attempted #3.

[Mirek Olšák]

Ad #2, there is the Turing.TM2.Stmt with a fixed number of possible stacks. Isn't it enough?

[Snir Broshi]

TongKe Xue said:

I don't have any answers. I just want to say that Mirek Olšák 's question 1 is a great question that In the spirit of increasing # of questions w/o increasing # of answers, some other hazy thoughts I've been thinking about with regards to NP-Completeness reductions. What do we use to express these NP-Completeness reductions?

I think you're missing the Boole language and Std.Do, you might want to read/ask in #CSLib > proofs with Std.Do

I know you're targeting Mathlib, but these are questions the CSLib project is now handling, and it's probably worth joining forces

[Snir Broshi]

See also #CSLib > Complexity Theory in CSLib and #CSLib > Proposal on Time Complexity for similar discussions

[TongKe Xue]

@Snir Broshi : I'm still skimming through these discussions -- but they look like precisely the issue I'm dealing with. Thanks for all the pointers! (I'm new to both zulip & lean, and haven't quite figured out how 'search' works yet.) Thanks!

[Palalansoukî]

TongKe Xue said:

What do we use to express these NP-Completeness reductions?

I wish to propose a #5 approach. I believe it is the most tractable one, at least from the mathematical perspective, on formalizing the computational complexity theory.

What I wish to argue is defining complexity classes based on implicit computational complexity (as I mentioned in #maths > Formalise the proposition P ≠NP ).

For example, the class of polynomial-time functions can be defined as follows.

import Mathlib

open Matrix

-- Usually we assume that α is fintype, or α = Bool
variable {α : Type*} [DecidableEq α]

inductive SafeFunction : {n s : ℕ} → ((Fin n → List α) → (Fin s → List α) → List α) → Prop
  | nil : SafeFunction fun _ _ => []
  | cons (a : α) : SafeFunction fun (_ : Fin 0 → List α) (w : Fin 1 → List α) ↦ a :: w 0
  | tail : SafeFunction fun (_ : Fin 0 → List α) (w : Fin 1 → List α) ↦ (w 0).tail
  | normal_proj (i : Fin n) : SafeFunction fun (v : Fin n → List α) (_ : Fin s → List α) ↦ v i
  | safe_proj (i : Fin s) : SafeFunction fun (_ : Fin n → List α) (w : Fin s → List α) ↦ w i
  | cond (a : α) : SafeFunction fun (_ : Fin 0 → List α) (w : Fin 3 → List α) ↦ if a ∈ (w 0).head? then w 1 else w 2
  | safe_comp
    {f : Fin n₂ → (Fin n₁ → List α) → (Fin 0 → List α) → List α}
    {g : Fin s₂ → (Fin n₁ → List α) → (Fin s₁ → List α) → List α}
    {h : (Fin n₂ → List α) → (Fin s₂ → List α) → List α}
    (hf : ∀ i, SafeFunction (f i))
    (hg : ∀ j, SafeFunction (g j))
    (hh : SafeFunction h) :
    SafeFunction fun (v : Fin n₁ → List α) (w : Fin s₁ → List α) ↦ h (fun i ↦ f i v ![]) (fun j ↦ g j v w)
  | safe_rec
    {f : (Fin n → List α) → (Fin s → List α) → List α}
    {g : α → (Fin (n + 1) → List α) → (Fin (s + 1) → List α) → List α}
    (hf : SafeFunction f)
    (hg : ∀ a, SafeFunction (g a)) :
    SafeFunction fun (v : Fin (n + 1) → List α) (w : Fin s → List α) ↦
      (vecHead v).rec (f (vecTail v) w) fun a k ih ↦ g a (vecCons k (vecTail v)) (vecCons ih w)

abbrev PolyTimeComputable (f : (Fin n → List α) → List α) : Prop := SafeFunction fun v (_ : Fin 0 → List α) ↦ f v

Concepts such as the P vs. NP problem and NP-completeness, etc. can also be defined straightforwardly.

variable (α)

def ClassP : Set (Set (List α)) :=
  {C | ∃ f, PolyTimeComputable f ∧ ∀ x, x ∈ C ↔ f ![x] = []}

def ClassNP : Set (Set (List α)) :=
  {C | ∃ f, PolyTimeComputable f ∧ ∃ n, ∀ x, x ∈ C ↔ ∃ z, z.length ≤ x.length ^ n ∧ f ![x, z] = []}

variable {α}

def PneNP : Prop := ClassP Bool ≠ ClassNP Bool

def IsKarpReducible (A B : Set (List α)) : Prop := ∃ f, PolyTimeComputable f ∧ ∀ x, x ∈ A ↔ f ![x] ∈ B

def IsNPComplete (A : Set (List α)) : Prop := ∀ B ∈ ClassNP α, IsKarpReducible B A

This follows the same style as the definitions of Primrec, Partrec and Computable in Mathlib. That is, we define them using function algebras, rather than relying on TM or other models of computation.

[Palalansoukî]

Cook-Levin's theorem can likely be proven by similar work to constructing a universal Turing machine. That is, doing a proof like the one in https://leanprover-community.github.io/mathlib4_docs//Mathlib/Computability/PartrecCode.html for PolyTimeComputable that takes a polynomial-sized certificate.

[TongKe Xue]

This looks interesting -- but I don't think I have enough fundamentals to understand it. My background is CS Theory. I've written a few compilers + bytecode interpreters in Rust/OCaml/Haskell. I don't recognize this SafeFunction "inductive/enum" that you have defined.

Is this (1) a well known theory, or (2) something you designed ? If (1), can you point me at the theory? If (2), can you motivate the "arms" of the inductive/enum? They look half-lisp-ish, half-continuation-ish; and I don't know what's going on / theory behind it.

Thanks!

[Palalansoukî]

TongKe Xue said:

Is this (1) a well known theory, or (2) something you designed ? If (1), can you point me at the theory? If (2), can you motivate the "arms" of the inductive/enum? They look half-lisp-ish, half-continuation-ish; and I don't know what's going on / theory behind it.

Of course (1)! I think it's well-known among mathematicians specializing in bounded arithmetic or finite model theory. see wikipedia article or Clote's comprehensive paper.

[Palalansoukî]

My definition is actually a slight extension of the original Bellantoni–Cook definition. However, it coincides when α = Bool, and even when it doesn't, it should be the same under appropriate coding if α is finite.

[Martin Dvořák]

I think formalizing Cook-Levin will be a huge undertaking but worth the effort.
IMHO the best material to follow is:
https://www.isa-afp.org/browser_info/current/AFP/Cook_Levin/document.pdf