Type System Turing Machine

It is possible to emulate a Turing machine in the Ceylon type system. We can store the entire configuration of a Turing machine – its current state and its tape – in a single type, and define a function that performs a single step of the Turing machine, returning the type for the next state.

The fundamental idea is that a function can declare multiple return types by returning a union of several type “branches”, and we assure that for every possible input (type arguments), exactly one branch will not be nothing. For example, given disjoint types A1 and A2, the return type of

I&A1 & X |
I&A2 & Y
    fun<I>(I i)
        given I of A1 | A2
        => nothing;

is assignable to

  • X if I is assignable to A1, and
  • Y if I is assignable to A2.

The other branch will always be reduced to Nothing because it includes the intersection of the disjoint types A1 and A2.

However, if we want to define a function that “swaps” between A1 and A2, we can’t do this:

I&A1 & A2 |
I&A2 & A1
    fun<I>(I i)
        given I of A1 | A2
        => nothing;

The result of this function is always Nothing, because while logically only the last part (A2 / A1) is the result we want, the typechecker only sees that we have an intersection of disjoint types here. To separate the result from the “selector”, we can use generics. Given a “box” type

interface Box<out T> {
    shared formal T first;

we can write the function like this:

I&A1 & B<A2> |
I&A2 & B<A1>
    fun<I>(B<I> i)
        given I of A1 | A2
        => nothing;

Note that the parameter also has the type B<I> rather than I, so that we can feed fun’s result into fun again directly.

Of course, our box can also hold more than one type. To emulate a Turing machine, we need to hold three things:

  • The current state of the Turing machine,
  • a stack representing the tape to the left of the Turing machine’s head, and
  • a stack representing the tape to the right of the Turing machine’s head.

The representation of the tape as two stacks also implicitly records the position of the head.

The stack is represented through a linked list of types, similar to Tuple:

shared interface RightSideStack
        of RightStackHead<Symbol, Stack> | RightStackEnd {
    shared formal Symbol first;
    shared formal RightSideStack rest;
shared interface RightStackHead<out Element, out Rest>
        satisfies RightSideStack
        given Element satisfies Symbol
        given Rest satisfies RightSideStack {
    shared actual formal Element first;
    shared actual formal Rest rest;
shared interface RightStackEnd
        satisfies RightSideStack {
    shared actual formal Nothing first;
    shared actual formal Nothing rest;

We also have LeftSideStack, LeftStackHead and LeftStackEnd, which are identical; we need to have two separate stack interfaces so that we can test them independently: If we had only one set of stack interfaces, and we tested that the right-side stack is a StackHead and the left-side stack is a StackEnd, we would end up with the type Nothing (because StackHead and StackEnd are disjoint).

The tape abc can now be represented through the type

    Symbol_A, RightStackHead<
        Symbol_B, RightStackHead<
            Symbol_C, RightStackEnd>>>

Now, we can begin defining the function that performs a Turing machine iteration. First, it needs a lot of type parameters:

<out CurrentState, out LeftStack, out LeftRest, out RightStack, out RightRest, out Left, out Right>
(B<CurrentState, LeftStack, RightStack> state, Left left, LeftRest leftRest, Right right, RightRest rightRest)
        given CurrentState satisfies State
        given Left satisfies Symbol
        given Right satisfies Symbol
        given LeftRest satisfies LeftSideStack
        given RightRest satisfies RightSideStack
        given LeftStack of LeftStackEnd|LeftStackHead<Left, LeftRest>
                     satisfies LeftSideStack
        given RightStack of RightStackEnd|RightStackHead<Right, RightRest>
                     satisfies RightSideStack

The return type is the union of all the “branches”. For each possible state of the Turing machine and each possible input symbol, as well as the option that the tape ends, we construct a branch as the intersection of:

  • CurrentState,
  • the tested state,
  • either:
    1. if we’re testing for an input symbol:
      • Right,
      • the tested symbol, OR
    2. if we’re testing for the end of the tape:
      • RightStack,
      • RightStackEnd
  • if we want to move left, there are two branches:
    1. check if we can move left:
      • LeftStack,
      • LeftStackHead<Symbol, LeftSideStack>, as well as
    2. check if we can’t move left:
      • LeftStack,
      • LeftStackEnd,
  • the box around:
    • the next state,
    • the left stack:
      1. if we’re moving left, depending on which branch from above we’re in:
        1. if we can move left: LeftRest
        2. if we can’t move left: LeftStackEnd
      2. if we’re not moving: LeftStack
      3. if we’re moving right: LeftStackHead around
        • the written symbol,
        • LeftStack
    • the right stack:
      1. if we’re moving left: RightStackHead around
        • depending on which branch from above we’re in:
        • if we can move left: Left,
        • if we can’t move left: the blank symbol
        • RightStack
      2. if we’re not moving: RightStackHead around
        • the written symbol,
        • RightRest
      3. if we’re moving right: RightRest

For example, for the transition

When in state SkipOverX and reading X, write X, move right, and stay in state SkipOverX

we produce the following branch:

State&State_SkipOverX & Right&Symbol_X & Box<State_SkipOverX, LeftStackHead<Symbol_X, LeftStack>, RightRest>

This is all done by the createTuringMachine() function.

The useTuringMachine() function creates a “driver” function for this Turing machine. For every iteration of the Turing machine, this function contains one value, which is derived from the previous one like this:

value s002 = t(s001, s001.second.first, s001.second.rest, s001.third.first, s001.third.rest);

(second and third are members of Box that yield the left and right stack, respectively.)

It also initializes the Turing machine by constructing an initial stack (tape) from the given input word.

The last iteration is then assigned to a value of type Accept. Accept is an alias that was created by createTuringMachine(); it’s a box around the union of all accepting states of the Turing machine (and any left and right stack). If the Turing machine accepts the input word after the last iteration, then this assignment is well-typed; otherwise, it isn’t well-typed, and will have a typechecker error.

The most important thing to note is that createTuringMachine() doesn’t know the input word, and useTuringMachine() doesn’t know the Turing machine, so the emulation of the Turing machine must really be happening in the type system.

leftSource Codeshared left left
noneSource Codeshared none none
Source Codeshared right right
createTuringMachineSource Codeshared CompilationUnit createTuringMachine(Set<String> states, Set<Character> symbols, Set<Character> inputSymbols, String initialState, Set<String> acceptingStates, [String, Character, Movement] transition(String state, Character symbol), String? stateDescription(String state) = ..., String? symbolDescription(Character symbol) = ...)

Creates the type system Turing machine.

  • states

    The set of states in which the turing machine can be.

  • symbols

    The set of symbols that can be written onto the tape (excluding the blank symbol).

  • inputSymbols

    The set of symbols that can be on the tape initially. Must be a subset of symbols.

  • initialState

    The initial state. Must be an element of states.

  • acceptingStates

    The accepting states. Must be a subset of states.

  • transition

    The transition function.


    1. next state,
    2. symbol to write,
    3. movement
  • stateDescription = stat

    Optionally: Descriptions for the states.

  • symbolDescription = ymbo

    Optionally: Descriptions for the symbols.

useTuringMachineSource Codeshared CompilationUnit useTuringMachine(String word, Integer iterations, String functionName = ...)

Creates a driver for the type system turing machine.

  • functionName = "run"
MovementSource Codeshared abstract Movement
TuringMachineCreatorSource Codeshared TuringMachineCreator

Creates the components of the type system Turing machine.

leftSource Codeshared left
noneSource Codeshared none
Source Codeshared right
IllegalStateExceptionSource Codeshared IllegalStateException
IllegalSymbolExceptionSource Codeshared IllegalSymbolException