Sudoku solver using SAT+

(This post is literate Haskell, available here.)

Inspired by an old(-ish) Galois post about using its SAT back end to solve sudokus, here is a similar sudoku solver written in Haskell using Koen Claessen’s SAT+ library.

Representing sudokus

We represent sudokus as a simple column-of-rows:

type Sudoku = [[Maybe Int]]

A valid sudoku will have 9 rows and 9 columns and each cell is either Nothing or a value between 1 and 9.

The rules of sudoku mandates that each of the 27 “blocks” (rows, columns and $3\times 3$ squares) only contain distincts numbers in the interval 1-9. So the first thing we need is a function for extracting the blocks of a sudoku:

blocks :: [[a]] -> [[a]]

The argument is a sudoku ($9\times 9$ elements) and the result is a list of blocks ($27\times 9$ elements). We use a polymorphic function in order to make it work also for the SAT representation of sudokus below.

(We omit the definition of blocks from this post, because it’s part of a lab here at Chalmers.)

Solving constraints using SAT+

SAT+ is a library that adds abstractions and convenience functions on top of the SAT solver MiniSAT. Here we will only make use of quite a small part of the library.

The inequality constraints of sudokus can be expressed using the following functions:

newVal   :: Ord a => Solver -> [a] -> IO (Val a)
val      :: a -> Val a
notEqual :: Equal a => Solver -> a -> a -> IO ()

Function newVal creates a logical value that can take on any of the values in the provided list. A specific known value is created using val, and finally, inequality between two values is expressed using notEqual.

The Solver object required by newVal and other functions is created by newSolver:

newSolver :: IO Solver

After a solver has been created and constraints have been added using the functions above, we can use solve to try to find a solution:

solve :: Solver -> [Lit] -> IO Bool

If solve returns True we can then use modelValue to find out what values were assigned to unknowns:

modelValue :: Solver -> Val a -> IO a

These are all the SAT+ functions we need to solve a sudoku.

The solver

In order to solve a sudoku, we first convert it to a “matrix” of logical values:

type Sudoku' = [[Val Int]]

fromSudoku :: Solver -> Sudoku -> IO Sudoku'
fromSudoku sol = mapM (mapM fromCell)
  where
    fromCell Nothing  = newVal sol [1..9]
    fromCell (Just c) = return (val c)

This simply converts the matrix of Maybe Int to a matrix of Val Int, such that Just c is translated to the logical value val c and Nothing is translated to a logical value in the range 1-9.

Next, we need to add inequality constraints according to the rules of sudoku. After obtaining the blocks using blocks, we just add constraints that all values in a block should be different:

isOkayBlock :: Solver -> [Val Int] -> IO ()
isOkayBlock sol cs = sequence_ [notEqual sol c1 c2  | c1 <- cs, c2 <- cs, c1/=c2]

isOkay :: Solver -> Sudoku' -> IO ()
isOkay sol = mapM_ (isOkayBlock sol) . blocks

After solving a sudoku, we need to be able to convert it back to the original representation. This is done using modelValue to query for the value of each cell:

toSudoku :: Solver -> Sudoku' -> IO Sudoku
toSudoku sol rs = mapM (mapM (fmap Just . modelValue sol)) rs

Now we have all the pieces needed to define the solver:

solveSud :: Sudoku -> IO (Maybe Sudoku)
solveSud sud = do
    sol  <- newSolver
    sud' <- fromSudoku sol sud
    isOkay sol sud'
    ok <- solve sol []
    if ok
      then Just <$> toSudoku sol sud'
      else return Nothing

Strictness can fix non-termination!

(This post is literate Haskell, available here.)

I’ve always thought that strictness annotations can only turn terminating programs into non-terminating ones. Turns out that this isn’t always the case. As always, unsafePerformIO changes things.

import Data.IORef
import System.IO.Unsafe

Consider the following function for turning an IORef into a pure value:

unsafeFreezeRef :: IORef a -> a
unsafeFreezeRef = unsafePerformIO . readIORef

(I explain why I’m interested in this function below.)

This function is of course unsafe, but we may naively expect it to work in the following setting where it’s used inside a function that returns in IO:

modRef :: (a -> a) -> IORef a -> IO ()
modRef f r = writeIORef r $ f $ unsafeFreezeRef r

However, this doesn’t work, because the readIORef inside unsafeFreezeRef happens to be performed after writeIORef, leading to a loop.

