Notation for single-tape TM programs

Enable with open scoped TMQuery. A do [TMQuery tm] block fixes the machine for its instructions.

• tape ←ₜ symbol writes a fixed Option Symbol, with none representing blank.
• state ←ₜ label updates the control state.
• moveₜ direction moves left, right, or stays in place.
• tape =ₜ symbol and state =ₜ label are machine conditions; notₜ negates one.
• ifₜ condition then ... else ... and whileₜ condition do ... select and repeat fixed bodies.

Conditions remain syntax, and every instruction returns Unit. The notation adds no queries. Instruction notation and control-flow unexpanders also display programs in this syntax.

def Algolean.Algorithms.TMQuery.tmWrite : Lean.ParserDescr

Write the symbol under the tape head.

Equations

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

def Algolean.Algorithms.TMQuery.tmUpdate : Lean.ParserDescr

Set the control-state label.

Equations

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

def Algolean.Algorithms.TMQuery.tmMove : Lean.ParserDescr

Move the tape head in a fixed direction.

Equations

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

def Algolean.Algorithms.TMQuery.«termTape=ₜ_» : Lean.ParserDescr

Test the head symbol without returning it to Lean.

Equations

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

def Algolean.Algorithms.TMQuery.«termState=ₜ_» : Lean.ParserDescr

Test an optional control-state label without returning it to Lean.

Equations

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

def Algolean.Algorithms.TMQuery.termNotₜ_ : Lean.ParserDescr

Negate a machine condition.

Equations

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

def Algolean.Algorithms.TMQuery.doElemIfₜ_Then__Else_ : Lean.ParserDescr

A machine-controlled branch with indented program bodies.

Equations

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

def Algolean.Algorithms.TMQuery.doElemWhileₜ_Do_ : Lean.ParserDescr

A machine-controlled loop with an indented program body.

Equations

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

def Algolean.Algorithms.TMQuery.tmBlock : Lean.ParserDescr

Specify the query type once for every instruction in a program block.

Equations

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

def Algolean.Algorithms.TMQuery.unexpandBranch : Lean.PrettyPrinter.Unexpander

Display a machine branch using its indented notation.

Equations

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

def Algolean.Algorithms.TMQuery.unexpandWhile : Lean.PrettyPrinter.Unexpander

Display a machine loop using its indented notation.

Equations

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