1RB3RB1LB---2RB 2LA1RA4LB2LA2RA: Difference between revisions
Jump to navigation
Jump to search
Opus Review |
nonhalting proof unfinished |
||
| (One intermediate revision by the same user not shown) | |||
| Line 23: | Line 23: | ||
== Opus 4.7 Review == | == Opus 4.7 Review == | ||
<pre> | <pre> | ||
Bug 1: "2a, 2b, …" includes 0 but rules only hold for positive even digits | Bug 1: "2a, 2b, …" includes 0 but rules only hold for positive even digits | ||
The notation 2a, 2b, … in rules 2–5 denotes "even digits" but reads naturally as allowing 0. The rules are | The notation 2a, 2b, … in rules 2–5 denotes "even digits" but reads naturally as allowing 0. The rules are | ||
false when any middle digit is 0. | false when any middle digit is 0. | ||
Counterexample: [1, 0, 2]. Rule 5 would predict [0, 0, 2, 0] (odd-increment applied to leftmost inner odd — | Counterexample: [1, 0, 2]. Rule 5 would predict [0, 0, 2, 0] (odd-increment applied to leftmost inner odd — | ||
but there's no inner odd, so actually rule 3 fires with middle [0], predicting [0, 0, 2, 0]). The actual | but there's no inner odd, so actually rule 3 fires with middle [0], predicting [0, 0, 2, 0]). The actual | ||
TM simulation instead collapses over the zero and produces [3, 2] in 9 steps (rule-1-like). | TM simulation instead collapses over the zero and produces [3, 2] in 9 steps (rule-1-like). | ||
Root cause: a digit y encodes 4^y on the tape (so y = 0 means NO 4s). Without the 4-run to sweep over, the | Root cause: a digit y encodes 4^y on the tape (so y = 0 means NO 4s). Without the 4-run to sweep over, the | ||
separator interaction is different, and the sweep dynamics used to derive rules 3–5 don't fire. | separator interaction is different, and the sweep dynamics used to derive rules 3–5 don't fire. | ||
Bug 2: rule 1 can produce length-1 lists | Bug 2: rule 1 can produce length-1 lists | ||
[0, a] → [a+3] has length 1 — subsequent rules require length ≥ 2. So rule 1 needs an explicit precondition | [0, a] → [a+3] has length 1 — subsequent rules require length ≥ 2. So rule 1 needs an explicit precondition | ||
that the input list has length ≥ 3 (i.e., there IS a b after a). | that the input list has length ≥ 3 (i.e., there IS a b after a). | ||
Corrected rules | Corrected rules | ||
[x, y, z] := 1 <B 4^x 12 4^y 12 4^z (encoding; B is state, 1<B means state B on symbol 1) | [x, y, z] := 1 <B 4^x 12 4^y 12 4^z (encoding; B is state, 1<B means state B on symbol 1) | ||
Start: [1, 1] | Start: [1, 1] | ||
(R1) [0, a, b, …] → [a+3, b, …] | (R1) [0, a, b, …] → [a+3, b, …] | ||
where the input has length ≥ 3 (the "…" allows empty tail, but `b` must exist). | where the input has length ≥ 3 (the "…" allows empty tail, but `b` must exist). | ||
(R2) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 0] → Halt | (R2) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 0] → Halt | ||
middle digits are strictly positive even (each 2aᵢ+2 ≥ 2); j ≥ 0. | middle digits are strictly positive even (each 2aᵢ+2 ≥ 2); j ≥ 0. | ||
(R3) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+2] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+2, 0] | (R3) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+2] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+2, 0] | ||
middle positive even, last digit positive even; j ≥ 0. | middle positive even, last digit positive even; j ≥ 0. | ||
(R4) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, 1] | (R4) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, 1] | ||
middle positive even, last digit odd; j ≥ 0. | middle positive even, last digit odd; j ≥ 0. | ||
(R5) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1, x, …] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, x+1, …] | (R5) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1, x, …] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, x+1, …] | ||
middle positive even, then an odd 2m+1, then at least one more digit x (plus possibly a tail). | middle positive even, then an odd 2m+1, then at least one more digit x (plus possibly a tail). | ||
(R6) [2n+2, a, …] → [2n+1, a+1, …] | (R6) [2n+2, a, …] → [2n+1, a+1, …] | ||
leading is positive even (≥ 2); a arbitrary; tail arbitrary (may be empty). | leading is positive even (≥ 2); a arbitrary; tail arbitrary (may be empty). | ||
Consequences for the non-halt argument | Consequences for the non-halt argument | ||
- R2 (halt) is still the "bad" pattern, but defined over positive even middles only — configurations with a | - R2 (halt) is still the "bad" pattern, but defined over positive even middles only — configurations with a | ||
0 in the middle don't trigger R2; they just aren't reached. | 0 in the middle don't trigger R2; they just aren't reached. | ||
| Line 70: | Line 70: | ||
reached from [1, 1]. This is an invariant to be proved, not a property to be checked. | reached from [1, 1]. This is an invariant to be proved, not a property to be checked. | ||
- Rules R3, R4, R5 each require the middle digits to be strictly positive (≥ 2). | - Rules R3, R4, R5 each require the middle digits to be strictly positive (≥ 2). | ||
The structural proof in §3 of the paper (the 3 "secure types") is not affected by this fix — it already | The structural proof in §3 of the paper (the 3 "secure types") is not affected by this fix — it already | ||
treats the middle digits as an abstract even-valued block. But the rule derivation (§2, currently a | treats the middle digits as an abstract even-valued block. But the rule derivation (§2, currently a | ||
| Line 77: | Line 77: | ||
</pre> | </pre> | ||
The proof given by @dyuan01 is not yet verified. | This version of the rules was proven in Lean. The nonhalting proof given by @dyuan01 is not yet verified. Opus got stuck and Aristotle couldn't finish from that point either. See the current state, esp. the Aristotle summary in https://github.com/rwst/bbchallenge/tree/main/1RB3RB1LB---2RB_2LA1RA4LB2LA2RA | ||
(to be continued..) | |||
[[Category:BB(2,5)]] | [[Category:BB(2,5)]] | ||
Latest revision as of 07:24, 19 April 2026
1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (bbch) is a BB(2,5) machine whose behavior is similar to Skelet 17. A proof was given by Daniel Yuan (@dyuan01) of the machine's nonhalting on July 30th 2024. 1RB3RA2LB1LB1RB_2LA2RA4LA1LA--- (bbch) is equivalent to this machine.
I just checked whenever the beaver reaches the 1 on the left side, and calculated the tape for when it next reaches the left side. It would be nice if someone can verify these rules.
[x, y, z] := 1 <B 4^x 12 4^y 12 4^z [0, a, b, …] -> [a+3, b, …] [2n+1, 2a, 2b, …, 0] -> Halt [2n+1, 2a, 2b, …, 2m+2] -> [2n, 2a, 2b, …, 2m+2, 0] [2n+1, 2a, 2b, …, 2m+1] -> [2n, 2a, 2b, …, 2m+1, 1] [2n+1, 2a, 2b, …, 2m+1, x, …] -> [2n, 2a, 2b, …, 2m+1, x+1, …] [2n+2, a, b, …] -> [2n+1, a+1, b, …] And you should start at [1, 1].
Review
Matthew House (@LegionMammal978) reviewed the above analysis on June 14th 2024 and agrees with it.
Opus 4.7 Review
Bug 1: "2a, 2b, …" includes 0 but rules only hold for positive even digits
The notation 2a, 2b, … in rules 2–5 denotes "even digits" but reads naturally as allowing 0. The rules are
false when any middle digit is 0.
Counterexample: [1, 0, 2]. Rule 5 would predict [0, 0, 2, 0] (odd-increment applied to leftmost inner odd —
but there's no inner odd, so actually rule 3 fires with middle [0], predicting [0, 0, 2, 0]). The actual
TM simulation instead collapses over the zero and produces [3, 2] in 9 steps (rule-1-like).
Root cause: a digit y encodes 4^y on the tape (so y = 0 means NO 4s). Without the 4-run to sweep over, the
separator interaction is different, and the sweep dynamics used to derive rules 3–5 don't fire.
Bug 2: rule 1 can produce length-1 lists
[0, a] → [a+3] has length 1 — subsequent rules require length ≥ 2. So rule 1 needs an explicit precondition
that the input list has length ≥ 3 (i.e., there IS a b after a).
Corrected rules
[x, y, z] := 1 <B 4^x 12 4^y 12 4^z (encoding; B is state, 1<B means state B on symbol 1)
Start: [1, 1]
(R1) [0, a, b, …] → [a+3, b, …]
where the input has length ≥ 3 (the "…" allows empty tail, but `b` must exist).
(R2) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 0] → Halt
middle digits are strictly positive even (each 2aᵢ+2 ≥ 2); j ≥ 0.
(R3) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+2] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+2, 0]
middle positive even, last digit positive even; j ≥ 0.
(R4) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, 1]
middle positive even, last digit odd; j ≥ 0.
(R5) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1, x, …] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, x+1, …]
middle positive even, then an odd 2m+1, then at least one more digit x (plus possibly a tail).
(R6) [2n+2, a, …] → [2n+1, a+1, …]
leading is positive even (≥ 2); a arbitrary; tail arbitrary (may be empty).
Consequences for the non-halt argument
- R2 (halt) is still the "bad" pattern, but defined over positive even middles only — configurations with a
0 in the middle don't trigger R2; they just aren't reached.
- The claim "the machine never halts" is now: no shape of the form [2n+1, positive-even…, 0] is ever
reached from [1, 1]. This is an invariant to be proved, not a property to be checked.
- Rules R3, R4, R5 each require the middle digits to be strictly positive (≥ 2).
The structural proof in §3 of the paper (the 3 "secure types") is not affected by this fix — it already
treats the middle digits as an abstract even-valued block. But the rule derivation (§2, currently a
placeholder) must use the stricter positivity hypothesis, and the base case "[1, 1] is secure" must be
shown without passing through any all-positive-even-middle configuration with a zero slipped in.
This version of the rules was proven in Lean. The nonhalting proof given by @dyuan01 is not yet verified. Opus got stuck and Aristotle couldn't finish from that point either. See the current state, esp. the Aristotle summary in https://github.com/rwst/bbchallenge/tree/main/1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (to be continued..)