Transporting stack-machine statements into a larger machine #
def
GapCVP.liftStatement
{K : Type u_1}
{K' : Type u_2}
{Λ : Type u_3}
{Λ' : Type u_4}
{σ : Type u_5}
{σ' : Type u_6}
{Γ : K' → Type u_7}
(stack : K → K')
(label : Λ → Λ')
(read : σ' → σ)
(write : σ' → σ → σ')
(onHalt : Turing.TM2.Stmt Γ Λ' σ')
:
Turing.TM2.Stmt (fun (k : K) => Γ (stack k)) Λ σ → Turing.TM2.Stmt Γ Λ' σ'
Embed stack and label indices, preserve extra state through a read/write interface, and replace the halt instruction with a caller-supplied continuation.
Equations
- One or more equations did not get rendered due to their size.
- GapCVP.liftStatement stack label read write onHalt (Turing.TM2.Stmt.push k f q) = Turing.TM2.Stmt.push (stack k) (fun (s : σ') => f (read s)) (GapCVP.liftStatement stack label read write onHalt q)
- GapCVP.liftStatement stack label read write onHalt (Turing.TM2.Stmt.load f q) = Turing.TM2.Stmt.load (fun (s : σ') => write s (f (read s))) (GapCVP.liftStatement stack label read write onHalt q)
- GapCVP.liftStatement stack label read write onHalt (Turing.TM2.Stmt.goto next) = Turing.TM2.Stmt.goto fun (s : σ') => label (next (read s))
- GapCVP.liftStatement stack label read write onHalt Turing.TM2.Stmt.halt = onHalt
Instances For
theorem
GapCVP.liftStatement_stepAux
{K : Type u_1}
{K' : Type u_2}
{Λ : Type u_3}
{Λ' : Type u_4}
{σ : Type u_5}
{σ' : Type u_6}
{Γ : K' → Type u_7}
[DecidableEq K]
[DecidableEq K']
(stack : K → K')
(label : Λ → Λ')
(read : σ' → σ)
(write : σ' → σ → σ')
(onHalt : Turing.TM2.Stmt Γ Λ' σ')
(state : σ → σ')
(embedStacks : ((k : K) → List (Γ (stack k))) → (k : K') → List (Γ k))
(configuration : Turing.TM2.Cfg (fun (k : K) => Γ (stack k)) Λ σ → Turing.TM2.Cfg Γ Λ' σ')
(read_state : ∀ (s : σ), read (state s) = s)
(write_state : ∀ (s t : σ), write (state s) t = state t)
(read_stacks : ∀ (source : (k : K) → List (Γ (stack k))) (k : K), embedStacks source (stack k) = source k)
(update_stacks :
∀ (source : (a : K) → List (Γ (stack a))) (k : K) (value : List (Γ (stack k))),
embedStacks (Function.update source k value) = Function.update (embedStacks source) (stack k) value)
(goto_configuration :
∀ (l : Λ) (s : σ) (source : (k : K) → List (Γ (stack k))),
configuration { l := some l, var := s, stk := source } = { l := some (label l), var := state s, stk := embedStacks source })
(halt_configuration :
∀ (s : σ) (source : (k : K) → List (Γ (stack k))),
Turing.TM2.stepAux onHalt (state s) (embedStacks source) = configuration { l := none, var := s, stk := source })
(statement : Turing.TM2.Stmt (fun (k : K) => Γ (stack k)) Λ σ)
(s : σ)
(source : (k : K) → List (Γ (stack k)))
:
Turing.TM2.stepAux (liftStatement stack label read write onHalt statement) (state s) (embedStacks source) = configuration (Turing.TM2.stepAux statement s source)
A stack/state embedding that commutes with reads and updates transports an entire statement execution. Only the caller's goto and halt configurations need separate proofs.