Transcript Chapter 21

Chapter 21
Interpreting Functional Music
Motivation
 A program written in any language, including a DSL,
must have a meaning, i.e. an interpretation, or
denotation, or model, or semantics (all of these
terms are equivalent).


A FAL program denotes a time-varying animation, captured
concretely in the type “Behavior” and the function
“reactimate”.
An IRL program denotes a state transformer, captured
concretely in the type “Robot” and the function
“runRobot”.
 What is the meaning of an MDL program?


Abstractly, an MDL program denotes a piece of music.
Concretely, it will denote a performance, which is a
sequence of musical events.
Performance
 An MDL program denotes a performance:
type Performance = [ Event ]
data Event
= Event { eTime :: Time, eInst :: IName,
ePitch :: AbsPitch, eDur :: DurT }
deriving (Eq, Ord, Show)
type Time
type DurT
= Float
= Float
 An event “Event t i p d” means that instrument i
sounds pitch p at time t for duration d.
 A performance p is assumed to be time-ordered,
and simultaneous events are allowed.
From Music to Performance
 To convert a Music value to a Performance, we need
to know the start time, default instrument, tempo,
and key. This is called the context:
data Context = Context { cTime :: Time,
cInst :: IName,
cDur :: DurT,
cKey :: Key }
deriving Show
type Key
-----
start time
instrument
tempo
key
= AbsPitch
 Then a Music value’s meaning is captured by:
perform :: Context -> Music -> Performance
Tempo and Metronomes
 The “tempo” is the duration, in seconds, of a whole
note.
 For convenience, we define a metronome function:
metro :: Float -> Dur -> DurT
metro setting dur = 60 / (setting * ratioToFloat dur)
 For example, “metro 96 qn” corresponds to a tempo
of 96 quarter notes per minute.
Time to Perform
perform :: Context -> Music -> Performance
perform c@(Context t i dt k) m =
case m of
Note p d -> let d' = rtf d * dt
in [Event t i (transpose p k i) d']
Rest d
-> []
m1 :+: m2 -> perform c m1 ++ perform
(c {cTime = t + rtf (dur m1) * dt}) m2
m1 :=: m2 -> merge (perform c m1) (perform c m2)
Tempo a m -> perform (c {cDur = dt / rtf a}) m
Trans p m -> perform (c {cKey = k + p}) m
Instr nm m -> perform (c {cInst = nm}) m
where transpose p k Percussion = absPitch p
transpose p k _
= absPitch p + k
rtf = ratioToFloat
[ Note: the treatment of (:+:) is inefficient (why?).
See the text for a more efficient solution. ]
Merge
 The function “merge” must preserve the timeordered nature of its arguments.
 A correct but inefficient solution would be:
merge :: Performance -> Performance -> Performance
merge es1 es2 = sort (es1 ++ es2)
 A more efficient solution is:
merge a@(e1:es1) b@(e2:es2) =
if e1 < e2 then e1 : merge es1 b
else e2 : merge a es2
merge [] es2 = es2
merge es1 [] = es1
 If we are willing to give up a certain algebraic
property (discussed later), the text gives an even
more efficient solution.
An Algebra of Music
 Consider these two Music values:
(m1 :+: m2) :+: m3
m1 :+: (m2 :+: m3)
 As Haskell values, they are not equal. But under any
reasonable interpretation of music, they should be.
“If they sound the same, they are the same.”
 Definition:
Two musical values m1 and m2 are equivalent,
written m1 ≡ m2, if and only if:
(∀c) perform c m1 = perform c m2
 Thus we expect that:
(m1 :+: m2) :+: m3 ≡ m1 :+: (m2 :+: m3)
 [ Note similarity to equivalence of regions in Ch. 8. ]
Axioms and Theorems
 The associative law just given can be proved by
unfolding “perform”.
[ This is left as an exercise, but see the text for other
examples of this technique. ]
 Laws that can only be proved by appealing to the
model are called axioms.
 Laws that can be proved using only the axioms are
called theorems.
 If an axiom is true it is said to be sound.
 If any equivalence can be expressed using the set
of axioms, the set is said to be complete.
 A sound and complete set of axioms is called an
axiomatic semantics.
Axioms for Music
 Tempo is multiplicative and Transpose is additive.
Tempo r1 (Tempo r2 m) ≡ Tempo (r1*r2) m
Trans p1 (Trans p2 m) ≡ Trans (p1+p2) m
 Function composition is commutative with respect
to both tempo scaling and transposition.
Tempo r1 . Tempo r2 ≡ Tempo r2 . Tempo r1
Trans p1 . Trans p2 ≡ Trans p2 . Trans p1
Tempo r1 . Trans p1 ≡ Trans p1 . Tempo r1
 Tempo scaling and transposition are distributive
over both sequential and parallel composition.
Tempo r (m1 :+: m2) ≡ Tempo r m1 :+: Tempo r m2
Tempo r (m1 :=: m2) ≡ Tempo r m1 :=: Tempo r m2
Trans p (m1 :+: m2) ≡ Trans p m1 :+: Trans p m2
Trans p (m1 :=: m2) ≡ Trans p m1 :=: Trans p m2
More Axioms
 Sequential and parallel composition are associative.
m0 :+: (m1 :+: m2) ≡ (m0 :+: m1) :+: m2
m0 :=: (m1 :=: m2) ≡ (m0 :=: m1) :=: m2
 Parallel composition is commutative.
m0 :=: m1 ≡ m1 :=: m0
 Rest 0 is a unit for Tempo and Trans, and a zero for
sequential and parallel composition.
Tempo r (Rest 0) ≡ Rest 0
Trans p (Rest 0) ≡ Rest 0
m :+: Rest 0 ≡ m ≡ Rest 0 :+: m
m :=: Rest 0 ≡ m ≡ Rest 0 :=: m
Completeness
 The set of axioms so far is sound.
 Adding this axiom (stated as an exercise in the
text) makes the set complete:
(m0 :+: m1) :=: (m2 :+: m3) ≡ (m0 :=: m2) :+: (m1 :=: m3)
if dur m0 = dur m2
 This is called the “serial-parallel axiom”.
 Pictorially:
m0
m2
m1
m3
≡
m0
m1
m2
m3