Skelet #26 and #15 do not halt - Coq proof

Individual machines
1

@meithecatte and I finished formalizing the proof that Skelet #26 (13134219) doesn’t halt, and the proof is available here. Thanks to @meithecatte for cleaning up the proof! Also thanks to @meithecatte for creating D0_nonhalt and using it to show that Skelet #15 (2204428, proof) doesn’t halt!

The only machine that doesn’t have a formal proof is Skelet #17.

In the rest of this post, I will give an overview of the formal proof. Here’s a summary of how Skelet #26 behaves:

  • D(0, 0, *) ⊢* (D_finish) D(*, 0, 2^k - 1) ⊢^+ (start_reset0) E0(*, 1, 2^k) ⊢* (do_reset0) E0(0, 1, *) = D(0, 1, *)
  • D(0, 1, *) ⊢* (D_finish) D(*, 1, 2^k - 1) ⊢^+ (start_reset1) E1(*, 0, 2^(k-1)) ⊢* (do_reset1) E0(0, *, *) = D(0, *, *)

The sections on D(n, a, m) and E0(n, a, m) are similar to Skelet #33’s proof. The sections on E1(n, a, m) and D0_nonhalt are completely new. Unlike Skelet #33, Skelet #26 reaches E1(n, a, m) often. The trickiest part was making reset_invariant(m) strong enough to handle E1(n, a, m).

Definitions

