undecgen.lhs -- Generator for Haskell type system TM encodings Keith Wansbrough 1998-07-31..1998-07-31 This module generates Haskell (Hugs-1.3c) programs that encode Turing machines in the type system. First we define some data types: - a machine state is (State n), written "Qn" - a tape symbol is (Sym n), written "Sn" - an operation is either MoveL (move left), MoveR (move right), (Write s) (write symbol), or Halt (halt) - a rule is (Rule q s o q'), meaning if in state q and current symbol is s, do operation o and enter state q' (note if o is Halt then q' is irrelevant) - a Turing machine is a list of states, a list of symbols, and a list of rules > data State = State Int > > instance Show State where > showsPrec _ (State n) = showString "Q" . shows n > data Sym = Sym Int > > instance Show Sym where > showsPrec _ (Sym n) = showString "S" . shows n > data Op = MoveL | MoveR | Write Sym | Halt > > instance Show Op where > showsPrec _ MoveL = showString "L" > showsPrec _ MoveR = showString "R" > showsPrec _ (Write s) = shows s > showsPrec _ Halt = showString "HALT" > data Rule = Rule State Sym Op State > > instance Show Rule where > showsPrec _ (Rule q s o q') = showString "(" . shows q . showString "," > . shows s . showString ")->(" > . shows o . showString "," > . shows q' . showString ")" > data Machine = Machine [State] [Sym] [Rule] We now define a function that generates the instance declaration for a transition. The generated text is of the form: * ==> (q,s)->(o,q'): * * > instance TM [... new config ...] => TM [... old config ...] where * > tmfinal [... old config ...] = tmfinal [... new config ...] Strictly the `tmfinal' part is optional; it merely gives us a way of inspecting the results of the Turing machine run. As can be seen by using a nonterminating Turing machine, the actual TM run occurs during the type checking phase, not at runtime! Configurations are class instances of the following form: * TM q lss s rss Here q is a state (a type Qn with a single element Qn), lss is the portion of the tape to the left of the head (represented as a snoc-list (lss',ls) where ls is the rightmost symbol and lss' is the rest), s is the current symbol, and rss is the portion of the tape to the right of the head (represented as a cons-list (rs,rss') where rs is the leftmost symbol and rss' is the rest). The instance declarations are generated in pairs, the second case automatically extending the potentially-infinite tape as necessary. No context is required for the Halt transitions; these simply display the final state and tape configuration. To display the configuration it is necessary that the tapes be Show-able; since they are pairs they are Show-able if symbols are themselves Show-able. We ensure this elsewhere. > gentransition :: Rule -> String > gentransition r@(Rule q s MoveL q') > = "==> " ++ show r ++ ":\n\n" > ++ "> instance TM " ++ show q' ++ " lss ls (" ++ show s > ++ ",rss) =>" > ++ " TM " ++ show q ++ " (lss,ls) " ++ show s ++ " rss where\n" > ++ "> tmfinal " ++ show q ++ " (lss,ls) " ++ show s ++ " rss =" > ++ " tmfinal " ++ show q' ++ " lss ls (" ++ show s ++ ",rss)\n\n" > ++ "> instance TM " ++ show q' ++ " () S0 (" ++ show s > ++ ",rss) =>" > ++ " TM " ++ show q ++ " () " ++ show s ++ " rss where\n" > ++ "> tmfinal " ++ show q ++ " () " ++ show s ++ " rss =" > ++ " tmfinal " ++ show q' ++ " () S0 (" ++ show s ++ ",rss)\n\n\n" > gentransition r@(Rule q s MoveR q') > = "==> " ++ show r ++ ":\n\n" > ++ "> instance TM " ++ show q' ++ " (lss," ++ show s ++ ") rs " > ++ "rss =>" > ++ " TM " ++ show q ++ " lss " ++ show s ++ " (rs,rss) where\n" > ++ "> tmfinal " ++ show q ++ " lss " ++ show s ++ " (rs,rss) =" > ++ " tmfinal " ++ show q' ++ " (lss," ++ show s ++ ") rs rss\n\n" > ++ "> instance TM " ++ show q' ++ " (lss," ++ show s ++ ") S0 " > ++ "() =>" > ++ " TM " ++ show q ++ " lss " ++ show s ++ " () where\n" > ++ "> tmfinal " ++ show q ++ " lss " ++ show s ++ " () =" > ++ " tmfinal " ++ show q' ++ " (lss," ++ show s ++ ") S0 ()\n\n\n" > gentransition r@(Rule q s (Write s') q') > = "==> " ++ show r ++ ":\n\n" > ++ "> instance TM " ++ show q' ++ " lss " ++ show s' > ++ " rss =>" > ++ " TM " ++ show q ++ " lss " ++ show s ++ " rss where\n" > ++ "> tmfinal " ++ show q ++ " lss " ++ show s ++ " rss =" > ++ " tmfinal " ++ show q' ++ " lss " ++ show s' ++ " rss\n\n\n" > gentransition r@(Rule q s Halt _) > = "==> " ++ show r ++ ":\n\n" > ++ "> instance (Show lss, Show rss) =>" > ++ " TM " ++ show q ++ " lss " ++ show s ++ " rss where\n" > ++ "> tmfinal " ++ show q ++ " lss " ++ show s ++ " rss =" > ++ " \"Halted at state " ++ show q ++ ". \"\n" > ++ "> ++ \"" > ++ "Final configuration is:\\n\"\n" > ++ "> ++ show lss ++ \" <# \"\n" > ++ "> ++ show S0 ++ \" #> \" " > ++ "++ show rss\n\n\n" Now some code to generate a state declaration and a symbol declaration: > genstatedecl q > = "> data " ++ show q ++ " = " ++ show q ++ "\n" > gensymdecl s > = "> data " ++ show s ++ " = " ++ show s ++ " deriving Show\n" Given all this, we now write the entire program: > writetmfile :: String -> Machine -> String -> IO () > > writetmfile file (Machine qs ss rs) init > = do { writeFile file $ > "This literate Haskell script has been automatically generated by\n" > ++ "Keith Wansbrough's undecgen.lhs script. Use Hugs 1.3c to run.\n\n" > ++ "> class TM q lss s rss where\n" > ++ "> tmfinal :: q -> lss -> s -> rss -> String\n\n"; > dumpList genstatedecl qs; > appendFile file "\n"; > dumpList gensymdecl ss; > appendFile file "\n\n"; > dumpList gentransition rs; > appendFile file $ > "\n" > ++ "> main :: IO ()\n\n" > ++ "> main = putStr (tmfinal " ++ init ++ ")\n\n"} > > where > dumpList :: (a->String) -> [a] -> IO () > dumpList f = foldl (\a b -> a >> appendFile file (f b)) (return ()) Now for a sample Turing machine, from p.188 of Harry Lewis and Christos Papadimitriou, _Elements of the Theory of Computation_, Prentice-Hall, 1981. tmDuplicate duplicates the word to the left of the head in the initial position, leaving the head to the right of the second copy. That is, it turns n n n ----- ----- ----- 01...10 into 01...101...10 ^ ^ > tmDuplicate = Machine (map State [0..10]) > (map Sym [0..1]) > [ Rule (State 0) (Sym 0) (MoveL) (State 1) > , Rule (State 0) (Sym 1) (MoveL) (State 1) > , Rule (State 1) (Sym 0) (MoveR) (State 2) > , Rule (State 1) (Sym 1) (MoveL) (State 1) > , Rule (State 2) (Sym 0) (MoveR) (State 10) > , Rule (State 2) (Sym 1) (Write (Sym 0)) (State 3) > , Rule (State 3) (Sym 0) (MoveR) (State 4) > , Rule (State 3) (Sym 1) (MoveR) (State 4) > , Rule (State 4) (Sym 0) (MoveR) (State 5) > , Rule (State 4) (Sym 1) (MoveR) (State 4) > , Rule (State 5) (Sym 0) (Write (Sym 1)) (State 6) > , Rule (State 5) (Sym 1) (MoveR) (State 5) > , Rule (State 6) (Sym 0) (MoveL) (State 7) > , Rule (State 6) (Sym 1) (MoveL) (State 7) > , Rule (State 7) (Sym 0) (MoveL) (State 8) > , Rule (State 7) (Sym 1) (MoveL) (State 7) > , Rule (State 8) (Sym 0) (Write (Sym 1)) (State 9) > , Rule (State 8) (Sym 1) (MoveL) (State 8) > , Rule (State 9) (Sym 0) (MoveR) (State 2) > , Rule (State 9) (Sym 1) (MoveR) (State 2) Two alternatives for the next rule: the first terminates as described; the second causes the machine to continue infinitely to copy the word. Choose one. > , Rule (State 10) (Sym 0) (Halt) (State 10) > -- , Rule (State 10) (Sym 0) (Write (Sym 0)) (State 0) > , Rule (State 10) (Sym 1) (MoveR) (State 10) > ] Clearly, this machine terminates. This can be seen by the fact that the type checker terminates successfully when checking the following sample expression: > sample = "Q0 ((((),S1),S1),S1) S0 ()" This represents 1110 ^ in an initial state Q0. (recall that the tape is potentially infinite in both directions, and full of S0s there). Finally, we write out the desired file: > main :: IO () > main = writetmfile "tmdupl.lhs" tmDuplicate sample EOF