FOP/ex4.2 - 大久保弘崇

4.7

定理4.1から4.3は帰納法による退屈な式変形で示せる。
定理4.4は不明。証明の過程で問題4.9の式を使うようだ。

4.8

dropM d _ | d < 0 = error "What to play?"
dropM d m         = droM d (padM m)
droM d (Prim (Note p d0)) = if d0 > d then Prim (Note p (d0− d)) else Prim (Rest 0)
droM d (Prim (Rest d0))   = Prim (Rest (max 0 (d0− d)))
droM d (m1 :=: m2)        = droM d m1 :=: droM d m2
droM d (Tempo a m)        = Tempo a (droM (d ∗ a) m)
droM d (Trans a m)        = Trans a (droM d m)
droM d (m1 :+: m2)        = let d1 = durM m1 in if d < d1 then droM d m1 :+: m2 else droM (d − d1) m2
 

同等であること示すのは、定理4.4の証明と同等に困難。

4.9

わかりません。

4.10

演奏とその長さを対にして返すようにする。

perform :: Context → Music → Performance
perform c m = fst (perf c (padM m))
perf :: Context → Music → (Performance, DurT)
perf c@(Context t dt k) m = per m where
  per (Prim (Rest d))   = ([ ], d ∗ dt)
  per (Prim (Note p d)) = ([Event t (absPitch p + k) (d ∗ dt)],d ∗ dt)
  per (m1 :+: m2) = let (p1,d1) = per m1
                        (p2,d2) = perf (c{cTime = t + d1}) m2
                    in  (p1 ++ p2, d2)
  per (m1 :=: m2) = let (p1,d1) = per m1
                        (p2,_ ) = per m2
                    in  (merge p1 p2, d1)
  per (Tempo a m) = perf (c{cDur = dt/a}) m
  per (Trans p m) = perf (c{cKey = k + p}) m
 

この答えは不完全である。
なぜなら、padMのpadがまたdurMを呼び出すところに、本質的に同じ無駄があるからである。
同様のアプローチでdurMも効率化しなければならない。

4.11

「時系列」を「時刻の昇順に整列されたイベントのリスト」として、帰納法で容易に証明できる。

4.12

いずれも退屈な証明と予想される。

コメント