Theory Minsky
section ‹Minsky machines›
theory Minsky
imports Recursive_Inseparability "Abstract-Rewriting.Abstract_Rewriting" "Pure-ex.Guess"
begin
text ‹We formalize Minksy machines, and relate them to recursive functions. In our flavor of
Minsky machines, a machine has a set of registers and a set of labels, and a program is a set of
labeled operations. There are two operations, @{term Inc} and @{term Dec}; the former takes a
register and a label, and the latter takes a register and two labels. When an @{term Inc}
instruction is executed, the register is incremented and execution continues at the provided label.
The @{term Dec} instruction checks the register. If it is non-zero, the register and continues
execution at the first label. Otherwise, the register remains at zero and execution continues at
the second label.
We continue to show that Minksy machines can implement any primitive recursive function. Based on
that, we encode recursively enumerable sets as Minsky machines, and finally show that
\begin{enumerate}
\item The set of Minsky configurations such that from state $1$, state $0$ can be reached,
is undecidable;
\item There is a deterministic Minsky machine $U$ such that the set of values $x$ such that
$(2, \lambda n.\, \text{if $n = 0$ then $x$ else $0$})$ reach state $0$ is recursively
inseparable from those that reach state $1$; and
\item As a corollary, the set of Minsky configurations that reach state $0$ but not state $1$ is
recursively inseparable from the configurations that reach state $1$ but not state $0$.
\end{enumerate}›
subsection ‹Deterministic relations›
text ‹A relation $\to$ is \emph{deterministic} if $t \from s \to u'$ implies $t = u$.
This abstract rewriting notion is useful for talking about deterministic Minsky machines.›
definition
"deterministic R ⟷ R¯ O R ⊆ Id"
lemma deterministicD:
"deterministic R ⟹ (x, y) ∈ R ⟹ (x, z) ∈ R ⟹ y = z"
by (auto simp: deterministic_def)
lemma deterministic_empty [simp]:
"deterministic {}"
by (auto simp: deterministic_def)
lemma deterministic_singleton [simp]:
"deterministic {p}"
by (auto simp: deterministic_def)
lemma deterministic_imp_weak_diamond [intro]:
"deterministic R ⟹ w◇ R"
by (auto simp: weak_diamond_def deterministic_def)
lemmas deterministic_imp_CR = deterministic_imp_weak_diamond[THEN weak_diamond_imp_CR]
lemma deterministic_union:
"fst ` S ∩ fst ` R = {} ⟹ deterministic S ⟹ deterministic R ⟹ deterministic (S ∪ R)"
by (fastforce simp add: deterministic_def disjoint_iff_not_equal)
lemma deterministic_map:
"inj_on f (fst ` R) ⟹ deterministic R ⟹ deterministic (map_prod f g ` R)"
by (auto simp add: deterministic_def dest!: inj_onD; force)
subsection ‹Minsky machine definition›
text ‹A Minsky operation either decrements a register (testing for zero, with two possible
successor states), or increments a register (with one successor state). A Minsky machine is a
set of pairs of states and operations.›