Revision #1452 → #2255 · back to history
modifiedClass P (informal)ce2903fe88e2
| Field | From #1452 | To #2255 |
|---|
| mathlib.decl | TM2ComputableInPolyTime | Turing.TM2ComputableInPolyTime |
| note | Mathlib formalizes polynomial-time Turing-machine computation via `TM2ComputableInPolyTime` but not the language class P itself. | Mathlib formalizes polynomial-time Turing-machine computation via `Turing.TM2ComputableInPolyTime` but not the language class P itself. |
modifiedClass P6264694b7824
| Field | From #1452 | To #2255 |
|---|
| mathlib.decl | TM2ComputableInPolyTime | Turing.TM2ComputableInPolyTime |
| note | Polynomial-time Turing-machine computation (`TM2ComputableInPolyTime`) exists, but the class P of decision problems is not defined. | Polynomial-time Turing-machine computation (`Turing.TM2ComputableInPolyTime`) exists, but the class P of decision problems is not defined. |
addedTime hierarchy theorem149d6d88a8d4
modifiedFischer–Rabin (Presburger arithmetic lower bound)1559d7264f82
| Field | From #1452 | To #2255 |
|---|
| mathlib.decl | Language.presburger | FirstOrder.Language.presburger |
| note | Presburger arithmetic is formalized as a first-order language (`Language.presburger`), but its doubly-exponential runtime lower bound is not. | Presburger arithmetic is formalized as a first-order language (`FirstOrder.Language.presburger`), but its doubly-exponential runtime lower bound is not. |
addedClass co-NP57e6c2a6b637
addedPolynomial hierarchy (PH)bcda14d17720
modifiedClass P (formal)8ee79c5f291d
| Field | From #1452 | To #2255 |
|---|
| mathlib.decl | TM2ComputableInPolyTime | Turing.TM2ComputableInPolyTime |
| note | Mathlib has polynomial-time Turing-machine computation (`TM2ComputableInPolyTime`) but does not bundle it into the language class P. | Mathlib has polynomial-time Turing-machine computation (`Turing.TM2ComputableInPolyTime`) but does not bundle it into the language class P. |
modifiedDeterministic polynomial-time Turing machineaa156b5ea6fc
| Field | From #1452 | To #2255 |
|---|
| mathlib.decl | TM2ComputableInPolyTime | Turing.TM2ComputableInPolyTime |
| note | `TM2ComputableInPolyTime` captures computation by a (deterministic) Turing machine within a polynomial time bound, over the `FinTM2` model. | `Turing.TM2ComputableInPolyTime` captures computation by a (deterministic) Turing machine within a polynomial time bound, over the `FinTM2` model. |