Lax58.RamComplexity

Time and word-capacity bounds on the word-RAM

concepts/Lax58/RamComplexity.lean · lax-58

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

One fixed program computes a mathematical function within explicit time and word-capacity bounds. It works at every word width satisfying the input-fit conditions and the supplied capacity threshold. The threshold is a number of representable values, not a number of bits. Output production is included in the instruction count. No computability or growth restriction on either bound is implicit: such restrictions belong in the theorem using this predicate.

$RamComputableWithinUsing$ is relative to explicitly supplied encodings; it does not certify them. The $RamComputableWithin$ frontend selects approved encodings from the input and output types. Inputs use structural arenas; natural and Boolean outputs use one word, and structured outputs use arenas.

Lean source view on GitHub

1	import Lax13.RamComputes
2	import Lax58.WordArena
3
4	/-!
5	---
6	title: Time and word-capacity bounds on the word-RAM
7	type: definition
8	---
9
10	One fixed program computes a mathematical function within explicit time and
11	word-capacity bounds. It works at every word width satisfying the input-fit
12	conditions and the supplied capacity threshold. The threshold is a number of
13	representable values, not a number of bits. Output production is included in
14	the instruction count. No computability or growth restriction on either bound
15	is implicit: such restrictions belong in the theorem using this predicate.
16
17	`RamComputableWithinUsing` is relative to explicitly supplied encodings; it
18	does not certify them. The `RamComputableWithin` frontend selects approved
19	encodings from the input and output types. Inputs use structural arenas;
20	natural and Boolean outputs use one word, and structured outputs use arenas.
21	-/
22
23	namespace Lax58.RamComplexity
24
25	open Lax13.Ram Lax13.RamComputes
26	open Lax58.StructuralPresentation Lax58.WordArena
27
28	universe u v
29
30	/-- Input size and payload magnitude for a specified presentation. -/
31	def inputMagnitudeUsing {α : Type u} (input : Presentation α) (x : α) : Nat :=
32	(input.toRaw x).nodes + (input.toRaw x).maxNat + 1
33
34	/-- A natural-number result occupies one output word. -/
35	def natOutput (n : Nat) : List Nat := [n]
36
37	/-- A Boolean result occupies one output word: false is zero, true is one. -/
38	def boolOutput (b : Bool) : List Nat := [if b then 1 else 0]
39
40	/-- A structured result uses the same root-plus-arena convention as input. -/
41	def arenaOutput {α : Type u} (raw : α → Raw) (x : α) : List Nat :=
42	(encodeRaw (raw x)).toInput
43
44	/-- One program for all inputs and all sufficient word widths, with explicit
45	encodings and exact instruction and word-capacity bounds. -/
46	def RamComputableWithinUsing {α : Type u} {β : Type v}
47	(input : Presentation α) (output : β → List Nat)
48	(f : α → β) (timeBound wordBound : α → Nat) : Prop :=
49	∃ program : Program,
50	∀ (x : α) (w : Nat),
51	(input.toRaw x).PayloadsFitInWord w →
52	3 * (input.toRaw x).nodes ≤ 2 ^ w →
53	wordBound x ≤ 2 ^ w →
54	ComputesInTime w program {(encode input x).toInput}
55	(fun _ => output (f x)) (fun _ => timeBound x)
56
57	end Lax58.RamComplexity
58

Builds on

Used by

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Time and word-capacity bounds on the word-RAM

Flags

Flag this concept