Talk:Tack
Proof of Turing completeness
Assuming that the stack can store unbounded integers, Tack is Turing complete.
Instructions can be represented as a one-hot vector encoded into non-! and ! for 0 and 1, respectively. While a more compressed representation is possible, it is unnecessary.
For clarity, the following names will be used for the following instructions:
Mnemonic | Opcode | Normalized Tack |
---|---|---|
swap |
5 | ....!...................... |
pop |
6 | .....!..................... |
jmp |
9 | ........!.................. |
div |
10 | .........!................. |
2 |
12 | ...........!............... |
dup |
13 | ............!.............. |
mul |
14 | .............!............. |
add |
15 | ..............!............ |
jnz |
21 | ....................!...... |
equ |
22 | .....................!..... |
not |
23 | ......................!.... |
Arbitrary numbers can be pushed to the stack by constructing them via powers of 2. When compiling, convert the constant number k into binary and for each bit starting from LSB + 1 (bit 1), and going MSBwards, with the current bit number n, add the following if the bit is set:
2 (repeated n many times) mul (repeated n - 1 many times)
If LSB is set, add:
2 2 div
Then, add popcount(k) - 1
many add
instructions where popcount(k) is the amount of set bits in k.
Jumps are done by first pushing a constant, then jumping to it, with the target immediately popping the value.
target: pop {body} other : pop (push target's address) jmp {body}
The program must start with a jump to one of these labeled sections.
An issue with this is alignment, jumps forward may move the label's address forward due to the pushing of the constant taking up more than one instruction.
If we have a fixed but arbitrarily large bitwidth for instruction addresses, then we can have a fixed maximum number of instructions per constant, equal to:
3 + sum([2n-1 for n in range(1, bit_width)])
For any representation using fewer instructions, simply insert enough no-ops (27 non-!) to fill the space.
With this, jumps use a fixed number of instructions determined at compile time.
To make conditional jumps easier, there are 2 pops at each label, instead of just one. Each constant push occurs after a constant push of nonzero (e.g 2
). This way, nonconditional jumps and conditional jumps behave the same. The beginning of the program must therefore have a nonzero push as well as a jump.
We organize the stack as a single element. This element is the counter.
Multiply by a constant is simple, using our constant construction system, we simply push a constant using our method for jumps, then multiply.
{push constant} mul
Division is more complex, as we will need to determine if the number is divisible. We do this by performing the division on temporary spaces, then checking if the constant times the division is equal to the original number. Note: the elements in [] illustrate the stack's state.
dup dup [ctr, ctr, ctr] {push constant} [ctr, ctr, ctr, con] div [ctr, ctr, ctr/con] {push constant} [ctr, ctr, ctr/con, con] mul [ctr, ctr, (ctr/con)*con] equ [ctr, 0 if not divisible/1 if divisible] not [ctr, 1 if not divisible/0 if divisible] jnz after pop pop {push constant} div 2 jmp label after: pop pop
Where jnz/jmp {label}
pushes the constant address of a label, then performs a jnz
or jmp
. All of the {push constant}
refer to the same compile-time constant.
Thus, a multiply and divide with divisibility test Minsky machine can be translated into Tack. Therefore, Tack is Turing complete.
Assumptions:
- Math operators work like in other stack languages where they pop two elements, then push (next of stack OP top of stack), such that
push(3) push(1) sub
is 2 and not -2. If it is reversed, simply insert a swap before each of the math operators used. - Division ultimately produces integers only. The exact rounding method does not matter.
- Equality testing pops two elements and pushes nonzero if they are equal, 0 otherwise.
- Logical negation pops a value and pushes nonzero if it is zero, zero otherwise.