So, strangely, the solution is to use a strictness annotation to force the read to happen before the write:

modRef' :: (a -> a) -> IORef a -> IO ()
modRef' f r = writeIORef r $! f $ unsafeFreezeRef r

This is the first time I’ve seen a strictness annotation turn a non-terminating program into a terminating one.

Here is a small test program that terminates for modRef' but not for modRef:

test = do
    r <- newIORef "hello"
    modRef' tail r
    putStrLn =<< readIORef r

I’m not sure this tells us anything useful. We should probably stay away from such ugly programming anyway… But at least I found this example quite interesting and counterintuitive.

Why on earth would anyone write unsafeFreezeRef?

In case you wonder where this strange example comes from, I’m working on a generic library for EDSLs that generate C code. Among other things, this EDSL has references that work like Haskell’s IORefs.

The purpose of unsafeFreezeRef in the library is to avoid temporary variables in the generated code when we know they are not needed. The idea is that the user of unsafeFreezeRef must guarantee that result is not accessed after any subsequent writes to the reference. Reasoning about when a value is used is quite easy in the EDSL due to its strict semantics. For example, we don’t need any strictness annotation in the definition of modRef due to the fact that setRef (the equivalent of writeIORef) is already strict.

The reason I noticed the problem of laziness and unsafeFreezeRef was that the EDSL evaluator turned out to be too lazy when writing to references. So I had a program which produced perfectly fine C code, but which ran into a loop when evaluating it in Haskell. The solution was to make the evaluator more strict; see this commit and this.

Trying out the Bound library

[UPDATE, 2015-02-23: The post has been slightly updated based on comments by Edward Kmett.]

In trying to understand the Bound library, and in particular, its limitations (if any) in terms of expressiveness and efficiency. I will here try to implement a small subset of the Feldspar EDSL using Bound.

DISCLAIMER: Statements in this text may very well reflect my misunderstandings rather than actual truths about Bound.

Note that I’m assuming basic familiarity with Bound. If you’re not familiar with the library, see its documentation.

I would be happy to receive feedback and hints for how to improve the code.

The whole code can be found here: FeldsparBound.lhs

Implementing Feldspar using Bound

Here is the subset of Feldspar that we will work with:

data Data a
    = Var a
    | Int Int
    | Add (Data a) (Data a)
    | Ix (Data a) (Data a)
    | Par (Data a) (Scope () Data a)
  deriving (Eq,Show,Functor,Foldable,Traversable)

Ix represents array indexing, and Par represents array construction, corresponding to the following function on lists:

parList :: Int -> (Int -> a) -> [a]
parList l f = [f i | i <- [0 .. l-1]]

For simplicity, I chose to put the Scope directly on Par instead of going through a lambda as we do in Feldspar.

The Monad instance defines substitution in a standard way:

instance Monad Data
  where
    return = Var
    Var a   >>= k = k a
    Int a   >>= k = Int a
    Add a b >>= k = Add (a >>= k) (b >>= k)
    Ix a i  >>= k = Ix (a >>= k) (i >>= k)
    Par l f >>= k = Par (l >>= k) (f >>>= k)

instance Applicative Data where pure = return; (<*>) = ap

User interface

Here I choose to represent free variables as strings:

type Name = String

type D = Data Name

The user interface is then as follows:

v :: Name -> D
v = Var

instance Num D
  where
    fromInteger = Int . fromInteger
    (+) = Add

(!) :: D -> D -> D
(!) = Ix

par :: Name -> D -> D -> D
par i l f = Par l $ abstract1 i f

Here are two simple example expressions:

ex1 = par "i" 10 $ v "i" + 0
  -- Corresponds to `parList 10 $ \i -> i + 0`

ex2 = par "i" 10 $ v "arr" ! (v "i" + 0)
  -- Corresponds to `parList 10 $ \i -> arr !! (i + 0)`

In the definition of par, we use abstract1 is to bind the free variable (convert to deBruijn). It has to traverse the whole body, so the complexity is quadratic in the number of nested binders.

Transformations

Now to the interesting question of how one goes about to transform terms in the above representation.

Ideally, we want to do this without looking at deBruijn indices at all. Two questions arise:

1. How to apply a transformation under a Scope?
2. How to pattern match on binders and variables and rewrite them?

For the first question, my initial naive attempt was to use a combination of instantiate1 and abstract1 to lift a transformation on D to a transformation on Scope:

