After reading the formal proof, I wrote a forward implementation of this decider that uses the Halting Segment graph construction and Remark 5.5. Sadly, I couldn’t find anything to compare my results with.
The official decider used a backward approach that decided ~2% fewer machines. e.g. on 710207, my decider said non-halt, but the official decider said undecided.
Here is my code and my results:
/*
g++ -O2 -std=c++17 "-Wl,--stack,524288000" bb5\5_halting_segment\dec_halting_segment.cpp -o bb5\5_halting_segment\dec_halting_segment.exe
remaining machines: 1538624
N = 1 decided 0 machines in 2 seconds
N = 2 decided 267268 machines in 3 seconds
N = 3 decided 602813 machines in 6 seconds
N = 4 decided 795673 machines in 9 seconds
N = 5 decided 897113 machines in 10 seconds
N = 6 decided 949970 machines in 13 seconds
N = 7 decided 979906 machines in 19 seconds
N = 8 decided 998380 machines in 26 seconds
N = 9 decided 1009465 machines in 41 seconds
N = 10 decided 1016092 machines in 65 seconds
N = 11 decided 1020095 machines in 110 seconds
N = 12 decided 1022536 machines in 198 seconds
N = 13 decided 1024140 machines in 364 seconds
N = 14 decided 1025054 machines in 702 seconds
N = 15 decided 1025665 machines in 1341 seconds
*/
#include <bits/stdc++.h>
using namespace std;
typedef string TM;
struct Tape {
const int x;
int get(const int pos) const {
return (x>>pos)&1;
}
Tape set(const int pos, const int val) const {
if (get(pos)==val) return {x};
return {x^(1<<pos)};
}
};
// a configuration consists of:
// state (5 choices)
// head position (N+2 choices)
// tape (2^N choices)
int N;
TM machine;
vector<vector<vector<bool>>> visited; // indices are: state, head position, tape
vector<vector<bool>> haltPos; // indices are: transition (10 choices), head position
void setHaltPos(const int offset, const int head) {
haltPos.at(offset/3).at(head+1)=1;
}
void dfs(const int state, const int head, const Tape tape) {
// base case
if (visited.at(state-1).at(head+1).at(tape.x)) return;
visited.at(state-1).at(head+1).at(tape.x)=1;
// recursive case
if (0<=head && head<N) {
// middle, follow the transition
const int offset=(state-1)*6+tape.get(head)*3;
if (machine[offset+2]==0) setHaltPos(offset, head);
else {
const int newHead=head+(machine[offset+1]?-1:1);
dfs(machine[offset+2],newHead,tape.set(head,machine[offset]));
}
return;
}
// either -1 or N
{
const int offset=(state-1)*6; // follow 0 transition
if (machine[offset+2]==0) setHaltPos(offset, head);
else {
// head position didn't change
dfs(machine[offset+2],head,tape);
// head position changed
const int newHead=head+(machine[offset+1]?-1:1);
if (0<=newHead && newHead<N) dfs(machine[offset+2],newHead,tape);
}
}
{
const int offset=(state-1)*6+3; // follow 1 transition
if (machine[offset+2]==0) setHaltPos(offset, head);
else {
// head position didn't change
dfs(machine[offset+2],head,tape);
// head position changed
const int newHead=head+(machine[offset+1]?-1:1);
if (0<=newHead && newHead<N) dfs(machine[offset+2],newHead,tape);
}
}
}
// modify "N" and "machine" before calling
bool decider_halting_segment() {
visited=vector<vector<vector<bool>>>(5,vector<vector<bool>>(N+2,vector<bool>(1<<N,0)));
haltPos=vector<vector<bool>>(10,vector<bool>(N+2,0));
// todo: this is very inefficient, because it traverses the entire graph. optimize it later.
for (int pos=-1; pos<=N; pos++) dfs(1,pos,{0});
// count covered and uncovered halting transitions
int covered=0, uncovered=0;
for (int i=0; i<10; i++) {
if (machine[i*3+2]!=0) continue;
int count=0;
for (int j=0; j<N+2; j++) {
if (haltPos.at(i).at(j)) count++;
}
if (count==N+2) covered++;
else uncovered++;
}
assert(covered>0 || uncovered>0);
return covered==0 && uncovered>0; // true = doesn't halt, see remark 5.5
}
// discard tm's from previous deciders
const int LIM=88664064;
char status[LIM];
int remain=LIM;
void discard(const char* filename) {
FILE* f=fopen(filename,"rb");
while (1) {
int a0=fgetc(f);
if (a0==EOF) break;
int a1=fgetc(f);
int a2=fgetc(f);
int a3=fgetc(f);
int a=(a0<<24)+(a1<<16)+(a2<<8)+a3;
assert(status[a]==0);
status[a]=1;
remain--;
}
fclose(f);
}
int main() {
discard("../2_cycler/cyclers-run-11c0ef00e9c2-time-1000-space-500-minIndex-0-maxIndex-14322029");
discard("../3_translated_cycler/translated-cyclers-run-8f5b2539279a-time-1000-space-500-minIndex-14322029-maxIndex-88664064");
discard("../3_translated_cycler/translated-cyclers-run-725fd45b37eb-time-10000-space-5000-minIndex-14322029-maxIndex-88664064");
discard("../3_translated_cycler/translated-cyclers-run-85454189d410-time-10000-space-5000-minIndex-14322029-maxIndex-88664064");
discard("../4_backward_reasoning/backward-reasoning-run-7edeea99bc2d-depth-50-minIndex-0-maxIndex-88664064");
vector<pair<int,TM>> machines;
FILE* f=fopen("../all_5_states_undecided_machines_with_global_header","r");
for (int i=0; i<LIM; i++) {
if (i==0) fseek(f,(i+1)*30LL,SEEK_SET);
char ch[30];
fread(ch,1,30,f);
if (status[i]==1) continue;
machines.push_back({i,string(ch,ch+30)});
}
fclose(f);
printf("remaining machines: %d\n",machines.size());
for (N=1; N<=15; N++) {
string filename="dec_halting_segment_out_"+to_string(N);
FILE* f=fopen(filename.c_str(),"wb");
int decided=0;
auto time0 = chrono::steady_clock::now();
for (auto [i,m] : machines) {
machine=m;
if (decider_halting_segment()) {
decided++;
fputc((i>>24)&255,f);
fputc((i>>16)&255,f);
fputc((i>>8)&255,f);
fputc((i>>0)&255,f);
}
}
auto time1 = chrono::steady_clock::now();
printf("N = %d decided %d machines in %d seconds\n",N,decided,chrono::duration_cast<std::chrono::seconds>(time1-time0).count());
fclose(f);
}
}
Afterwards, I wrote a weaker version that agrees with the official backward decider on N = 7, 9, 11, 13, 15. Here’s a list of changes that I made:
- If the head position is outside of the segment, don’t keep track of the state.
- Only run the decider on odd N.
- For each halting transition, only check the segment’s middle position. (This is Remark 5.5 except weaker)
Here is my code and my results:
/*
g++ -O2 -std=c++17 "-Wl,--stack,524288000" bb5\5_halting_segment\dec_halting_segment_weaker.cpp -o bb5\5_halting_segment\dec_halting_segment_weaker.exe
remaining machines: 1538624
N = 1 decided 0 machines in 2 seconds
N = 3 decided 301723 machines in 5 seconds
N = 5 decided 674458 machines in 8 seconds
N = 7 decided 855186 machines in 14 seconds
N = 9 decided 943633 machines in 29 seconds
N = 11 decided 983961 machines in 75 seconds
N = 13 decided 1002808 machines in 240 seconds
N = 15 decided 1012659 machines in 897 seconds
*/
#include <bits/stdc++.h>
using namespace std;
typedef string TM;
struct Tape {
const int x;
int get(const int pos) const {
return (x>>pos)&1;
}
Tape set(const int pos, const int val) const {
if (get(pos)==val) return {x};
return {x^(1<<pos)};
}
};
// a configuration consists of:
// state (5 choices)
// head position (N+2 choices)
// tape (2^N choices)
int N;
TM machine;
vector<vector<vector<bool>>> visited; // indices are: state, head position, tape
vector<vector<bool>> haltPos; // indices are: transition (10 choices), head position
void setHaltPos(const int offset, const int head) {
haltPos.at(offset/3).at(head+1)=1;
}
void dfs(int state, const int head, const Tape tape) {
// base case
if (head==-1 || head==N) state=1; // consolidate states
if (visited.at(state-1).at(head+1).at(tape.x)) return;
visited.at(state-1).at(head+1).at(tape.x)=1;
// recursive case
if (0<=head && head<N) {
// middle, follow the transition
const int offset=(state-1)*6+tape.get(head)*3;
if (machine[offset+2]==0) setHaltPos(offset, head);
else {
const int newHead=head+(machine[offset+1]?-1:1);
dfs(machine[offset+2],newHead,tape.set(head,machine[offset]));
}
return;
}
// either -1 or N, follow all transitions
for (int offset=0; offset<30; offset+=3) {
if (machine[offset+2]==0) setHaltPos(offset, head);
else {
// head position changed
const int newHead=head+(machine[offset+1]?-1:1);
if (0<=newHead && newHead<N) dfs(machine[offset+2],newHead,tape);
}
}
}
// modify "N" and "machine" before calling
bool decider_halting_segment() {
visited=vector<vector<vector<bool>>>(5,vector<vector<bool>>(N+2,vector<bool>(1<<N,0)));
haltPos=vector<vector<bool>>(10,vector<bool>(N+2,0));
// todo: this is very inefficient, because it traverses the entire graph. optimize it later.
for (int pos=-1; pos<=N; pos++) dfs(1,pos,{0});
// count covered and uncovered halting transitions
int covered=0, uncovered=0;
for (int i=0; i<10; i++) {
if (machine[i*3+2]!=0) continue;
if (haltPos.at(i).at((N+1)/2)) covered++;
else uncovered++;
}
assert(covered>0 || uncovered>0);
return covered==0 && uncovered>0; // true = doesn't halt
}
// discard tm's from previous deciders
const int LIM=88664064;
char status[LIM];
int remain=LIM;
void discard(const char* filename) {
FILE* f=fopen(filename,"rb");
while (1) {
int a0=fgetc(f);
if (a0==EOF) break;
int a1=fgetc(f);
int a2=fgetc(f);
int a3=fgetc(f);
int a=(a0<<24)+(a1<<16)+(a2<<8)+a3;
assert(status[a]==0);
status[a]=1;
remain--;
}
fclose(f);
}
int main() {
discard("../2_cycler/cyclers-run-11c0ef00e9c2-time-1000-space-500-minIndex-0-maxIndex-14322029");
discard("../3_translated_cycler/translated-cyclers-run-8f5b2539279a-time-1000-space-500-minIndex-14322029-maxIndex-88664064");
discard("../3_translated_cycler/translated-cyclers-run-725fd45b37eb-time-10000-space-5000-minIndex-14322029-maxIndex-88664064");
discard("../3_translated_cycler/translated-cyclers-run-85454189d410-time-10000-space-5000-minIndex-14322029-maxIndex-88664064");
discard("../4_backward_reasoning/backward-reasoning-run-7edeea99bc2d-depth-50-minIndex-0-maxIndex-88664064");
vector<pair<int,TM>> machines;
FILE* f=fopen("../all_5_states_undecided_machines_with_global_header","r");
for (int i=0; i<LIM; i++) {
if (i==0) fseek(f,(i+1)*30LL,SEEK_SET);
char ch[30];
fread(ch,1,30,f);
if (status[i]==1) continue;
machines.push_back({i,string(ch,ch+30)});
}
fclose(f);
printf("remaining machines: %d\n",machines.size());
for (N=1; N<=15; N+=2) {
string filename="dec_halting_segment_weaker_out_"+to_string(N);
FILE* f=fopen(filename.c_str(),"wb");
int decided=0;
auto time0 = chrono::steady_clock::now();
for (auto [i,m] : machines) {
machine=m;
if (decider_halting_segment()) {
decided++;
fputc((i>>24)&255,f);
fputc((i>>16)&255,f);
fputc((i>>8)&255,f);
fputc((i>>0)&255,f);
}
}
auto time1 = chrono::steady_clock::now();
printf("N = %d decided %d machines in %d seconds\n",N,decided,chrono::duration_cast<std::chrono::seconds>(time1-time0).count());
fclose(f);
}
}