Firstly, here are a few definitions:

  • 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).
  • K0(n) is a tape defined by K0(0) = 0^∞, K0(2n) = K0(n) 0000, and K0(2n+1) = K0(n) 0100. Note that L(n) = K0(n) 0 for all n. (This is the same as K(n) from my post on Skelet #33)
  • K1(n) is a tape defined by K1(0) = 0^∞, K1(2n) = K1(n) 0000, and K1(2n+1) = K1(n) 0001. Note that L(n) = K1(n) 000 for all n.
  • D(n, a, m) = L(n) <D 101a R(m).
  • E0(n, a, m) = K0(n) <D 101a R(m).
  • E1(n, a, m) = K1(n) <D 101a R(m).
  • Let reset_invariant(m) be the statement that m ≥ 2, and b(m)+1 = 2^k (2n'+1) for some k ≥ 0 and n' ≥ 2.

The definitions for K1(n), E1(n, a, m), and reset_invariant(m) are completely new. The remaining definitions are copied or slightly modified from the Skelet #33 proof.

D(n, a, m) represents a counter phase configuration. E0(n, a, m) and E1(n, a, m) represent a reset phase configuration.

Counter phase - D(n, a, m)

Depending on a and m, the machine will follow either D_inc, start_reset0, or start_reset1.

  • Lemma D_inc. If m contains a 0 in base-2, then D(n, a, m) ⊢* D(n+1, a, m+1).
  • Theorem start_reset0. If m contains only 1’s in base-2, then D(n, 0, m) ⊢^+ E0(n+1, 1, m+1). (This is analogous to start_reset from my post on Skelet #33)
  • Theorem start_reset1. If m contains only 1’s in base-2, then D(n, 1, m) ⊢^+ E1(2n+2, 0, (m+1)/2). (The Coq proof uses m' to represent (m+1)/2, because / is hard to use)

There is also Corollary D_finish. D(n, a, m) ⊢* D(n+b(m), a, m+b(m)). The proof is to repeatedly apply D_inc until it is no longer possible. □

In summary, if the machine starts on D(n, a, m), it will follow D_finish to get to D(n+b(m), a, m+b(m)). Since m+b(m) contains only 1’s in base-2, the machine will follow either start_reset0 or start_reset1 and enter the reset phase. Both E0 and E1 are part of the reset phase.

Reset phase - E0(n, a, m)

Theorem step_reset0. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ b(m). Then there exist 0 ≤ n' < n and m' ≥ 1 such that E0(n, a, m) ⊢* E0(n', 1, m'), n' ≤ b(m'), and reset_invariant(m') is true.

Proof

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

  • Proof that n' < n. This follows from n = 2^k (2n'+1).
  • Proof that m' ≥ 1. See the proof that m' ≥ 2.
  • Proof that E0(n, a, m) ⊢* E0(n', 1, m'). This follows from a sequence of steps:
    • E0(n, a, m) = E0(2^k (2n'+1), a, m) = K0(n') 0100 0000^k <D 101a R(m)
    • K0(n') 0100 0000^k <D 101a R(m) ⊢* K0(n') 0100 1000^k <D 101a R(2^k - 1 + m) (see LaR_max). Also, the right side does not overflow because 2^k - 1 < n ≤ b(m).
    • The machine runs on 0100 1000^k <D 101a until it reaches <D 1011 1010^k 111a. This configuration corresponds to E0(n', 1, m'). See eat_bin_max0 and drop_K0I for the Coq proof.
  • Proof that n' ≤ b(m'). This is split into 2 parts.
    • Proof that n' ≤ b(2^k - 1 + m). Since 2^k - 1 < n ≤ b(m), it follows that b(2^k - 1 + m) = b(m) - (2^k - 1). Also, b(m) - (2^k - 1) ≥ n - (2^k - 1) > 2^k (2n') ≥ n'.
    • Proof that b(2^k - 1 + m) ≤ b(m'). On the right side, repeatedly apply b(2x) = 2b(x)+1 ≥ b(x) and b(2x+1) = 2b(x) ≥ b(x) until the inequality becomes b(2^k - 1 + m) ≤ b(2^k - 1 + m).
  • Proof that m' ≥ 2. This follows from the definition of m'.
  • Proof that b(m')+1 = 2^k' (2n''+1) for some k' ≥ 0 and n'' ≥ 2. We claim that k' = 2k and n'' = b(2(2^k - 1 + m) + a).
    • Proof that b(m')+1 = 2^k' (2n''+1). Expand b(m') with b(2x) = 2b(x)+1 and b(2x+1) = 2b(x). Then the result follows.
    • Proof that n'' ≥ 2. Note that n'' = b(2(2^k - 1 + m) + a) = 2b(2^k - 1 + m) + (1-a). Since 2^k - 1 < n ≤ b(m), it follows that b(2^k - 1 + m) > 0. So n'' ≥ 2*1+(1-1) = 2. □

Here’s a more useful version that repeatedly applies step_reset0 until n' = 0.

Corollary do_reset0. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ b(m). Then there exists m' ≥ 1 such that E0(n, a, m) ⊢* E0(0, 1, m') and reset_invariant(m') is true.
Proof. Use strong induction on n. Apply step_reset0 to obtain 0 ≤ n'' < n and m'' ≥ 1 such that E0(n, a, m) ⊢* E0(n'', 1, m''), n'' ≤ b(m''), and reset_invariant(m'') is true. If n'' = 0 then use m' = m'' and we’re done. Otherwise, apply the strong induction hypothesis on (n'', m'', 1) to obtain m'. Finish the proof with E0(n, a, m) ⊢* E0(n'', 1, m'') ⊢* E0(0, 1, m'). □

Reset phase - E1(n, a, m)

When Skelet #26 reaches E1(n, a, m), n is always even (see start_reset1), but the inequality “n ≤ b(m)” doesn’t always hold. As a result, I used the weaker statement that “n ≤ 4b(m), n = 2^(k+1) * (odd integer), and 2^(k+1) ≤ b(m)”.

Theorem step_reset1. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ 4b(m). Suppose n = 2^(k+1) (2n'+1) where k ≥ 0, 2^(k+1) ≤ b(m), and n' ≥ 0. Firstly, n' < n. Secondly, there exists m' ≥ 1 such that E1(n, a, m) ⊢* E0(n', 0, m'), n' ≤ b(m'), and reset_invariant(m') is true.

Proof

Define m' = (4(2^(k+1) - 1 + m) + 2a + 1) * 2 * 4^k. We claim that m' satisfies the theorem.

  • Proof that n' < n. This follows from n = 2^(k+1) (2n'+1).
  • Proof that m' ≥ 1. See the proof that m' ≥ 2.
  • Proof that E1(n, a, m) ⊢* E0(n', 0, m'). This follows from a sequence of steps:
    • E1(n, a, m) = E1(2^(k+1) (2n'+1), a, m) = K1(n') 0001 0000^(k+1) <D 101a R(m)
    • K1(n') 0001 0000^(k+1) <D 101a R(m) ⊢* K1(n') 0001 1000^(k+1) <D 101a R(2^(k+1) - 1 + m) (see LaR_max). Also, the right side does not overflow because 2^(k+1) - 1 < 2^(k+1) ≤ b(m).
    • The machine runs on 0001 1000^(k+1) <D 101a until it reaches 00 <D 10 1010^(k+1) 111a. Note that K1(n') 00 = K0(n'). This configuration corresponds to E0(n', 0, m'). See eat_bin_max1 and drop_K1I for the Coq proof.
  • Proof that n' ≤ b(m'). Split the inequality into n' ≤ b(2^(k+1) - 1 + m) and b(2^(k+1) - 1 + m) ≤ b(m'), and do the same approach as step_reset0. The Coq proof is copy-pasted too, except I added unfold b.
  • Proof that m' ≥ 2. This follows from the definition of m'.
  • Proof that b(m')+1 = 2^k' (2n''+1) for some k' ≥ 0 and n'' ≥ 2. We claim that k' = 2k+1 and n'' = b(2(2^(k+1) - 1 + m) + a).
    • Proof that b(m')+1 = 2^k' (2n''+1). Expand b(m') with b(2x) = 2b(x)+1 and b(2x+1) = 2b(x). Then the result follows.
    • Proof that n'' ≥ 2. Note that n'' = b(2(2^(k+1) - 1 + m) + a) = 2b(2^(k+1) - 1 + m) + (1-a). Since 2^(k+1) - 1 < 2^(k+1) ≤ b(m), it follows that b(2^(k+1) - 1 + m) > 0. So n'' ≥ 2*1+(1-1) = 2. □

step_reset1 says that E1(n, a, m) ⊢* E0(n', 0, m'). If n' > 0, we can apply do_reset0 to get E0(n', 0, m') ⊢* E0(0, 1, m''). The full details are in Corollary do_reset1.

Corollary do_reset1. Let n > 0, m ≥ 1, and a ∈ {0,1}. Suppose n ≤ 4b(m). Suppose n = 2^(k+1) (2n'+1) where k ≥ 0, 2^(k+1) ≤ b(m), and n' ≥ 0. Then there exist m' ≥ 1 and a' ∈ {0,1} such that E1(n, a, m) ⊢* E0(0, a', m') and reset_invariant(m') is true.
Proof. Apply step_reset1 to obtain 0 ≤ n'' < n and m'' ≥ 1 such that E1(n, a, m) ⊢* E0(n'', 0, m''), n'' ≤ b(m''), and reset_invariant(m'') is true. Then do cases on n'':

  • If n'' = 0 then use (m', a') = (m'', 0) and we’re done.
  • If n'' > 0 then apply do_reset0 on (n'', m'', 1) to obtain m'. Use m' and a' = 1. □

Putting the results together - D0_nonhalt

Theorem D0_next. Let m ≥ 1. There exists m' ≥ 1 such that D(0, 0, m) ⊢^+ D(0, 1, m') and reset_invariant(m') is true.
Proof. Follow D_finish to reach D(b(m), 0, b(m)+m). Follow start_reset0 to reach E0(b(m)+1, 1, b(m)+m+1). Following do_reset0 is enough to finish the proof, because E0(0, 1, m') = D(0, 1, m'). However, we need to show that b(m)+1 ≤ b(b(m)+m+1). b(m)+m+1 is a power of 2, so let b(m)+m+1 = 2^k to obtain b(b(m)+m+1) = b(2^k) = 2^k-1 = b(m)+m ≥ b(m)+1. □

Theorem D1_next. Let m ≥ 1 and suppose reset_invariant(m) is true. There exist m' ≥ 1 and a' ∈ {0,1} such that D(0, 1, m) ⊢^+ D(0, a', m') and reset_invariant(m') is true.

Proof

Follow D_finish to reach D(b(m), 1, b(m)+m). Follow start_reset1 to reach E1(2b(m)+2, 0, (b(m)+m+1)/2). Following do_reset1 is enough to finish the proof, because E0(0, a', m') = D(0, a', m'). However, do_reset1 needs the following proofs:

  • Proof that 2b(m)+2 ≤ 4b((b(m)+m+1)/2). Since b(m)+m+1 is a power of 2 and is at least 2, let b(m)+m+1 = 2^(x+1) for some x ≥ 0. Then 4b((b(m)+m+1)/2) = 4b(2^x) = 2(2^(x+1))-4 = 2(b(m)+m+1)-4 ≥ 2(b(m)+2+1)-4 = 2b(m)+2.
  • Proof that 2b(m)+2 = 2^(k+1) (2n'+1) where k ≥ 0, 2^(k+1) ≤ b((b(m)+m+1)/2), and n' ≥ 0. From reset_invariant(m), we have b(m)+1 = 2^k (2n'+1) for some k ≥ 0 and n' ≥ 2. It remains to show 2^(k+1) ≤ b((b(m)+m+1)/2). Since 2b(m)+2 ≤ 4b((b(m)+m+1)/2), it is enough to show 2^(k+1) ≤ (b(m)+1)/2. This is true because 2^(k+1) * 2 < 2^k * 5 ≤ 2^k (2n'+1) = b(m)+1. □

Theorem D_next. Let m ≥ 1 and a ∈ {0,1}. Suppose reset_invariant(m) is true. There exist m' ≥ 1 and a' ∈ {0,1} such that D(0, a, m) ⊢^+ D(0, a', m') and reset_invariant(m') is true.
Proof. If a = 0 then apply D0_next. If a = 1 then apply D1_next. □

Theorem D0_nonhalt. For all m ≥ 1, D(0, 0, m) will not reach a halting configuration. (Thanks to @meithecatte for contributing this theorem!)
Proof. Follow D0_next to reach D(0, 1, m') where m' ≥ 1 and reset_invariant(m') is true. Then follow D_next indefinitely. □

Skelet #26 and #15 do not halt

Corollary nonhalt. Skelet #26 does not halt.
Proof. Simulate Skelet #26 until it reaches D(0, 0, 11). Then apply D0_nonhalt. □

Corollary nonhalt (in Skelet15.v). Skelet #15 does not halt. (Thanks to @meithecatte for contributing this proof!)
Proof. Permute the states and flip the left/right transitions. As a result, Skelet #15 is Skelet #26 with the starting state as E. Simulate Skelet #15 until it reaches D(0, 0, 1), then apply D0_nonhalt. □

2 Likes
2

Amazing work to both of you! I’m so excited to see that my “proof sketches” panned out! I’ve updated https://www.sligocki.com/2023/02/05/shift-overflow.html to link here.

Great work, but I think this needs a bit of a caveat. We don’t have a formal proof for most TMs IIUC. Most notably we don’t have a formal proof for the FAR decider, right? IIUC, the true statement is something like: among the “holdout” machines in The 30 to 34 CTL holdouts from BB(5) unproven by general deciders, only Skelet #17 is missing a formal proof.

3

That’s correct if coq/Lean/etc. is the standard.
And we’re still fussing with “the best” way to handle weighted automata proof-certs, including whether we can easily add non-determinism and cover the 5 “finned” TMs in the other thread. (That discussion is Discord-only for now.)

1 Like
4

Yeah, I’m not saying we need to prove all TMs in Coq or anything. I think the holdouts are certainly the most important since they had the most unique proofs with the least “independent verification”. Of course if we could get all of bb5 in Coq that would be pretty amazing.

5

It’s amusing to imagine a day when the weak link in the coq-formal proof is actually the TNF enumeration and elimination of non-champion halters…

1 Like