transScopeBAD :: (D -> D) -> Scope () Data Name -> Scope () Data Name
transScopeBAD f = abstract1 "x" . f . instantiate1 (Var "x")

The use of instantiate1 changes all occurrences of the bound variable to the free variable Var "x" and abstract1 re-binds that variable after f has been applied to the body. Unfortunately, this doesn’t work. If there are nested scopes, their corresponding variables will all be renamed to "x", so the innermost abstract1 is going to capture all of them. Also, since abstract1 has to traverse the whole body, nested uses of transScope are going to be inefficient.

A better approach is to work more directly with the representation and use fromScope and toScope (here with the type specialized to Data):

transScope :: (Data (Var b a) -> Data (Var b a)) -> Scope b Data a -> Scope b Data a
transScope f = toScope . f . fromScope

(This version of transScope was suggested by Edward. In my initial attempt, I used hoistScope instead.)

Note how the type clearly expresses the fact that the term passed to the transformation function f has one extra variable (of type b) in addition to the free variables (of type a). This information was missing in transScopeBAD.

Using transScope, we can now write the following simplifier:

simplify :: Data a -> Data a
simplify e = simp $ case e of
    Add a b -> Add (simplify a) (simplify b)
    Ix a i  -> Ix (simplify a) (simplify i)
    Par l f -> Par (simplify l) $ transScope simplify f
    _ -> e
  where
    simp (Add (Int 0) b) = b
    simp (Add a (Int 0)) = a
    -- The catch-all case `simp e = e` will come later

Note that it is important for simplify to be polymorphic in the free variables since we’re using it at a different type when passing it to transScope. This requirement was not obvious to me at first. (In retrospect, it is obvious that the polymorpic type is preferred, since I don’t want the simplifier to do anything with the free variables.)

To make the simplifier more interesting, we add a case corresponding to the following rule for parList (defined above):

parList l f !! i   ==>   f i

This turns out to be easy:

    simp (Ix (Par l f) i) = instantiate1 i f

Another similar rule that we may want to express is

parList l (\i -> arr !! i)   ==>   arr   (where i `notElem` freeVars arr)

(In both of these rules, we ignore out-of-bounds indexing for simplicity.)

To express this rule, we need to pattern match on binders and variables. My initial attempt was the following:

--     simp (Par l f)
--       | Ix arr i <- instantiate1 (v "i") f
--       , i == v "i"
--       , "i" `Foldable.notElem` arr
--       = arr

This looks quite nice from a readability perspective, but it doesn’t work because transScope does not permit free variables as strings. (And, in general, using instantiate1 in this way has the same problem as transScopeBAD above, that the variable "i" might easily clash with other instantiated variables.)

Instead, it seems that one has to work more directly with the deBruijn representation:

    simp (Par l f)
      | Ix arr i   <- fromScope f
      , Var (B ()) <- i
      , Just arr'  <- lower arr
      = arr'

    -- Catch-all case to complete the definition of `simp`:
    simp e = e

The lower function tries to lower the scope of an expression, and succeeds if the expression does not refer to the closest bound variable:

lower :: Data (Var b a) -> Maybe (Data a)
lower = traverse $ unvar (const Nothing) Just

Note the use of fromScope rather than unscope above. This is to change the generalized deBruijn representation into one the standard representation which lower expects.

I would have hoped to avoid matching explicitly on the deBruijn representation of i (namely Var (B ())). But I guess this is just unavoidable?

The check that i does not occur in arr is replaced by the pattern match on the result of lower. One nice thing here is that the type system does not allow us to return arr directly, so we cannot accidentally forget to check whether i occurs in arr (which I tend to forget everytime!).

Examples

*Main> ex1
Par (Int 10) (Scope (Add (Var (B ())) (Int 0)))

*Main> simplify ex1
Par (Int 10) (Scope (Var (B ())))

*Main> ex2
Par (Int 10) (Scope (Ix (Var (F (Var "arr"))) (Add (Var (B ())) (Int 0))))

*Main> simplify ex2
Var "arr"

Discussion

At first I was tempted to use instantiate1 and abstract1 everywhere and to represent free variables as strings. Although this leads to code that looks readable, it does not work in general:

• Representing free variables as strings can easily lead to capturing bugs
• It leads to inefficient code:
  • abstract1 has to traverse the whole expression, so it should be used sparingly
  • instantiate1 may not have to traverse the whole expression due to the generalized deBruijn representation, but I’m not sure what this means in practice

