Polynomial-time many-one reductions on the word RAM
Lax470956.PolynomialReduction · concepts/Lax470956/PolynomialReduction.lean · lax-470956
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A polynomial-time many-one reduction from one set of words to another is a map on words, computable by a word RAM program in time polynomial in the bit-size of its input, that preserves and reflects membership. A reduction whose image additionally lies in a given class witnesses hardness on that class.
Concept map
Lean source view on GitHub
| 1 | import Lax759944.RamPolytime |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Polynomial-time many-one reductions on the word RAM |
| 6 | type: definition |
| 7 | --- |
| 8 | A *polynomial-time many-one reduction* from one set of words to another is a map on |
| 9 | words, computable by a word RAM program in time polynomial in the bit-size of its input, |
| 10 | that preserves and reflects membership. A reduction whose image additionally lies in a |
| 11 | given class witnesses hardness on that class. |
| 12 | |
| 13 | # Formalization notes |
| 14 | |
| 15 | Computability is `Lax759944.RamPolytime`, which measures time in the bit-size of the |
| 16 | input rather than the number of entries, and quantifies the program before the word |
| 17 | length as everything on this machine does. Taking it rather than restating it is the |
| 18 | point: the same submission proves it equivalent to polynomial time on a Turing machine, |
| 19 | so a reduction certified here is a reduction in the classical sense, and no statement of |
| 20 | this submission has to choose between the two models. |
| 21 | |
| 22 | Both directions of membership are required, as for any many-one reduction: a map |
| 23 | preserving yes-instances only would not transport hardness. |
| 24 | |
| 25 | The class a reduction lands in is a predicate on words, and appears as a third |
| 26 | conjunct rather than by restricting the target set. Keeping it separate lets one |
| 27 | reduction witness both a plain hardness claim and a claim on a slice; the second theorem of |
| 28 | this submission needs both. |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax470956.PolynomialReduction |
| 32 | |
| 33 | /-- `P` reduces to `Q` in polynomial time on the word RAM. -/ |
| 34 | def PolyReduces (P Q : Set (List ℕ)) : Prop := |
| 35 | ∃ f : List ℕ → List ℕ, |
| 36 | Lax759944.RamPolytime.RamPolytime f ∧ ∀ x, (x ∈ P ↔ f x ∈ Q) |
| 37 | |
| 38 | /-- `P` reduces to `Q` in polynomial time by a reduction whose image lies in `C`. -/ |
| 39 | def PolyReducesOn (P Q : Set (List ℕ)) (C : List ℕ → Prop) : Prop := |
| 40 | ∃ f : List ℕ → List ℕ, |
| 41 | Lax759944.RamPolytime.RamPolytime f ∧ (∀ x, C (f x)) ∧ ∀ x, (x ∈ P ↔ f x ∈ Q) |
| 42 | |
| 43 | end Lax470956.PolynomialReduction |
| 44 |
Formalization notes
Computability is , which measures time in the bit-size of the input rather than the number of entries, and quantifies the program before the word length as everything on this machine does. Taking it rather than restating it is the point: the same submission proves it equivalent to polynomial time on a Turing machine, so a reduction certified here is a reduction in the classical sense, and no statement of this submission has to choose between the two models.
Both directions of membership are required, as for any many-one reduction: a map preserving yes-instances only would not transport hardness.
The class a reduction lands in is a predicate on words, and appears as a third conjunct rather than by restricting the target set. Keeping it separate lets one reduction witness both a plain hardness claim and a claim on a slice; the second theorem of this submission needs both.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments