Polynomial time with polynomial word length

Lax560851.BitPolynomialTime · concepts/Lax560851/BitPolynomialTime.lean · lax-560851

definition

Loading review…

Natural Language Statement

Definition

This variant bounds both running time and sufficient word length by polynomials in a specified input size, normally its binary size. Input still uses the distinguished structural arena. A bound of $q$ bits means capacity $2 ^ q$ , so this is an instance of the existing RAM resource predicate, not a different machine model.

The arena must fit already at the stated sufficient width. This prevents oversized payloads from making the guarantee vacuous. The one program works at every larger width, and must produce the exact encoded output.

In contrast, $RamComplexityExample.PolynomialTime$ measures time in sequence length and permits only a constant-times-input-magnitude capacity threshold. Polynomially many sufficient bits can accommodate exponentially large natural-number outputs; that linear capacity convention cannot in general.

Concept map

6 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax560851.RamComplexity
2	import Mathlib.Algebra.Polynomial.Eval.Defs
3
4	/-!
5	---
6	title: Polynomial time with polynomial word length
7	type: definition
8	---
9
10	This variant bounds both running time and sufficient word length by
11	polynomials in a specified input size, normally its binary size. Input still
12	uses the distinguished structural arena. A bound of `q` bits means capacity
13	`2 ^ q`, so this is an instance of the existing RAM resource predicate, not
14	a different machine model.
15
16	The arena must fit already at the stated sufficient width. This prevents
17	oversized payloads from making the guarantee vacuous. The one program works
18	at every larger width, and must produce the exact encoded output.
19
20	In contrast, `RamComplexityExample.PolynomialTime` measures time in sequence
21	length and permits only a constant-times-input-magnitude capacity threshold.
22	Polynomially many sufficient bits can accommodate exponentially large
23	natural-number outputs; that linear capacity convention cannot in general.
24	-/
25
26	namespace Lax560851.BitPolynomialTime
27
28	open Lax560851.StructuralPresentation Lax560851.WordArena Lax560851.RamComplexity
29
30	universe u v
31
32	/-- Polynomial instruction count and polynomial sufficient word length,
33	relative to a presentation, output encoding, and input-size measure.
34	Both polynomials are chosen once, independently of the input and runtime
35	word width. The input remains a root word followed by its structural arena. -/
36	def BitPolynomialTimeUsing {α : Type u} {β : Type v}
37	(input : Presentation α) (output : β → List Nat)
38	(inputSize : α → Nat) (f : α → β) : Prop :=
39	∃ wordBits time : Polynomial Nat,
40	(∀ x, (input.toRaw x).PayloadsFitInWord (wordBits.eval (inputSize x)) ∧
41	3 * (input.toRaw x).nodes ≤ 2 ^ wordBits.eval (inputSize x)) ∧
42	RamComputableWithinUsing input output f
43	(fun x => time.eval (inputSize x))
44	(fun x => 2 ^ wordBits.eval (inputSize x))
45
46	end Lax560851.BitPolynomialTime
47