From a capturing point of view, it may be considered OK to use abstract1 and variables as strings the way I did in the user interface above. The user will just have to make sure to use distinct variable names. However, due to the nested uses of abstract1, it is still very inefficient to construct terms in this way. A better way is probably to construct terms in a different representation and then convert them all to deBruijn in a single pass.

Once I realized that I couldn’t use instantiate1 and abstract1 for transformations under a Scope, I was forced to use fromScope/toScope which expose a bit the representation of variables. However, this turned out to be a very good thing that just made the code safer.

The resulting code does not use abstract1, so it avoids that source of inefficiency. There is one use of instantiate1, but that is a substitution coming from the rewrite rule – it has nothing to do with the Bound library (and it could be avoided by rewriting to a let binding instead of performing the substitution).

In the end, there appears to be only one problematic inefficiency left: the lower function. In order to know whether an expression refers to the closest bound variable, lower naturally has to traverse the whole expression. Of course, this is true regardless of how variables are represented. But in a standard named representation of variables, it is e.g. possible to return a set of free variables from simplify, so that membership can be tested without traversing the expression. I don’t see how that could be done here.

In conclusion, I see many advantages of using Bound, especially when it comes to safety and not worrying about capturing. However, there are some things that make me hesitate on adopting it for something like Feldspar:

• I wasn’t able to completely hide the deBruijn indices in the simplifier. Can it be done? Is this going to be a big problem for people trying to express rewrite rules?
• The lower function is a potential source of inefficiency in a simplifier. Can it be fixed? Will there be other inefficiencies as the rules get more complex?

If someone has the answers to those questions, I would be happy to know!

Relating Syntactic and CompData

Update: toAST/fromAST have been rewritten using catamorphisms.

Syntactic and CompData are two packages for modeling compositional data types. Both packages use the technique from Data Types à la Carte to model polymorphic variants, but they model recursion quite differently: Syntactic uses an application tree, while CompData uses a type-level fixed-point.

This post demonstrates the relation between the two approaches by showing how to translate one to the other. As a side effect, I also show how to obtain pattern functors for free, avoiding the need to derive instances for various type classes in CompData.

To remain focused on the matter at hand, I will only introduce Syntactic briefly. For more information, see this paper. I will also assume some familiarity with CompData.

Preliminaries

We start by importing the necessary stuff from Syntactic:

import Language.Syntactic
    ( AST (..)
    , Full
    , (:->)
    , DenResult
    , Args (..)
    , mapArgs
    , appArgs
    , fold
    )

Data types in Syntactic correspond to Generalised Compositional Data Types in CompData. These are found under Data.Comp.Multi in the module hierarchy:

import Data.Comp.Multi
    ( Cxt (Term)
    , Term
    , HFunctor (..)
    , cata
    )

import Data.Comp.Multi.HFoldable (HFoldable (..))

Cxt is the type-level fixed-point operator, which I will use by its alias Term. The type classes HFunctor and HFoldable are used for traversing terms.

Our example will also make use of the Monoid class.

import Data.Monoid

Syntactic

The idea behind Syntactic is to model a GADT such as the following

data Expr a
  where
    Int :: Int -> Expr Int
    Add :: Expr Int -> Expr Int -> Expr Int

as a simpler non-recursive data type:

data ExprSym a
  where
    IntSym :: Int -> ExprSym (Full Int)
    AddSym :: ExprSym (Int :-> Int :-> Full Int)

If we think of Expr as an AST, then ExprSym defines the symbols in this tree, but not the tree itself. The type parameter of each symbol is called the symbol signature. The signature for Add – (Int :-> Int :-> Full Int) – should be read as saying that Add expects two integer sub-expressions and produces an integer result. In general, an ordinary constructor of the type

C :: T a -> T b -> ... -> T x

is modeled as a symbol of the type

CSym :: TSym (a :-> b :-> ... :-> Full x)

The AST type can be used to make an actual AST from the symbols:

type Expr' a = AST ExprSym (Full a)

This type is isomorphic to Expr. So, in what way is Expr' better than Expr? The answer is that Expr' can be traversed generically by matching only on the constructors of AST. For example, to compute the size of an AST, we only need two cases:

size :: AST sym sig -> Int
size (Sym _)  = 1
size (s :$ a) = size s + size a

