Minsky Machines

Title:	Minsky Machines
Author:	Bertram Felgenhauer (int-e /at/ gmx /dot/ de)
Submission date:	2018-08-14
Abstract:	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.
BibTeX:	@article{Minsky_Machines-AFP, author = {Bertram Felgenhauer}, title = {Minsky Machines}, journal = {Archive of Formal Proofs}, month = aug, year = 2018, note = {\url{http://isa-afp.org/entries/Minsky_Machines.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Abstract-Rewriting, Recursion-Theory-I
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.