José Manuel Rodriguez Caballero
2018-08-25 03:26:11 UTC
A beautiful number-theoretic application of the undecidability results of
Minsky Machines is J. Conway's proof of the undecidability of the
generalized 3x+1 problem. Paul Erdos commented, concerning the
intractability of the original 3x+1 problem: Mathematics is not yet ready
for such problems.
http://mathworld.wolfram.com/CollatzProblem.html
So, a formal verification in Isabelle/HOL of Conway's proof could be a nice
way to apply the Minsky Machines library to a mathematical result which is
important in contemporary number theory.
https://www.isa-afp.org/entries/Minsky_Machines.html
If someone is interested at looking at Conway's proof, which is extremely
simple and elegant, the name of the paper is
Conway, J. (1972). Unpredictable iterations,
which can be found in the following book (page 219):
Jeffrey C. Lagarias, The Ultimate Challenge: The 3x+1 Problem
https://www.amazon.com/Ultimate-Challenge-3x-Problem/dp/0821849409
Kind Regards,
Jose M.
Date: Tue, 14 Aug 2018 11:36:18 +0200
Minsky Machines is J. Conway's proof of the undecidability of the
generalized 3x+1 problem. Paul Erdos commented, concerning the
intractability of the original 3x+1 problem: Mathematics is not yet ready
for such problems.
http://mathworld.wolfram.com/CollatzProblem.html
So, a formal verification in Isabelle/HOL of Conway's proof could be a nice
way to apply the Minsky Machines library to a mathematical result which is
important in contemporary number theory.
https://www.isa-afp.org/entries/Minsky_Machines.html
If someone is interested at looking at Conway's proof, which is extremely
simple and elegant, the name of the paper is
Conway, J. (1972). Unpredictable iterations,
which can be found in the following book (page 219):
Jeffrey C. Lagarias, The Ultimate Challenge: The 3x+1 Problem
https://www.amazon.com/Ultimate-Challenge-3x-Problem/dp/0821849409
Kind Regards,
Jose M.
Date: Tue, 14 Aug 2018 11:36:18 +0200
Subject: [isabelle] New AFP article: Minsky Machines
Content-Type: text/plain; charset="utf-8"
Minsky Machines
Bertram Felgenhauer
We formalize undecidablity results for Minsky machines. To this end, we
also
formalize recursive inseparability.
We start by proving that Minsky machines can compute arbitrary primitive
recursive and recursive functions. We then show that there is a
deterministic
Minsky machine with one argument and two final states such that the set of
inputs that are accepted in one state is recursively inseparable from the
set of
inputs that are accepted in the other state.
As a corollary, the set of Minsky configurations that reach the first
state but
not the second recursively inseparable from the set of Minsky
configurations
that reach the second state but not the first. In particular both these
sets are
undecidable.
We do not prove that recursive functions can simulate Minsky machines.
https://www.isa-afp.org/entries/Minsky_Machines.html
Enjoy!
Content-Type: text/plain; charset="utf-8"
Minsky Machines
Bertram Felgenhauer
We formalize undecidablity results for Minsky machines. To this end, we
also
formalize recursive inseparability.
We start by proving that Minsky machines can compute arbitrary primitive
recursive and recursive functions. We then show that there is a
deterministic
Minsky machine with one argument and two final states such that the set of
inputs that are accepted in one state is recursively inseparable from the
set of
inputs that are accepted in the other state.
As a corollary, the set of Minsky configurations that reach the first
state but
not the second recursively inseparable from the set of Minsky
configurations
that reach the second state but not the first. In particular both these
sets are
undecidable.
We do not prove that recursive functions can simulate Minsky machines.
https://www.isa-afp.org/entries/Minsky_Machines.html
Enjoy!