The first case says that a symbol has size 1, and the second says how to join the sizes of a symbol and a sub-expression. (Note that s can contain nested uses of (:$).) Another advantage of using AST is that it supports composable data types.

Listing arguments

The size function is a bit special in that it operates on every symbol application in a compositional way. For more complex generic traversals, it is often needed to operate on a symbol and all its arguments at once. For example, Syntactic provides the following function for folding an AST:

fold :: (forall sig . sym sig -> Args c sig -> c (Full (DenResult sig)))
     -> AST sym (Full a)
     -> c (Full a)

The caller provides a function that, given a symbol and a list of results for its sub-expressions, produces a result for the combined expression. fold uses this function to compute a result for the whole AST. The type of fold requires some explanation. The c type (the folded result) is indexed by the type of the corresponding sub-expression; i.e. folding a sub-expression of type AST sym (Full a) results in a value type c (Full a). The type function DenResult gives the result type of a symbol signature; e.g. DenResult (Int :-> Full Bool) = Bool.

For our current purposes, the most important part of the type is the argument list. Args c sig is a list of results, each one corresponding to an argument in the signature sig (again, more information is found in the Syntactic paper). Args is defined so as to ensure that the length of the list is the same as the number of arguments in the signature. For example, Args c (Int :-> Int :-> Full Int) is a list of two elements, each one of type c (Full Int).

Pattern functors for free

Now to the gist of this post. Using Args, we can easily define a pattern functor (actually a higher-order functor) corresponding to a symbol:

data PF sym f a
  where
    PF :: sym sig -> Args f sig -> PF sym f (Full (DenResult sig))

A pattern functor here is simply a symbol paired with an argument list. Each argument is of type f (Full b), where b is the type of the corresponding sub-expression. The HFunctor instance is straightforward (mapArgs is provided by Syntactic):

instance HFunctor (PF sym)
  where
    hfmap f (PF s as) = PF s (mapArgs f as)

Now we can actually use the symbols defined earlier to make an expression type using CompData’s fixed-point operator:

type Expr'' = Term (PF ExprSym)

The correspondence between expressions based on AST and expressions based on Term can be seen by the following functions mapping back and forth between them (appArgs is provided by Syntactic):¹

toAST :: Term (PF sym) (Full a) -> AST sym (Full a)
toAST = cata (\(PF s as) -> appArgs (Sym s) as)

fromAST :: AST sym (Full a) -> Term (PF sym) (Full a)
fromAST = fold (\s as -> Term (PF s as))

The translations are simply defined using catamorphisms; cata for CompData terms and fold for Syntactic terms.

To make the experiment a bit more complete, we also give an instance of HFoldable. For this, we need a helper function which is currently not included in Syntactic:

foldrArgs
    :: (forall a . c (Full a) -> b -> b)
    -> b
    -> (forall sig . Args c sig -> b)
foldrArgs f b Nil       = b
foldrArgs f b (a :* as) = f a (foldrArgs f b as)

After this, the instance follows naturally:

instance HFoldable (PF sym)
  where
    hfoldr f b (PF s as) = foldrArgs f b as

Testing

To try out the code, we define a small expression using the Expr' representation:

expr1 :: Expr' Int
expr1 = int 2 <+> int 3 <+> int 4

int :: Int -> Expr' Int
int i = Sym (IntSym i)

(<+>) :: Expr' Int -> Expr' Int -> Expr' Int
a <+> b = Sym AddSym :$ a :$ b

Next, we define the size function for expressions based on CompData’s Term (Sum is provided by Data.Monoid):

size' :: HFoldable f => Term f a -> Sum Int
size' (Term f) = Sum 1 `mappend` hfoldMap size' f

And, finally, the test:

*Main> size expr1
5

*Main> size' $ fromAST expr1
Sum {getSum = 5}

Summary

Hopefully, this post has provided some insights into the relation between Syntactic and CompData. The key observation is that symbol types defined for Syntactic give rise to free pattern functors that can be used to define terms in CompData. As we can translate freely between the two representations, there doesn’t appear to be any fundamental differences between them. A practical difference is that CompData uses type classes like HFunctor and HFoldable for generic traversals, while syntactic provides more direct access to the tree structure. As an interesting aside, the free pattern functors defined in this post avoids the need to use TemplateHaskell to derive instances for higher-order functor type classes in CompData.

The code in this post is available has been tested with GHC 7.6.1, syntactic-1.5.1 and compdata-0.6.1.

