1
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ In case we might get into the XY problem, can you tell us why you are interested in "the type signature of a Turing Machine"? In plain words, for a function/procedure/subroutine/method (method in short) in a programming language, its type signature defines how code/program can call that method with appropriate input and expect appropriate output. That is why we are interested in the type signature of methods (and, similarly, in classes and so on). $\endgroup$ – Apass.Jack Oct 29 '18 at 7:05
  • $\begingroup$ @Apass.Jack, I am asking this because (1) I want to conceptually clarify the "ontological status" (not sure if that's the right word) of various objects in math and computer science such as Turing Machines. I am learning recently about type theory which has clarified my understanding of pure math and thereby has helped me in practical math applications. (2) I think that clarifying what the relation is between type theory, and objects like Turing machines, will both help me understand type theory better, and think more clearly about pure math and CS concepts like Turing Machines. (3) I think $\endgroup$ – user600670 Oct 29 '18 at 7:17
  • $\begingroup$ this is especially helpful if I connect it to concrete things that I know about programming (e.g. what would the datatype of a pure math object be if we encoded it in a computer program, or in a dependent type theory-based theorem prover). That's why I'm asking what the "type signature" of a Turing machine is. (Btw, even if this question is not a question that is "typically asked", I am still interested in it for conceptual clarification purposes.) $\endgroup$ – user600670 Oct 29 '18 at 7:18
2
$\begingroup$

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} $$

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ "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." This is really not standard in type theory as far as I know, and definitiely not what I'm interested in. $\endgroup$ – user600670 Oct 29 '18 at 8:03

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.