Skip to content

Instantly share code, notes, and snippets.

@savask
Last active May 20, 2023 09:05
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save savask/888aa5e058559c972413790c29d7ad72 to your computer and use it in GitHub Desktop.
Save savask/888aa5e058559c972413790c29d7ad72 to your computer and use it in GitHub Desktop.
The bouncers decider
{-
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:
<S u1 w1^n1 u2 w2^n2 ... uk wk^nk (*)
and after a finite number of steps and shift rules we end at a tape
<S u1 w1^(n1+c1) u2 w2^(n2+c2) ... uk wk^(nk+ck)
where c1, ..., ck are some positive constants. Then the language specified by the regular expression
<S u1 (w1) u2 (w2) ... uk (wk)
is "eventually closed" (here (w) means that the string w is repeated one or more times) with respect to our Turing machine,
i.e. given a tape from that language, the machine reaches a tape from the language in a finite amount of steps and shift rules
(and does not halt in the process). We call a Turing machine a bouncer if it satisfies conditions above (and similar conditions
for the case when the tape is ... S>), and one can reach a tape of the form <S u1 w1^n1 ... uk wk^nk (or ... S>) 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) = <S u1 w1^n u2 w2^n ... uk wk^n.
One can prove that one abstract variable is enough, so we do not lose anything by using only n.
We find s(n) with a dynamic programming algo (see function toPowers), and we output
<S u1 (w1) u2 (w2) ... uk (wk) (**)
as our candidate tape formula. Similarly, we look for tapes ending in S>.
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 () = -- ??? <S
case runTillBorder prg tape of
Halt -> 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 <S).
extractShiftRule :: Program -> 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) -- . <S
doMacroMove prg (FTape l (Right s) ((Const r):rs)) = do -- l S> 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 <S r
Tape l' h' r' <- maybeToResult $ doMove prg (Tape l (Left s) [])
return $ FTape ((Const l'):ls) h' ((Const r'):r)
doMacroMove prg (FTape ((Power l):ls) (Left s) r) = -- ls l^e <S r
let (r1, r2) = takeConstPrefix r in
case extractShiftRule prg (Tape l (Left s) r1) of
Nothing -> Halt
Just (Tape _ h' r') -> let ll = length l
la = length r' - ll
(l1a, r1') = splitAt la r1 -- ls l^e <S r == ls l^e <S r1 r2 == ls l^e <S a r1' r2
(a, l') = splitAt la r' -- Shift rule: l <S a -> <S a l'
in return $ FTape ls h' ((Const a):(Power l'):(Const r1'):r2) -- ls <S a l'^e r1' r2
doMacroMove prg _ = Halt -- Report error if we cannot make a move.
-- Check if two tapes are increasing, i.e. the second tape is a special case of the first.
-- For example, tapes 1(0) and 10(0) are increasing, while 10(0)1 and 1(0)1 are not.
-- We assume that powers in input tapes are right-aligned.
isIncreasing :: FTape -> 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 .<S ...
isRecord :: Tape -> 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 <tab> STEP N", meaning one needs to make N usual steps from the tape tp,
-- "tp <tab> RULE r", meaning one needs to apply a shift rule r, or
-- "tp <tab> 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) <S r
case extractShiftRule' (Tape l (Left h) (fst $ takeConstPrefix r)) of
Nothing -> ""
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
@sligocki
Copy link

sligocki commented May 14, 2023

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
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment