Fixed-Parameter Computations Compose

Lax496464.WH_A4_MachineFacts · concepts/Lax496464/WH_A4_MachineFacts.lean · lax-496464

proven

Loading review…

Natural Language Statement

Theorem

The identity is computable in fixed-parameter time, and fixed-parameter computations compose: if $F$ is computable in time $f(\kappa(x))\cdot|x|^{O(1)}$ on $D$ , maps $D$ into $E$ and increases the parameter by at most a computable function, and $G$ is computable in time $f'(\kappa'(y))\cdot|y|^{O(1)}$ on $E$ , then $G \circ F$ is computable in time $f''(\kappa(x))\cdot|x|^{O(1)}$ on $D$ for a computable $f''$ . Restricting the set of inputs, or changing the function outside it, preserves the bound.

Two facts about the input size, from which running-time bounds are usually derived, complete the list: a word has at most as many entries as bits, and each entry is below $2^{|x|}$ .

These are the only facts about programs that the calculus of reductions ( $WH_A3_ReductionCalculus$ ) uses.

Concept map

5 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

1	import Lax496464.WH_A1_FptTime
2
3	/-!
4	---
5	title: Fixed-Parameter Computations Compose
6	type: theorem
7	---
8	The identity is computable in fixed-parameter time, and fixed-parameter computations compose: if
9	$F$ is computable in time $f(\kappa(x))\cdot\|x\|^{O(1)}$ on $D$ , maps $D$ into $E$ and increases the
10	parameter by at most a computable function, and $G$ is computable in time
11	$f'(\kappa'(y))\cdot\|y\|^{O(1)}$ on $E$ , then $G \circ F$ is computable in time
12	$f''(\kappa(x))\cdot\|x\|^{O(1)}$ on $D$ for a computable $f''$ . Restricting the set of inputs, or
13	changing the function outside it, preserves the bound.
14
15	Two facts about the input size, from which running-time bounds are usually derived, complete the
16	list: a word has at most as many entries as bits, and each entry is below $2^{\|x\|}$ .
17
18	These are the only facts about programs that the calculus of reductions (`WH_A3_ReductionCalculus`)
19	uses.
20
21	# Formalization Notes
22
23	The composite runs the first program, keeps its output in memory, and runs the second program on
24	it. The output of the first program has at most $B_1 = f(\kappa(x))(\|x\|+1)^d$ entries of at most
25	$B_1$ bits each, so its bit size is at most $B_1(B_1+1)$ , and the second program runs within
26	$f'(\kappa'(F x))\,(B_1(B_1+1)+1)^{d'}$ steps. Since $\kappa'(F x) \le g(\kappa(x))$ and $f'$ may be
27	replaced by the computable nondecreasing function $m \mapsto \sum_{i\le m} f'(i)$ , this is again a
28	bound $f''(\kappa(x))\,(\|x\|+1)^{d''}$ with $f''$ computable.
29	-/
30
31	namespace Lax496464.WH_A4_MachineFacts
32
33	open Lax496464.WH_A1_FptTime Lax759944.BinaryWordEncoding
34
35	/-- The identity is computable in fixed-parameter time (indeed in linear time). -/
36	axiom fptTimeOn_id (D : Set (List ℕ)) (κ : List ℕ → ℕ) : FptTimeOn D κ fun x => x
37
38	/-- Composition. A fixed-parameter computation followed by one on its outputs, whose parameter
39	is bounded by a computable function of the first parameter, is a fixed-parameter computation. -/
40	axiom fptTimeOn_comp {D E : Set (List ℕ)} {κ κ' : List ℕ → ℕ} {F G : List ℕ → List ℕ}
41	{g : ℕ → ℕ} (hF : FptTimeOn D κ F) (hmaps : ∀ x ∈ D, F x ∈ E) (hg : Computable g)
42	(hκ : ∀ x ∈ D, κ' (F x) ≤ g (κ x)) (hG : FptTimeOn E κ' G) :
43	FptTimeOn D κ fun x => G (F x)
44
45	/-- A bound on a set of inputs holds on every subset. -/
46	axiom fptTimeOn_mono {D D' : Set (List ℕ)} {κ : List ℕ → ℕ} {F : List ℕ → List ℕ} :
47	D' ⊆ D → FptTimeOn D κ F → FptTimeOn D' κ F
48
49	/-- Only the values on the inputs of `D` matter. -/
50	axiom fptTimeOn_congr {D : Set (List ℕ)} {κ : List ℕ → ℕ} {F G : List ℕ → List ℕ} :
51	(∀ x ∈ D, F x = G x) → FptTimeOn D κ F → FptTimeOn D κ G
52
53	/-- Polynomial time is fixed-parameter time, for every parameter. -/
54	axiom fptTimeOn_of_polyTimeOn {D : Set (List ℕ)} {F : List ℕ → List ℕ} (κ : List ℕ → ℕ) :
55	PolyTimeOn D F → FptTimeOn D κ F
56
57	/-- A word has at most as many entries as bits: each entry costs at least its separator. -/
58	axiom length_le_bitSize (x : List ℕ) : x.length ≤ bitSize x
59
60	/-- Every entry of a word is smaller than `2` to the bit size of the word. -/
61	axiom lt_two_pow_bitSize {x : List ℕ} {v : ℕ} : v ∈ x → v < 2 ^ bitSize x
62
63	end Lax496464.WH_A4_MachineFacts
64

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Formalization Notes

The composite runs the first program, keeps its output in memory, and runs the second program on it. The output of the first program has at most $B_1 = f(\kappa(x))(|x|+1)^d$ entries of at most $B_1$ bits each, so its bit size is at most $B_1(B_1+1)$ , and the second program runs within $f'(\kappa'(F x))\,(B_1(B_1+1)+1)^{d'}$ steps. Since $\kappa'(F x) \le g(\kappa(x))$ and $f'$ may be replaced by the computable nondecreasing function $m \mapsto \sum_{i\le m} f'(i)$ , this is again a bound $f''(\kappa(x))\,(|x|+1)^{d''}$ with $f''$ computable.

Builds on

Lax496464.WH_A1_FptTime

Used by

none

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Fixed-Parameter Computations Compose

Flags

Flag this concept

Natural Language Statement

Theorem

1 `fptTimeOn_comp` proven

2 `fptTimeOn_congr` proven

3 `fptTimeOn_id` proven

4 `fptTimeOn_mono` proven

5 `fptTimeOn_of_polyTimeOn` proven

6 `length_le_bitSize` proven

7 `lt_two_pow_bitSize` proven

Lean source view on GitHub

Discussion

Settings