Fixed-Parameter Time on the Word RAM

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

definition

Loading review…

Natural Language Statement

Definition

A function $F$ on words is computable in fixed-parameter time with respect to a parameter $\kappa$ if a single word-RAM program computes it within $f(\kappa(x))\cdot(|x|+1)^d$ steps, for a computable function $f$ and a constant $d$ , where $|x|$ is the bit size of the input [FG06, Definition 1.4]. It is computable in polynomial time if $f$ can be taken constant. Both notions are relative to a set $D$ of admissible inputs; on words outside $D$ the program is unconstrained.

These are the running times of fpt-algorithms and fpt-reductions; every notion of the hierarchies is built on them.

Concept map

4 concepts; 23 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Lax759944.RamPolytime
2	import Mathlib.Computability.Partrec
3
4	/-!
5	---
6	title: Fixed-Parameter Time on the Word RAM
7	type: definition
8	---
9	A function $F$ on words is computable in fixed-parameter time with respect to a parameter
10	$\kappa$ if a single word-RAM program computes it within $f(\kappa(x))\cdot(\|x\|+1)^d$ steps, for a
11	computable function $f$ and a constant $d$ , where $\|x\|$ is the bit size of the input
12	[FG06, Definition 1.4]. It is computable in polynomial time if $f$ can be taken constant. Both
13	notions are relative to a set $D$ of admissible inputs; on words outside $D$ the program is
14	unconstrained.
15
16	These are the running times of fpt-algorithms and fpt-reductions; every notion of the hierarchies
17	is built on them.
18
19	# Formalization Notes
20
21	The machine is the word RAM `Lax808846.Ram`, with the conventions of the archive's polynomial-time
22	word RAM `Lax759944.RamPolytime`:
23
24	* the input word $x$ is given as the length-prefixed tape `x.length :: x`;
25	* the input size is the bit size `Lax759944.BinaryWordEncoding.bitSize`, so a number counts with
26	its binary length;
27	* the program must halt with the correct output within the bound at every word length from the
28	bound on;
29	* the tape and the output fit in words of that length.
30
31	A single bound $B = f(\kappa(x))\cdot(\|x\|+1)^d$ serves as the time bound and as the least admissible
32	word length. That the word length may depend on the parameter is what makes fixed-parameter
33	computations compose (`WH_A4_MachineFacts`): the output of a first program, of size up to
34	$f(k)\cdot\|x\|^d$ , is the input of the second.
35
36	On the set of all words, `PolyTimeOn` is the archive's `Lax759944.RamPolytime.RamPolytime`
37	(`WH_A5_Bridges.polyTimeOn_univ_iff`).
38	-/
39
40	namespace Lax496464.WH_A1_FptTime
41
42	open Lax808846.Ram Lax759944.BinaryWordEncoding Lax759944.RamPolytime
43
44	/-- The fixed-parameter bound `f(k) · (n + 1)^d`, for a parameter value `k` and an input size `n`. -/
45	def fptBound (f : ℕ → ℕ) (d k n : ℕ) : ℕ := f k * (n + 1) ^ d
46
47	/-- On every word `x` of `D`, the program `p` computes `F x` from the tape `x.length :: x`
48	within `B = f(κ x) · (bitSize x + 1)^d` instructions, at every word length `w ≥ B`; and the
49	tape and the output fit in words of length `B`. -/
50	def ComputesInFptTime (p : Program) (D : Set (List ℕ)) (κ : List ℕ → ℕ)
51	(F : List ℕ → List ℕ) (f : ℕ → ℕ) (d : ℕ) : Prop :=
52	∀ x ∈ D,
53	FitsInWords (fptBound f d (κ x) (bitSize x)) ((x.length :: x) ++ F x) ∧
54	∀ w : ℕ, fptBound f d (κ x) (bitSize x) ≤ w →
55	∃ t ≤ fptBound f d (κ x) (bitSize x), RunsTo w p (x.length :: x) (F x) t
56
57	/-- Fixed-parameter time. `F` is computable on the words of `D` in time `f(κ x) · (\|x\| + 1)^d`
58	by one program, for a computable `f` and a constant `d`. -/
59	def FptTimeOn (D : Set (List ℕ)) (κ : List ℕ → ℕ) (F : List ℕ → List ℕ) : Prop :=
60	∃ (p : Program) (f : ℕ → ℕ) (d : ℕ), Computable f ∧ ComputesInFptTime p D κ F f d
61
62	/-- Polynomial time. `F` is computable on the words of `D` in time `c · (\|x\| + 1)^d` by one
63	program. -/
64	def PolyTimeOn (D : Set (List ℕ)) (F : List ℕ → List ℕ) : Prop :=
65	∃ (p : Program) (c d : ℕ), ComputesInFptTime p D (fun _ => 0) F (fun _ => c) d
66
67	end Lax496464.WH_A1_FptTime
68

Formalization Notes

The machine is the word RAM $Lax808846.Ram$ , with the conventions of the archive's polynomial-time word RAM $Lax759944.RamPolytime$ :

the input word $x$ is given as the length-prefixed tape $x.length :: x$ ;
the input size is the bit size $Lax759944.BinaryWordEncoding.bitSize$ , so a number counts with its binary length;
the program must halt with the correct output within the bound at every word length from the bound on;
the tape and the output fit in words of that length.

A single bound $B = f(\kappa(x))\cdot(|x|+1)^d$ serves as the time bound and as the least admissible word length. That the word length may depend on the parameter is what makes fixed-parameter computations compose ( $WH_A4_MachineFacts$ ): the output of a first program, of size up to $f(k)\cdot|x|^d$ , is the input of the second.

On the set of all words, $PolyTimeOn$ is the archive's $Lax759944.RamPolytime.RamPolytime$ ( $WH_A5_Bridges.polyTimeOn_univ_iff$ ).

Builds on

Lax759944.RamPolytime

Used by

From Mathlib

Mathlib.Computability.Partrec

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 Time on the Word RAM

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments