Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: Minsky Machines


view this post on Zulip 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: Nov 21 2024 at 12:39 UTC