Piet is Turing-complete

I proved Turing-completeness of the programming language Piet by defining a translation from brainfuck to Piet.

translation approach

1. Correspond brainfuck's tape and piet's stack.

• The top of the piet's stack must equal to the value that the brainfuck's pointer indicates.
• The second top must equal to current index of pointer, plus 3.
• The third top must equal to total length of the whole tape, plus 3.
• The remain part of the stack must equal to data of type except the value on the current pointer.

For example, the following brainfuck's tape:

+---+---+---+---+---+---+
| A | B | C | D | E | F |
+---+---+---+---+---+---+
              ^
           pointer

corresponds to the following piet's stack:

(top) D 6 9 A B C E F (bottom)
 where 6 is current index of pointer + 3
       9 is total length of tape + 3

2. Define auxiliary functions.

pick(n): push the n-th top value of the stack.

(top) A B C D E F (bottom)
 |
 | pick(3)
 v
(top) D A B C D E F (bottom)

deposit: insert the top value to the n-th index

(top) D 6 9 A B C E F (bottom)
 |
 | deposit
 v
(top) 6 9 A B C D E F (bottom)

withdraw: pull the n-th value to the top (inversion of deposit)

(top) 5 9 A B C D E F (bottom)
 |
 | withdraw
 v
(top) C 5 9 A B D E F (bottom)

definitions:

pick(0) = dup
pick(n) = push(n+1); push(-1); roll; dup; push(n+2); push(1); roll
deposit: pick(1); push(1); roll
withdraw: dup; push(-1); roll

3. Put initializer of the piet's stack.

initial state of the stack:

(top) 0 3 3 (bottom)

4. Put piet's instractions correspoinding to each brainfuck's instruction.

+: push(1); add
-: push(1); sub
>: deposit
   if (the second top value) > (top value)
     # extend tape
     # (top) 9 9 A B C D E F (bottom)
     # |
     # | extend
     # v
     # (top) 0 10 10 A B C D E F (bottom)
     pop; push(1); add; dup; push(0)
   else
     push(1); iadd; withdraw
   end
<: deposit; push(1); sub; withdraw
[: if (top value) * 2 <= 0
     jump the corresponding ']'
   end
]: jump the corresponding '['
,: pop; in(char)
.: dup; out(char)

Of course, branches and jumps are represented by "greater", "switch" and "pointer". Note that the piet's stack is not required to hold arbitrarily long number.

5. Put a terminator of execution.

See Piet Speficication.

full implementation

http://github.com/mame/piet-misc/blob/master/bf2piet.rb

example

An echo program written in brainfuck

,[.,]

is translated to the following Piet program:

$ ruby19 bf2piet.rb echo.bf > echo.piet.png

You can see ',', '[', '.', ',' and ']' above each corresponding sequence of instructions.

$ echo foobar | ../npiet-1.1/npiet -q echo.piet.png
foobar

You can also see hello.piet.png which is translated from brainfuck's Hello world!

$ ../npiet-1.1/npiet hello.piet.png
Hello, world!

And now, we can obtain brainfuck interpreter written in Piet, by translating Keymaker's brainfuck interpreter written in brainfuck!

$ ruby19 bf2piet.rb -c 1 kbfi.b > kbfi.piet.png
$ time ../npiet-1.1/npiet -q kbfi.b < hello.bf
Hello, world!
real    2m35.729s
user    2m35.342s
sys     0m0.128s

conclusion

Given a stack of unlimited size, Piet is Turing-complete. It does not require the stack holding arbitrarily long number.

translated from mamememo in Japanese (2009-09-25).