Finite stack subroutines and their interfaces
Lax218471.Subroutine · concepts/Lax218471/Subroutine.lean · lax-218471
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A subroutine has access to the caller's stacks and finite control, together with a private finite collection of working stacks and private finite control. At entry and return its private stacks are empty and its private control is reset. Execution counts actual TM2 transitions. This interface makes repeated calls and preservation of unrelated caller data explicit.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Computability.TuringMachine.Computable |
| 2 | import Mathlib.Data.Fintype.Sum |
| 3 | import Mathlib.Data.Fintype.Prod |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Finite stack subroutines and their interfaces |
| 8 | type: definition |
| 9 | --- |
| 10 | A subroutine has access to the caller's stacks and finite control, together |
| 11 | with a private finite collection of working stacks and private finite control. |
| 12 | At entry and return its private stacks are empty and its private control is |
| 13 | reset. Execution counts actual TM2 transitions. This interface makes repeated |
| 14 | calls and preservation of unrelated caller data explicit. |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax218471.Subroutine |
| 18 | |
| 19 | open Turing |
| 20 | |
| 21 | /-- The data visible to a caller between subroutine calls. -/ |
| 22 | structure Store {K : Type} (Γ : K → Type) (σ : Type) where |
| 23 | state : σ |
| 24 | stk : ∀ k, List (Γ k) |
| 25 | |
| 26 | /-- An ordinary finite TM2 program with a private working region. -/ |
| 27 | structure Routine {K : Type} (Γ : K → Type) (σ : Type) where |
| 28 | W : Type |
| 29 | [workEq : DecidableEq W] |
| 30 | [workFin : Fintype W] |
| 31 | Δ : W → Type |
| 32 | τ : Type |
| 33 | [stateFin : Fintype τ] |
| 34 | initial : τ |
| 35 | Label : Type |
| 36 | [labelFin : Fintype Label] |
| 37 | entry : Label |
| 38 | code : Label → TM2.Stmt (Sum.elim Γ Δ) Label (σ × τ) |
| 39 | |
| 40 | namespace Routine |
| 41 | |
| 42 | variable {K σ : Type} {Γ : K → Type} (p : Routine Γ σ) |
| 43 | |
| 44 | instance : DecidableEq p.W := p.workEq |
| 45 | instance : Fintype p.W := p.workFin |
| 46 | instance : Fintype p.τ := p.stateFin |
| 47 | instance : Fintype p.Label := p.labelFin |
| 48 | |
| 49 | /-- A boundary configuration contains no private working data. -/ |
| 50 | def boundary (l : Option p.Label) (s : Store Γ σ) : |
| 51 | TM2.Cfg (Sum.elim Γ p.Δ) p.Label (σ × p.τ) where |
| 52 | l := l |
| 53 | var := (s.state, p.initial) |
| 54 | stk := fun | .inl k => s.stk k | .inr _ => [] |
| 55 | |
| 56 | /-- Exact execution from a clean entry to a clean return. -/ |
| 57 | def Executes [DecidableEq K] (s t : Store Γ σ) (n : ℕ) : Prop := |
| 58 | (fun c => c.bind (TM2.step p.code))^[n] (some (p.boundary (some p.entry) s)) = |
| 59 | some (p.boundary none t) |
| 60 | |
| 61 | end Routine |
| 62 | end Lax218471.Subroutine |
| 63 |
Builds on
none
Used by
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments