Skelet #33 doesn't halt - Coq proof

Individual machines
1

A few weeks ago, I saw a few machines that weren’t formally proven yet, in particular, Skelet #15, #17, #26, and #33. @meithecatte and I finished formalizing the proof that Skelet #33 (11896833) doesn’t halt, and the proof is available here. Thanks to @meithecatte for proving Theorem nonhalt and cleaning up the proof!

In the rest of this post, I will give an overview of the formal proof. The proof begins similarly to Skelet #34’s proof, but the proof diverged after I introduced invariant(n, m). This invariant made the TM configurations easier to reason about, and made the 3 theorems step_reset + do_reset + E_next work properly.

Counter phase

These definitions were copied over:

  • b(n) is the first non-negative integer such that n + b(n) contains only 1’s in base-2. For example, b(15) = 0 and b(16) = 15. (Note: b(0) is not defined)
  • L(n) is a tape defined by L(0) = 0^∞, L(2n) = L(n) 0000, and L(2n+1) = L(n) 1000.
  • R(n) is a tape defined by R(0) = 0^∞, R(2n) = 10 R(n), and R(2n+1) = 11 R(n).
  • K(n) is a tape defined by K(0) = 0^∞, K(2n) = K(n) 0000, and K(2n+1) = K(n) 0100. Note that L(n) = K(n) 0 for all n.

These definitions were slightly modified to fit Skelet #33:

  • D(n, m) = L(n) <C 101010 R(m). D(n, m) represents a counter phase configuration.
  • E(n, m) = K(n) <C 1010 R(m). E(n, m) represents a reset phase configuration.

First, we analyze the configuration D(n, m). Depending on m, the machine will follow either D_inc or start_reset.

  • Lemma D_inc. If m contains a 0 in base-2, then D(n, m) ⊢* D(n+1, m+1).
  • Theorem start_reset. If m contains only 1’s in base-2, then D(n, m) ⊢* E(n+1, 2(m+1)+1).

In summary, if the machine starts on D(n, m), it will repeatedly follow D_inc to get to D(n+b(m), m+b(m)) (see D_inc and D_finish in the proof). Since m+b(m) contains only 1’s in base-2, the machine will follow start_reset.

Now that the counter phase D(*, *) is analyzed, let’s move on to the reset phase E(*, *).

Reset phase

E(n, m) is easy to analyze when n is odd.

Lemma step_reset_odd. Let n, m be positive integers. Then E(2n+1, m) ⊢* E(n, 4m+2).
Proof. Simulate the machine. E(2n+1, m) = K(n) 0100 <C 1010 R(m) ⊢* K(n) <C 1010 1011 R(m) = E(n, 4m+2). □

The general case requires more setup:

  • Let leads(n) be the statement that either n = 1, or n starts with 11 in base-2.
  • Suppose q ≥ 0 and 0 ≤ r < 2^q. Then leads(3 * 2^q + r).
  • Let invariant(n, m) be the statement that leads(n) is true, and b(m) = 3 * 2^q + r for some q ≥ 0 and 2n ≤ r < 2^q.

Theorem step_reset. Let n > 1 and m ≥ 1. Suppose invariant(n, m) is true. Then there exist 1 ≤ n' < n and m' ≥ 1 such that E(n, m) ⊢* E(n', m') and invariant(n', m') is true.

Proof

Factor n as n = 2^k (2n'+1) for some k ≥ 0 and n' ≥ 0. Define m' = (2(2(2^k - 1) + m) + 1) * 4^k + 1. We claim that n' and m' satisfy the theorem.

  • Proof that n' ≥ 1. For the sake of contradiction, suppose n' = 0. As a result, n = 2^k. Since n > 1, it follows that leads(n) is false. This contradicts invariant(n, m).
  • Proof that n' < n. This follows from n = 2^k (2n'+1).
  • Proof that m' ≥ 1. This follows from the definition of m'.
  • Proof that E(n, m) ⊢* E(n', m'). This follows from a sequence of steps:
    • E(n, m) = E(2^k (2n'+1), m) = K(n') 0100 0000^k <C 1010 R(m)
    • K(n') 0100 0000^k <C 1010 R(m) ⊢* K(n') 0100 1000^k <C 1010 R(2(2^k - 1) + m) (see LaR_max). Also, the right side does not overflow because b(m) = 3 * 2^q + r > r ≥ 2n > 2(2^k - 1).
    • The machine runs on 0100 1000^k <C 1010 and eventually reaches E(n', m'). See eat_bin_max and drop_KI for more details.
  • Proof that leads(n') is true. Note that n = 2^k (2n'+1) and leads(n) is true. Trailing 0’s don’t matter, so leads(2n'+1) is true. Lastly, since n' ≥ 1, a little bit of work shows that leads(n') is true.
  • Proof that b(m') = 3 * 2^q' + r' for some q' ≥ 0 and 2n' ≤ r' < 2^q'. For this proof, use q' = q+2k+2 and r' = 2^(2k+2) * (r-2(2^k - 1)) + 3 * 2^(2k) - 2. See the proof for more details. □

Here’s a more useful version of Theorem step_reset.

Corollary do_reset. Let n ≥ 1 and m ≥ 1. Suppose invariant(n, m) is true. Then there exists m' ≥ 1 such that E(n, m) ⊢* E(1, m') and leads(b(m')) is true.
Proof. Use strong induction on n. For n = 1, use m' = m. From invariant(1, m), it follows that b(m) = 3 * 2^q + r where r < 2^q, and therefore, leads(b(m)). This finishes the base case. For n > 1, apply step_reset to go to a smaller case. □

Here’s the theorem that brings all of the previous work together.

Theorem E_next. Let m ≥ 1 and suppose leads(b(m)) is true. Then there exists m' ≥ 1 such that E(1, m) ⊢^+ E(1, m') and leads(b(m')) is true.

Proof

Firstly, direct simulation shows that E(1, m) ⊢^+ D(0, 2m+1). Follow D_finish to reach D(b(2m+1), 2m+1+b(2m+1)). Follow start_reset to reach E(b(2m+1)+1, 4m+5+2b(2m+1)). This simplifies to E(2b(m)+1, 4(m+b(m)+1)+1). Follow step_reset_odd to reach E(b(m), 16(m+b(m)+1)+6). Following do_reset is enough to finish the proof, but we still need to show that invariant(b(m), 16(m+b(m)+1)+6) is true. Here’s the proof that the invariant is true:

  • Proof that leads(b(m)) is true. This is already given.
  • Proof that b(16(m+b(m)+1)+6) = 3 * 2^q + r for some q ≥ 0 and 2b(m) ≤ r < 2^q. First, let m+b(m)+1 = 2^k for some k ≥ 1. Then b(16(m+b(m)+1)+6) = b(2^(k+4)+6) = 2^(k+4)-7 = 3 * 2^(k+2) + (2^(k+2)-7). Therefore, q = k+2 and r = 2^(k+2)-7. Lastly, Coq proved the inequality 2b(m) ≤ r using just lia. □

Theorem nonhalt. Skelet #33 does not halt.
Proof. The machine reaches E(1, 17). Also, leads(b(17)) = leads(14) is true. The conditions of Theorem E_next are satisfied. Apply Theorem E_next infinitely. □

2 Likes