# Turing machine

(Difference between revisions)
 Revision as of 23:00, 22 April 2006 (edit)m (typos, and Prolog terminology mistake correction)← Previous diff Current revision (05:32, 16 July 2012) (edit) (undo)m (→Syntax) (35 intermediate revisions not shown.) Line 1: Line 1: - __TOC__ + {{Template:Foundations infobox}} + __TOC__ == Introduction == == Introduction == - [http://en.wikipedia.org/wiki/Turing_machine Wikipedia article] + An article on Turing machines, maybe growing to a project to specify (and implement) a general purpose (toy or educational) programming language, that can describe each concrete Turing machine directly: a ''Turing machine definition language''. - == Planning a programming language: incarnating most concepts == + This article wants also to show an example how Haskell (and in general: functional programming) can have an impact on or suggest ideas even in (seemingly) entirely distant, remote areas. + + The impact of Haskell to this Turing machine definition language is more than simply using Haskell as an implementation language for this project. The very [[#Syntax|syntax]] of this Turing machine definition language (and its main feature, its [[#Tagging structure|tagging structure]]) comes directly from functional programming languages (Haskell and [[combinatory logic]]). + + == Links == + + * [http://en.wikipedia.org/wiki/Turing_machine Wikipedia article] + * [http://www.ams.org/featurecolumn/archive/turing.html Turing machines] page of the American Mathematical Society + + == Implementations == + + * Found following links from the previously mentioned AMS site: + ** [http://www.nmia.com/~soki/turing/ Virtual Turing Machine (VTM)] + ** Paul R. C. Ming's [http://infohost.nmt.edu/~prcm/turing/ Virtual Turing Machine 2 (VTM2)] + * David S. Woodruff's [http://www2.lns.mit.edu/~dsw/turing/turing.html Turing machine interpreter TM] + + == Variants == + + There are several variants of defining the concept of a Turing machine. These variants 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 + === A classifying aspect === + + ==== Transition ==== + + I make a distinction between sum-like and product-like transition behavior: + ;product-like 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. + ;sum-like 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 economical 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. + + ==== 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 + + === A construct called Maybe2 === + Sum-like transition and avoiding the concept halting state -- they look like two independent, orthogonal aspects. But a construct (called Maybe2 in a -- maybe deprecated -- Hugs library module) can implement both aspect in one construct. + + data Maybe2 a b = Nothing2 | Just2 a b + + [[Programming guidelines#Types|Programming guidelines]] page recommends to avoid using this construct, and suggests modularizing it to Maybe (a, b). But here I prefer using Maybe2, because at this particular problem (defining Turing definition language) this deconstruction pattern does not appear in any other situations, so no redundance is caused by the use of Maybe2. And, to tell the truth, I like this construct. + + === Moves === + + There are variants of the Turing machine concept also across 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 appropriate 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. + + == 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 === Syntax === === 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 (like ''start is for starting state, everything else...'') -- I like the concept of ''tag''s much better. + I was dreaming of a syntax reflecting the conceptual structure of the main concepts -- maybe reflecting even the logic of the Haskell implementation! In general, I do not like special names (like ''start is for starting state, everything else...'') -- I like the concept of ''tag''s much better -- I mean the concept of tags as shown in classical examples -- e.g. direct sum or Maybe. ==== Verbose syntax ==== ==== Verbose syntax ==== ===== Example ===== ===== Example ===== - starting : blank : move right with starting; + - starting : letter 1 : write letter 1 with becoming processing; + Incrementing a number represented in the [http://en.wikipedia.org/wiki/Tally_marks tally] (in other words, [http://en.wikipedia.org/wiki/Unary_numeral_system unary]) notation: - becoming processing : blank : write letter 1 with becoming extended + - becoming processing : letter 1 : move right with becoming processing + starting ''':''' blank ''':''' ''Move'' right '''WITH''' starting; - becoming extended : blank : stop + starting ''':''' ''Letter'' * ''':''' ''Write'' ''Letter'' * '''WITH''' ''Becoming'' processing; - becoming extended : letter '1 : stop + ''Becoming'' processing ''':''' blank ''':''' ''Write'' ''Letter'' * '''WITH''' ''Becoming'' extended; + ''Becoming'' processing ''':''' ''Letter'' * ''':''' ''Move'' right '''WITH''' ''Becoming'' processing; + ''Becoming'' extended ''':''' blank ''':''' stop; + ''Becoming'' extended ''':''' ''Letter'' * ''':''' stop; + + ==== 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 sum-like datatypes (Maybe, Maybe2, Either) and from the [[Continuation|continuation-passing-style]] implementation of sum-like datatypes ([[Combinatory logic#Direct sum|direct sum]] and [[Combinatory logic#Maybe|Maybe]]) 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. + + As symbols and states are different concept, most Turing machine definition languages allow us to use the 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 burnt-in presupposition is required (e.g. restricting the set of symbols for characters). Special keyword for declaring sets of states and sets of symbols are also superfluous. + + ==== Algebraic background of the tagging structure ==== + + Keywords can be classified according their corresponding type and tag coordinates, and coloring scheme can reflect this. + + ===== Types (represented with colors) ===== + + ;Special keywords + :are common in all Turing machines. They are colored. + ;user-given names + :are specific for a concrete Turing machine. They are colorless, more exactly, black in case of light background, and white in case of dark background. + + ====== 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 worth of distinguishing a special state (the starting state) -- and the same is true at symbols (blank symbol). This has a consequence: the ''tagging structure'' is the same for these two rather different concepts, and this common tagging structure can be covered by Maybe. + + {| border="1" cellpadding="5" cellspacing="0" + | colspan=2 rowspan = 2 | + ! colspan=2 | Tag Maybe-like + |- + ! style="background:lightgray" | Just + ! style="background:lightgray" | Nothing + |- + ! rowspan=2 | Concept (type) + ! style="background:lightgray" | Symbol + | ''Letter'' + | blank + |- + ! style="background:lightgray" | State + | ''Becoming'' + | starting + |} + + ====== Result of transition ====== + + Representation of halting, and in non-halting cases maintaining new state and action -- this has also a tagging structure. It is Maybe2. + + {| border="1" cellpadding="5" cellspacing="0" + | colspan=2 rowspan = 2 | + ! colspan=2 | Tag Maybe2-like + |- + ! style="background:lightgray" | Just2 + ! style="background:lightgray" | Nothing2 + |- + ! rowspan=2 | Concept (type) + ! style="background:lightgray" | Result of transition + | '''WITH''' + | stop + |} + + ===== Arity (represented with font) ===== + + The keywords have different arities, and it can be represented with syntax highlighting (by mapping a font type to each arity). But also pure ASCII text can contain this information by appropriate capitalization rules. + + ;Constant keywords + :are either Nothing-like things for special cases (symbol blank, state starting), the Nothing2-like solution for halting (stop), or direction constants like left, right, or user-named things (state or symbol names, varying in each concrete Turing machine). They are typeset with normal font, and it is recommended to type them without any capitals (of course, user-given state and symbol names can ignore this, because state and symbol names are part of the specific Turing machine, so the Turing machine definition language does not restrict their use). + ;''Unary'' keywords + :are one-parameter commands like ''Write'', ''Move'', or one-parameter state/symbol constructors like ''Becoming'', ''Letter''. They are typeset with italic, and just the beginning letter is capitalized. + ;'''Binary''' keywords + :like '''WITH''', but considering the idea of currying, the colon sign ''':''' is also typeset the same way: they are typeset with bold, and they are either typed with all capitals ('''WITH'''), or they consist of a symbol (''':''') ==== Concise syntax ==== ==== Concise syntax ==== Line 24: Line 155: ===== Example ===== ===== Example ===== 0 : _ : -> / 0 0 : _ : -> / 0 - 0 : '1 : !'1 / @processing + 0 : '* : !'* / @processing - @processing : _ : !'1 / @extended + @processing : _ : !'* / @extended - @processing : '1 : -> / @processing + @processing : '* : -> / @processing @extended : _ : . @extended : _ : . - @extended : '1 : . + @extended : '* : . ===== Motivation of signs ===== ===== Motivation of signs ===== * 0 signing starting state comes from David S. Woodruff's [http://www2.lns.mit.edu/~dsw/turing/turing.html Turing machine interpreter TM] * 0 signing starting state comes from David S. Woodruff's [http://www2.lns.mit.edu/~dsw/turing/turing.html Turing machine interpreter TM] - * Exclamation mark signing the concept of writing comes from the [http://www.comp.lancs.ac.uk/computing/resources/IanS/SE6/IG/Z.pdf Z model-based formal specification language], where exclamation mark is used to mark output (variables) + * Exclamation mark signing the concept of writing comes from the [http://www.comp.lancs.ac.uk/computing/resources/IanS/SE6/IG/Z.pdf Z model-based formal specification language], where exclamation mark is used to mark ''output'' variables * Repeated colons signing compound cases come from the concept of currying. * Repeated colons signing compound cases come from the concept of currying. * At-character 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 e-mail addresses * At-character 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 e-mail addresses Line 38: Line 169: * Slash-character signing the concept of ''compound action'' (allowing the possibility of halting instead) comes from the theory of automata * Slash-character 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! * 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! + + === Examples === + + Let us see some “source code” examples, mainly from [Mon:MathLog]. + + ==== Simple moves ==== + + $T_\leftarrow$ moves head one cell to the left and stops. It is identical to Definition 1.3. of [Mon:MathLog], only the notation is changed: + + starting ''':''' blank ''':''' ''Move'' left '''WITH''' ''Becoming'' ready; + starting ''':''' ''Letter'' * ''':''' ''Move'' left '''WITH''' ''Becoming'' ready; + ''Becoming'' ready ''':''' blank ''':''' stop; + ''Becoming'' ready ''':''' ''Letter'' * ''':''' stop; + + $T_\rightarrow$ moves head one cell to the right and stops. It is identical to Definition 1.5. of [Mon:MathLog], only the notation is changed: + + starting ''':''' blank ''':''' ''Move'' right '''WITH''' ''Becoming'' ready; + starting ''':''' ''Letter'' * ''':''' ''Move'' right '''WITH''' ''Becoming'' ready; + ''Becoming'' ready ''':''' blank ''':''' stop; + ''Becoming'' ready ''':''' ''Letter'' * ''':''' stop; + + ==== Simple rewritings ==== + + $T_{\!-}$ rewrites the actual cell into blank and stops. Its definition contains a nice trick, that is why it can be more concise than those of $T_\leftarrow$ and $T_\rightarrow$. It is identical to Definition 1.7. of [Mon:MathLog], only the notation is changed: + + starting ''':''' blank ''':''' stop; + starting ''':''' ''Letter'' * ''':''' ''Write'' blank '''WITH''' starting; + + $T_{\!+}$ rewrites the actual cell into non-blank and stops. Its definition is now straightforward (Definition 1.9. of [Mon:MathLog]): + + starting ''':''' blank ''':''' ''Write'' ''Letter'' * '''WITH''' starting; + starting ''':''' ''Letter'' * ''':''' stop; + + ==== Search ==== + + Let us modularize, decompose the Definition 1.12. of [Mon:MathLog]: let us separate a more simple version! + + $T_{\leftarrow^*\;0}$ seeks the first blank to the left, and it stops if it finds the blank. We inlude the starting in the process of search (i.e. it can stop immediatelly): + + starting ''':''' blank ''':''' stop; + starting ''':''' ''Letter'' * ''':''' ''Move'' left '''WITH''' starting; + + $T_{\leftarrow^+\;0}$ is more complicated. It exludes starting from the process of search: it begins with a left move unconditionally. Its definition is identical to Definition 1.12. of [Mon:MathLog] (with changed notation, talky names): + + starting ''':''' blank ''':''' ''Move'' left '''WITH''' ''Becoming'' searching; + starting ''':''' ''Letter'' * ''':''' ''Move'' left '''WITH''' ''Becoming'' searching; + ''Becoming'' searching ''':''' blank ''':''' stop; + ''Becoming'' searching ''':''' ''Letter'' * ''':''' ''Move'' left '''WITH''' ''Becoming'' searching; === Implementation === === Implementation === Line 49: Line 228: import Util (Maybe2 (Nothing2, Just2)) import Util (Maybe2 (Nothing2, Just2)) - type Turing state symbol = Turing0 (Maybe state) (Maybe symbol) + type Turing becoming letter = UnsafeTuring (Maybe becoming) (Maybe letter) - type Turing0 state symbol = state -> symbol -> Maybe2 (Action symbol) state + type UnsafeTuring state symbol = state -> symbol -> Maybe2 (Action symbol) state data Action symbol = Write symbol | Move Bool data Action symbol = Write symbol | Move Bool - ====== Defaults or non-emptyness restriction ====== + ====== Observable non-emptiness: special state, special symbol ====== - The trick of Turing0 and Maybe solves the problem of default state and symbol. I mean Turing machines allow us a big liberty at chosing the set of states and symbols -- but empty set is not allowed. This restriction is reflected directly in the representation of language concepts. Default symbol is called ''blank'' and default state is called ''start'' and both are represented by Nothing. + Most conceptual frameworks of Turing machine concept allow us a big liberty at choosing the set of states and symbols -- but empty set is not allowed. Of course Haskell types are never empty, but non-emptiness provided by undefined is not enough. We need discernible, observable non-emptiness. This restriction is reflected directly in the representation of language concepts: we require the presence of a special symbol and a special state. + The trick of Turing versus UnsafeTuring distinction with Maybe solves the problem of special state and symbol. Special symbol is called blank and special 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 Nothing. + + This way allows us a big liberty at choosing 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, enumerations, characters, booleans... ====== Halting ====== ====== Halting ====== Another -- maybe analogous -- problem is the representation of halting. Another -- maybe analogous -- problem is the representation of halting. Line 62: Line 244: ===== Tape ===== ===== Tape ===== - At first I wrote a [http://www.haskell.org/hawiki/CircularProgramming circular program] to make double linked list to implement a bidirectionally infinite tape. It is superfluous, there is a more simple solution: + At first I wrote a [[Circular programming|circular program]] to make double linked list to implement a Bi-directionally infinite tape. It is superfluous, there is a more simple solution: Line 84: Line 266: === Extending language === === Extending language === - A pattern language, or some other extending possibilities, to avoid redundances. Maybe a macro language as at David S. Woodruff's [http://www2.lns.mit.edu/~dsw/turing/turing.html Turing machine interpreter TM]. Other syntactic sugar. + A pattern language, or some other extending possibilities, to avoid redundancies. Maybe a macro language as at David S. Woodruff's [http://www2.lns.mit.edu/~dsw/turing/turing.html Turing machine interpreter TM]. Other syntactic sugar. + + == Bibliography == + + ;[Mon:MathLog] + :Monk, J. Donald: Mathematical Logic. Springer-Verlag, New York * Heidelberg * Berlin, 1976. [[Category:Theoretical foundations]] [[Category:Theoretical foundations]]

## 1 Introduction

An article on Turing machines, maybe growing to a project to specify (and implement) a general purpose (toy or educational) programming language, that can describe each concrete Turing machine directly: a Turing machine definition language.

This article wants also to show an example how Haskell (and in general: functional programming) can have an impact on or suggest ideas even in (seemingly) entirely distant, remote areas.

The impact of Haskell to this Turing machine definition language is more than simply using Haskell as an implementation language for this project. The very syntax of this Turing machine definition language (and its main feature, its tagging structure) comes directly from functional programming languages (Haskell and combinatory logic).

## 4 Variants

There are several variants of defining the concept of a Turing machine. These variants 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

### 4.1 A classifying aspect

#### 4.1.1 Transition

I make a distinction between sum-like and product-like transition behavior:

product-like 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.
sum-like 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 economical 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.

#### 4.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

### 4.2 A construct called Maybe2

Sum-like transition and avoiding the concept halting state -- they look like two independent, orthogonal aspects. But a construct (called
Maybe2
in a -- maybe deprecated -- Hugs library module) can implement both aspect in one construct.
data Maybe2 a b = Nothing2 | Just2 a b
Programming guidelines page recommends to avoid using this construct, and suggests modularizing it to
Maybe (a, b)
. But here I prefer using
Maybe2
, because at this particular problem (defining Turing definition language) this deconstruction pattern does not appear in any other situations, so no redundance is caused by the use of
Maybe2
. And, to tell the truth, I like this construct.

### 4.3 Moves

There are variants of the Turing machine concept also across 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

• 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 appropriate 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.

## 5 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

### 5.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 general, I do not like special names (like start 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
Maybe
.

#### 5.1.1 Verbose syntax

##### 5.1.1.1 Example

Incrementing a number represented in the tally (in other words, unary) notation:

starting : blank : Move right WITH starting;
starting : Letter * : Write Letter * WITH Becoming processing;
Becoming processing : blank  : Write Letter * WITH Becoming extended;
Becoming processing : Letter * : Move right WITH Becoming processing;
Becoming extended : blank : stop;
Becoming extended : Letter * : stop;


#### 5.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 sum-like datatypes (
Maybe
,
Maybe2
,
Either
) and from the continuation-passing-style implementation of sum-like datatypes (direct sum and Maybe) in Combinatory logic (see also 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.

As symbols and states are different concept, most Turing machine definition languages allow us to use the 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 burnt-in presupposition is required (e.g. restricting the set of symbols for characters). Special keyword for declaring sets of states and sets of symbols are also superfluous.

#### 5.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.

##### 5.1.3.1 Types (represented with colors)
Special keywords
are common in all Turing machines. They are colored.
user-given names
are specific for a concrete Turing machine. They are colorless, more exactly, black in case of light background, and white in case of dark background.
###### 5.1.3.1.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 worth of distinguishing a special state (the starting state) -- and the same is true at symbols (blank symbol). This has a consequence: the tagging structure is the same for these two rather different concepts, and this common tagging structure can be covered by
Maybe
.
 Tag Maybe-like Just Letter blank Becoming starting
###### 5.1.3.1.2 Result of transition
Representation of halting, and in non-halting cases maintaining new state and action -- this has also a tagging structure. It is
Maybe2
.
 Tag Maybe2-like Just2 WITH stop
##### 5.1.3.2 Arity (represented with font)

The keywords have different arities, and it can be represented with syntax highlighting (by mapping a font type to each arity). But also pure ASCII text can contain this information by appropriate capitalization rules.

Constant keywords
are either
Nothing
-like things for special cases (symbol blank, state starting), the
Nothing2
-like solution for halting (stop), or direction constants like left, right, or user-named things (state or symbol names, varying in each concrete Turing machine). They are typeset with normal font, and it is recommended to type them without any capitals (of course, user-given state and symbol names can ignore this, because state and symbol names are part of the specific Turing machine, so the Turing machine definition language does not restrict their use).
Unary keywords
are one-parameter commands like Write, Move, or one-parameter state/symbol constructors like Becoming, Letter. They are typeset with italic, and just the beginning letter is capitalized.
Binary keywords
like WITH, but considering the idea of currying, the colon sign : is also typeset the same way: they are typeset with bold, and they are either typed with all capitals (WITH), or they consist of a symbol (:)

#### 5.1.4 Concise syntax

##### 5.1.4.1 Example
0 : _ : -> / 0
0 : '* : !'* / @processing
@processing : _ : !'* / @extended
@processing : '* : -> / @processing
@extended : _ : .
@extended : '* : .

##### 5.1.4.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 model-based formal specification language, where exclamation mark is used to mark output variables
• Repeated colons signing compound cases come from the concept of currying.
• At-character 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 e-mail addresses
• Apostrophe signing a (non-blank) letter comes from using apostrophes in programming languages for character literals and from using apostrophes (or upper corners) for quotations in mathematical logic
• Slash-character 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!

### 5.2 Examples

Let us see some “source code” examples, mainly from [Mon:MathLog].

#### 5.2.1 Simple moves

$T_\leftarrow$ moves head one cell to the left and stops. It is identical to Definition 1.3. of [Mon:MathLog], only the notation is changed:

starting : blank : Move left WITH Becoming ready;
starting : Letter * : Move left WITH Becoming ready;
Becoming ready : blank : stop;
Becoming ready : Letter * : stop;


$T_\rightarrow$ moves head one cell to the right and stops. It is identical to Definition 1.5. of [Mon:MathLog], only the notation is changed:

starting : blank : Move right WITH Becoming ready;
starting : Letter * : Move right WITH Becoming ready;
Becoming ready : blank : stop;
Becoming ready : Letter * : stop;


#### 5.2.2 Simple rewritings

$T_{\!-}$ rewrites the actual cell into blank and stops. Its definition contains a nice trick, that is why it can be more concise than those of $T_\leftarrow$ and $T_\rightarrow$. It is identical to Definition 1.7. of [Mon:MathLog], only the notation is changed:

starting : blank : stop;
starting : Letter * : Write blank WITH starting;


$T_{\!+}$ rewrites the actual cell into non-blank and stops. Its definition is now straightforward (Definition 1.9. of [Mon:MathLog]):

starting : blank : Write Letter * WITH starting;
starting : Letter * : stop;


#### 5.2.3 Search

Let us modularize, decompose the Definition 1.12. of [Mon:MathLog]: let us separate a more simple version!

$T_{\leftarrow^*\;0}$ seeks the first blank to the left, and it stops if it finds the blank. We inlude the starting in the process of search (i.e. it can stop immediatelly):

starting : blank : stop;
starting : Letter * : Move left WITH starting;


$T_{\leftarrow^+\;0}$ is more complicated. It exludes starting from the process of search: it begins with a left move unconditionally. Its definition is identical to Definition 1.12. of [Mon:MathLog] (with changed notation, talky names):

starting : blank : Move left WITH Becoming searching;
starting : Letter * : Move left WITH Becoming searching;
Becoming searching : blank : stop;
Becoming searching : Letter * : Move left WITH Becoming searching;


### 5.3 Implementation

#### 5.3.1 Representations of main concepts

##### 5.3.1.1 Language
module Language where

import Util (Maybe2 (Nothing2, Just2))

type Turing becoming letter = UnsafeTuring (Maybe becoming) (Maybe letter)
type UnsafeTuring state symbol = state -> symbol -> Maybe2 (Action symbol) state
data Action symbol = Write symbol | Move Bool
###### 5.3.1.1.1 Observable non-emptiness: special state, special symbol
Most conceptual frameworks of Turing machine concept allow us a big liberty at choosing the set of states and symbols -- but empty set is not allowed. Of course Haskell types are never empty, but non-emptiness provided by
undefined
is not enough. We need discernible, observable non-emptiness. This restriction is reflected directly in the representation of language concepts: we require the presence of a special symbol and a special state. The trick of
Turing
versus
UnsafeTuring
distinction with
Maybe
solves the problem of special state and symbol. Special symbol is called blank and special 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
Nothing
.

This way allows us a big liberty at choosing 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, enumerations, characters, booleans...

###### 5.3.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 that
Maybe2
(Hugs has this data type in a library module) is a conceptually esthetic solution.
##### 5.3.1.2 Tape

At first I wrote a circular program to make double linked list to implement a Bi-directionally 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

...

##### 5.3.1.3 Utility module
module Util where

data Maybe2 a b = Nothing2 | Just2 a b
data Stream a = Cons a (Stream a)

### 5.4 Extending language

A pattern language, or some other extending possibilities, to avoid redundancies. Maybe a macro language as at David S. Woodruff's Turing machine interpreter TM. Other syntactic sugar.

## 6 Bibliography

[Mon:MathLog]
Monk, J. Donald: Mathematical Logic. Springer-Verlag, New York * Heidelberg * Berlin, 1976.