Polynomial-time maps
Lax213208.PolynomialComputation · concepts/Lax213208/PolynomialComputation.lean · lax-213208
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A map is polynomial-time computable on a domain if one program returns its encoded value within a polynomial resource bound in the encoded input size. The encodings are fixed; no behavior is required outside the domain.
Concept map
Lean source view on GitHub
| 1 | import Lax213208.Programs |
| 2 | import Lax759944.BinaryWordEncoding |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Polynomial-time maps |
| 7 | type: definition |
| 8 | --- |
| 9 | A map is polynomial-time computable on a domain if one program returns its |
| 10 | encoded value within a polynomial resource bound in the encoded input size. |
| 11 | The encodings are fixed; no behavior is required outside the domain. |
| 12 | -/ |
| 13 | |
| 14 | namespace Lax213208.PolynomialComputation |
| 15 | |
| 16 | open Programs Lax759944.BinaryWordEncoding |
| 17 | |
| 18 | variable {Input Output : Type*} |
| 19 | |
| 20 | def PolynomialTimeComputable (input : Input → List ℕ) (output : Output → List ℕ) |
| 21 | (f : Input → Output) (domain : Set Input) : Prop := |
| 22 | ∃ alg : Program, ∃ c d : ℕ, 0 < c ∧ 0 < d ∧ |
| 23 | ∀ x ∈ domain, |
| 24 | RunsWithin alg (input x) (output (f x)) (c * (bitSize (input x) + 2) ^ d) |
| 25 | |
| 26 | end Lax213208.PolynomialComputation |
| 27 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments