Solutions to Problem Set 9 ========================== Written by Paul Hudak in literate Haskell style. November 12, 2004 > module PS9 where > import Music > import Perform > import MDL 1. Create some music using MDL. It doesn't have to be sophisticated, and it doesn't have to sound good. You are free to use some kind of an algorithm to generate the music, but you must use each of the constructors in the Music type at least once. To do this you should import the module MDL from Chapter 22, which will automatically import modules Music and Perform from Chapters 20 and 21, respectively. Read Chapter 22 to see how to generate the Midi file. The right function to use to play the Midi file is testNT on Windows XP. [ Listen to "Glove", which was generated by Haskore, but using the CSound back-end, which generates better sound than Midi. ] 2. Do Exercise 20.3 in SOE. Define a version of (/=:) that shortens correctly when either one of its arguments is infinite in duration (but not both). (Hint: first define a function "minDur" that returns the minimum duration of two Music values, even if one is infinite.) Harder: define a version that works properly even when both arguments are infinite. Solution: > (/=/) :: Music -> Music -> Music > m1 /=/ m2 = cut (minDur m1 m2) (m1 :=: m2) "minDur m1 m2" returns the minimum duration of m1 and m2, even if one is infinite. The key to minDur is the function pseudoPerform, which is like perform, except that "pseudoPerform m" returns a list of times corrresponding to the end of each note or rest. This is computed for both m1 and m2, and minDur scans them simultaneously to determine which is the shortest. > minDur :: Music -> Music -> Dur > minDur m1 m2 = > let p1 = pseudoPerform m1 > p2 = pseudoPerform m2 > in lt p1 p2 0 > where lt [] p2 d = d > lt p1 [] d = d > lt p1@(t1:ts1) p2@(t2:ts2) d = > if t1 < t2 > then lt ts1 p2 t1 > else lt p1 ts2 t2 > > pseudoPerform :: Music -> [Dur] > pseudoPerform = fst . pseudoPerf 0 1 > > pseudoPerf :: Dur -> Dur -> Music -> ([Dur], Dur) > pseudoPerf t dt m = > case m of > Note p d -> let d' = d*dt in ([t+d'], d') > Rest d -> let d' = d*dt in ([t+d'], d') > m1 :+: m2 -> let (pf1,d1) = pseudoPerf t dt m1 > (pf2,d2) = pseudoPerf (t+d1) dt m2 > in (pf1++pf2, d1+d2) > m1 :=: m2 -> let (pf1,d1) = pseudoPerf t dt m1 > (pf2,d2) = pseudoPerf t dt m2 > in (merge' pf1 pf2, max d1 d2) > Tempo a m -> pseudoPerf t (dt/a) m > Trans _ m -> pseudoPerf t dt m > Instr _ m -> pseudoPerf t dt m > > merge' :: [Dur] -> [Dur] -> [Dur] > merge' [] ts = ts > merge' ts [] = ts > merge' p1@(t1:ts1) p2@(t2:ts2) = > if t1 else t2 : merge' p1 ts2 Tests: > mu1 = c 4 10 > mu2 = c 4 5 > > t1 = mu1 /=/ mu2 > t2 = mu2 /=/ mu1 > t3 = mu1 /=/ repeatM mu2 > t4 = repeatM mu1 /=/ mu2 > t5 = repeatM mu1 /=/ repeatM mu2 -- won't terminate > t6 = Rest 5 /=/ repeatM mu1 > t7 = (Rest 5 :=: repeatM mu2) /=/ mu1 3. Do Exercise 21.3 in SOE. Prove that: (m0 :+: m1) :=: (m2 :+: m3) === (m0 :=: m2) :+: (m1 :=: m3) if dur m0 = dur m2. Solution: This is an axiom whose proof involves unfolding "perform". Let pf = perform c and pf' = perform (c {cTime = t + rtf (dur m0) * cDur c}) in the following. pf ((m0 :+: m1) :=: (m2 :+: m3)) => merge (pf (m0 :+: m1)) (pf (m2 :+: m3)) -- unfold perform => merge (pf m0 ++ pf' m1) (pf m2 ++ pf' m3) -- unfold perform => sort (sort (pf m0) (pf' m1)) (sort (pf m2) (pf' m3)) -- Lemmas 1&2 => sort (sort (pf m0) (pf m2)) (sort (pf' m1) (pf' m3)) -- Lemmas 3&4 => merge (pf m0) (pf m2) ++ merge (pf' m1) (pf' m3) -- Lemmas 1&2 => pf (m0 :=: m2) ++ pf' (m1 :=: m3) -- fold perform => pf ((m0 :=: m2) :+: (m1 :=: m3)) -- fold perform Lemma 1: if p1 and p2 are time-ordered, then merge p1 p2 = sort p1 p2 Lemma 2: if p1 and p2 are time-ordered, and last p1 >= head p2, then p1 ++ p2 = sort p1 p2 Lemma 3: sort p1 p2 = sort p2 p1 Lemma 4: sort p1 (sort p2 p3) = sort (sort p1 p2) p3 [ Lemmas left unproved :-] 4. Do Exercise 21.4 in SOE. Recall the function revM defined in Chapter 20, and note that, in general, "revM (revM m)" is not equal to "m". However, the following is true: revM (revM m) === m Prove this fact by calculation. Solution: This is theorem that can be proved by induction using the axioms of music, as follows: There are two base cases. Base case 1 (m = Note _ _): revM (revM m) => revM m -- unfold revM => m -- unfold revM Base case 2 (m = Rest _): revM (revM m) => revM m -- unfold revM => m -- unfold revM There are five induction steps. Induction step 1 (m = Tempo a m): revM (revM (Tempo a m)) => revM (Tempo a (revM m)) -- unfold revM => Tempo a (revM (revM m)) -- unfold revM => Tempo a m -- ind hyp Induction steps 2 and 3 (m = Trans i m, m = Instr i m) are very similar to Tempo, and are omitted. Induction step 4 (m = m1 :+: m2): revM (revM (m1 :+: m2)) => revM (revM m2 :+: revM m1) -- unfold revM => revM (revM m1) :+: revM (revM m2) -- unfold revM => m1 :+: m2 -- ind hyp Induction step 5 (m = m1 :=: m2): revM (revM (m1 :=: m2)) => revM (let d1 = dur m1 -- unfold revM d2 = dur m2 in if d1>d2 then revM m1 :=: (Rest (d1-d2) :+: revM m2) else (Rest (d2-d1) :+: revM m1) :=: revM m2 ) Assume d1>d2: => revM (revM m1 :=: (Rest (d1-d2) :+: revM m2)) -- unfold conditional => let d1' = dur (revM m1) -- unfold revM d2' = dur (Rest (d1-d2) :+: revM m2)) in if d1'>d2' then revM (revM m1) :=: (Rest (d1'-d2') :+: revM (Rest (d1-d2) :+: revM m2)) else (Rest (d2'-d1') :+: revM (revM m1)) :=: revM (Rest (d1-d2) :+: revM m2)) Note: d1' = d1 -- Lemma d2' = (d1-d2) + d2 = d1 -- unfold dur & Lemma => (Rest (d2'-d1') :+: revM (revM m1)) :=: -- unfold conditional revM (Rest (d1-d2) :+: revM m2) => (Rest 0 :+: revM (revM m1)) :=: revM (Rest 0 :+: revM m2) -- arithmetic === revM (revM m1) :=: revM (revM m2) -- axiom => m1 :=: m2 -- ind hyp The case where d1 <= d2 is similar, and is omitted. Lemma: dur (revM m) = dur m [ Lemma left unproved :-]