scatur icon indicating copy to clipboard operation
scatur copied to clipboard

A Turing Machine encoded in the scala type system

#+TITLE: README.org #+AUTHOR: Mike (stew) O'Connor #+EMAIL: [email protected] #+DATE: 2012-05-19 Sat #+LANGUAGE: en #+OPTIONS: H:3 num:t toc:t \n:nil @:t ::t |:t ^:t -:t f:t *:t <:t #+OPTIONS: TeX:t LaTeX:t skip:nil d:nil todo:t pri:nil tags:not-in-toc #+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js #+EXPORT_SELECT_TAGS: export #+EXPORT_EXCLUDE_TAGS: noexport

This project creates implements a Turing Machine using the scala type system, which are run completely by the compiler. The turing machine and initial state are encoded using the scala type system and implicit defs and implicit vals, and the final state of the Turing machine (if one can be calculated) is determined at compile time

This is probably not useful, other than being an interesting exploration of what is possible with the scala type system.

  • The Turing Machine

    The turing machine we are trying to implement is a single tape turing machine. The tape is made up of cells which can be in one of three states: One, Zero, X.

    The machine is always looking at one particular cell.

    The machine is a finite state machine. Each state has transitions defined which describe the next state of the machine based on the current state of the machine and the current cell being looked at.

  • The Finite State Machine

    There are three types of states the state machine might be in:

    • Halt The program terminates when reaching this state, there is only one instance of this state

    • LeftState When the machine arrives in a state which is a left state, the tape is re-positioned so that the machine is looking at a cell which is to the left of the previous current cell

    • RightState When the machine arrives in a state which is a left state, the tape is re-positioned so that the machine is looking at a cell which is to the left of the previous current cell

  • Examples ** AddOne

    Here we describe a simple machine which can add one to a binary number.

    It is assumed that the Machine starts looking at the most significant byte of a number, with the less significant digits to the right. The program should increment this binary number and terminate with the machine looking at the most significant digit.

    The Machine starts in the FindEnd state. It remains in the find end state until we find the cell to the right of the least significant digit.

    The machine transitions to the Adding state. During the adding state, it scans to the left, looking for a 0 or X it can replace with a 1. After which we have successfully incremented the number.

    Then the machine Enters the FindBeginning state, which just scans to the left looking for and X, at which point we are one cell to the left of the most significant digit.

    Then the RightOneMore state just advances the tape to the right so we are pointing at the MSD.

    In this diagram, state transitions are labeled N:M which means, follow this transition if the tape is pointing at N, and replace the N with M.

#+BEGIN_EXAMPLE
1:1 0:0 +----+ +----+ | | | | | v | v +- ------------ -+ | FindEnd(right) | +----------------+ | | X:X | v +------- -+ | Adding(left) | +------- -+
X:1 | | ^ 0:1 | | 1:0 | | +-----+ V
+---------------------+
| FindBeginning(left) | +---------------------+
| | X:X | V 0:0 +---------------------+ 1:0 +------+ | RightOneMore(right) | -----------> | Halt | +---------------------+ +------+ #+END_EXAMPLE

** AddOne implementation

The implementation of the AddOne turing machine is found in src/test/scala/add.scala

First we create state objects to represent all the states of the turing machine:

#+BEGIN_EXAMPLE
class FindEnd extends RightState case object FindEnd extends FindEnd

class Adding extends LeftState case object Adding extends Adding

class FindBeginning extends LeftState case object FindBeginning extends FindBeginning

class RightOneMore extends RightState case object RightOneMore extends RightOneMore

#+END_EXAMPLE

Then we add Transitions between all the states as implicit vals:

#+BEGIN_EXAMPLE
implicit val findEndOne = TransitionFindEnd.type, FindEnd.type, One.type, One.type implicit val findEndZero = TransitionFindEnd.type, FindEnd.type, Zero.type, Zero.type implicit val findEndX = TransitionFindEnd.type, Adding.type, X.type, X.type

implicit val addingOne = TransitionAdding.type, Adding.type, One.type, Zero.type implicit val addingZero = TransitionAdding.type, FindBeginning.type, Zero.type, One.type implicit val addingX = TransitionAdding.type, FindBeginning.type, X.type, One.type

implicit val fbOne = TransitionFindBeginning.type, FindBeginning.type, One.type, One.type

implicit val fbZero = TransitionFindBeginning.type, FindBeginning.type, Zero.type, Zero.type

implicit val fbX = TransitionFindBeginning.type, RightOneMore.type, X.type, X.type

implicit val romX = TransitionRightOneMore.type, Halt.type, X.type, X.type implicit val romOne = TransitionRightOneMore.type, Halt.type, One.type, One.type implicit val romZero = TransitionRightOneMore.type, Halt.type, Zero.type, Zero.type #+END_EXAMPLE

Then we create the starting tape that has the number 0b1101 in the
expected starting position

#+BEGIN_EXAMPLE
val startTape = Tape( X :: TNil, One, One :: Zero :: One :: X :: X :: TNil)

#+END_EXAMPLE

We create a val named completed which is the result of running the
Turing machine:

#+BEGIN_EXAMPLE
val completed = startTape.run(FindEnd) #+END_EXAMPLE

HOWEVER! we don't actually have to run the program.  In the
process of compiling this program, the scalac compiler has already
figured out what the type of completed is, which is the Tape at
the time that the Turing Machine halts.  And since the Tape has
all of the cells encoded in the type, we already know what the
ending state of the Tape is. 

We can verify at compile time that we get the result we are expecting:

#+BEGIN_EXAMPLE
// this is a utility to witness that a type is the type we think it // is without influencing the compiler's type inference def typed[T](t : => T) {}

// if this compiles, then "completed" is the type we think it is typedTape[X :: TNil, One, One :: One :: Zero :: X :: X :: TNil ] #+END_EXAMPLE

And we verify that that our Turing machine added one to 0b1101 and got 0b1110

** AddTwoNumbers

  • Credits:

I couldn't have done this without the pioneering work that Miles Sabin has done in this area. The implementation of the heterogeneous lists that encode the tape are lifted right from his [[https://github.com/milessabin/shapeless][shapeless]] project.

  • License

    This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

    This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

    You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/.