Closed Tape Language (CTL)

Closed tape language (CTL) is a class of methods to prove that a Turing machine does not stop. A Turing machine may go through an infinite number of configurations while running, but we can classify them into a finite number of classes in a suitable way, and prove that each configuration in a class reaches another configuration (instead of halting) in some class after running for one step.

Regular CTL

See also: https://www.sligocki.com/2022/06/10/ctl.html

We use two DFAs (one with state sets L and R respectively) and an accepting set A to describe each classes.

The elements in set A have the form (l,r,q,s): L×R×Q×Σ, where Q is the state set of the TM, Σ is the symbol set of the TM, and (l,r,q,s) means the class of configurations in the form of 0^inf x q> s y 0^inf s.t. the DFA L gets state l when the string x is input, the DFA R gets state r when the string y (reversed) is input.

A variant is use (l,r,q,d): L×R×Q×{-1,+1}, and d=-1 means 0^inf x <q y 0^inf, d=+1 means 0^inf x q> y 0^inf.

DFA generator

Assume we have set S, function f:S×Σ→S and s0∈S, we can build a DFA incrementally: the starting state of the DFA is s0, the transtion (s0,0) is defined as s0, all other transitions are undefined at the beginning, and whenever we need to use a transition (a,b): S×Σ, we define it as f(a,b).

The DFA L,R and the accepting set A can be generated using this method.

Initially we have A={(s0,s0,q0,+1)}, where q0∈Q is the initial state of the TM, then we update A until it's closed under running for one step:

If (l,f(r,s),q,+1)∈A, and r is a visited state in R, and TM(q,s) = (q',s',+1), we add (f(l,s'),r,q',+1) to A.

If (l,f(r,s),q,+1)∈A, and r is a visited state in R, and TM(q,s) = (q',s',-1), we add (l,f(r,s'),q',-1) to A.

If (f(l,s),r,q,-1)∈A, and l is a visited state in L, and TM(q,s) = (q',s',-1), we add (l,f(r,s'),q',-1) to A.

If (f(l,s),r,q,-1)∈A, and l is a visited state in L, and TM(q,s) = (q',s',+1), we add (f(l,s'),r,q',+1) to A.

A state of a DFA is visited iff it appears at least once in A.

If we visit TM(q,s) and it's a halting transition, this method failed.

TM: Q×Σ→Q×Σ×{-1,+1} is the transition table of the turing machine.

This algorithm may not halt when |S| is infinite (or very slow when |S| is large), so we usually add a time limit or step limit to it.

RWL_mod

s0 = []
f([(x,n,m)]+z,x) = g([(x,min(n+1,N),(m+1)%M)]+z)
f(z,x) = g([(x,1,1)]+z), otherwise
g(a+[b]) = a, len(a+[b])>=L
g(a) = a, len(a)<L
where L,N,M are parameters, typical values ​​are N=2, M=1,2,3, 1<=L<=16.

CPS_LRU

s0 = ([],[],[])
f((s1,s2,        s3),x) = (s1,s2,[x]+s3), len(s3)<N3
f((s1,s2,        s3),x) = ([x]+s1,s2,s3), len(s1)<N1
f((s1,s2+[z],    s3),x) = (s1',[y]+s2,s3), len(s2+[z])=N2 and y not in s2 and [x]+s1=s1'+[y]
f((s1,s2,        s3),x) = (s1',[y]+s2,s3), y not in s2 and [x]+s1=s1'+[y]
f((s1,s2+[y]+s2',s3),x) = (s1',[y]+s2+s2',s3), y not in s2 and [x]+s1=s1'+[y]
when multiple rules match, take the first one.
s1 is a queue, s2 is an LRU cache, s3 is a stack that never pops.
N1,N2,N3 are parameters, typical values are N1=0,1, N3=0,1, N2=0,1,2,3.

n-gram CPS

n-gram CPS is the special case of CPS_LRU where N2=N3=0, N1=n.

FAR-direct

TODO

See https://github.com/bbchallenge/bbchallenge-deciders/tree/main/decider-finite-automata-reduction

machine transform

n-gram CPS can be much more powerful if we transform the TM properly. Such a transformation should not cause a halting Turing machine to nonhalt.

macro machine

Divide the tape into fixed size blocks, each block is a symbol in the transformed machine.

local transition history

The Turing machine can be modified to write down and update extra data at each step. We use the f defined in CPS_LRU (update the extra data as f(h,(q,s)) when the machine is at state q, read symbol (s,h) where s is the original symbol and h is extra data).

MITMWFAR

See Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR).