### 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.

### License

BSD License

### Topics

- Logic/Computability

### Session Minsky_Machines

- Recursive_Inseparability
- Minsky

### Depends on

- Abstract Rewriting
- Recursion Theory I

## Cite

×

Minsky_Machines-AFP

    @article{Minsky_Machines-AFP,
      author  = {Bertram Felgenhauer},
      title   = {Minsky Machines},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Minsky_Machines.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Aug 14, 2018 : Isabelle2017