As you know in computation theory, there is a simple programming language equivalent in power to Turing machines. It is described as follows:Values: natural numbers only, but of unlimited precision. Variables: Input variables X1, X2, X3, . . .  An output variable Y -Local variables Z1, Z2, Z3, . . .  Instructions: 1 ) $V  V + 1$ Increase by 1 the value of the variable V .2 ) $V  V  1$ If the value of V is 0, leave it unchanged; otherwise decrease by 1 the value of V.3 ) $ IF \;V \neq 0\; GOTO \;L$ , If the value of V is nonzero, perform the instruction with label L next; otherwise proceed to the next instruction in the list.  Labels: A1, B1, C1, D1, E1, A2, B2, C2, D2, E2, A3, . . .  Exit label: E.  All variables and labels are in the global scope . for example the following program computes f(x) such that if x = 0 , f(x) = 1 otherwise f(x) = x\begin{align}[A] \quad &X  X  1 \\    &Y  Y + 1 \\    &IF\; X \neq 0\; GOTO \;A \\ \end{align}this language can use infinite number of variables.What restrictions should be added to this language so its power will be the same as Linear Bounded Automata? One of them is clear about the variables but I will appreciate if anybody helps me about any others, if they exist. I have searched a lot but I couldn't find any source that describes both topics. I would appreciate any relevant pointers.
Restrictions to counter machines capturing LBA
computability;turing machines;linear bounded automata
Programs with natural numbers as data and as instructions increment, decrement and zero test are know as register machines or counter automata. (Wikipedia cites several sources, usually I refer to Minsky). Their power is that of the Turing machine, that is, they accept recursively enumerable sets (strings or numbers).Thus they are more general than the LBA, which is more a complexity class (as mentioned in the comments). The length of the space used for computations is linear, otherwise the LBA are Turing Machines.  To translate that restriction to counter automata I would suggest to restrict the variables to at most exponential in the size (length) of the input. First, you can code such variable by markers on the tape. That would prove one inclusion. I expect that every LBA can be simulated by an exponentially bounded counter automaton, after all, the tape is just a number an writing on the tape is changing a digit. There is a standard construction that translates the two sides of the tape (right and left from the reading position) as two numbers, and moving the head is just a multiplication/division, deciding the element under the reading head is modulo counting. You need extra counters (variables) for these operations and in particular you need the zero test.