Turing Machine Emulator in FOST (First-Order Set Theory)

N is a fixed positive integer written into the final formula.

// Halting state
HALT = N
// States, not including halt
States* = N
// States, including halt
States = N ∪ {HALT} = N + 1
// Colors
Colors = {0, 1}
// Left and Right movements. The values don't matter as long as they're different.
Moves = {L, R}
L ≠ R

IsRuleset?(func) ->
Is func a ruleset for a 2-color N-state TM?

// Ensure that all members of the function are of the form ((State, Color), (State', Color', Move))
// Note that (a, b, c) is a shortcut for (a, (b, c))
∀x: x ∈ func ⇔
(∃s,c,s',c',m:
x = ((s, c), (s', c', m)) ∧
s ∈ States* ∧
c ∈ Colors ∧
s' ∈ States ∧
c' ∈ Colors ∧
m ∈ Moves)
// Ensure that for each (State, Color) there is exactly one (State', Color', Move)
∀s: ∀c: (s ∈ States* ∧ c ∈ Colors) →
(∃s',c',m:
s' ∈ States* ∧
c' ∈ Colors ∧
m ∈ Moves
(∀x: ((s, c), x) ∈ func ⇔ x = (s', c', m)))

IsTape?(func) ->

Is func a 2-color tape?

// Ensure that all members of the function are of the form (Pos, Color)
∀x: x ∈ func ⇔
(∃p,c:
x = (p, c) ∧
p ∈ ω ∧
c ∈ Colors)
// Ensure that for each Pos there is exactly one Color
∀p: p ∈ ω →
(∃c: c ∈ Colors ∧ (∀x: (p, x) ∈ func ⇔ x = c))

InitializeTape() -> (tape)
Creates a zero-filled tape.

∀x: x ∈ tape ⇔ (∃p: (p, 0) = x ∧ p ∈ ω)

Shift(tape, fill) -> (tape')
Shifts the tape over by one step, adding a zero at the left.

∀x: x ∈ tape' ⇔
((∃p,c: (Sp, c) = x ∧ (p, c) ∈ tape) ∨
(x = (0, fill)))

Read(tape, position) -> (color)
Read a color at a certain position.

(position, color) ∈ tape

Write(tape, position, color) -> (tape')
Write a color at a certain position.

∀x: x ∈ tape' ⇔
(∃p,c: (p, c) = x ∧ ((p ≠ position ∧ (p, c) ∈ tape) ∨
(p = position ∧ c = color))) // This is an example of an if statement in FOST

Transition(ruleset, tape, state, position) -> (tape', state', position')
Simulates one step of a Turing machine with a given ruleset, returning the altered tape, state, and position.

(state', color', move) = Apply(ruleset, (state, Read(tape, position))) ∧
(tape' = Shift(Write(tape, position, color'), 0)) ∧
((move = L ∧ position' = position) ∨ (move = R ∧ position' = S(S(position))))

Steps(ruleset) -> (steps)
Simulates a Turing machine, returning a set with all the steps.

∀tape',state',pos': (tape', state', pos') ∈ Steps ⇔
(IsTape?(tape') ∧ state' ∈ States ∧ pos' ∈ ω ∧
((tape' = InitializeTape() ∧ state' = 0 ∧ pos' = 0) ∨
(∃tape,state,pos: (tape, state, pos) ∈ Steps ∧
IsTape?(tape) ∧ state ∈ States* ∧ pos ∈ ω ∧
Transition(ruleset, tape, state, pos) = (tape', state', pos'))))

Output(ruleset) -> (output)

∀tape',count': (tape', count') ∈ CountOnes ⇔
(IsTape?(tape') ∧ count' ∈ ω ∧
((tape' = InitializeTape() ∧ count' = 0) ∨
(∃tape,count: (tape, count) ∈ Steps ∧
IsTape?(tape) ∧ count ∈ ω ∧
((tape' = Shift(tape, 0) ∧ count' = count) ∨
(tape' = Shift(tape, 1) ∧ count' = S(count))))))

(∃t,p: (t, HALT, p) ∈ Steps(ruleset) ∧ (output = Apply(CountOnes, t))) ∨
(¬∃t,p: (t, HALT, p) ∈ Steps(ruleset) ∧ (output = 0))

∀ruleset: IsRuleset?(ruleset) ⇔ Output(ruleset) ∈ Outputs

T = Max(Outputs)