Asking an assumed solver questions

This file lets a tape program ask an assumed solver for answers to a yes/no problem. Such a solver is called an oracle. The program asks about the word under the tape head, ending at the first blank. Its answer is recorded in the machine state, so later branches and loops can depend on it.

A request costs one time step and leaves the tape and head unchanged. Head moves also cost one time step. Every instruction and loop test uses fuel. The solver's own work is outside this count.

Main definitions and results

• OracleInterface chooses distinct states for requests, yes answers, and no answers.
• queryWord reads the word being asked about.
• ask issues a request.
• interpreter supplies the rules for executing requests to the shared runner.
• execute_ask_succ describes the answer and cost of a request.
• execute_cellsAllocated counts the cells added to the recorded tape range during execution.

structure Algolean.Algorithms.OracleInterface (tm : Cslib.Turing.SingleTapeTM Bool) : Type

This interface chooses three distinct machine states for issuing a request and recording a yes or no answer.

• request : tm.State

  Setting this state with an update instruction asks the solver about the word under the head.

• yes : tm.State

  The interpreter sets this state when the solver answers yes.

• no : tm.State

  The interpreter sets this state when the solver answers no.

• request_ne_yes : self.request ≠ self.yes

  The request state differs from the yes state.

• request_ne_no : self.request ≠ self.no

  The request state differs from the no state.

• yes_ne_no : self.yes ≠ self.no

  The yes and no states differ, so the program can distinguish the answers.

def Algolean.Algorithms.OracleInterface.queryWord (contents : Cslib.Turing.BiTape Bool) : List Bool

The question is the word starting under the head and ending before the first blank.

Equations

• Algolean.Algorithms.OracleInterface.queryWord contents = match contents.head with | none => [] | some bit => bit :: List.filterMap id (List.takeWhile Option.isSome contents.right.toList)

@[simp]

theorem Algolean.Algorithms.OracleInterface.queryWord_mk₁ (input : List Bool) : queryWord (Cslib.Turing.BiTape.mk₁ input) = input

Reading a word placed on the initial tape gives back exactly that word.

def Algolean.Algorithms.OracleInterface.ask {tm : Cslib.Turing.SingleTapeTM Bool} (interface : OracleInterface tm) : Prog (TMQuery tm) Unit

This program issues a request and leaves the answer in the machine state.

Equations

• interface.ask = Cslib.FreeM.lift (Algolean.Algorithms.TMQuery.update interface.request)

def Algolean.Algorithms.OracleInterface.step {tm : Cslib.Turing.SingleTapeTM Bool} [DecidableEq tm.State] {α β : Type} (interface : OracleInterface tm) (oracle : List Bool → Bool) (q : TMQuery tm α) (next : α → Prog (TMQuery tm) β) (s : TMState tm) : FuelExecMonad.Step (TMQuery tm) (TMState tm) TMCost β

One instruction follows the ordinary rules, except that setting the request state obtains an answer from the solver.

Equations

• One or more equations did not get rendered due to their size.
• interface.step oracle (Algolean.Algorithms.TMQuery.write symbol) next_2 s = (Algolean.Algorithms.TMQuery.write symbol).step next_2 s
• interface.step oracle (Algolean.Algorithms.TMQuery.move direction) next_2 s = (Algolean.Algorithms.TMQuery.move direction).step next_2 s
• interface.step oracle (Algolean.Algorithms.TMQuery.branchCode condition yes no) next_2 s = (Algolean.Algorithms.TMQuery.branchCode condition yes no).step next_2 s
• interface.step oracle (Algolean.Algorithms.TMQuery.whileCode condition body) next_2 s = (Algolean.Algorithms.TMQuery.whileCode condition body).step next_2 s

@[reducible, inline]

abbrev Algolean.Algorithms.OracleInterface.interpreter {tm : Cslib.Turing.SingleTapeTM Bool} [DecidableEq tm.State] (interface : OracleInterface tm) (oracle : List Bool → Bool) : FuelExecMonad.Interpreter (TMQuery tm) (TMState tm) TMCost

These execution rules use the shared runner to handle fuel, program sequencing, and costs. Requests work inside branches and loops.

Equations

• interface.interpreter oracle = { step := fun {α β : Type} => interface.step oracle, step_bind := ⋯ }

@[reducible, inline]

abbrev Algolean.Algorithms.OracleInterface.model {tm : Cslib.Turing.SingleTapeTM Bool} [DecidableEq tm.State] (interface : OracleInterface tm) (oracle : List Bool → Bool) : ModelStateM (TMQuery tm) (TMQuery.ExecutionM tm) TMCost

This model records the results and costs of executing programs with access to the solver.

Equations

• interface.model oracle = (interface.interpreter oracle).toModel

@[reducible, inline]

abbrev Algolean.Algorithms.OracleInterface.execute {tm : Cslib.Turing.SingleTapeTM Bool} [DecidableEq tm.State] {α : Type} (interface : OracleInterface tm) (oracle : List Bool → Bool) (fuel : ℕ) (p : Prog (TMQuery tm) α) (s : TMState tm) : Option (AddWriter TMCost α × FuelExecState (TMState tm))

The shared execution function runs the program with the supplied solver, starting state, and fuel.

Equations

• interface.execute oracle fuel p s = Algolean.Algorithms.FuelExecMonad.execute (interface.model oracle) fuel p s

@[simp]

theorem Algolean.Algorithms.OracleInterface.execute_ask_succ {tm : Cslib.Turing.SingleTapeTM Bool} [DecidableEq tm.State] (interface : OracleInterface tm) (oracle : List Bool → Bool) (fuel : ℕ) (s : TMState tm) : interface.execute oracle (fuel + 1) interface.ask s = have answer := if oracle (queryWord s.config.BiTape) = true then interface.yes else interface.no; some ({ ret := (), tell := { steps := 1, cellsAllocated := 0 } }, { machine := { config := have __src := s.config; { state := some answer, BiTape := __src.BiTape }, headPos := s.headPos, cellsAllocated := s.cellsAllocated, cellsVisited := s.cellsVisited }, fuel := fuel })

A request costs one time step and one unit of fuel. The answer is recorded in the machine state, while the tape and head position stay unchanged.

theorem Algolean.Algorithms.OracleInterface.step_cellsAllocated {tm : Cslib.Turing.SingleTapeTM Bool} [DecidableEq tm.State] {α β : Type} (interface : OracleInterface tm) (oracle : List Bool → Bool) (q : TMQuery tm α) (next : α → Prog (TMQuery tm) β) (s : TMState tm) : s.cellsAllocated.card + (interface.step oracle q next s).cost.cellsAllocated = (interface.step oracle q next s).machine.cellsAllocated.card

One instruction counts exactly the cells it adds to the recorded tape range.

theorem Algolean.Algorithms.OracleInterface.execute_cellsAllocated {tm : Cslib.Turing.SingleTapeTM Bool} [DecidableEq tm.State] {α : Type} (interface : OracleInterface tm) (oracle : List Bool → Bool) (fuel : ℕ) (p : Prog (TMQuery tm) α) (s : TMState tm) (result : AddWriter TMCost α) (final : TMQuery.ExecutionState tm) (h : interface.execute oracle fuel p s = some (result, final)) : s.cellsAllocated.card + result.tell.cellsAllocated = final.machine.cellsAllocated.card

The final number of recorded tape cells is the initial number plus the cells newly counted during execution. Requests preserve this accounting.