TM ↔ Generalized Shift (Moore 1991)
TM ↔ Generalized Shift (Moore 1991)
Moore's Theorem 7: any Turing machine is conjugate to a generalized shift via state-into-tape encoding. Bisimulation with σ = 1, τ = 1.
Reference: C. Moore, Generalized shifts: unpredictability and undecidability in dynamical systems, Nonlinearity 4 (1991) 199-230.
Setup
SetEnvironment["PATH"->Environment["PATH"]<>":"<>FileNameJoin[{$HomeDirectory,".elan","bin"}]]PacletDirectoryLoad[FileNameJoin[{NotebookDirectory[],"..","Resources","LeanLink","LeanLink"}]];Get["LeanLink`"]leanProjectDir=FileNameJoin[{NotebookDirectory[],"..","Lean"}]gs=ResourceFunction["GeneralizedShift"]
1. Machine Definitions
Turing Machine (BiTM)
Turing Machine (BiTM)
Bi-infinite tape TM: state in {0, ..., s}, symbols in {0, ..., k-1}, state 0 = halted.
Import[FileNameJoin[{NotebookDirectory[],"..","Resources","TuringMachine","Proofs","BiTM","Basic.lean"}],"Text"]//Style[#,"Code"]&
Generalized Shift
Generalized Shift
Stateless machine on a bi-infinite tape. The active cell (value ≥ k) encodes the head position and state.
Import[FileNameJoin[{leanProjectDir,"Machine","GS","Defs.lean"}],"Text"]//Style[#,"Code"]&
2. Encoding
Moore's encoding merges the TM state into the tape cell at the head position. Extended alphabet of size s*k + k: plain cells 0..k-1, active cells A(q, c) = k + (q-1)*k + c.
Import[FileNameJoin[{leanProjectDir,"Proof","TMtoGS.lean"}],"Text"]//Style[#,"Code"]&
3. Validation
Define a 2-state 2-color TM and run the equivalent generalized shift. converts TM rules to a GS spec and evolves it using Moore's encoding internally.
ResourceFunction["GeneralizedShift"]
tmRules={{1,0}->{2,1,1},{1,1}->{1,1,-1},{2,0}->{1,1,-1},{2,1}->{2,0,1}};nSteps=30;
gsSpec=gs[tmRules];gsResult=gs[gsSpec,{{0,0,0},1},nSteps];
ArrayPlot[gsResult[[All,2]],Frame->False,ImageSize->600,PlotLabel->"GS evolution (active cell encodes TM state)"]
4. Lean Verification
Import the Lean proof and inspect the formalization:
env=LeanImportString[Import[FileNameJoin[{leanProjectDir,"Proof","TMtoGS.lean"}],"Text"],"ProjectDir"->leanProjectDir]
Formalized constants
Formalized constants
Keys[env]//Select[StringContainsQ["GS"]]
Key definitions and theorems
Key definitions and theorems
Grid[{#,env[#]["Kind"],env[#]["TypeForm"]}&/@{"GS.encodeActive","GS.decodeActive","GS.encodeBiTM","GS.decodeBiTM","GS.fromBiTM","GS.decodeActive_encodeActive","GS.decode_encode","GS.step_commutes"},Frame->All,Alignment->Left]
Core bisimulation statement
Core bisimulation statement
The theorem asserts that one BiTM step corresponds to exactly one GS step under Moore's encoding:
step_commutes
env["GS.step_commutes"]["TypeForm"]
Dependency graph
Dependency graph
env["GS.step_commutes"]["ExprGraph"]
Proof status
Proof status
Theorems with are type-checked but not yet fully proved:
sorry
sorryConstants=Select[Keys[env],StringContainsQ["GS"]];Grid[{#,env[#]["Kind"]}&/@sorryConstants,Frame->All,Alignment->Left]