Lax489179.WordPrograms
Word-RAM programs with optional fair coins
concepts/Lax489179/WordPrograms.lean · lax-489179
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
We use the finite word-RAM instruction set of lax-67 and add one instruction writing a fresh fair bit to a specified cell. In deterministic mode this instruction is forbidden. All arithmetic, indirect addressing, input access and output use lax-67's word semantics. Input is a read-only array, writable memory starts at zero, and output is append-only.
Each fetched instruction costs one step, including a coin or a halt. Detecting an out-of-range program counter also costs one step in this wrapper. Halted configurations are unchanged by further padding steps. The bound thus includes the full output and termination. A random word can be assembled from fair bits using the ordinary instructions. The probability space is the uniform distribution on the finite bit strings supplied to these transitions; it does not provide random advice.
Lean source view on GitHub
| 1 | import Lax67.Ram |
| 2 | import Lax489179.Algorithms |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Word-RAM programs with optional fair coins |
| 7 | type: definition |
| 8 | --- |
| 9 | We use the finite word-RAM instruction set of lax-67 and add one |
| 10 | instruction writing a fresh fair bit to a specified cell. In deterministic |
| 11 | mode this instruction is forbidden. All arithmetic, indirect addressing, |
| 12 | input access and output use lax-67's word semantics. Input is a read-only |
| 13 | array, writable memory starts at zero, and output is append-only. |
| 14 | |
| 15 | Each fetched instruction costs one step, including a coin or a halt. |
| 16 | Detecting an out-of-range program counter also costs one step in this |
| 17 | wrapper. Halted configurations are unchanged by further padding steps. |
| 18 | The bound thus includes the full output and termination. A random word |
| 19 | can be assembled from fair bits using the ordinary instructions. |
| 20 | The probability space is the uniform distribution on the finite bit |
| 21 | strings supplied to these transitions; it does not provide random advice. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax489179.WordPrograms |
| 25 | |
| 26 | open Lax67.Ram |
| 27 | |
| 28 | inductive Instruction |
| 29 | | ordinary (instruction : Instr) |
| 30 | | coin (destination : ℕ) |
| 31 | |
| 32 | abbrev Program := List Instruction |
| 33 | |
| 34 | structure Config where |
| 35 | state : State |
| 36 | halted : Bool |
| 37 | |
| 38 | def init (input : List ℕ) : Config := ⟨initState input, false⟩ |
| 39 | |
| 40 | def step (w : ℕ) (p : Program) (bit : Bool) (c : Config) : Config := |
| 41 | if c.halted then c else |
| 42 | match p[c.state.pc]? with |
| 43 | | none => { c with halted := true } |
| 44 | | some (.ordinary instruction) => |
| 45 | match instruction.effect w c.state with |
| 46 | | none => { c with halted := true } |
| 47 | | some s => ⟨s, false⟩ |
| 48 | | some (.coin a) => |
| 49 | ⟨{ c.state with |
| 50 | pc := c.state.pc + 1 |
| 51 | mem := setCell w c.state.mem a bit.toNat }, false⟩ |
| 52 | |
| 53 | def run (w : ℕ) (p : Program) : (t : ℕ) → (Fin t → Bool) → Config → Config |
| 54 | | 0, _, c => c |
| 55 | | t + 1, r, c => run w p t (fun i => r i.succ) (step w p (r 0) c) |
| 56 | |
| 57 | def output (c : Config) : Option (List ℕ) := |
| 58 | if c.halted then some c.state.out else none |
| 59 | |
| 60 | def Deterministic (p : Program) : Prop := |
| 61 | ∀ a, Instruction.coin a ∉ p |
| 62 | |
| 63 | def ComputesWithin (w : ℕ) (p : Program) (input : List ℕ) |
| 64 | (correct : List ℕ → Prop) (t : ℕ) : Prop := |
| 65 | Algorithms.CorrectWithin t (fun r => output (run w p t r (init input))) correct |
| 66 | |
| 67 | end Lax489179.WordPrograms |
| 68 |
Builds on
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