0
$\begingroup$

Introduction

I'm trying to formalize (generalized) Turing machines in Mizar (Wikipedia) and I'm looking for the optimal way to formalize the (generalized) tape. Note that you don't need familiarity with the system to answer. I will present two ways for formalization and I ask you to think of different approaches that may be suited for the task. The best answer (after some reasonable time, a moth or so) will be judged by the following criteria in that order:

  1. How good the approach is explained. Something like "use groups" isn't sufficient and not in the spirit of the site, I expect detailed answers. If you haven't just thought of that approach yourself but seen it somewhere, please provide a reference.
  2. How easy the approach can be understood by undergraduate students who just completed their first course introducing Turing machines.
  3. How easy it seems to be implemented in Mizar with the use of the current library. (Note that you don't need to judge that, so please don't let your unfamiliarity with the system get in the way of your fancy ideas.)

I know this question has a strongly subjective flavour. I've read the "What types of questions should I avoid asking?" site in the help center and tried hard to make a constructive subjective question. My motivation is to learn more about formalizations, I'm not asking you to make my task easier. In fact, any but the second approach I'll present would possibly make it harder since I've already sketched that approach in Mizar. The motivation for this question comes from my other question, where one comment (which I sadly cannot comprehend in this short form) from Derek Elkins was:

@SK19 In that case, I would take a more "axiomatic"/"abstract" approach. Instead of trying to pick a "most general" representation, avoid picking any representation. For example (just a random idea I thought up just now which is probably terrible), maybe it makes sense to have the transition function return the generators of a group, and the tape is a set acted upon by that group (and it's values are just a function from the set to the alphabet). 1D 1-sided is $\mathbb{Z}$ acting on $\mathbb{N}$. 2D $\langle U,R | UR=RU\rangle$ acting on $\mathbb{N}\times\mathbb{N}$.

The most obvious approach

So everyone can think of the tape of the classical Turing machine as a function $\mathbb{Z}\rightarrow\Sigma$ where $\mathbb{Z}$ describes the set of integers. For a $d$-dimensional TM one simple uses $\mathbb{Z}^d\rightarrow\Sigma$, for a $k$-band TM $\{0,\ldots,k-1\}\times\mathbb{Z}\rightarrow\Sigma$ would be enough. Now if we want to generalize this concept, one could say let $D$ be a non empty subset of $\mathbb{Z}^d$ for some positive $d$ and let the "tape" be a function $D\rightarrow\Sigma$. This generalization is simple to understand, but $D$ could be disconnected, making parts of it useless for the actual machine. A definition is needed (in Mizar) to grasp the concept of "connectedness" in Subsets of $\mathbb{Z}^d$ which effectively (in terms of work in Mizar) leads to

The second most obvious approach

Instead of thinking of subsets of a specific metric space where two cells are connected if their distance is 1 (in the previous case, $D$ as a metric subspace of $(\mathbb{R}^d, ||.||_1)$, we omit the notion what set of cells we are talking about and only care if two cells are connected or not. In short, we use graphs. And while we are at it, we use digraphs where loops are allowed and the machine head can only go from one vertex to another if there is an edge in this direction. This even allows "teleports" on the tapes and so this can easily be seen as a generalization of the previous concept with more tape moves allowed. Looking at $k$-band TMs shows that we need a number of heads with their own underlying graphs to enable easy independent movement. Of course, for a $d$-dimensional TM we need only 1 head, but the underlying graph has to be an $d$-dimensional grid.
I think this is still understandable for students. An obvious drawback is that the transition function becomes much more complicated, because there are no simple directions left, but a set of vertices to go to, which can differ depending on which vertex the head looks right now. Luckily, going back to regular graphs the old notion of the transition function can be given in terms of the new one again, so the usability for problems that simple use classical TMs wouldn't be restricted in Mizar.

If you feel familiar with the second approach, please check out this question.

Thanks for your input in advance!

$\endgroup$
  • $\begingroup$ Since a one tape Turing machine is a $1$-band, the definition of a classical Turing machine is included in the definition of a $k$-band Turing machine. So does your problem just stand in : how to include $d$-dimensional TMs in your definition ? $\endgroup$ – user80502 Jan 24 '18 at 18:29
  • $\begingroup$ @AbdousKamel While I would be more found of general definitions to allow e.g. TMs with a circular tape, this would be sufficient, I guess. $\endgroup$ – SK19 Jan 25 '18 at 9:56
  • $\begingroup$ You missed the point of my comment which is the first two sentences. The example just clouds the issue hence Andrej's following comment on that question which I upvoted. You are still trying to think up some suitably "general" representation. I assume you have some experience writing software, so just think about what interfaces a Turing machine would need for its "tape". This may (or may not) lead to an interface that is like a group (or more likely a monoid) action but you don't have to even realize that (let alone be an expert in group theory). $\endgroup$ – Derek Elkins Feb 3 '18 at 1:33
  • $\begingroup$ Imagine you were writing a simple minimax AI for board games. The approach you're taking is like thinking: "Well, the boards might be different sizes so I'll allow any size, they might also be 1D or 3D so I'll allow any dimensionality, but they may not be (hyper)rectangles, so I'll consider arbitrary subsets, but there may be some important notion of distance so I'll consider weighted graphs, but the positions might be colored, so I'll allow arbitrary node labelings" and so forth. $\endgroup$ – Derek Elkins Feb 3 '18 at 1:40
  • $\begingroup$ What I'm suggesting is the following thought process: "I need to be given a starting board state. All I need to know about board states is what new board states are reachable from it and what score it should be assigned." This leads to something like the C# interface interface BoardState<T : BoardState<T>> { List<T> NextStates(); double Value(); } This handles all the variations of board state in the previous comment and many others, because the minimax algorithm doesn't actually care what the "board" is. This way you don't impose a (complicated) representation upon the user. $\endgroup$ – Derek Elkins Feb 3 '18 at 1:40

Your Answer

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

Browse other questions tagged or ask your own question.