FANDOM


Work in progress, but you know how I never finish what I sta

I'm slowly assembling all the pieces for writing \(\Sigma(n)\) in first-order set theory. Since \(\Sigma(n)\) is a well-known and well-respected function, it'd be nice to bound Rayo's function with it despite having Xi and FGH.

This code is an abstraction of what the final FOST formula will look like; I'll be writing a short paper on this bound.

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)

FOST feels like a stone-age ancestor of Scheme. Someday we'll have a program that compiles a dialect of Scheme into FOST.

Ad blocker interference detected!


Wikia is a free-to-use site that makes money from advertising. We have a modified experience for viewers using ad blockers

Wikia is not accessible if you’ve made further modifications. Remove the custom ad blocker rule(s) and the page will load as expected.