Turing machine
From HaskellWiki
EndreyMark (Talk  contribs) (Explaning the motivation, why a  →Tagging structure: has been incorporated in the Turing machine definition language) 
EndreyMark (Talk  contribs) (Citing original source of the idea of  →Tagging structure: and its relatedness to Haskell and functional programming) 

Line 66:  Line 66:  
===== Tagging structure ===== 
===== Tagging structure ===== 

−  As we can see, this Turing machine definition language language has an algebraically motivated tagging structure. 
+  As we can see, this Turing machine definition language has an algebraically motivated tagging structure. I have taken the idea from Haskell's sumlike datatypes (<hask>Maybe</hask>, <hask>Maybe2</hask>, <hask>Either</hask>) and from the continuationpassingstyle implementation of sumlike datatypes ([[Combinatory logic#Direct sumdirect sum]] and [[Combinatory logic#MaybeMaybe]]) in [[Combinatory logic]] (see also [http://www.madore.org/~david/programs/unlambda/#howto_lists Unlambda's union type]). 
This tagging structure makes such programs (i.e Turing machine definitions) more readable, that make use of different namespaces for symbols and states. 
This tagging structure makes such programs (i.e Turing machine definitions) more readable, that make use of different namespaces for symbols and states. 
Revision as of 12:18, 1 May 2006
Contents 
1 Introduction
2 Variants
There are several variants of defining the concept of a Turing machine. These varants can be classified across several aspects. I shall classify possible variants in terms of two questions:
 how the machine behaves at transitions
 how the the running of the machine terminates
2.1 A classifying aspect
2.1.1 Transition
I make a distinction between sumlike and productlike transition behavior:
 productlike transition
 means that the head moves and writes at each transition (this may have a funny consequence: sometimes, we have to undo the last moving step of the head at the end of running  i.e. there may remain a superfluous last moving that has to be undone). Maybe that is why some of these variants extend the moving possibilities: besides left, right there is also an idle move.
 sumlike transition
 means that the head moves or writes at each transition (never both). [Mon:MathLog] describes this approach. I like this approach better, because it looks more ecomical conceptually (we do not have to undo any superfluous final movings, nor do we need to introduce idle moves) and because it looks nicer for me even conceptually.
