Ideas tutorial (version 1.8)

Solutions to suggested exercises

This document shows a possible solution to the suggested exercises in the tutorial.

module Main where

import Ideas.Common.Library
import Ideas.Main.Default

We extend the expression datatype with constructors for multiplication and division. The term instance needs to be extended with new symbols for multiplication and division.

data Expr  =  Con Int
           |  Negate Expr 
           |  Add Expr Expr 
           |  Mul Expr Expr 
           |  Div Expr Expr
   deriving (Eq, Show, Read)

negateSymbol, addSymbol, mulSymbol, divSymbol :: Symbol
negateSymbol = newSymbol "negate"
addSymbol    = newSymbol "add"
mulSymbol    = newSymbol "mul"
divSymbol    = newSymbol "div"

instance IsTerm Expr where
   toTerm (Con x)    = TNum (toInteger x)
   toTerm (Negate x) = unary negateSymbol (toTerm x)
   toTerm (Add x y)  = binary addSymbol (toTerm x) (toTerm y)
   toTerm (Mul x y)  = binary mulSymbol (toTerm x) (toTerm y)
   toTerm (Div x y)  = binary divSymbol (toTerm x) (toTerm y)
   
   fromTerm (TNum x) = return (Con (fromInteger x))
   fromTerm term     = fromTermWith f term
    where
      f s [x]    | s == negateSymbol = return (Negate x)
      f s [x, y] | s == addSymbol    = return (Add x y)
      f s [x, y] | s == mulSymbol    = return (Mul x y)
      f s [x, y] | s == divSymbol    = return (Div x y)
      f _ _ = fail "invalid expression"

We add some examples in which we use multiplication and division.

