Configurations and Computations

We have seen how the computation performed by a machine M (e.g., a DFA, FST, TM, etc.) can be specified by formally defining a set of configurations C_M, representing shapshots of the system during a computation, and a transition system consisting of the following elements

• an initial configuration function I_M : Σ^* → C_M
• a transition relation R_M ⊆ C_M × C_M
• a set of halting configurations H_M ⊆ C_M
• an output function O_M : H_M → R

Here R is the type of values resulting from a computation, e.g., R = {0, 1} for DFAs, or R = Γ^* for FSTs.

We describe how to implement these configuration systems in Haskell. We start by defining a type to represent Configuration Transition Systems (CTS):

type CTS c r = (String -> c, c -> [c], c -> Bool, c -> r)

We parametrize this type by the underlying type of configurations c, and the result of computations r. Making the definition parametric with reslect to c and r will allow to use the same definition and functions to model the comptuation of different types of automata. For example, for finite state automata (DFA st) we will use c = (st,String) and r = Bool, i.e. configurations are pairs (q,w) where q :: st is a state and w :: String is an input string, while the final result is a boolean denoting the automaton final acceptance decision.

According to the above definition, a configuration transition system cts :: CTS c r (with configurations of type c and final result of type r) consists of four components cts = (initConf, transRel, isHalting, outFun) where

• initConf :: String -> c is the initial configuration function (I_M(w)), which on input a string w :: String, outputs the initial configuration (initConf w) of the automaton on input w.

• transRel :: c -> [c] is a function representing the transition relation R_M, which on input a configuration c₀ outputs a list of all configurations c₁ such that (c0, c1)∈R_M.

• isHalting :: c -> Bool is a predicate to test membership in the set H_M of halting configurataions

• outFun :: c -> r is the output function, mapping any halting configurations to the final result of the computation.

Configurations Transition Systems can be used to define computations in a very general way, applicable to different types of automata. For simplicity/efficiency we focus on deterministic computation, and define a function compute that on input a cts and an input string w, runs the computation and outputs

• just the final result, if the computation proceeds deterministically
• nothing, if some form of non-deterministic is encountered during the computation

compute :: CTS c o -> String -> Maybe o
compute (initConf, transRel, isHalting,  outFun) w =
  run (initConf w) where
    run c = case (transRel c, isHalting c) of
             ([],True) -> Just (outFun c)
             ([c'],False) -> run c'
             otherwise -> Nothing

The code is pretty much self-explanatory: the final result is obtained by running the system starting from the initial configuration initConf w. The run function, on input the current configuration/snapshot c, checks if c is halting, and computes the list of possible “next” possible configurations. If there are no next configurations and c is halting, then we can compute the final output outFun c. If the configuration is not halting, and there is only one possible “next” configuration c', we update the current configuration to c' and keep running. In all other cases, we have detected that the system is not deterministic, and terminate the computation with Nothing.

In order to apply our compute function, we need to define a specific configuration transition system for our automata. Below is the implementation of the transition system for DFAs described in the lecture notes, and a symilar transition system for FSTs.

ctsDFA :: (Eq st) => (DFA st) -> CTS (st,String) Bool
ctsDFA (qs,sigma,delta,s,fs)
	= (initConf, transRel, isHalting, outFun)
  where initConf w = (s,w)
        transRel (q,"") = []
        transRel (q,x:xs) = [(delta q x,xs)]
        isHalting (q,w) = null w
        outFun (q,"") = elem q fs
        
ctsFST :: (Eq st) => (FST st) -> CTS (st,String,String) String
ctsFST (qs,alphaIn,alphaOut,delta,s,out)
	= (initConf, transRel, isHalting, outFun)
  where initConf w = (s,w,"")
        transRel (q,"",u) = []
        transRel (q,x:xs,u) = [(delta q x,xs,u ++ out q)]
		isHalting (q,w,u) = null w
        outFun (q,"",u) = u ++ out q

You can find all functions defined here in the module CTS.hs. If our transition systems are correct, we should expect compute to return the same output values as the evalDFA and evalFST functions defined in DFA.hs and FST.hs.

> f <- readFile "dfa1.jff"
> let (Just m) = JFF.readDFA f
> DFA.evalDFA m "abbbaa"
True
> CTS.compute (CTS.ctsDFA m) "abbbaa"
Just True

As expected, the computation proceeds deterministically, and terminates with the same answer as the one produced by evalDFA.