CMPUT 325 Schedule and Outcomes
15. Week 13 - April 7




15.1 Topics



15.2 Racket Question

There will be one Racket question, and it will be based on the following code that you will be requested to modify. Think about how you would take functions of n variables rather than 2, and how you would compute the first k satisfying assignments and do no more. Think about fold.

code/Week13/satisfy.rkt

    #lang racket
     
    ; generate all 2^n possible truth assignments of n boolean variables.
    (define (gen-assign n)
       (define (gen-assign-r m assigns)
            (if (<= m 1) 
                assigns
                (append
                  (map (lambda (a) (cons #f a) ) (gen-assign-r (- m 1) assigns))
                  (map (lambda (a) (cons #t a) ) (gen-assign-r (- m 1) assigns))
                  )
            )
        )
       (gen-assign-r n '( (#f) (#t) ))
    )
     
     
     
    ; find first satisfying assignment for a function of 2 variables
    ; result is 
    ; '(#t "solved" assignment)
    ; '(#f "no solution")
     
    (define (satisfy fn)
        ; RESUME                 
        (call/cc
         ; when everything is finished we invoke RESUME to give the call/cc a value
         (lambda (RESUME)  
           
           (let ( 
                 [exception 
                  
                  ; the context around this is the catch, it expects an exception result
                  (call/cc 
                   (lambda (THROW)  
                     ; TRY
                     ; here is the body of the try, which computes result
                     (map (lambda (assig) 
                            (if (apply fn assig)
                                (RESUME (list #t "solved" assig))
                                '()
                            )) 
                          (gen-assign 2))
                     
                     (THROW '(#f "no solution"))
                     )
                   )  ; THROW gives this a value, assigned to exception
                   ] )
             
             ; CATCH - if we get here, it is because of THROW
            
             exception
             
             ))
           ) ; RESUME gives this a value, which is returned as the result of satisfy
         
         )
     
    (define (f1 v0 v1) (and (not v0) v1))
    (satisfy f1)
     
    (define (f2 v0 v1) (eq? v0 v1))
    (satisfy f2)
     
    (define (f3 v0 v1) #f)
    (satisfy f3)
     


Note: The point of the question which is to think about the interaction between doing a foldl (which is a natural form of an accumulator function) and call/cc.

Think about another variant: suppose you are folding over a generator that on each invocation generates the next assignment to try with the function (this way you don't do any unnecesary work). The main fold can use the call/cc idea to break out of the folding when the k solutions are found. And, suppose that you had a list of generators to use, where each generator only produced some of the assignments. Then the generator itself could use the call/cc try-catch-resume idea to signal when it was finished and needs to be replaced by the next generator.

15.3 Haskell Questions Part 1

Here are a number of Haskell small questions:

  1. Suppose a = [1, 2, 3] and we have functions f x = [ 0, x] and g x = [ 1, x]

    Then we have this interesting observation:
    *Main> concat $ map g (concat $ map f a)
    [1,0,1,1,1,0,1,2,1,0,1,3]
    *Main> concat $ concat (map (map g) (map f a))
    [1,0,1,1,1,0,1,2,1,0,1,3]
    Note how concat and map can move across each other. Find and prove a general rule for this phenomena.

  2. In Racket lists can contain anything, unlike lists in Haskell which must have all elements of the list being the same type. If you really do want to pass around lists of many different kinds of things, you need to wrap them in a common type. So for example, you might create a new type:
    data PolyType = PT_Int Int | PT_String String


    Note how map on PolyType -> a works fine on [ PolyType ].

    Write a function of type [ PolyType ] -> [ PolyType ] that generates a string from its input.

    Given a function f, can you write a function that lifts it into PolyType?

    Write a compare function between any PolyType and use it in a sort.


15.4 Haskell Questions Part 2

A question involving use of the State monad. Suppose that you have the expression tree as discussed in the course notes.

code/Week13/exptree.hs

    {-
        Now lets build expression trees with variable assignment
     
        a is the type of the values in the tree, 
        f is the type of the operations performed on the values
     
        Variable names are strings.
    -}
     
    data ExpTree a f = V a | Op f (ExpTree a f) (ExpTree a f) |
        Get String | Set String (ExpTree a f)
        deriving (Eq, Show)
     
    -- (10 + 20)
    t1 = (Op (+) (V 10) (V 20))
     
    -- (4 * -1)
    t2 = (Op (*) (V 4) (V (- 1)))
     
    -- ( (10+20) + (4 * -1) )
    t3 = (Op (+) t1 t2)
     
    -- assign and fetch from variables
    -- ( (x = (2 + 3)) + (3 * y))
    t4 = (Op (+) (Set "x" (Op (+) (V 2) (V 3))) (Op (*) (V 3) (Get "y")))
     
    -- and here is an evaluator on expression trees
    evalExp (V n) = n
    evalExp (Op f e1 e2) = (f (evalExp e1) (evalExp e2))
     
    -- very bad implementations of Get and Set
    evalExp (Get "y") = 3
    evalExp (Set "x" e1) = evalExp e1
     
    test = [
        evalExp t1,
        evalExp t2,
        evalExp t3
        ]
Using the State monad, implement the ability to assign to and reference variables by name in expressions. Setting a variable x gives x a value for all futher computations up and to the right in the expression tree. The value of x can be changed, so the new value is used until changed again.

The Get and Set constructors have already been defined for the expression tree, and there are some illustrative expressions.

Hint: look at code/Week12/tree.hs

15.5 Haskell Questions Part 3

The nights, knaves, and normals constraint solver we talked about in class; along with one version of a pretty printer is given below.

Code up the following properties:
If two normals say the same thing, then it is true.
If only one normal says something, then it is false.
If two people say statements that are logically equal (i.e. iff) then those statements are the same.
Now, with these assumptions above, if you encounter two people, can you determine what they types are, and the truth of any statement?

code/Week13/solver-v2.hs

    {- Constraint satisfaction solving
     
    Modifed from
     
    from http://www.haskell.org/haskellwiki/All_About_Monads#StateT_with_List 
     
    -}
     
    import Data.Maybe
    import Control.Monad
    import Control.Monad.State
    import Text.Printf
     
     
    {-  pretty printer for models, display using putStrLn 
        Assumes that the list of variables in the assignments are ordered the
        same way for all assignments.
    -}
     
    showModels :: [Variables] -> String
    showModels models = 
        if (length models) == 0 
        then
            "No solution exists!"
        else
            (concatMap fmtStr (namesOf (models !! 0)))
            ++ "\n" ++
            concatMap (++ "\n") (
                map (concatMap fmtStr) (map valuesOf models)
                )
      where
        namesOf pairs = map fst pairs
        valuesOf pairs = map snd pairs
        fmtStr :: String -> String
        fmtStr s = printf "%8s" s
     
    {-
        A language to express logic problems
     
        Name are variables, named with strings
        Value are values of variables, values are strings
        VarType are the type of a variable, mapped to set of values
        Predicates are functions with values are true or false
    -}
     
    type Name   = String
    type Value = String
    type VarType = String
    data Predicate = 
                 Is    Name Value            -- var has specific value
               | Equal Name Name              -- vars have same (unspecified) value
               | And   Predicate Predicate  -- both are true
               | Or    Predicate Predicate  -- at least one is true
               | Not   Predicate            -- it is not true
      deriving (Eq, Show)
     
    type Variables = [(Name,Value)]
     
    -- derived predicates
     
    -- test for a variable NOT equaling a value
    isNot :: Name -> Value -> Predicate
    isNot var value = Not (Is var value)
     
    -- if a is true, then b must also be true
    implies :: Predicate -> Predicate -> Predicate
    implies a b = Not (a `And` (Not b))
     
    -- iff
    iff :: Predicate -> Predicate -> Predicate
    iff a b = (a `implies` b) `And` (b `implies` a)
     
    -- exclusive or
    orElse :: Predicate -> Predicate -> Predicate
    orElse a b = (a `And` (Not b)) `Or` ((Not a) `And` b)
     
    {-
        Check a predicate with the given variable bindings.
        An unbound variable causes a Nothing return value.
        otherwise you get Just True or Just False.
     
        lookup takes a list of name-value tuples, and returns the
        corresponding value Just v, or Nothing if name is not present.
     
        lookup :: Eq a => a -> [(a, b)] -> Maybe b
    -}
     
    check :: Predicate -> Variables -> Maybe Bool
    check (Is var value) vars = do val <- lookup var vars
                                   return (val == value)
    check (Equal v1 v2)  vars = do val1 <- lookup v1 vars
                                   val2 <- lookup v2 vars
                                   return (val1 == val2)
     
    {- 
        lifting takes a function (a1 -> r) and turns it into a function
        on monads (m a1 -> m r)
     
        liftM :: Monad m => (a1 -> r) -> m a1 -> m r
        liftM2 :: Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m rSource
     
    Promote a function to a monad, scanning the monadic arguments from left 
    to right. For example, 
     
        liftM2 (+) [0,1] [0,2] = [0,2,1,3]
        liftM2 (+) (Just 1) Nothing = Nothing
    -}
     
    check (And p1 p2)    vars = liftM2 (&&) (check p1 vars) (check p2 vars)
    check (Or  p1 p2)    vars = liftM2 (||) (check p1 vars) (check p2 vars)
    check (Not p)        vars = liftM (not) (check p vars)
     
    {-
        Machinery for representing and solving constraint satisfaction problems. 
        This is where we will define our combined monad.
     
        ProblemState is the type of our logic problem.  Note the use of named 
        fields where:
            vars is the environment, binding variables to values.   
            constraints are a collection of predicates that must be satisfied
                in order for an environment to be a solution. 
    -}
     
    data ProblemState = PS {vars::Variables, constraints::[Predicate]}
     
    -- this is our monad type for non-determinstic computations with state
    -- StateT is a ???
    type NDS a = StateT ProblemState [] a
     
    -- lookup a variable in the environment.
    getVar :: Name -> NDS (Maybe Value)
    getVar v = do vs <- gets vars
                  return $ lookup v vs
     
    -- set a variable in the environment.
    setVar :: Name -> Value -> NDS ()
    setVar v x = do st <- get
                    vs' <- return $ filter ((v/=).fst) (vars st)
                    put $ st {vars=(v,x):vs'}
     
    {- 
    Check if the variable assignments satisfy all of the predicates.
    The partial argument determines the value used when a predicate returns
    Nothing because some variable it uses is not set.  Setting this to True
    allows us to accept partial solutions, then we can use a value of
    False at the end to signify that all solutions should be complete.
     
    Note:  maybe :: b -> (a -> b) -> Maybe a -> b
           (maybe x id) (Just y) = y
           (maybe x id) Nothing = x
    is the way you yield a default value
     
    Note:  (maybe x id) (Just y) = y
           (maybe x id) Nothing = x
    is the way you yield a default value
    -}
     
    isConsistent :: Bool -> NDS Bool
    isConsistent partial = do cs <- gets constraints
                              vs <- gets vars
                              let results = map (\p->check p vs) cs
                              return $ and (map (maybe partial id) results)
     
    -- Return only the variable bindings that are complete consistent solutions.
    getFinalVars :: NDS Variables
    getFinalVars = do c <- isConsistent False
                      guard c
                      gets vars
     
    {-
     
    Get the first solution to the problem, by evaluating the solver computation
    with an initial problem state and then returning the first solution in the
    result list, or Nothing if there was no solution.
     
    -}
     
    getSolution :: NDS a -> ProblemState -> Maybe a
    getSolution c i = listToMaybe (evalStateT c i)
     
    -- Get a list of all possible solutions to the problem by evaluating the solver
    -- computation with an initial problem state.
     
    getAllSolutions :: NDS a -> ProblemState -> [a]
    getAllSolutions c i = evalStateT c i
     
     
    -- Test consistency over all allowed settings of the variable.
     
    tryAllValues :: (Name,VarType) -> NDS ()
    tryAllValues (var,vtype) = do 
        -- try all the possible values of the type of var using
        -- lookupType :: VarType -> [ Value ]
        -- note the use of monad sum to put plus between each possibility
        msum $ map (setVar var) (lookupType vtype) 
        c <- isConsistent True
        guard c
     
    {-
    All that remains to be done is to define the puzzle in the predicate language
    and get a solution that satisfies all of the predicates:
    -}
     
    -- Define the problem, try all of the variable assignments and print a solution.
     
    {-
        solve takes a set of constraints and returns a list of all the variable
        assignments that satisfy the constraints.
     
    Each call to tryAllValues will fork the solution space, assigning the named
    variable to be "knight" in one fork and "knave" in the other. The forks which
    produce inconsistent variable assignments are eliminated (using the guard
    function). The call to getFinalVars applies guard again to eliminate
    inconsistent variable assignments and returns the remaining assignments as the
    value of the computation.  
     
    if only asking for a few solutions, lazyness should stop further search
     
    -}
     
    solve :: [(Name,VarType)] -> [Predicate] -> [Variables]
    solve varOrder constraints = do 
                let variables   = []
                    problem     = PS variables constraints
     
                (getAllSolutions
                        (do 
                           sequence $ map tryAllValues varOrder
                           getFinalVars)
                         problem)   
     
    pSolve :: [Predicate] -> IO ()
    pSolve constraints = putStrLn (showModels $ solve varOrder constraints)
     
    {- 
     
    We introduce types for the variables using a function lookupType that
    for each type gives the possible values it can have.
     
    The we identify the variables in the problem and their types, along with
    the order in which they should be searched, with the earliest variables
    being the most frequently changed (in model checking the order in which
    variables are examined can dramatically affect solution time).  
     
    -}
     
    lookupType :: VarType -> [ Value ]
    varOrder :: [ (Name, VarType) ]
     
    {- Here is where the problem-specific definitions occur.  -}
     
    -- a generic person
    lookupType "Per" = ["knight", "knave", "normal" ]
    -- just knights and knaves
    lookupType "KK" = ["knight", "knave" ]
    -- paths are good or bad
    lookupType "Path" = ["good", "bad" ]
     
    varOrder = [ 
        ("B", "KK"),
        ("A", "KK"),
        ("R", "Path"),
        ("L", "Path")
        ]
     
    said :: Name -> Predicate -> Predicate
    said v p = ((v `Is` "knight") `implies` p) `And`
               ((v `Is` "knave") `implies` (Not p)) `And`
               ((v `Is` "normal") `implies` (p `Or` (Not p))) 
     
    -- lying is saying something is true when it isn't, or not saying anything
    lied :: Name -> Predicate -> Predicate
    lied v p = (v `said` p) `And` (Not p) 
     
    -- telling truth is saying something is true when it is, or not saying anything.
    toldTruth :: Name -> Predicate -> Predicate
    toldTruth v p = (v `said` p) `implies` p 

15. Week 13 - April 7
CMPUT 325 Schedule / Version 2.31 2014-04-04