Lax489179.Algorithms

Deterministic and bounded-error algorithms

concepts/Lax489179/Algorithms.lean · lax-489179

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

We distinguish deterministic algorithms from randomized algorithms with two-sided error at most $1/3$ and a worst-case running-time bound. For a computation of at most $t$ steps, all $2^t$ strings of independent fair bits are equally likely. Every string must lead to termination; at least two thirds must give a correct answer. Unused bits are ignored.

Both machine models below have finite programs. In deterministic mode the program cannot use randomness. The hypotheses themselves are propositions, available as explicit premises in later theorems.

Lean source view on GitHub

1	import Mathlib.SetTheory.Cardinal.Finite
2	import Mathlib.Data.Fintype.Pi
3
4	/-!
5	---
6	title: Deterministic and bounded-error algorithms
7	type: definition
8	---
9	We distinguish deterministic algorithms from randomized algorithms with
10	two-sided error at most $1/3$ and a worst-case running-time bound.
11	For a computation of at most $t$ steps, all $2^t$ strings of independent
12	fair bits are equally likely. Every string must lead to termination;
13	at least two thirds must give a correct answer. Unused bits are ignored.
14
15	Both machine models below have finite programs. In deterministic mode
16	the program cannot use randomness. The hypotheses themselves are
17	propositions, available as explicit premises in later theorems.
18	-/
19
20	namespace Lax489179.Algorithms
21
22	inductive Mode
23	\| deterministic
24	\| randomized
25	deriving DecidableEq
26
27	/-- Deterministic mode restricts the program; randomized mode allows it. -/
28	def Allowed (mode : Mode) (isDeterministic : Prop) : Prop :=
29	mode = .deterministic → isDeterministic
30
31	/-- Every random tape terminates, and at least two thirds return a
32	correct result. `none` means that the computation has not terminated. -/
33	def CorrectWithin {α : Type} (t : ℕ)
34	(result : (Fin t → Bool) → Option α) (correct : α → Prop) : Prop :=
35	(∀ r, (result r).isSome = true) ∧
36	2 * 2 ^ t ≤ 3 * Nat.card {r : Fin t → Bool //
37	∃ y, result r = some y ∧ correct y}
38
39	end Lax489179.Algorithms
40

Builds on

none

Used by

From Mathlib

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

Deterministic and bounded-error algorithms

Flags

Flag this concept