FOP/ex4.1 - 大久保弘崇

4.1

前半

absPitch . pitch
= λap → (absPitch . pitch) ap
= λap → 12 ∗ div ap 12 + pcToInt ([C,Cs,···,As,B] !! mod ap 12)
= λap → 12 ∗ div ap 12 + [0..11] !! mod ap 12  --(1)
= λap → 12 ∗ div ap 12 + mod ap 12  --(2)
= λap → ap  --(3)
= id

1は f (xs !! k) = (map f xs) !! k より。
2は x ≤ k ならば [0..k] !! x = x より。
3は除算演算子の定義の x = y ∗ q + r の形になっているところから。

後半
まず「異名同音を考慮して音が等しい」とは、絶対音階に変換して等しいことと定義する。
すなわち、pitch.absPitch と id が異名同音を考慮して音が等しいとは、
任意の音 p に対して、pitch (absPitch p) と id p に absPitch を施した結果が等しいということである。
式で書くと

∀p . absPitch (pitch (absPitch p)) == absPitch (id p)

左辺は前半より absPitch p と等しいので、題意は満たされた。

4.2

trans i (trans j p)
= pitch (absPitch (pitch (absPitch p + j)) + i)
= pitch ((absPitch p + j) + i)
= pitch (absPitch p + (i + j))
= trans (i + j) p

4.3

trilln i k n@(Prim (Note p nd)) = trill i (nd / k) n
trilln' i k n@(Prim (Note p nd)) = trill' i (nd / k) n

4.4

証明するべき式を正しく書く。

∀n = Prim (Note p nd) . durM (trill i d n) = durM n

右辺はndである。
左辺の値がこれに等しいことを、区間で分ける帰納法で証明する。
■基底 0 ≤ nd ≤ d の場合

durM (trill i d n)
= durM (trill i d (Prim (Note p nd)))
= durM (Prim (Note p nd))
= nd

■帰納 ある 0 ≤ nd0について題意が満たされていると仮定する。このとき、nd = nd0 + d を考える。

durM (trill i d n)
= durM (trill i d (Prim (Note p nd)))
= durM (Prim (Note p d) :+: trill (…) d (Prim (Note (…) (nd − d))))
= durM (Prim (Note p d) + durM (trill (…) d (Prim (Note (…) nd0))))
= d + nd0
= nd

4.6

data Mode = Ionian | Dorian | Phrygian | Lydian | Mixolydian | Aeolian | Locrian
scale :: Mode -> Note -> [Music]
scale mode n = m :+: applyM m (mode2scale mode) where
  m = Prim n
  mode2scale Ionian     = ionian
  mode2scale Dorian     = dorian
  mode2scale Phrygian   = phrygian
  mode2scale Lydian     = lydian
  mode2scale Mixolydian = mixolydian
  mode2scale Aeolian    = aeolian
  mode2scale Locrian    = locrian
  major = Trans 2
  minor = Trans 1
  rotate (x:xs) = xs ++ [x]
  applyM m [] = []
  applyM m (trans:ts) = trans m : applyM (trans m) ts
  ionian     = [major, major, minor, major, major, major, minor]
  dorian     = rotate ionian
  phrygian   = rotate dorian
  lydian     = rotate phrygian
  mixolydian = rotate lydian
  aeolian    = rotate mixolydian
  locrian    = rotate aeolian
 

コメント