Turing Machine Parser

This module provides a parser for defining a Turing machine from a simple string description. The main entry point is the turing_machine% elaborator, which takes a string representing the machine's transitions and constructs a term of type Machine (Fin m) StateType where StateType is an inductive type generated on the fly.

Encoding format

The machine's transitions are encoded as a single string, with each state's transitions separated by an underscore (_). For each state, a 3m-character substring defines the behavior:

• The first 3 characters "ABC" describe the action when the head reads 0:
  • A: The symbol to write (0, 1, ..., m-1).
  • B: The direction to move the head (L or R).
  • C: The new state (A through Z).
• The next 3 characters "DEF" describe the action when the head reads 1 using the same format.
• The next 3 characters "GHI" describe the action when the head reads 2 using the same format.
• So on...

The character Z is reserved for the halting state. The string "---" can be used to represent a transition to the halting state without writing or moving.

Example of a tape: 1RA0LB_0LA---

There are more examples in ForMathlib/Test/Computability.

def mkMachineMatchAltExpr (L : List String) (stateName : Lean.Name) (numSymbols numStates : ℕ) : Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAltExpr))

Take as input a list of strings and return an array of matchAltExpr syntaxes mapping (state, symbol) pairs to actions of a Turing Machine, given by a term of type Option (State n).

Equations

• One or more equations did not get rendered due to their size.

def mkStateType (n : ℕ) (stateName : Lean.Name) : Lean.Elab.TermElabM Unit

mkStateType n adds to the environment an inductive type with n states names State{n} with constructors the symbols A, B, ..., together with the instance Inhabited (State{n}).

Equations

• One or more equations did not get rendered due to their size.

def parseTuring (descr : String) : Lean.Elab.TermElabM Lean.Expr

parseTuring tmStringDescription outputs the Expr corresponding to the Turing Machine described by the string tmStringDescription.

To do so, it

1. Runs mkStateType to add the state type to the environment
2. Defines the corresponding Turing Machine as a function using the match syntax.

Warning: if a state type (i.e. something with the name State1, State2, ...) already exists in the environment then this will be reused without checking that this is the right inductive type - such checks are left to the user.

Equations

• One or more equations did not get rendered due to their size.

def «termTuring_machine%_» : Lean.ParserDescr

turing_machine% tmStringDescription outputs a term of type Machine Γ Λ where Γ = Fin 2 and Λ is an inductive type constructed on the fly with constructors A, B, ..., and named State{n} where n is the number of states of the machine.

Warning: if State{n} already exists in the environment then this will be reused without checking that this is the right inductive type - such checks are left to the user.

Equations

• One or more equations did not get rendered due to their size.