FMFP Exercise Session 7 Outline ======= Organizational matters Discussion of the previous sheet Pointers for the next sheet * Organizational matters Next week, the FM part of the course starts. The lecturers and tutors change and here is the new list of sessions. Note that the CAB group is discontinued, please move to ETZ or Wednesday. In general, Wednesday groups are very small, so consider joining those. Tuesday Alex Summers - English (ETZ G91) Milos Novacek - English (NO D11) Uri Juhasz - English (NO E11) Wednesday Cyril Steimer - German (IFW C33) Alex Viand - German (IFW A34) We will not correct Sheet 7; use the master solution provided to check your own solutions. However, feel free to e-mail me if there is something unclear about the master solution. Starting with sheet 8 please follow the FM assistants instructions where to hand in for correction. We will also hold a Q&A session roughly a week or two before the exam. Good Q&A questions are specific: - I don't understand w4.pdf slide 35 - I'm stuck on problem xyz, here's an attempt but I can't figure out what to do Bad Q&A questions: - Explain higher-order functions to me - Explain the whole course to me * Previous sheet ** Assignment 1 (i) lazy evaluation of f g: (\x -> x (\y -> x y)) (\x -> (\y -> y) x) t2 is substituted without evaluation = (\x -> (\y -> y) x) (\y -> (\x -> (\y -> y) x) y) t2 is substituted without evaluation = (\y -> y) (\y -> (\x -> (\y -> y) x) y) t2 is substituted without evaluation = (\y -> (\x -> (\y -> y) x) y) evaluation stops since no evaluation under an abstraction (ii) eager evaluation of f g: (\x -> x (\y -> x y)) (\x -> (\y -> y) x) since t1 is evaluated, t2 is evaluated (prior to substitution) = (\x -> x (\y -> x y)) (\x -> x) substitution of t2 = (\x -> x) (\y -> (\x -> x) y) since evaluation is carried out under an abstraction and since t2 is evaluated prior to substitution, we obtain = (\x -> x) (\y -> y) substitution of t2 = \y -> y ** Assignment 2 Already repeated several times: - when you use induction, *CLEARLY STATE* what the inductive predicate you're proving is; otherwise it is not clear what you're proving (and consequently also not clear whether your proof is correct!) - be explicit about ALL-introduction by using the 'Let x::type be arbitrary' construction. This assignment illustrates why these things are important. Let's go through it step by step. Recall the definitions: addShifted :: [Int] -> Int -> [Int] addShifted [] i = [i] -- addShifted.1 addShifted (x:xs) i = (x + i):addShifted xs x -- addShifted.2 sum :: [Int] -> Int sum [] = 0 -- sum.1 sum (x:xs) = x + sum xs -- sum.2 We are asked to prove: Lemma: FORALL xs::[Int]. sum (addShifted xs 1) = 1 + 2 * sum xs. *** Proof attempt 1 We define: P(xs) := sum (addShifted xs 1) = 1 + 2 * sum xs. and then prove FORALL xs :: [Int]. P(xs) by induction on xs Base case: P([]) sum (addShifted [] 1) = sum ( [1] ) -- addShifted.1 = 1+sum([]) -- sum.2 = 1 + 0 -- sum.1 = 1 + 2*(0) -- arith = 1 + 2* (sum []) -- sum.1 Step case: Let x :: Int and xs :: [Int] be arbitrary and assume P(xs) In other words, assume: sum (addShifted xs 1) = 1 + 2 * sum xs. Now we try to prove P(x:xs) sum (addShifted (x:xs) 1) -- = 1 + 2 * sum (x:xs) = sum ((x+1):addShifted xs x) -- addShifted.1 = (x+1) + sum (addShifted xs x) -- sum.2 = 1 + x + sum (addShifted xs x) Ooops. We clearly can't use our induction hypothesis here (good thing we stated it explicitly!). The problem: it mentions one number explicitly (number 1), but we need to use with another number in the proof. *** Proof attempt 2 Let's try to use that other number in our induction hypothesis: P(xs) := sum (addShifted xs x) = x + 2 * sum xs. Base case works again Step case: Let x :: Int and xs :: [Int] be arbitrary and assume P(xs) Ooops. why does this not work? *** Proof attempt 3 We can change the name of the variable in the step case: Let y :: Int and xs :: [Int] be arbitrary and assume P(xs) But this will not work either - why? *** Proof attempt 4 Whatever number we put in the P(xs), it will not work; our induction hypothesis will end up being *too weak*. We need to *generalize* or *strengthen* it. That is, we need a more general P(xs), which works for all numbers. P(xs) := FORALL i::Int. sum (addShifted xs i) = i + 2 * sum xs. If we can show FORALL xs::[Int]. P(xs) by induction, we can clearly use this to prove our original statement. Now we have some more proving to do, but our hypothesis will be stronger. Proof: We show FORALL xs::[Int]. P(xs) by induction on xs. Base Case: Show P([]). Let i::Int be arbitrary. sum (addShifted [] i) = ... Step Case: Let x :: a and xs :: [a] be arbitrary. Assume P(xs). Show P(x:xs). Let i::Int be arbitrary. sum (addShifted (x:xs) i) = sum ((x+i):addShifted xs x) -- addShifted.1 = (x+i) + sum (addShifted xs x) -- sum.2 = (x+i) + x + 2*sum xs -- P(xs) where i is instantiated with x = i + 2*(x+sum xs) -- arith = i + 2*(sum (x:xs)) -- sum.2 qed. From the lemma above, the following proposition is obvious. You can play with the FORALL rules (intro/elim) to get the desired statement. ** Assignment 4: > generate :: Int -> [[Int]] > generate n = gen n > where > gen 0 = [[]] > gen k = [ q:qs | q <- [1..n], qs <- gen (k-1) ] test for more than one queen in a column: no test needed even, as it holds by design! test for more than one queen in a row: easy - compare the head of the list with all other list elements, then drop it test for more than one queen in a diagonal: - this is done by computing the difference in row - [those are the entries in our list] and comparing it to the column - difference, which we get by zipping with the list [1..] to the - remainder of the list in question. test recursively for the remainder of the list > test :: [Int] -> Bool > test [] = True > test (q:qs) = row q qs && diag q (zip [1..] qs) && test qs > where > row q = all (/=q) > diag q [] = True > diag q ((colDiff, row):qs) = (abs(q - row) /= colDiff) && diag q qs > naivequeens n = filter test $ generate n For the headache note a number of things. The order in which the tests and generates happen are crucial. The earlier positions can be discarded, the better. For this reason our improved solution first computes all VALID boards that are one column smaller, then adds the possible assignments for the queen in question and tests those again right away. > queens n = genQueens n > where > genQueens 0 = [[]] > genQueens k = [ q:qs | qs <- genQueens (k-1) , q <- [1..n] , test q qs ] > test q qs = row q qs && diag q (zip [1..] qs) > row q qs = all (/=q) qs > diag q [] = True > diag q ((colDiff, row):qs) = (abs(q - row) /= colDiff) && diag q qs With this, we can solve the problem for 11 queens in under 10 seconds: *Main> queens 11 (5.33 secs, 2405335696 bytes) *** Preview for sheet 7 * Assignment 1 Just traverse the tree in-order and rename all elements. Consider doing it efficiently by reusing the result from subtrees. Note this requires the internal helper function to return both the tree, and the current 'next index'. * Assignment 2 Typing and type inference again. No surprises. * Assignment 3 Parts a and b are independent of each other. * Assignment 4 (a) and (b) also look very much independent. That is true, but part (d) ties them back together! More typing... \f -> map (<) f :: Ord a => [a] -> [a->Bool] \x y z -> z (x y) :: (a->b) -> (a) -> (b->c) -> c \x -> x (<) :: Ord a=> ((a->a->Bool)->b)-> b map (elem 0) :: Num a, Eq a => [[a]]->[Bool] \p xs -> (\a -> map (\_ -> 0)) (xs==) (takeWhile p xs) :: Num b => (a->Bool) -> [a] -> [b]