1 files changed, 55 insertions, 0 deletions
diff --git a/src/assets/writeup/proof.md b/src/assets/writeup/proof.md
new file mode 100644
index 0000000..1f5eeda
--- /dev/null
+++ b/src/assets/writeup/proof.md
@@ -0,0 +1,55 @@
+---
+name: Brainfucked
+desc: trimills turing completeness proof for brainfucked
+---
+
+### Turing-completeness proof for Brainfucked
+
+By producing an algorithm that can translate arbitrary Brainfuck programs into
+Brainfucked, we prove that the latter must have computational class greater than
+or equal to the former, thus proving that Brainfucked is Turing-complete.
+
+Proof that Brainfucked is not of a greater computational class than Brainfuck is
+left as an exercise to the reader.
+
+Since Brainfucked tapes have a limited amount of memory, we will implement a
+tape as a linked list. Each item in the linked list will be a tape of length
+ten with the following structure:
+
+- The first cell contains the item's value
+- The second cell is 1 if the next item has already been allocated and 0 otherwise
+- The remaining 8 cells are the pointer to the next item
+
+The second byte is not strictly necessary, as we could just check whether the pointer
+is null, however it makes the translation significantly easier.
+
+First, we prefix the output program with `++++++++++*(`. Since the original tape is
+only 8 bytes wide, we need to make a new one with a size of 10. `+`, `-`, `[`, `]`,
+`.`, and `,` all translate to themselves.
+
+`>` can be translated as `>-[>++++++++++*<+]+>(`. This will allocate the next tape
+if it does not yet exist and then enter it.
+
+First, consider the case where next tape has not yet been allocated. We decrement the
+allocation marker cell, which wraps around to 255, allowing us to enter the loop. We
+then allocate the next tape and increment the allocation marker back to 0. After exiting
+the loop, it is incremented again to 1, signalling that the next tape is now allocated.
+We can then enter the newly allocated tape. If the tape was already allocated, the loop
+will never be entered and the marker will remain 1.
+
+`<` can be translated as `)<<`. We exit the current tape and move back over to the data cell.
+
+This proof only uses a subset of Brainfucked consisting of the characters `+-<>[]()*,.`.
+One of `+` or `-` can be trivially eliminated by replacing it with 255 copies of the other.
+Additionally, `,` and `.` are not required for Turing-completeness, as input can be encoded into
+the initial tape configuration and output can be read off the tape once the program halts.
+I conjecture that no smaller subset of Brainfucked is Turing-complete.
+
+#### Example translation script (Lua)
+```lua
+src = io.read("*a")
+src = src:gsub("%<", ")<<")
+src = src:gsub("%>", ">-[>++++++++++*<+]+>(")
+src = "++++++++++*(" .. src
+io.write(src)
+```