Decisions that depend on a bounded amount of data

A constraint of a constraint graph looks at two symbols and a little local data, and says yes or no. The rule may be described by something noncomputable — an alphabet embedding chosen by Classical.choice, say — but it still runs in polynomial time, because it is a table lookup on a bounded key.

That is the content of this module: if a polynomial-time function extracts a key of bounded length, then any predicate of that key is polynomial-time decidable.

The same argument gives functions, not just decisions: a value that depends on the key alone is a table lookup too, whatever wrote the table.

Main results

• Complexity.mem_P_of_bounded_key — a bounded-key predicate is in P
• Complexity.mem_FP_of_bounded_key — a bounded-key value is in FP
• Complexity.mem_FP_of_key_congr — and so is a value that merely agrees wherever the key does

noncomputable def Complexity.keySet (L : ℕ) (Q : List Bool → Prop) : Finset (List Bool)

The strings of length at most L satisfying P.

Equations

• Complexity.keySet L Q = (Finset.range (L + 1)).biUnion fun (n : ℕ) => (List.filter (fun (s : List Bool) => decide (Q s)) (Complexity.allVecs n)).toFinset

theorem Complexity.mem_keySet {L : ℕ} {Q : List Bool → Prop} {s : List Bool} : s ∈ keySet L Q ↔ s.length ≤ L ∧ Q s

theorem Complexity.mem_P_of_bounded_key {key : List Bool → List Bool} (hkey : key ∈ FP) {L : ℕ} (hL : ∀ (z : List Bool), (key z).length ≤ L) (Q : List Bool → Prop) : {z : List Bool | Q (key z)} ∈ P

A bounded-key predicate is in P. The predicate itself need not be computable; only the key extraction must be.

theorem Complexity.mem_FP_of_bounded_key {key : List Bool → List Bool} (hkey : key ∈ FP) {L : ℕ} (hL : ∀ (z : List Bool), (key z).length ≤ L) (g : List Bool → List Bool) : (fun (z : List Bool) => g (key z)) ∈ FP

A bounded-key value is in FP. The rule computing the value from the key need not be computable; only the key extraction must be.

theorem Complexity.mem_FP_of_key_congr {key : List Bool → List Bool} (hkey : key ∈ FP) {L : ℕ} (hL : ∀ (z : List Bool), (key z).length ≤ L) {val : List Bool → List Bool} (hcongr : ∀ (z z' : List Bool), key z = key z' → val z = val z') : val ∈ FP

A value that depends on its input only through a bounded key is in FP. No rule computing the value from the key need be exhibited: agreeing wherever the key agrees is enough.