2.1.2 Halting
Halting can be done in several ways  a (second) special state (final state), or a special action (termination action) etc... Here, I avoid the concept of halting state. The only special state is the starting state, but I do not overload the concept of state in any other way  halting is achieved in another way
2.2 A construct called Maybe2
Sumlike transition and avoiding the concept halting state  they look like two independent, orthogonal aspects. But a construct (called data Maybe2 a b = Nothing2  Just2 a b
2.3 Moves
There are variants of the Turing machine concept also accross other problems, e.g. how the head and the tape moves related from each other: which is regarded as moving, which is immobile.
Using the facts that
 the head is
 finite (even if the states are included)
 and even limited, even constant (having fixed a concrete Turing machine): it does not grow during a run
 the tape is infinite, or (in some approaches to Turing machine concept) finite but unlimited, maintaining dynamically its approporiate size
I prefer a convention taken from a physical view: I regard the head as being mobile even if it is made from the heaviest transuranium metal or a black hole, and tape being (or growing) immobile even if it is made of the finest membrane.
3 Turing machine definition language as a programming language
I use term Turing machine definition language for what we generally mean when talking on the language of Turing simulator softwares: a language which can represent infinite  even all possible  concrete Turing machines, so it is able to serve as an (of course Turing complete, in the most literal meaning) programming language
3.1 Syntax
I was dreaming of a syntax reflecting the conceptual structure of the main concepts  maybe reflecting even the logic of the Haskell implementation! In generally, I do not like special names (likestart
is for starting state, everything else...)  I like the concept of tags much better  I mean the concept of tags as shown in classical examples  e.g. direct sum or 3.1.1 Verbose syntax
3.1.1.1 Example
Incrementing a number represented in the tally (in other words, unary) notation:
starting : blank : move right with starting; starting : letter 1 : write letter 1 with becoming processing; becoming processing : blank : write letter 1 with becoming extended; becoming processing : letter 1 : move right with becoming processing; becoming extended : blank : stop; becoming extended : letter 1 : stop;
3.1.1.2 Tagging structure
As we can see, this Turing machine definition language has an algebraically motivated tagging structure. I have taken the idea from Haskell's sumlike datatypes (This tagging structure makes such programs (i.e Turing machine definitions) more readable, that make use of different namespaces for symbols and states.
As symbols and states are different concept, most Turing machine definition languages allow us to use te same symbol for a state and a symbol  they are simply in different namespaces. This is a natural consequence of the essential concept of Turing machine. [Mon:MathLog] leverages namespaces in an extreme way: everything  states, symbols, even actions  are coded as natural numbers.
The tagging structure enables us also to define the set of states and symbols in an easy way: no burntin presupposition is required (e.g. restricting the set of symbols for characers). Special keyword for declaring sets of states and sets of symbols are also superfluous.
3.1.1.3 Algebraic background of the tagging structure
Keywords can be classified according their corresponding type and tag coordinates, and coloring scheme can reflect this.
3.1.1.3.1 States, symbols
States and symbols are rather different concepts in the theory of Turing machines, but they both have (maybe incidentally) a common feature. It is wort of distinguishing a special state (the starting state)  and the same is true at symbols (blank symbol). This has a cosequence: the tagging structure is the same for these two rather different concepts, and this common tagging structure can be covered by Tag Maybe  

Just  Nothing  
Concept (type)  Symbol  letter

blank

State  becoming

starting

3.1.1.3.2 Result of transition
Representation of halting, and in nonhalting cases maintaing new state and action  this has also a tagging structure. It is Tag Maybe2  

Just2  Nothing2  
Concept (type)  Result of transition  with

stop

3.1.2 Concise syntax
3.1.2.1 Example
0 : _ : > / 0 0 : '1 : !'1 / @processing @processing : _ : !'1 / @extended @processing : '1 : > / @processing @extended : _ : . @extended : '1 : .
3.1.2.2 Motivation of signs
 0 signing starting state comes from David S. Woodruff's Turing machine interpreter TM
 Exclamation mark signing the concept of writing comes from the Z modelbased formal specification language, where exclamation mark is used to mark output variables
 Repeated colons signing compound cases come from the concept of currying.
 Atcharacter signing state comes from its literal meaning in natural languages (in everyday English language, as a preposition for expressing being at places times or states)  also reflected in its use in email addresses
 Apostrophe signing a (nonblank) letter comes from using apostrophes in programming languages for character literals and from using apostrophes (or upper corners) for quotations in mathematical logic
 Slashcharacter signing the concept of compound action (allowing the possibility of halting instead) comes from the theory of automata
 Dot signing termination is hard to explain. In Prolog, dot is a terminating symbol, but in another sense: it terminates syntactical units (rules and facts), not processes!
3.2 Implementation
3.2.1 Representations of main concepts
3.2.1.1 Language
module Language where import Util (Maybe2 (Nothing2, Just2)) type Turing state symbol = Turing0 (Maybe state) (Maybe symbol) type Turing0 state symbol = state > symbol > Maybe2 (Action symbol) state data Action symbol = Write symbol  Move Bool
3.2.1.1.1 Discernable nonemptyness: special state, special symbol
Most conceptual frameworks of Turing machine concept allow us a big liberty at chosing the set of states and symbols  but empty set is not allowed. Of course Haskell types are never empty, but nonemptyness provided byblank
and default state is called starting
. The presence of special symbol, special state is reflected directly in the representation of language concepts  and both are represented by This way allows us a big liberty at chosing the set of states and symbols  we do not have to restrict the user's freedom to use any types for both symbols and states. Strings, integers, enumarations, characters, booleans...
3.2.1.1.2 Halting
Another  maybe analogous  problem is the representation of halting.
There may be alternative solutions: introduction of concepts like halting state or halting action, etc... I felt that3.2.1.2 Tape
At first I wrote a circular program to make double linked list to implement a bidirectionally infinite tape. It is superfluous, there is a more simple solution:
module Tape where import Util (Stream (Cons)) data Tape a = Tp {left, right :: Stream a, cell :: a} move :: Bool > Tape a > Tape a put :: a > Tape a > Tape a get :: Tape a > a
...
3.2.1.3 Utility module
module Util where data Maybe2 a b = Nothing2  Just2 a b data Stream a = Cons a (Stream a)
3.3 Extending language
A pattern language, or some other extending possibilities, to avoid redundances. Maybe a macro language as at David S. Woodruff's Turing machine interpreter TM. Other syntactic sugar.
4 Bibliography
 [Mon:MathLog]
 Monk, J. Donald: Mathematical Logic. SpringerVerlag, New York * Heidelberg * Berlin, 1976.