From 36ffe95fcbc3ce4994152206a367025fdcad37a7 Mon Sep 17 00:00:00 2001
From: Ben Fiedler
Date: Sat, 12 Dec 2020 18:03:29 +0100
Subject: [PATCH] update
---
.../{the-miu-system.md => the-mu-puzzle.md} | 69 +++++++++++++++----
1 file changed, 56 insertions(+), 13 deletions(-)
rename content/blog/{the-miu-system.md => the-mu-puzzle.md} (54%)
diff --git a/content/blog/the-miu-system.md b/content/blog/the-mu-puzzle.md
similarity index 54%
rename from content/blog/the-miu-system.md
rename to content/blog/the-mu-puzzle.md
index cbe0fd3..d73e88e 100644
--- a/content/blog/the-miu-system.md
+++ b/content/blog/the-mu-puzzle.md
@@ -1,14 +1,15 @@
---
-title: "The MIU system"
+title: "The MU puzzle"
date: 2020-12-12T00:00:00+01:00
tags: math
draft: true
---
-In [Gödel, Escher, Bach](https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach),
-Hofstadter introduces a formal system called the MIU-system. The MIU-system
-consists of four simple rules for manipulating strings consisting of the
-characters `M`, `I` and `U`.
+[Gödel, Escher, Bach](https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach)
+takes the reader on a journey through mind, music, machines and self-reference.
+In the first few chapters, Hofstadter introduces a formal system called the
+MIU-system. The MIU-system consists of four simple rules for manipulating
+strings consisting of the characters `M`, `I` and `U`.
1. `Mx -> Mxx`, where `x` can be any string
2. `xIIIy -> xUy`, where `x` and `y` can be any strings
@@ -19,13 +20,15 @@ Note that the placeholders `x` and `y` must always match the entire string,
i.e. the application `MII -> MIII`, choosing `x = I`, is not valid. The correct
application is `MII -> MIIII`.
-Hofstadter asks the following:
+Then Hofstadter asks the reader to answer the MU-puzzle:
-> Given the initial string `MI`, is it possible to construct the string `MU` using only the four rules above?
+> Given the initial string `MI`, is it possible to construct the string `MU` using only the four above rules?
Take a few minutes and try for yourself. Many people quickly suspect that it is
impossible, but why?
+# The solution
+
Let us add an additional, imaginary rule.
@@ -86,20 +89,20 @@ We can express this more succinctly as
We have just shown that any string with value divisible by three cannot be
generated in the MIU system if starting from `MI`. The question remains: Which
strings can we generate? Is it possible to generate all other strings `Mx`, i.e.
-those with value not divisible by three?
+all strings `Mx` such that `value(Mx) != 0 (mod 3)`?
-The answer turns out to be yes, using a simple algorithm.
+The answer turns out to be yes, using for example the following algorithm.
1. Generate `My = MIIIIII...III` by applying rule 1 to `MI`, such that the following holds:
the value of `My` is larger than `Mx` and `value(My) = value(Mx) (mod 3)`.
2. Append `U` if `value(My) != value(Mx) (mod 6)`.
-3. Merge `IIIIII` to `UU` and delete until the value of `My` is the value of `Mx`.
+3. Merge `IIIIII` to `UU` and delete until `value(My) == value(Mx)`.
4. Replace the `MIIII...III` with `Mx` by applications of rules 2 and 3.
It is always possible to apply step 1: the infinite sequence of strings
generated by repeatedly applying rule 1 to `MI` has values `1, 2, 4, 8, 16, 32,
...`, generating all powers of 2. Taking these values modulo 3 we get `1, 2, 1,
-2, 1, 2, 1, 2, ...`, i.e. `2^i (mod 3)` is 1 if i is odd, and 2 otherwise. Since
+2, 1, 2, 1, 2, ...`, i.e. `2^i (mod 3)` is `1` if `i` is even, and 2 otherwise. Since
`value(Mx) != 0` by assumption, there always exists a longer string `My` such that
`value(My) = value(Mx) (mod 3)`.
@@ -107,11 +110,51 @@ In step 3 we need to delete `U` pairs until we have that `value(My) =
value(Mx)`. Unfortunately, we can only decrease `value(My)` in steps of six,
since we can only `U`s in pairs. This is where rule 2 comes into play: if
`value(My) != value(Mx) (mod 6)`, then there would be one `U` left over. (Note:
-since these values are congruent modulo 3 the only possible case is that
-`value(Mx) + 3 == value(My) (modulo 6)`). Appending an additional `U` before
+since these values are congruent modulo 3, the only possible case is that
+`value(Mx) == value(My) + 3 (modulo 6)`). Appending an additional `U` before
deleting `UU`s, increases `value(My)` be 3, and everything works out.
Step 4 is simple: `Mx` has the same value as `My` and we can use rule 2 to
convert `III`s to `U`s, in the right positions. Thus we have shown that the
`MIU` system lets us generate precisely the strings which have a value not
divisible by 3.
+
+# The MIU-system and decidability
+
+The MIU-system isn't just a neat puzzle to solve: Hofstadter shows the reader
+that some questions about formal systems cannot be answered solely from within.
+Rather, we had to step outside the restrictions placed upon us by the four rules
+to successfully answer the question.
+
+Given infinite time we could have concluded this ourselves, by generating all
+possible strings: however, in this case there exists a solution which is finite.
+We have constructed a [*decision
+procedure*](https://en.wikipedia.org/wiki/Decision_problem) which solves not
+only the MU-problem, but any decision problem of the form "Does candidate string
+`Mx` belong to the MIU-system?".
+
+It is not always possible to find a finite decision procedure. Take for example
+all strings which are valid C programs (or choose any other [sufficiently
+powerful](https://en.wikipedia.org/wiki/Turing_completeness) language, it
+doesn't matter). The decision problem "Does a given C program terminate at some
+point?" is not solvable in finite time, as shown by [Alan Turing
+(1936)](https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf). This problem
+is also known as the [halting
+problem](https://en.wikipedia.org/wiki/Halting_problem), and is one of the most
+famous [undecidable
+problems](https://en.wikipedia.org/wiki/List_of_undecidable_problems).
+
+These abstract problems can even have real world consequences: This year it was
+shown that type-checking a Swift program is [also an undecidable
+problem](https://forums.swift.org/t/swift-type-checking-is-undecidable/39024),
+by showing that in order to solve type-checking, the compiler must solve the
+[word problem for finitely generated
+groups](https://en.wikipedia.org/wiki/Word_problem_for_groups). I like how this
+example shows us that some abstract problems pop up in unexpected places, and
+why seemingly purely theoretical knowledge matters, even for applied problems
+such as building compilers.
+
+If you have any questions or comments feel free to reach out to me via my
+[public inbox](https://lists.sr.ht/~bfiedler/public-inbox). If you are
+interested in undecidability in other programming languages, you might like
+[typing-is-hard.ch](https://typing-is-hard.ch).
--
2.30.1