Finite query programs shared by the geometry-specific trial machines

inductive V7.CausalProgram.Program (d : ℕ) : ℕ → Type

A finite oracle-query program indexed by an upper bound on its remaining queries.

• query {d fuel : ℕ} (point : Point d) (next : Observation d → Program d fuel) : Program d (fuel + 1)
• finish {d fuel : ℕ} (guards : List (ObservableGuardCheck d)) (outcome : TrialOutcome d) : Program d fuel

@[reducible, inline]

abbrev V7.CausalProgram.PackedProgram (d : ℕ) : Type

A finite query program paired with its query bound.

Equations

• V7.CausalProgram.PackedProgram d = ((fuel : ℕ) × V7.CausalProgram.Program d fuel)

noncomputable def V7.CausalProgram.Program.action {d : ℕ} : PackedProgram d → LocalTrialAction d (PackedProgram d)

The next local-trial action exposed by a packed finite program.

Equations

• V7.CausalProgram.Program.action ⟨fst, V7.CausalProgram.Program.finish guards outcome⟩ = V7.LocalTrialAction.finish guards outcome
• V7.CausalProgram.Program.action ⟨fuel.succ, V7.CausalProgram.Program.query point next⟩ = V7.LocalTrialAction.query point fun (obs : V7.Observation d) => ⟨fuel, next obs⟩

noncomputable def V7.CausalProgram.Program.eval {d : ℕ} (oracle : PairOracle d) (fuel : ℕ) : Program d fuel → List (Observation d) → TrialReport d

The report obtained by evaluating the finite program against an oracle.

Equations

• One or more equations did not get rendered due to their size.
• V7.CausalProgram.Program.eval oracle x✝¹ (V7.CausalProgram.Program.finish guards outcome) x✝ = { trace := x✝, checkedGuards := guards, outcome := outcome }

noncomputable def V7.CausalProgram.programTrial {d : ℕ} (initial : ℝ → ℝ → CachedPair d → PackedProgram d) : LocalTrial d

The local trial induced by a family of initial finite query programs.

Equations

• V7.CausalProgram.programTrial initial = { State := V7.CausalProgram.PackedProgram d, initial := initial, action := V7.CausalProgram.Program.action }

theorem V7.CausalProgram.Program.runFuel_eq_eval {d : ℕ} (oracle : PairOracle d) (initial : ℝ → ℝ → CachedPair d → PackedProgram d) (fuel : ℕ) (program : Program d fuel) (history : List (Observation d)) : (programTrial initial).runFuel oracle (fuel + 1) ⟨fuel, program⟩ history = some (eval oracle fuel program history)

theorem V7.CausalProgram.programTrial_executes {d : ℕ} (oracle : PairOracle d) (initial : ℝ → ℝ → CachedPair d → PackedProgram d) (M D : ℝ) (cached : CachedPair d) : (programTrial initial).Executes M D cached oracle (Program.eval oracle (initial M D cached).fst (initial M D cached).snd [])