Email Gateway (Aug 22 2022 at 18:17): Email Gateway (Aug 22 2022 at 18:17):From: Tobias Nipkow <nipkow@in.tum.de>
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!
smime.p7s
Last updated: Apr 20 2024 at 12:26 UTC