What is the type signature of a Turing Machine?

Question

Maybe my question is a bad question, but if it is, I want to know eactly how it is a bad question.

Suppose we have some Turing machien $M$ that takes as input a natural number $n$ in the form of a binary string, writes $n^2$ in binary on its output tape, and then halts.

What is the type signature of this machine? Here is why I am confused:

• We can treat $M$ as a function: $M(\cdot)$ denotes the function that maps $n\mapsto n^2$, which suggests that it has type $\{0,1\}^*\to\{0,1 \}^*$

• But $M$, intuitively speaking, is not a function, but a "device". This means that we can extract more information from it. e.g. potentially we could define $M_{235}(\cdot)$ to be the function that takes an input and outputs: "what is the string on the output tape after 235 steps, given this input?".

• In the formal definition, a turing machine is a tuple $M=\langle Q,\Gamma ,b,\Sigma ,\delta ,q_{0},F\rangle$ (with some properties on these elements). But I am confused about how this tuple relates to type theory. Is this the "type signature" of $M$? If so, what kind of type theory captures this kind of type?

Answer 1

Usually, Turing machines are presented using set theory rather than type theory.

There might be many ways to represent a TM in type theory, each one with its advantages and disadvantages. I would not represent it as a function $\{0,1\}^* \to\{0,1\}^*$ since the function implemented by a TM is a partial function, because the TM might fail to terminate, while in type theory functions are total.

If we wanted to follow the set theoretic definition, we might define a TM as a dependent tuple. This tuple would include:

• $\Sigma:\sf Type$ a type representing the tape "alphabet"
• $Q:\sf Type$ a type representing the states
• $b:\Sigma$ the blank symbol
• $q_0 : Q$ the initial state
• $\delta : Q \to \Sigma \to (Q \times \Sigma \times 3)$ for the transition function (assuming a deterministic TM) where $3=1+1+1$ represents the directions
• $F : Q \to 2$ with $2=1+1$ the halting states

Technically, this would be a huge dependent sum such as

$$ \sum_{\Sigma\sf Type} \sum_{Q:\sf Type} \Sigma \times Q \times (Q\to \Sigma \to(Q\times \Sigma\times 3))\times(Q\to 2) $$

The above would be a possible representation of a TM. (I'm unsure it would be a very good one, especially if we work without functional extensionality, but I'll neglect that.)

In a similar way one could define the type of the configurations of a TM ${\sf Conf}\ T$ and a step function $step: {\sf Conf}\ T \to 1 + {\sf Conf}\ T$ (the $1+$ is to report "no next step" when the TM halts).

One could even define a function to run $n$ steps, or a predicate for "the TM $T$ on input $x$ halts with output $y$".

$$ \begin{array}{l} {\sf runTM} : \prod_{T:TM} {\sf Conf}\ T \to \mathbb N \to 1+{\sf Conf}\ T \\ {\sf semanticsTM} : \prod_{T:TM} (\pi_{\Sigma} T)^* \to (\pi_{\Sigma} T)^* \to \sf Type \end{array} $$

Answer 2

One could see a type as a subset of values, among all the possible values. For instance, int is the type of all the bitstrings on 8 bits.

However, a Turing machine does restrict the values it works with: it is untyped.

Now, when you look at the definition of a Turing machine, you can ask yourself whether the (meta)language in which this definition is written has types and if the definition statement is well-typed. Here I used say that the answers are "yes". For instance, you can give a type to, say, $\delta$ which is consistant with the types of $b$, of the elements in $Q$, $\Gamma$, etc.