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

@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

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.

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

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.

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