From 5e3a009a4d1c8cb055211e034b40f2fc47a16d17 Mon Sep 17 00:00:00 2001 From: Ben Fiedler Date: Sat, 12 Dec 2020 18:18:32 +0100 Subject: [PATCH] Another update --- ...d => on-decidability-and-the-mu-puzzle.md} | 43 +++++++++---------- 1 file changed, 21 insertions(+), 22 deletions(-) rename content/blog/{the-mu-puzzle.md => on-decidability-and-the-mu-puzzle.md} (83%) diff --git a/content/blog/the-mu-puzzle.md b/content/blog/on-decidability-and-the-mu-puzzle.md similarity index 83% rename from content/blog/the-mu-puzzle.md rename to content/blog/on-decidability-and-the-mu-puzzle.md index d73e88e..6bfc1ee 100644 --- a/content/blog/the-mu-puzzle.md +++ b/content/blog/on-decidability-and-the-mu-puzzle.md @@ -1,7 +1,7 @@ --- -title: "The MU puzzle" +title: "On Decidability and the MU-puzzle" date: 2020-12-12T00:00:00+01:00 -tags: math +tags: math, decidability draft: true --- @@ -11,10 +11,10 @@ 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. `xI -> xIU`, where `x` can be any string 1. `Mx -> Mxx`, where `x` can be any string -2. `xIIIy -> xUy`, where `x` and `y` can be any strings -3. `xUUy -> xy`, where `x` and `y` can be any strings -4. `xI -> xIU`, 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 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 @@ -58,25 +58,22 @@ value(MU) = 3 value(MI) = 1 ``` -The rules 2, 3, and 4 preserve value of a string modulo 3. The only operation -which changes the number of `I`s is rule 1: it duplicates `x`, hence it doubles -the value of a string. - 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. -Our goal is to show that, starting with a string of value not divisible by 3, -every rule application cannot create a string with value divisible 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 2, 3 and 4 +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 1 doubles the value of a string. However, by doubling any number which is +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. By doubling a number -the only prime factor we potentially add is 2, hence the resulting number also -cannot have 3 as a prime factor, and is not divisible by 3. +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 @@ -88,10 +85,10 @@ 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. +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 for example the following algorithm. +The answer turns out to be yes, using (among others) 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)`. @@ -144,17 +141,19 @@ 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 +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 +by showing that in order to type-check 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 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). +interested in undecidability in other programming languages, you might also like +this website I made: [typing-is-hard.ch](https://typing-is-hard.ch). -- 2.30.1