Notes

Chapter 12: The Principle of Computational Equivalence

Section 8: Undecidability and Intractability


Satisfiability [emulating Turing machines]

Given variables 𝕤[t, s], 𝕒[t, x, a], 𝕟[t, n] representing whether at step t a non-deterministic Turing machine is in state s, the tape square at position x has color a, and the head is at position n, the following CNF expression represents the assertion that a Turing machine with stot states and ktot possible colors follows the specified rules and halts after at most t steps:

NDTMToCNF[rules_, {s_, a_, n_}, t_] := {Table[Or @@ Table[𝕤[i, j], {j, stot}], {i, t - 1}], Table[!𝕤[i, j] || !𝕤[i, k], {i, 0, t - 1}, {j, stot}, {k, j + 1, stot}], Table[Or @@ Table[𝕟[i, j], {j, n + i, Max[0, n - i], -2}], {i, 0, t}], Table[!𝕟[i, j] || !𝕟[i, k], {i, 0, t}, {j, n + i, Max[0, n - i], -2}, {k, j + 2, n + i}], Table[Or @@ Table[𝕒[i, j, k], {k, 0, ktot - 1}], {i, 0, t - 1}, {j, Max[1, n - i], n + i}], Table[!𝕒[i, j, k] || !𝕒[i, j, m], {i, 0, t - 1}, {j, Max[1, n - i], n + i}, {k, 0, ktot - 1}, {m, k + 1, ktot - 1}], 𝕤[0, s], Cases[MapIndexed[𝕒[Abs[n - First[#2]], First[#2], #1] & , a], 𝕒[x_, _, _] /; x < t], Table[𝕒[Abs[n - i], i, 0], {i, Length[a] + 1, n + t - 1}], Table[!𝕒[i, j, k] || If[EvenQ[n + i - j], 𝕟[i, j], False] || 𝕒[i + 1, j, k], {i, 0, t - 2}, {j, Max[1, n - i], n + i}, {k, 0, ktot - 1}], Table[Function[z, Outer[!𝕟[i, j] || !𝕤[i, z[[1,1]]] || !𝕒[i, j, z[[1,2]]] || ##1 & , Sequence @@ (If[i < t - 1, {𝕤[i + 1, #1[[1]]], 𝕟[i + 1, j - #1[[3]]], 𝕒[i + 1, j, #1[[2]]]}, {𝕟[i + 1, j - #1[[3]]]}] & ) /@ z[[2]]]] /@ rules, {i, 0, t - 1}, {j, n + i, Max[1, n - i], -2}], Or @@ Table[𝕟[i, 0], {i, n, t, 2}]} /. List -> And


From Stephen Wolfram: A New Kind of Science [citation]