Occurrence programs with word oracles

The existing shared machine program separates occurrence-index queries from word-oracle calls. Its List interpreter keeps the oracle's private state local to each branch: sibling occurrences start with the same state, while successive calls within a branch share the updated state. The observer records every live transition index, including indices of query instructions. Equal actions at different positions remain distinct occurrences.

This is an interpretation of MultiTapeMachine.runConfigFrom, not another machine model. A query instruction costs one native transition; request construction and reply-head access use ordinary transitions. The oracle's computation is external. Retaining a complete reply in this semantic configuration is not a claim that an encoded interpreter can copy it at unit cost.

Main definitions

• Turing.MultiTapeMachine.occurrenceOracleSpec: separate occurrence and word-query interfaces.
• Turing.MultiTapeMachine.runOccurrenceProgram: the existing shared run with occurrence choices.
• Turing.MultiTapeMachine.occurrenceTraceHandler: branch-local state and an occurrence observer.
• Turing.MultiTapeMachine.runOccurrenceTrace: full configurations, traces and private states.

Main results

• Turing.MultiTapeMachine.interpret_runOccurrenceProgram_succ: actual indexed transitions.
• Turing.MultiTapeMachine.runOccurrenceTrace_erase: erasure gives the ordinary interpretation.

The raw clocked run retains live endpoints. Attempting an empty local list has no outcome. Neither the List interpretation nor a clock alone asserts nonblocking, halting or polynomial-time realizability. In particular, the generic PMF-based MultiTapeMachine.HaltsWithin is not used: the occurrence interface includes Fin 0, which admits no probability distribution.

References

Reuses the shared native machine and program infrastructure credited in MultiTape.Machine and MultiTape.Machine.Program, and occurrence enumeration from MultiTape.Counting.Program. The typed oracle calculus credits Samuel Schlesinger, Devon Tuma, Quang Dao and VCVio in Languages.Probabilistic.Basic. Language-oracle/path-counting conventions are described in L. Fortnow, Counting Complexity, Section 2 and Definition 3.1; arbitrary stateful word handlers here are an explicit generalization of the language-oracle interface.

@[reducible, inline]

abbrev Turing.MultiTapeMachine.occurrenceOracleSpec (Operation Symbol : Type) : ℕ ⊕ Operation × List Symbol → Type

Occurrence positions and external word calls are separate effects.

def Turing.MultiTapeMachine.runOccurrenceProgram {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (fuel : ℕ) (cfg : Config k Symbol Control Operation input) : Cslib.OracleComp (occurrenceOracleSpec Operation Symbol) (Config k Symbol Control Operation input)

The shared clocked program with occurrence choices and actual buffered word queries.

def Turing.MultiTapeMachine.occurrenceTraceHandler {Symbol Operation S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (q : ℕ ⊕ Operation × List Symbol) : StateT (List ℕ × S) List (occurrenceOracleSpec Operation Symbol q)

Enumerate occurrences with separate copies of the incoming state. Queries update only the state of their own branch; the trace records indices, not external calls or terminal padding.

def Turing.MultiTapeMachine.runOccurrenceTrace {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (fuel : ℕ) (cfg : Config k Symbol Control Operation input) {S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (s : S) : List ((List ℕ × Config k Symbol Control Operation input) × S)

Observe the shared run from an empty trace, retaining live cutoff configurations.

@[simp]

theorem Turing.MultiTapeMachine.runOccurrenceProgram_zero {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (cfg : Config k Symbol Control Operation input) : machine.runOccurrenceProgram 0 cfg = pure cfg

theorem Turing.MultiTapeMachine.runOccurrenceProgram_halted {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (fuel : ℕ) {cfg : Config k Symbol Control Operation input} (h : cfg.tapes.state = none) : machine.runOccurrenceProgram fuel cfg = pure cfg

No further occurrence or oracle call is made after halting.

theorem Turing.MultiTapeMachine.interpret_runOccurrenceProgram_succ {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (fuel : ℕ) (cfg : Config k Symbol Control Operation input) (state : Control) (h : cfg.tapes.state = some state) {S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (trace : List ℕ) (s : S) : (Cslib.OracleComp.interpret (occurrenceTraceHandler oracle) (machine.runOccurrenceProgram (fuel + 1) cfg)).run (trace, s) = List.flatMap (fun (index : Fin (machine.tr state cfg.tapes.inputSymbol cfg.tapes.workTapeSymbols cfg.answerSymbols).length) => match (machine.tr state cfg.tapes.inputSymbol cfg.tapes.workTapeSymbols cfg.answerSymbols)[index] with | Action.step action symbol move => (Cslib.OracleComp.interpret (occurrenceTraceHandler oracle) (machine.runOccurrenceProgram fuel (cfg.step action symbol move))).run (trace ++ [↑index], s) | Action.query op next => match oracle (op, (cfg.channels op).queryBuffer) s with | (answer, nextState) => (Cslib.OracleComp.interpret (occurrenceTraceHandler oracle) (machine.runOccurrenceProgram fuel (cfg.receive op next answer))).run (trace ++ [↑index], nextState)) (List.ofFn id)

One live instruction preserves index order and threads private state only along its branch.

def Turing.MultiTapeMachine.occurrenceHandler {Symbol Operation S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (q : ℕ ⊕ Operation × List Symbol) : StateT S List (occurrenceOracleSpec Operation Symbol q)

The same branch-local interpreter without the trace observer.

theorem Turing.MultiTapeMachine.interpret_occurrenceTraceHandler_erase {Symbol Operation S α : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (program : Cslib.OracleComp (occurrenceOracleSpec Operation Symbol) α) (trace : List ℕ) (s : S) : List.map (fun (x : α × List ℕ × S) => match x with | (a, fst, state) => (a, state)) ((Cslib.OracleComp.interpret (occurrenceTraceHandler oracle) program).run (trace, s)) = (Cslib.OracleComp.interpret (occurrenceHandler oracle) program).run s

Erasing the observer preserves the ordinary interpretation and the complete private state.

theorem Turing.MultiTapeMachine.runOccurrenceTrace_erase {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (fuel : ℕ) (cfg : Config k Symbol Control Operation input) {S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (s : S) : List.map (fun (x : (List ℕ × Config k Symbol Control Operation input) × S) => match x with | ((fst, final), state) => (final, state)) (machine.runOccurrenceTrace fuel cfg oracle s) = (Cslib.OracleComp.interpret (occurrenceHandler oracle) (machine.runOccurrenceProgram fuel cfg)).run s

The recorded run differs from the ordinary shared-program interpretation only by its log.