From 3aa9cda6110c3e53813b60533161cfe1c3557bc5 Mon Sep 17 00:00:00 2001
From: Ben Fiedler
Date: Sat, 12 Dec 2020 23:50:23 +0100
Subject: [PATCH] publish miu post

.../blog/ondecidabilityandthemupuzzle.md  66 +++++++++
1 file changed, 33 insertions(+), 33 deletions()
diff git a/content/blog/ondecidabilityandthemupuzzle.md b/content/blog/ondecidabilityandthemupuzzle.md
index 9bbe885..f2ce15c 100644
 a/content/blog/ondecidabilityandthemupuzzle.md
+++ b/content/blog/ondecidabilityandthemupuzzle.md
@@ 1,8 +1,7 @@

title: "On Decidability and the MUpuzzle"
date: 20201212T00:00:00+01:00
tags: [math, decidability]
draft: true
+title: "On Decidability and the MU puzzle"
+date: 20201213T00:00:00+00:00
+tags: [math, decidability, shortandsweet]

[Gödel, Escher, Bach](https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach)
@@ 11,16 +10,16 @@ In the first few chapters, Hofstadter introduces a formal system called the
MIUsystem. The MIUsystem consists of four simple rules for manipulating
strings consisting of the characters `M`, `I` and `U`.
1. `xI > xIU`, where `x` can be any string
1. `Mx > Mxx`, where `x` can be any string
1. `xIIIy > xUy`, where `x` and `y` can be any strings
1. `xUUy > xy`, where `x` and `y` can be any strings
+1. `xI > xIU`, where `x` matches the rest of the string
+1. `Mx > Mxx`, where `x` matches the rest of the string
+1. `xIIIy > xUy`, where `x` and `y` match the rest of the string
+1. `xUUy > xy`, where `x` and `y` match the rest of the string
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`.
Then Hofstadter asks the reader to answer the MUpuzzle:
+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 above rules?
@@ 58,37 +57,38 @@ value(MU) = 3
value(MI) = 1
```
The value of our target `MU` is 3 which is divisible by 3, while the value of
our starting string `MI` is 1, which is not divisible by 3.

If we can show that, starting with a string of value not divisible by 3, every
rule application cannot create a string with value divisible 3, then it is also
impossible to get `MU` by starting with `MI`.
+The value of our target `MU` is 3, which is divisible by 3, while the value of
+our starting string `MI` is 1, which is not divisible by 3. If we can show that,
+starting with a string of value not divisible by 3, every rule application
+cannot create a string with value divisible 3, then it is also impossible to get
+`MU` by starting with `MI`.
So take a string `Mx` whose value is not divisible by 3. Rules 1, 3 and 4
preserve the value of `Mx` modulo 3, so by assumption the resulting string also
has value not divisible by 3.
Rule 2 doubles the value of a string. However, by doubling any number which is
not a multiple of 3 we can never create a number divisible by 3: a number is
divisible by 3 iff 3 is one of its (unique) prime factors. When doubling, the
only prime factor we potentially add is 2, hence the resulting number also
cannot have 3 as a prime factor. Thus it is not divisible by 3.

We can express this more succinctly as
+not a multiple of 3 we can never create a number divisible by 3: a number `n` is
+divisible by 3 iff 3 is one of its prime factors. When doubling `n` the only
+prime factor we add is 2, hence the resulting number also cannot
+have 3 as a prime factor. We can express this more succinctly as
```
∀x. x ≠ 0 (mod 3) > 2x ≠ 0 (mod 3)
```
+Thus `2*n` is not divisible by 3, and we can never construct the string `MU`
+starting from `MI`.
+
+
# Characterizing all generatable strings
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, i.e.
all strings `Mx` such that `value(Mx) != 0 (mod 3)`?
+Not only have we shown that `MU` is not constructible, but also any other string
+with a value divisible by 3, starting from `MI`. The question remains: which
+strings can we generate? Is it possible to generate all other strings, i.e. all
+strings `Mx` such that `value(Mx) != 0 (mod 3)`?
The answer turns out to be yes, using (among others) the following algorithm.
+The answer turns out to be yes, using 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)`.
@@ 105,11 +105,11 @@ generated by repeatedly applying rule 1 to `MI` has values `1, 2, 4, 8, 16, 32,
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
+since we can only remove `U`s in pairs. This is where rule 2 comes into play: if
+`value(My) != value(Mx) (mod 6)`, then there would always be one `U` left over.
+(Note: 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.
+deleting `UU`s, increases `value(My)` by 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
@@ 128,7 +128,7 @@ 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 MUproblem, but any decision problem of the form "Does candidate string
`Mx` belong to the MIUsystem?".
+`Mx` belong to the MIUsystem, starting from `MI`?".
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
@@ 143,8 +143,8 @@ 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 typechecking a Swift program is [also an undecidable
problem](https://forums.swift.org/t/swifttypecheckingisundecidable/39024),
by showing that in order to typecheck a program, the compiler must solve the
+problem](https://forums.swift.org/t/swifttypecheckingisundecidable/39024).
+The author shows that in order to typecheck a program, 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

2.30.1