Download the source code (literate Haskell).

---

1. As noted by Patrick Bahr, the toAST/fromAST translations destroy compositionality since a compound domain (S1 :+: S2) in Syntactic is mapped to a monolithic functor PF (S1 :+: S2) in CompData. However, with suitable type-level programming it should be possible to make the mapping to the compound type (PF S1 :+: PF S2) instead.↩

DSLs Are Generic Solutions

Last week, I wrote a grant proposal to develop generic methods for implementation of embedded domain-specific languages (DSLs). I tried to argue that DSLs are becoming increasingly important as software development is getting more and more complicated. The goal of the project is to make it dead easy to implement high-quality DSLs embedded in Haskell. As I was trying to promote this idea, I realized that it might not at all be obvious to the reviewer that an ever-increasing number of DSLs is a good thing. Is there not a risk of just causing a confusing jungle of different language flavors?

This is a valid concern; if the primary purpose of introducing a DSL is provide domain-specific syntax, then having multitude of different DSLs is indeed going to be confusing. However, the most important part of DSLs is not their syntax (even if syntax is important). My view of a DSL is this:¹

A DSL is a way for an experienced programmer to make a generic solution available to other (perhaps less experienced) programmers in such a way that only problem-specific information needs to be supplied.

The Unix DSL jungle

Consider the following example: A Unix shell has access to lots of small programs aimed to solve specific classes of problems. For example, the program ls is a solution to the problem of listing the contents of a directory. Moreover, it is a generic solution, since it can list the contents in many different ways. Specific solutions are obtained by providing options at the command line. The command ls -a will include hidden files in the listing, and ls -a -R will additionally list the contents of sub-directories recursively. The different options to ls can be seen as a DSL to specialize ls to specific use-cases. ls is a very successful DSL – compare to programming the same functionality using lower-level constructs, e.g. looping over the directory contents testing whether or not a file is hidden, etc.² Still, the important aspect of ls is not its syntax (though, again, that is also important), but rather the program ls itself (the DSL implementation), which is a generic solution that can be reused in many different situations.

If we consider all commands in a Unix shell environment, it may appear as a jungle of different DSLs. However, this is not at all a problem. Every command is a rather limited sub-DSL which can usually be summarized in a relatively short manual page. Moreover, the interaction between the sub-DSLs is done using a common data format, text strings, which makes it possible to write shell programs that seamlessly combine different sub-DSLs.

What would be confusing is if there were several different versions of ls, all with slightly different syntax. Luckily that is not the case.

The Hackage library jungle

We can also draw a parallel to programming libraries. A library can be seen as a DSL. (Especially when considering embedded DSLs, the border to libraries is not very clear.) The Haskell package database Hackage has since the launch in 2007(?) received nearly 4000 packages (2012-04-16). There are quite some occurrences of confusingly similar libraries, which may give a feeling of Hackage as a jungle, but in all Hackage has been a huge success. The risk of confusion does not mean that we should stop developing libraries, merely that some extra care is needed to specify the purpose of and relation between different libraries.

Reusability is key

I have claimed that a DSL is a way for an experienced programmer to make a generic solution available to other (perhaps less experienced) programmers in such a way that only problem-specific information needs to be supplied. Clearly, syntax is an important component to this definition (“only problem-specific information”), but I think the main focus should be on “making a generic solution available”. It is all about reusing programming effort! We might just as well say that a DSL is a way to have a one-time implementation effort potentially benefit a large number of DSL users for a long time.

As long as there are generalizable solutions out there, there will be a need for new DSLs!

---

1. The general definition is, of course, broader.↩

2. OK, I know at least one language where looping and testing can be expressed very succinctly, but you get the point.↩

Difference between LTL and CTL

(Note that this article assume some intuitive understanding of CTL.)

I’m currently teaching a course on Hardware Description and Verification, in which we cover computation tree logic (CTL) model checking. In preparing for the course, I wanted to fully understand the differences between CTL and LTL. The common informal explanation that LTL has linear time while CTL has branching time is useless without further explanation. I had a certain understanding of CTL, and my initial assumption was that LTL is what you get by excluding all $E$ formulas from CTL. This assumption turned out to be wrong.

My assumption would imply that LTL is a subset of CTL, but the Wikipedia page claims that neither logic is a subset of the other. It seems like I’m not alone in being confused about the difference between the two logics: This Stack Exchange page has the same question. The answer on that page talks about the LTL formula

