Instantly share code, notes, and snippets.

Last active May 20, 2023 09:05
Show Gist options
The bouncers decider
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {- This is an implementation of a bouncers decider. It should roughly correspond to Tony's bouncers, Skelet's linearly increasing sequence and Shawn's diff rules. We assume that the Turing machine head lives in between the cells, and can point to the left or to the right. If there are strings a, b, b' and a state S such that starting from tape a S> b we can reach b' a S> in several steps, we say that we have a "shift rule". A shift rule allows the machine to jump over a power of b: a S> b^n --> b'^n a S> Similarly one defines a shift rule with the head pointing to the left. Let u1, ..., uk, w1, ..., wk be (possibly empty) strings, and let n1, ..., nk be abstract variables. Say we are given a tape: ), and one can reach a tape of the form ) from the starting tape. Clearly bouncers do not halt by the usual CTL argument. The algorithm for deciding bouncers consists of two steps. First, we try to find a candidate tape formula of the form (*). To do that, we run the machine for stepLimit amount of steps, and record tapes where the head is at the border and looks outside Then we use Tony's heuristic and find 4 tapes such that their lengths are in an arithmetic progression and step counts are in a quadratic progression. We take 3 such tapes s0, s1, s2 and try to express them as s(n) = . For example, if we have s0 = 101 S> s1 = 110011 S> s2 = 110100111 S> then s(n) = 1 10^n 0 1^n 1 S> and the tape formula will be 1 (10) 0 (1) 1 S>. On the second step we try to prove that our tape formula is "increasing", that is, after a finite number of steps and shift rules we end up in a less general tape formula. To do that, we run the machine for stepLimit macro steps starting from (**), where one macro step is just a usual Turing machine step if the head points at a constant segment (i.e. u1, ..., uk) and a shift rule if the head points at a power (i.e. (w1), ..., (wk)). After each macro step we align powers away from the head (i.e. to the left on the left half of the tape, and to the right on the right half). If we have "... (w) x ..." on the tape and wx = xw' for some string w', then we can move (w) to the right and obtain "... x (w') ...". "Aligning" means that we move powers in that manner as far as possible. (As a small digression for people with rule-based deciders: the reason for aligning is that instead of using real formulae like "C> 110^(n+3)" this decider uses "C> 110110110(110)". Sometimes we need to decrease the formula, like C> 110^(n+3) --> C> 110 110^(n+2) --> 101 D> 110^(n+2) --> 101 111^(n+2) D> so by aligning all powers away from the machine head we side-step this problem, as we defer shift rule application as much as we can.) For example, we could have the following steps: 1 (10) 0 A> 1 (1) --> 1 (10) 00 B> (1) [a usual step] 1 (10) 00 B> (1) --> 1 (10) 0 (0) 0 B> [used a shift rule 0 B> 1 --> 0 0 B>] The resulting tape 1 (10) 0 (0) 0 B> will be aligned to 1 (10) (0) 00 B>. After each macro step we check if the resulting tape is a special case of the original tape. For example, suppose we started with 1 (10) 0 (1) 1 S> and after some steps and shift rules we end in 1 (10) 100 (1) 11 S>. The second tape formula is a special case of the first, since (10) 10 lies in (10) and (1) 1 lies in (1). Since all powers are aligned, we can check if the second string is a special case of the first with a greedy algorithm (see function isIncreasing). If we found an increasing pair of tape formulae then the decider succeeds and outputs the tape formula. If we cannot find an increasing tape in a given amount of time, or if the machine halts or it is not possible to perform a macro step (say, the machine head faces a power but there is no relevant shift rule to jump over it), then we output failure. The decider tries the above procedure for all triplets s0, s1, s2 satisfying Tony's heuristic, with some minor optimizations (for example, to avoid checking tapes which lie in the same arithmetic progression). Essentially the only parameter is stepLimit, one can also comment out "take 10" in function increasingSequence to check all tape formulae instead of the first 10 only (that slows down the decider considerably, though). stepLimit equal to 1000000 and "take 10" commented out are enough to reproduce Justin's bouncers run on the current undecided index. -} import qualified Data.Map as M import qualified Data.Array as A import Data.Maybe (catMaybes, mapMaybe) import Data.List (nubBy, inits, isPrefixOf) import Control.Monad (guard) -- States are represented by integers starting from 1. type State = Int -- We assume that the Turing machine head lives in between the cells of the tape, -- so at each stage the head has a fixed state and can point either to the left or right. type Head = Either State State -- Get current state. state :: Head -> State state = either id id -- The tape is a zipper, i.e. we store the left part of the tape, the head and the right part of the tape. -- For example, configuration 110 A> 001 is represented by Tape [False, True, True] (Right 1) [False, False, True]. data Tape = Tape { left :: [Bool], at :: Head, right :: [Bool] } deriving (Eq) -- showBools [True, False, True] == "101" showBools :: [Bool] -> String showBools = map (\b -> if b then '1' else '0') -- We use 0 and 1 for cell symbols, A to Z for machine states, -- a dash - for the invalid state and <, > to signify the direction the head is pointing to. instance Show Tape where show (Tape l a r) = showBools (reverse l) ++ (either (\s -> "<" ++ [('-':['A'..'Z']) !! s]) (\s -> [('-':['A'..'Z']) !! s] ++ ">") a) ++ showBools r -- Tell the symbol the head is looking at. peek :: Tape -> Bool peek (Tape l a r) = case a of Left s -> if null l then False else head l Right s -> if null r then False else head r -- The Turing machine program is a mapping from (current symbol, state) to (new symbol, new state + direction). type Program = M.Map (Bool, State) (Bool, Head) -- Remove the top symbol from a list, and do nothing if it's empty. pop :: [a] -> [a] pop ls | null ls = [] | otherwise = tail ls -- Do one move of the Turing machine. Returns Nothing if the machine halts. doMove :: Program -> Tape -> Maybe Tape doMove prg t@(Tape l a r) = do (c, a') <- M.lookup (peek t, state a) prg case (a, a') of (Left _, Left _) -> return $Tape (pop l) a' (c:r) (Left _, Right _) -> return$ Tape (c:(pop l)) a' r (Right _, Right _) -> return $Tape (c:l) a' (pop r) (Right _, Left _) -> return$ Tape l a' (c:(pop r)) -- Replace Either contents by (). direction :: Either a b -> Either () () direction = either (const $Left ()) (const$ Right ()) -- The simulation may halt, loop indefinitely or return some result. data Result a = Halt | Loop | Result a deriving (Eq, Show) instance Functor Result where fmap f (Result a) = Result (f a) fmap _ Halt = Halt fmap _ Loop = Loop instance Applicative Result where pure a = Result a (Result f) <*> (Result a) = Result (f a) (Result f) <*> Halt = Halt (Result f) <*> Loop = Loop Halt <*> _ = Halt Loop <*> _ = Loop instance Monad Result where (Result a) >>= f = f a Halt >>= _ = Halt Loop >>= _ = Loop -- Empty tape. start :: Tape start = Tape [] (Right 1) [] -- Run the machine for a given amount of steps. -- Returns the intermediate tapes. runFor :: Program -> Int -> [Tape] runFor prg imax = go 1 start where go i t | i > imax = [] | otherwise = case doMove prg t of Nothing -> [] Just t' -> t : go (i+1) t' -- Given a program and a preset tape, run the Turing machine until -- it exits from one of the two sides of the tape. -- If the machine halts or loops in the process, we report that. runTillBorder :: Program -> Tape -> Result Tape runTillBorder prg tape = go 0 tape where len = length (left tape) + length (right tape) stepsCap :: Integer stepsCap = 1 + (fromIntegral $M.size prg)*(fromIntegral$ len+1)*2^(fromIntegral len) -- Upper bound on the number of iterations go step t@(Tape l a r) | null l && direction a == Left () = return t | null r && direction a == Right () = return t | step > stepsCap = Loop | otherwise = case doMove prg t of Nothing -> Halt Just t' -> go (step+1) t' -- A shift rule is a rule of the form "a S> b -> b' a S>". -- Given a program and a rule (represented as a tape) we check if it is a shift rule and return the resulting tape, if it is. -- For example, if "10 B> 1 -> 0 10 B>" is a shift rule, then -- isShiftRule prg (Tape [False, True] (Right 2) [True]) == Just (Tape [False, True, False] (Right 1) []) isShiftRule :: Program -> Tape -> Maybe Tape isShiftRule prg tape | direction (at tape) == Right () = -- S> ??? case runTillBorder prg tape of Halt -> Nothing Loop -> Nothing Result t -> if at tape == at t && ((left tape) isPrefixOf (left t)) then return t else Nothing | direction (at tape) == Left () = -- ??? Nothing Loop -> Nothing Result t -> if at tape == at t && ((right tape) isPrefixOf (right t)) then return t else Nothing | otherwise = Nothing type Segment = [Bool] -- A tape expression consists of constant segments and powers, i.e. one-or-more repetitions of some string. data TapeExpr = Const Segment | Power Segment deriving (Eq, Ord) instance Show TapeExpr where show (Const s) = showBools s show (Power s) = "(" ++ showBools s ++ ")" turnAround :: TapeExpr -> TapeExpr turnAround (Const s) = Const (reverse s) turnAround (Power s) = Power (reverse s) -- Formula tape, analogue of Tape but with tape expressions. data FTape = FTape { leftF :: [TapeExpr], atF :: Head, rightF :: [TapeExpr] } deriving (Eq, Ord) instance Show FTape where show (FTape l h r) = (unwords . map (show . turnAround) $reverse l) ++ " " ++ (either (\s -> "<" ++ [('-':['A'..'Z']) !! s]) (\s -> [('-':['A'..'Z']) !! s] ++ ">") h) ++ " " ++ unwords (map show r) -- Concatenate constant segments together. glueConsts :: [TapeExpr] -> [TapeExpr] glueConsts [] = [] glueConsts ((Const []):xs) = glueConsts xs glueConsts [x] = [x] glueConsts ((Const x1):(Const x2):xs) = glueConsts ((Const$ x1++x2):xs) glueConsts (x:xs) = x : glueConsts xs -- Align all powers to the right, i.e. (10|n)1 -> 1(01|n). alignRight :: [TapeExpr] -> [TapeExpr] alignRight [] = [] alignRight [x] = [x] alignRight ((Power x):(Const y):xs) = let -- We can replace "t (a as) a bs" by "t a (as a) bs". Function roll does that while it's possible roll t a [] = [Const (reverse t), Power a] roll t p@(a:as) c@(b:bs) | a == b = roll (b:t) (as ++ [a]) bs | otherwise = [Const (reverse t), Power p, Const c] in (roll [] x y) ++ alignRight xs alignRight ((Const y):xs) = (Const y) : alignRight xs alignRight (x:xs) = x : alignRight xs -- Pack the tape, i.e. glue constant blocks and align all powers to the right. pack :: FTape -> FTape pack (FTape l h r) = FTape (p l) h (p r) where p = glueConsts . alignRight . glueConsts -- Return the first Just value in a list. firstJust :: [Maybe a] -> Maybe a firstJust [] = Nothing firstJust ((Just a):ls) = Just a firstJust (Nothing:ls) = firstJust ls -- For tape "l S> r" try all suffixes l' of l to find a shift rule (same for Tape -> Maybe Tape extractShiftRule prg (Tape l (Right s) r) = firstJust [isShiftRule prg (Tape li (Right s) r) | li <- inits l] extractShiftRule prg (Tape l (Left s) r) = firstJust [isShiftRule prg (Tape l (Left s) ri) | ri <- inits r] -- Split a tape expression into a constant segment and the rest. takeConstPrefix :: [TapeExpr] -> (Segment, [TapeExpr]) takeConstPrefix ((Const s):t) = (s, t) takeConstPrefix t = ([], t) maybeToResult :: Maybe a -> Result a maybeToResult Nothing = Halt maybeToResult (Just a) = Result a -- Do one macro move of the machine, i.e. a usual move or run through a power (if it corresponds to a shift-rule). doMacroMove :: Program -> FTape -> Result FTape doMacroMove prg (FTape l (Right s) []) = doMacroMove prg (FTape l (Right s) [Const [False]]) -- S> . doMacroMove prg (FTape [] (Left s) r) = doMacroMove prg (FTape [Const [False]] (Left s) r) -- . r rs Tape l' h' r' <- maybeToResult $doMove prg (Tape [] (Right s) r) return$ FTape ((Const l'):l) h' ((Const r'):rs) doMacroMove prg (FTape l (Right s) ((Power r):rs)) = -- l S> r^e rs let (l1, l2) = takeConstPrefix l in case extractShiftRule prg (Tape l1 (Right s) r) of Nothing -> Halt Just (Tape l' h' _) -> let lr = length r la = length l' - lr (l1a, l1') = splitAt la l1 -- l S> r^e rs == l2 l1 S> r^e rs == l2 l1' a S> r^e rs (a, r') = splitAt la l' -- Shift rule: a S> r -> r' a S> in return $FTape ((Const a):(Power r'):(Const l1'):l2) h' rs -- l2 l1' r'^e a S> rs doMacroMove prg (FTape ((Const l):ls) (Left s) r) = do -- ls l Halt Just (Tape _ h' r') -> let ll = length l la = length r' - ll (l1a, r1') = splitAt la r1 -- ls l^e FTape -> Bool isIncreasing (FTape l h r) (FTape l' h' r') = h == h' && incr l l' && incr r r' where incr [] [] = True incr ((Const w):ws) ((Const w'):ws') = w isPrefixOf w' && incr ws (if w == w' then ws' else (Const$ drop (length w) w'):ws') incr ((Power w):ws) ((Power w'):ws') = w == w' && incr ws ws' incr t@((Power w):ws) ((Const w'):ws') = w isPrefixOf w' && incr t (if w == w' then ws' else (Const $drop (length w) w'):ws') incr _ _ = False -- Simulate the machine till it visits an increasing tape. runTillIncreasing :: Program -> FTape -> Result FTape runTillIncreasing prg tape = oneMove tape >>= go stepLimit where oneMove t = fmap pack$ doMacroMove prg t go 0 _ = Halt go s t | isIncreasing tape t = return tape | otherwise = oneMove t >>= go (s-1) -- Output tape lengths, step counts and head states when the machine is in a record position. recordStats :: [Tape] -> [(Int, Int, Head)] recordStats = map (\(s, t) -> (length (left t) + length (right t), s, at t)) . filter (\(_, t) -> isRecord t) . zip [0..] where -- Check if the machine just visited a new cell, i.e. if the tape is either ... S>. or . Bool isRecord (Tape [] (Left _) _) = True isRecord (Tape _ (Right _) []) = True isRecord _ = False -- Produces a list of tuples, where the first element -- of each tuple precedes the second. pairs :: [a] -> [(a, a)] pairs [] = [] pairs (x:xs) = [(x, y) | y <- xs] ++ pairs xs -- Check if the list is [a, a, ... a] isConst :: Eq a => [a] -> Bool isConst [] = True isConst (x:xs) = all (x == ) xs -- Find step counts which are in a polynomial progression such that at corresponding times -- the machine is in a record position and tape lengths are in an arithmetic progression. -- First argument is the polynomial degree, second is the list of tapes. Returns maximal progressions. linPolyTest :: Int -> [Tape] -> [[Int]] linPolyTest deg tapes = concatMap checkPair $pairs steps where records = recordStats tapes steps = map (\(s, _, _) -> s) records msteps = maximum steps arr = M.fromList$ map (\(s, l, h) -> (s, (l, h))) records -- Check if numbers are in a polynomial progression arePoly ls = let diff xs = zipWith (-) (tail xs) xs in isConst ((iterate diff ls) !! deg) checkPair (a1, a2) | snd (arr M.! a1) == snd (arr M.! a2) = -- check that machine heads at steps a1 and a2 are the same case mapM (M.lookup arr) [k*(a2 - a1) + a1 | k <- [0..(msteps - a1) div (a2-a1)]] of Just ts -> if length ts >= 4 && isConst (map snd ts) && arePoly (map fst ts) then [map fst ts] else [] _ -> [] | otherwise = [] -- Given three strings s0, s1, s2, try to express each as s(x) = u1 w1^x u2 w2^x ..., where wi, ui are some words. -- Such an expression is not unique (an example by J. Blanchard: 001^x 0^x 01001001^x == 0010010^x 01^x 001^x for x = 0, 1, 2), -- and we output only one possible expression. toPowers :: Segment -> Segment -> Segment -> Maybe [TapeExpr] toPowers s0 s1 s2 = mem A.! (0, 0) where mem = A.array ((0, 0), (ls0, ls1)) [((x, y), go x y) | x <- [0..ls0], y <- [0..ls1]] ls0 = length s0 ls1 = length s1 ls2 = length s2 -- Uses memoization with array mem. i0 and i1 are symbols dropped from s0 and s1 respectively. go i0 i1 | i0 == ls0 && i1 == ls1 && i2 == ls2 = return [] -- If all strings are empty | i1 < i0 = Nothing | otherwise = firstJust (skip : map pow (reverse . zip [1..] . take ((ls2 - i2) div 2) . tail $inits v1)) where v0 = drop i0 s0 v1 = drop i1 s1 v2 = drop i2 s2 i2 = i0 + (i1 - i0)*2 -- number of symbols dropped from s2 -- If strings start at the same symbol, try skipping it skip | null v0 || null v1 || null v2 = Nothing | head v0 == head v1 && head v1 == head v2 = fmap ((Const [head v0]):)$ mem A.! (i0+1, i1+1) | otherwise = Nothing -- If v1 = w v1' and v2 = w w v2', try reducing the problem to v0, v1', v2'. -- Here k is the length of w. pow (k, w) = if (w ++ w) isPrefixOf v2 then fmap (Power w :) $mem A.! (i0, i1+k) else Nothing -- Given three tapes, try obtaining a corresponding formula tape. toPowersTape :: Tape -> Tape -> Tape -> Maybe FTape toPowersTape t0 t1 t2 = do l <- toPowers (left t0) (left t1) (left t2) r <- toPowers (right t0) (right t1) (right t2) return . pack$ FTape l (at t2) r -- This constant is used when applying Tony's heuristic and -- when running the machine till it meets an increasing tape. stepLimit = 10000 -- Search for 3 tapes s0, s1, s2 in an arithmetic-quadratic progression (Tony's heuristic), -- and try obtaining a formula tape s(x) for those. s(1) is added to the output, for example, -- for s0 = 1, s1 = 10, s2 = 100 we'll have s(x) = 1 0^x and the output will contain "1 (0)". setupIncreasingTape :: Program -> [FTape] setupIncreasingTape prg = do let tapes = runFor prg (stepLimit+1) incts = map reverse . nubBy (\a b -> take 3 a == take 3 b) . map reverse . -- Remove sequences of steps which are a suffix of another sequence filter (\i -> length i >= 4) $linPolyTest 2 tapes -- Linear-quadratic heuristic history = A.listArray (0, stepLimit) tapes goodThread ts = let [s0, s1, s2] = take 3 ts t0 = history A.! s0 t1 = history A.! s1 t2 = history A.! s2 in toPowersTape t0 t1 t2 guard$ length tapes == (stepLimit+1) guard . not $null incts catMaybes$ map goodThread incts -- Returns the first result in a list, if it exists. firstResult :: [Result a] -> Maybe a firstResult [] = Nothing firstResult ((Result r):rs) = return r firstResult (_:rs) = firstResult rs -- Try to decide the machine as a bouncer. -- If the decider succeeded and there two increasing tapes s(1) and s(2), then it returns s(1). -- We consider only first 10 potential tape formulae, that is not enough sometimes, see exampleComplex. increasingSequence :: Program -> Maybe FTape increasingSequence prg = firstResult . map (runTillIncreasing prg) . take 10 $setupIncreasingTape prg -- A version of increasingSequence which outputs a detailed certificate. -- First line is "STEP N" , where N is the number of steps from the empty tape to the initial formula tape. -- The following lines have the form: -- "tp STEP N", meaning one needs to make N usual steps from the tape tp, -- "tp RULE r", meaning one needs to apply a shift rule r, or -- "tp END", meaning that we reached a tape, which is a special case of the initial formula tape. certificate :: Program -> Maybe String certificate prg = do tape <- increasingSequence prg let -- Tape history history = zip [0..]$ runFor prg stepLimit clean = concatMap (\c -> case c of Const x -> x; Power x -> x) -- Initial tape (converted from formula tape) tape' = Tape (clean $leftF tape) (atF tape) (clean$ rightF tape) firstStep = fst . head $filter (\(_, t) -> t == tape') history -- A version of isShiftRule which returns the full rule isShiftRule' start = isShiftRule prg start >>= \end -> return (start, end) -- A version of extractShiftRule which returns the full rule extractShiftRule' :: Tape -> Maybe (Tape, Tape) extractShiftRule' (Tape l (Right s) r) = firstJust [isShiftRule' (Tape li (Right s) r) | li <- inits l] extractShiftRule' (Tape l (Left s) r) = firstJust [isShiftRule' (Tape l (Left s) ri) | ri <- inits r] -- Comment what happens on the current step comment t@(FTape ((Power l):_) (Left h) r) = -- (l) "" Just (start, end) -> "RULE " ++ show start ++ " --> " ++ show end comment t@(FTape l (Right h) ((Power r):_)) = -- l S> (r) case extractShiftRule' (Tape (fst$ takeConstPrefix l) (Right h) r) of Nothing -> "" Just (start, end) -> "RULE " ++ show start ++ " --> " ++ show end comment t | isIncreasing tape t = "END" | otherwise = "STEP" -- Do one macro move with packing oneMove t = fmap pack $doMacroMove prg t -- Return the history of formula tapes go 0 _ = Halt go s t | isIncreasing tape t = return [t] | otherwise = fmap (t:) (oneMove t >>= go (s-1)) -- The history of formula tapes Result fhistory = oneMove tape >>= go stepLimit annotated = (tape, "STEP") : map (\t -> (t, comment t)) fhistory -- Replace STEP .. STEP by STEP n clumpSteps [] = [] clumpSteps cs = let (steps, rest) = span ((== "STEP") . snd) cs in if null steps then head rest : clumpSteps (tail rest) else (fst$ head steps, "STEP " ++ (show $length steps)) : clumpSteps rest -- The certificate string cert = unlines . map (\(t, c) -> show t ++ "\t" ++ c)$ clumpSteps annotated return $"STEP " ++ show firstStep ++ "\n" ++ cert -- Parse one transition of the machine description. parseOne :: String -> Maybe (Bool, Head) parseOne "1RZ" = Nothing parseOne "---" = Nothing parseOne (c:d:s:[]) | c elem "01" && d elem "LR" && s elem ['A'..'Z'] = let st = fromEnum s - fromEnum 'A' + 1 in return (c == '1', if d == 'L' then Left st else Right st) | otherwise = Nothing parseOne _ = Nothing -- Parse the compact machine description. parse :: String -> Program parse str = M.fromList . mapMaybe toCmd$ zip cells [(s, c) | s <- [1..states], c <- [False, True]] where states = (length str + 1) div 7 cells = concatMap (\w -> [take 3 w, drop 3 w]) . words $map (\c -> if c == '_' then ' ' else c) str toCmd (str, (s, c)) = parseOne str >>= \a -> return ((c, s), a) -- A bouncer. example :: Program example = parse "1RB1LE_1RC0LC_1LD0RA_0LA1RA_---0LB" -- A bouncer with "four partitions" in Tony's terminology. exampleFour :: Program exampleFour = parse "1RB0RD_1LC1LE_1RA1LB_---0RC_1LB0LE" -- A moving bouncer. Adds a lot of trailing zeros. exampleMoving :: Program exampleMoving = parse "1RB0LC_0LA1RC_0LD0LE_1LA1RA_---1LC" -- A bouncer which requires one to remove the "take 10" optimization. exampleComplex :: Program exampleComplex = parse "1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE" exampleHalt :: Program exampleHalt = parse "1RB1LC_0LA0LD_1LA1RZ_1LB1RE_0RD0RB" exampleLoop :: Program exampleLoop = parse "1RB0RC_0LA0LA_1LD---_1RE1LB_1LB0RD" -- Run the bouncers decider on standard input. -- Takes a list of machines in text format (one per line), outputs the machines solved. main = do file <- lines fmap getContents let rs = map (\p -> (p, increasingSequence (parse p))) file mapM_ (putStrLn . fst)$ filter (\(_, r) -> case r of Just _ -> True; _ -> False) rs -- Output solved -- mapM_ (putStrLn . fst) $filter (\(_, r) -> r == Nothing) rs -- Output unsolved machines -- print . length$ filter (\(_, r) -> case r of Just _ -> True; _ -> False) rs -- Output the number of solved -- let rs' = map (\p -> (p, certificate (parse p))) file -- mapM_ (\(m, Just c) -> putStrLn $m ++ "\n" ++ c)$ filter (\(_, r) -> r /= Nothing) rs' -- Output solved with certificates

This is really cool, it's interesting to see how you approached this without any computer algebra complexity :)

is "almost closed"

Is it not completely closed? What makes it almost?

after a finite number of steps and shift rules

Does this mean a constant number of steps and shift rules (irrespective of the tape exponents)? That is how I define rules like this, that each rule is a fixed sequence like [step, step, shift, shift, step, shift]. But I'm not sure if that's what you're saying here as well.

As a small digression for people with rule-based deciders

Really interesting, thanks for this targeted digression!

### savask commented May 14, 2023

Is it not completely closed? What makes it almost?

I think usually a closed tape language is supposed to be closed under one step, while in my case you may need several steps (and shift rules) to return to the same language.

Does this mean a constant number of steps and shift rules (irrespective of the tape exponents)?

Yes, since it depends only on the input tape formula which does not keep track of any exponents.