-- expression 
expr1, expr2, expr3, expr4, expr5, expr6, expr7 :: Expr
expr1 = Add (Con 5) (Negate (Con 2))                                      -- 5+(-2)
expr2 = Add (Negate (Con 2)) (Add (Con 3) (Con 5))                        -- (-2)+(3+5)
expr3 = Mul (Con 3) (Add (Mul (Con 2) (Con 5)) (Negate (Con 3)))          -- 3 * (2*5 - 3)
expr4 = Mul (Div (Con 3) (Con 6)) (Add (Con 1) (Con 1))                   -- 3/6 * 1+1
expr5 = Add (Con 7) (Negate (Mul (Con 5) (Negate (Div (Con 1) (Con 2))))) -- 7 + -(5*-(1/2))
expr6 = Div (Div (Con 4) (Con 5)) (Div (Con 9) (Con 8))                   -- (4/5)/(9/8)
expr7 = Mul (Div (Div (Con 3) (Con 4)) (Con 7)) (Div (Con 1) (Div (Con 2) (Con 3))) 
                                                                          -- ((3/4)/7)*(1/(2/3)

We copy the negateRule and addRule from the tutorial,

negateRule :: Rule Expr
negateRule = describe "Negate number" $ makeRule "eval.negate" f
 where
   f :: Expr -> Maybe Expr
   f (Negate (Con x))  =  Just $ Con (-x)
   f _                 =  Nothing

addRule :: Rule Expr
addRule = describe "Add two numbers" $ makeRule "eval.add" f
 where
   f :: Expr -> Maybe Expr
   f (Add (Con x) (Con y))  =  Just $ Con (x+y)
   f _                      =  Nothing

and add a rule for multiplication.

mulRule :: Rule Expr
mulRule = describe "Multiply two numbers" $ makeRule "eval.mul" f
 where
   f :: Expr -> Maybe Expr
   f (Mul (Con x) (Con y))  =  Just $ Con (x*y)
   f _                      =  Nothing

Multiplication distributes over addition. This can be viewed as pushing multiplications as far as possible downwards in the expression.

mulAddRule :: Rule Expr
mulAddRule = describe "Distribute multiplication over addition" $ makeRule "eval.dist" f
 where
   f :: Expr -> Maybe Expr
   f (Mul x (Add y z))  =  Just $ Add (Mul x y) (Mul x z)
   f (Mul (Add x y) z)  =  Just $ Add (Mul x z) (Mul y z)
   f _                  =  Nothing

When we evaluate an expression, we no longer return an integer, but an expression in which divisions still may appear. Alternatively, we can use the type Ratio as the result type, but that might look slightly less attractive when there are no divisions in the argument.

We introduce a number of rules that push divisions as far as possible upwards.

divNegateRule :: Rule Expr
divNegateRule = describe "Push negation through division" $ makeRule "eval.divNegate" f
 where
   f :: Expr -> Maybe Expr
   f (Negate (Div x y))  =  Just $ Div (Negate x) y
   f _                   =  Nothing

divAddRule :: Rule Expr
divAddRule = describe "Push add through divisions" $ makeRule "eval.divAdd" f
 where 
   f :: Expr -> Maybe Expr
   f (Add (Div x y) (Div v w))  =  Just $ Div (Add (Mul x w) (Mul v y)) (Mul y w)
   f (Add (Div x y) v)          =  Just $ Div (Add x (Mul v y)) y
   f (Add x (Div y v))          =  Just $ Div (Add (Mul x v) y) v
   f _                          =  Nothing

divMulRule :: Rule Expr
divMulRule = describe "Push multiply through divisions" $ makeRule "eval.divMul" f
 where 
   f :: Expr -> Maybe Expr
   f (Mul (Div x y) (Div v w))  =  Just $ Div (Mul x v) (Mul y w)
   f (Mul (Div x y) v)          =  Just $ Div (Mul x v) y
   f (Mul x (Div v w))          =  Just $ Div (Mul x v) w
   f _                          =  Nothing

The divDivRule is the only rule where Div is not pushed to top-level. These are the standard rules for calculating divisions of divisions. Since the Mul and Add rules do not produce divisions of divisions, there is no risk for a loop in the final evaluation strategy.

divDivRule :: Rule Expr
divDivRule = describe "Push divisions through divisions" $ makeRule "eval.divDiv" f
 where 
   f :: Expr -> Maybe Expr
   f (Div (Div x y) (Div v w))  =  Just $ Mul (Div x y) (Div w v)
   f (Div (Div x y) v)          =  Just $ Div x (Mul y v)
   f (Div x (Div v w))          =  Just $ Mul x (Div w v)
   f _                          =  Nothing

I have two simplification rules for divisions; the topHeavyRule splits a division into an addition and a division. I cannot combine the topHeavyRule with the other division rules (in particular: divAdd) since evaluation will loop otherwise.

divSimplificationRule :: Rule Expr
divSimplificationRule = describe "Simplify a division" $ makeRule "eval.divSimplification" f
 where 
   f :: Expr -> Maybe Expr
   f (Div (Con x) (Con y)) 
     | x == 0    = Just $ Con 0
     | x == y    = Just $ Con 1
     | g >  1    = Just $ Div (Con (div x g)) (Con (div y g)) 
     where g = gcd x y
   f _ = Nothing

topHeavyRule :: Rule Expr
topHeavyRule = describe "Simplify a top heavy division" $ makeRule "eval.topHeavy" f
 where 
   f :: Expr -> Maybe Expr
   f (Div (Con x) (Con y)) 
     | x > y  =  Just $ Add (Con (div x y)) (Div (Con (mod x y)) (Con y))
   f _ = Nothing

allEvaluationRules is the strategy that combines all rules that move multiplications downwards, and divisions upwards, and evaluates all expressions with constants. I do not apply divSimplificationRule, but this could be done.

allEvaluationRules :: LabeledStrategy Expr
allEvaluationRules = label "all rules" $
   negateRule .|. addRule .|. mulRule .|. mulAddRule .|. divNegateRule .|. divAddRule .|. divMulRule .|. divDivRule 
   -- .|. divSimplificationRule this simplification can also be done during evaluation

allSimplificationRules is the strategy that combines all simplification rules.

allSimplificationRules :: LabeledStrategy Expr
allSimplificationRules = label "all rules" $
   topHeavyRule .|. divSimplificationRule .|. addRule

Evaluation consists of applying allEvaluationRules as often as possible, resulting in pushing divisions up as much as possible, followed by applying allSimplificationRules, which simplifies the divisions, replaces top heavy divisions by additions, and does some additional simplications using the addRule in the resulting expression.

evalStrategy :: LabeledStrategy (Context Expr)
evalStrategy = label "eval" $
   repeatS (somewhere (liftToContext allEvaluationRules)) .*. repeatS (somewhere (liftToContext allSimplificationRules))

Evaluation has been extended with a case for Mul, but not for Div.

eval :: Expr -> Int
eval (Add x y)  = eval x + eval y
eval (Mul x y)  = eval x * eval y
eval (Negate x) = -eval x
eval (Con x)    = x 

An expression is in normal form if it is a Con, a non-top heavy division, or the addition of a constant and a division.

isConOrAddDivOrDiv                          :: Expr -> Bool
isConOrAddDivOrDiv (Con _)                  =  True
isConOrAddDivOrDiv (Add (Con _) (Div _ _))  =  True
isConOrAddDivOrDiv (Div (Con _) (Con _))    =  True
isConOrAddDivOrDiv _                        =  False

evalExercise :: Exercise Expr
evalExercise = emptyExercise
   { exerciseId    = describe "Evaluate an expression (full)" $
                        newId "eval.full"
   , status        = Experimental
   , strategy      = evalStrategy
   , prettyPrinter = show
   , navigation    = termNavigator
   , parser        = readM
   , equivalence   = withoutContext eqExpr
   , similarity    = withoutContext (==)
   , ready         = predicate isConOrAddDivOrDiv
   , examples      = examplesFor Easy [expr1, expr2, expr3]
   }

eqExpr :: Expr -> Expr -> Bool
eqExpr x y = eval x == eval y

dr :: DomainReasoner
dr = describe "Domain reasoner for tutorial" (newDomainReasoner "eval") 
   { exercises = [Some evalExercise]
   , services  = myServices
   }

myServices :: [Service]
myServices = metaServiceList dr ++ serviceList

main :: IO ()
main = defaultMain dr
This tutorial is based on ideas-1.8. Last changed: September 2019