$$\mathit{\text{FG}}p$$

which, apparently, is not the same as the CTL formula

$$\mathit{\text{AF}}\mathit{\text{AG}}p$$

(as I previously thought). After reading the Stack Exchange answer I started to get a sense of the difference, but I still wasn’t able to formulate it easily. So I had no more excuses not to look into the actual formal semantics of LTL and CTL. This survey by Emerson served as a good reference for that.

Common superset: CTL*

The difference between LTL and CTL is easiest to understand by considering CTL* which has both LTL and CTL as subsets. CTL* has two syntactic categories giving rise to two different kinds of formulas: state formulas and path formulas. A state formula is something that holds for a given state in a system (modeled as a Kripke structure), while a path formula holds for a given path. A path is an infintie sequence of states such that each consecutive pair of states is in the transition relation; i.e. a trace of an infinite run of the system. Note that, even though a state formula is a property of a single state, it can still talk about future states by using the path quantifiers $A$ and $E$.

Now, the important thing to note is that an LTL formula is a (restricted) CTL* path formula while a CTL formula is a (restricted) CTL* state formula. Path formulas are not very interesting on their own, since one is usually interested in expressing properties of all or some paths from the initial state. Hence, the real meaning of an LTL formula is obtained by adding an implicit $A$ quantifier to it turning it into a state formula. Thus the meaning of the LTL formula $f$ is the meaning of the CTL* formula $Af$.

The example

With this understanding, we can try to reformulate the above examples in English:

The LTL formula $\mathit{\text{FG}}p$ can be read as

“Every path (implicit $A$) will eventually ($F$) reach a point after which $p$ is always true ($Gp$).”

Or perhaps more clearly:

“Every path has a finite prefix after which $p$ is always true.”

The CTL formula $\mathit{\text{AF}}\mathit{\text{AG}}p$ can be read as

“Every path ($A$) will eventually ($F$) reach a state from which every path ($A$) has the property that $p$ is always true ($Gp$).”

These formulas are subtly different, and they can be distinguished by the following system of three states:

$S_1\mapsto S_1\mathrm{\text{or}}{S}_2(\mathrm{\text{atomic:}}p)$

$S_2\mapsto S_3(\mathrm{\text{atomic:}}\neg p)$

$S_3\mapsto S_3(\mathrm{\text{atomic:}}p)$

Every run of this system will either (1) stay in $S_1$ forever, or (2) wait some finite time and then make a transition to $S_2$ and $S_3$. In both cases, it holds that the trace has a finite prefix after which $p$ is always true. Hence the LTL formula holds.

However, the CTL formula does not hold, because there is a path that never reaches a state at which $\mathit{\text{AG}}p$ holds. This is the path in which the system stays in $S_1$ forever. Even if it stays in $S_1$ forever, it always has the possibility to escape to $S_2$.

Summary

As demonstrated by the above example, the difference between LTL and CTL (except for the absense of $E$ in LTL) is that an LTL formula can be verified by considering each path in isolation. If each individual path obeys the path formula, the LTL formula is true. To verify a CTL formula, one may also have to consider the alternative possibilities for each state in a path.

FunDeps weaker than type families

I’ve just run into a situation where functional dependencies seem to propagate less type information than the corresponding type family. This seems to be related to the GHC feature request #4894. I just want to document here it for future reference.

The Data.Tuple.Select module in the tuple package has general methods for selecting elements from tuples. The Sel1class relates any tuple (up to a certain limit) to its first element (omitting the select method):

class Sel1 a b | a -> b

The instance for pairs looks as follows:

instance Sel1 (a,b) a

According to my understanding, the functional dependency of Sel1 should be equivalent to the following type function:

type family S1 a
type instance S1 (a,b) = a

If this is the case, the two constructors A and B in this data type should be equivalent

data AB a
  where
    A :: (Sel1 a b) => AB (a -> b)
    B :: (S1 a ~ b) => AB (a -> b)

Yet, the following example demonstrates that this is not the case:

data PairWitness a
  where
    PairWitness :: PairWitness (a,b)

test :: PairWitness a -> AB (a -> b) -> (a -> b)
test PairWitness A (a,b) = a
test PairWitness B (a,b) = a

This gives rise to a type error at the line matching on A. However, the B line works fine.

This has been tested with GHC 6.12.3 and GHC 7.0.2.

Download the source of this post (literate Haskell).