Running a computation for a bounded number of steps

Computation.runFor s n is the result of the computation s after n steps, or none if s has not terminated by then. Once s has terminated it keeps its result, so a ∈ s.runFor n exactly when s terminates with result a within n steps (Computation.mem_runFor_iff_exists_results). The steps add up along bind (Computation.mem_runFor_bind), and map takes no steps of its own (Computation.runFor_map).

Main results

• Computation.mem_runFor_of_le: a result available after m steps is available after n ≥ m steps.
• Computation.mem_iff_exists_mem_runFor, Computation.mem_runFor_iff_exists_results: results of a computation and their times.
• Computation.runFor_map, Computation.mem_runFor_bind: map and bind against the clock.

@[simp]

theorem Computation.runFor_pure {α : Type u_1} (a : α) (n : ℕ) : (pure a).runFor n = some a

A pure computation has its result after any number of steps.

@[simp]

theorem Computation.runFor_empty {α : Type u_1} (n : ℕ) : (empty α).runFor n = none

The nonterminating computation has no result after any number of steps.

theorem Computation.mem_runFor_of_le {α : Type u_1} {s : Computation α} {a : α} {m n : ℕ} (h : m ≤ n) (ha : a ∈ s.runFor m) : a ∈ s.runFor n

A result available after m steps is available after n ≥ m steps.

theorem Computation.mem_of_mem_runFor {α : Type u_1} {s : Computation α} {a : α} {n : ℕ} (h : a ∈ s.runFor n) : a ∈ s

A result available after n steps is a result of the computation.

theorem Computation.mem_iff_exists_mem_runFor {α : Type u_1} {s : Computation α} {a : α} : a ∈ s ↔ ∃ (n : ℕ), a ∈ s.runFor n

a is a result of s exactly when it is available after some number of steps.

theorem Computation.eq_of_mem_runFor {α : Type u_1} {s : Computation α} {a a' : α} {m n : ℕ} (h : a ∈ s.runFor m) (h' : a' ∈ s.runFor n) : a = a'

Two results of the same computation, at any two times, are equal.

theorem Computation.Results.mem_runFor {α : Type u_1} {s : Computation α} {a : α} {n : ℕ} (h : s.Results a n) : a ∈ s.runFor n

A computation terminating after exactly n steps has its result after n steps.

theorem Computation.mem_runFor_iff_exists_results {α : Type u_1} {s : Computation α} {a : α} {n : ℕ} : a ∈ s.runFor n ↔ ∃ (m : ℕ), m ≤ n ∧ s.Results a m

A computation has the result a after n steps exactly when it terminates with result a after at most n steps.

theorem Computation.Results.mem_runFor_iff {α : Type u_1} {s : Computation α} {a a' : α} {m n : ℕ} (h : s.Results a m) : a' ∈ s.runFor n ↔ a' = a ∧ m ≤ n

For a computation terminating after exactly m steps with result a, the result after n steps is a exactly when m ≤ n.

@[simp]

theorem Computation.runFor_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : Computation α) (n : ℕ) : (map f s).runFor n = Option.map f (s.runFor n)

map takes no steps of its own.

theorem Computation.mem_runFor_map {α : Type u_1} {β : Type u_2} {s : Computation α} {a : α} {n : ℕ} (f : α → β) (h : a ∈ s.runFor n) : f a ∈ (map f s).runFor n

If a is available from s after n steps, then f a is available from s.map f after n steps.

theorem Computation.mem_runFor_bind {α : Type u_1} {β : Type u_2} {s : Computation α} {f : α → Computation β} {a : α} {b : β} {m n : ℕ} (ha : a ∈ s.runFor m) (hb : b ∈ (f a).runFor n) : b ∈ (s.bind f).runFor (m + n)

The steps of a computation and of its continuation add up along bind.