1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
<title>Haskore Tutorial: Equivalence of Literal Performances </title>
<body bgcolor="#ffffff"><i>The Haskore Tutorial</i><br><a href="index.html">top</a> <a href="Chords.html">back</a> <a href="related.html">next</a><hr>
<a name="equivalence"></a><a name="sect8"></a>
<h2>8<tt> </tt>Equivalence of Literal Performances</h2>
<p>
A <I>literal performance</I> is one in which no aesthetic
interpretation is given to a musical object. The function
<tt>perform</tt> in fact yields a literal performance; aesthetic nuances must
be expressed explicitly using note and phrase attributes.<p>
There are many musical objects whose literal performances we expect to
be <I>equivalent</I>. For example, the following two musical objects
are certainly not equal as data structures, but we would expect their
literal performances to be identical:
<div align=center><tt>(m1 :+: m2) :+: (m3 :+: m4)</tt> <br>
<tt>m1 :+: m2 :+: m3 :+: m4
</tt></div>
Thus we define a notion of equivalence:<p>
<h3>Definition:</h3>
Two musical objects <tt>m1</tt> and <tt>m2</tt> are <I>equivalent</I>, written
<tt>m1</tt> = <tt>m2</tt>, if and only if:
<div align=center>(forall <tt>imap,c</tt>) <tt>perform imap c m1 = perform imap c m2
</tt></div>
where "<tt>=</tt>" is equality on values (which in Haskell is defined
by the underlying equational logic).<p>
One of the most useful things we can do with this notion of
equivalence is establish the validity of certain <I>transformations
</I>on musical objects. A transformation is <I>valid</I> if the result of
the transformation is equivalent (in the sense defined above) to the
original musical object; i.e. it is "meaning preserving." <p>
The most basic of these transformation we treat as <I>axioms</I> in an
<I>algebra of music</I>. For example:<p>
<p>
<B>Axiom<br>
</B>For any <tt>r1</tt>, <tt>r2</tt>, <tt>r3</tt>, <tt>r4</tt>, and <tt>m</tt>:
<div align=center><tt>Tempo r1 r2 (Tempo r3 r4 m)</tt> = <tt>Tempo (r1*r3) (r2*r4) m
</tt></div>
<p>
<p>
To prove this axiom, we use conventional equational reasoning (for
clarity we omit <tt>imap</tt> and simplify the context to just <tt>dt</tt>):
<h3>Proof:</h3>
<tt> <br>
perform dt (Tempo r1 r2 (Tempo r3 r4 m))<br>
= perform (r2*dt/r1) (Tempo r3 r4 m) -- unfolding perform<br>
= perform (r4*(r2*dt/r1)/r3) m -- unfolding perform<br>
= perform ((r2*r4)*dt/(r1*r3)) m -- simple arithmetic<br>
= perform dt (Tempo (r1*r3) (r2*r4) m) -- folding perform<br>
</tt> <p>
Here is another useful transformation and its validity proof (for
clarity in the proof we omit <tt>imap</tt> and simplify the context to
just <tt>(t,dt)</tt>):<p>
<p>
<B>Axiom<br>
</B>For any <tt>r1</tt>, <tt>r2</tt>, <tt>m1</tt>, and <tt>m2</tt>:
<div align=center><tt>Tempo r1 r2 (m1 :+: m2)</tt> = <tt>Tempo r1 r2 m1 :+: Tempo r1 r2 m2
</tt></div>
<p>
In other words, <I>tempo scaling distributes over sequential
composition</I>.
<h3>Proof:</h3>
<tt> <br>
perform (t,dt) (Tempo r1 r2 (m1 :+: m2))<br>
= perform (t,r2*dt/r1) (m1 :+: m2) -- unfolding perform<br>
= perform (t,r2*dt/r1) m1 ++ perform (t',r2*dt/r1) m2 -- unfolding perform<br>
= perform (t,dt) (Tempo r1 r2 m1) ++ <br>
perform (t',dt) (Tempo r1 r2 m2) -- folding perform<br>
= perform (t,dt) (Tempo r1 r2 m1) ++ <br>
perform (t'',dt) (Tempo r1 r2 m2) -- folding dur<br>
= perform (t,dt) (Tempo r1 r2 m1 :+: Tempo r1 r2 m2) -- folding perform<br>
where t' = t + (dur m1)*r2*dt/r1<br>
t'' = t + (dur (Tempo r1 r2 m1))*dt<br>
</tt> <p>
An even simpler axiom is given by:<p>
<p>
<B>Axiom<br>
</B>For any <tt>r</tt> and <tt>m</tt>:
<div align=center><tt>Tempo r r m</tt> = <tt>m
</tt></div>
<p>
In other words, <I>unit tempo scaling is the identity</I>.
<h3>Proof:</h3>
<tt> <br>
perform (t,dt) (Tempo r r m)<br>
= perform (t,r*dt/r) m -- unfolding perform<br>
= perform (t,dt) m -- simple arithmetic<br>
</tt> <p>
Note that the above proofs, being used to establish axioms, all
involve the definition of <tt>perform</tt>. In contrast, we can also
establish <I>theorems</I> whose proofs involve only the axioms. For
example, Axioms 1, 2, and 3 are all needed to prove the following:
<p>
<B>Theorem<br>
</B>For any <tt>r1</tt>, <tt>r2</tt>, <tt>m1</tt>, and <tt>m2</tt>:
<div align=center><tt>Tempo r1 r2 m1 :+: m2</tt> = <tt>Tempo r1 r2 (m1 :+: Tempo r2 r1 m2)
</tt></div>
<p>
<h3>Proof:</h3>
<tt> <br>
Tempo r1 r2 (m1 :+: Tempo r2 r1 m2)<br>
= Tempo r1 r2 m1 :+: Tempo r1 r2 (Tempo r2 r1 m2) -- by Axiom 1<br>
= Tempo r1 r2 m1 :+: Tempo (r1*r2) (r2*r1) m2 -- by Axiom 2<br>
= Tempo r1 r2 m1 :+: Tempo (r1*r2) (r1*r2) m2 -- simple arithmetic<br>
= Tempo r1 r2 m1 :+: m2 -- by Axiom 3<br>
</tt>
For example, this fact justifies the equivalence of the two phrases
shown in Figure 9.<p>
<table border=2 cellpadding=3>
<tr><td><div align=center><img src="equiv.gif" alt="Equivalent Phrases">
<div align=center><B>Figure 9: Equivalent Phrases</B></div>
</td></tr></table>
<p>
Many other interesting transformations of Haskore musical objects can
be stated and proved correct using equational reasoning. We leave as
an exercise for the reader the proof of the following axioms (which
include the above axioms as special cases).<p>
<p>
<B>Axiom<br>
</B><tt>Tempo</tt> is <I>multiplicative</I> and <tt>Transpose</tt> is
<I>additive</I>. That is, for any <tt>r1</tt>, <tt>r2</tt>, <tt>r3</tt>, <tt>r4</tt>,
<tt>p</tt>, and <tt>m</tt>:
<div align=center><tt>Tempo r1 r2 (Tempo r3 r4 m)</tt> = <tt>Tempo (r1*r3) (r2*r4) m<br>
Trans p1 (Trans p2 m)</tt> = <tt>Trans (p1+p2) m
</tt></div>
<p>
<p>
<B>Axiom<br>
</B>Function composition is <I>commutative</I> with respect to both tempo
scaling and transposition. That is, for any <tt>r1</tt>, <tt>r2</tt>,
<tt>r3</tt>, <tt>r4</tt>, <tt>p1</tt> and <tt>p2</tt>:
<div align=center><tt>Tempo r1 r2 . Tempo r3 r4</tt> = <tt>Tempo r3 r4 . Tempo r1 r2<br>
Trans p1 . Trans p2</tt> = <tt>Trans p2 . Trans p1<br>
Tempo r1 r2 . Trans p1</tt> = <tt>Trans p1 . Tempo r1 r2<br>
</tt></div>
<p>
<p>
<B>Axiom<br>
</B>Tempo scaling and transposition are <I>distributive</I> over both
sequential and parallel composition. That is, for any <tt>r1</tt>,
<tt>r2</tt>, <tt>p</tt>, <tt>m1</tt>, and <tt>m2</tt>:
<div align=center><tt>Tempo r1 r2 (m1 :+: m2)</tt> = <tt>Tempo r1 r2 m1 :+: Tempo r1 r2 m2<br>
Tempo r1 r2 (m1 :=: m2)</tt> = <tt>Tempo r1 r2 m1 :=: Tempo r1 r2 m2<br>
Trans p (m1 :+: m2)</tt> = <tt>Trans p m1 :+: Trans p m2<br>
Trans p (m1 :=: m2)</tt> = <tt>Trans p m1 :=: Trans p m2
</tt></div>
<p>
<p>
<B>Axiom<br>
</B>Sequential and parallel composition are <I>associative</I>. That is,
for any <tt>m0</tt>, <tt>m1</tt>, and <tt>m2</tt>:
<div align=center><tt>m0 :+: (m1 :+: m2)</tt> = <tt>(m0 :+: m1) :+: m2<br>
m0 :=: (m1 :=: m2)</tt> = <tt>(m0 :=: m1) :=: m2
</tt></div>
<p>
<p>
<B>Axiom<br>
</B>Parallel composition is <I>commutative</I>. That is, for any <tt>m0
</tt>and <tt>m1</tt>:
<div align=center><tt>m0 :=: m1</tt> = <tt>m1 :=: m0
</tt></div>
<p>
<p>
<B>Axiom<br>
</B><tt>Rest 0</tt> is a <I>unit</I> for <tt>Tempo</tt> and <tt>Trans</tt>, and a
<I>zero</I> for sequential and parallel composition. That is, for any
<tt>r1</tt>, <tt>r2</tt>, <tt>p</tt>, and <tt>m</tt>:
<div align=center><tt>Tempo r1 r2 (Rest 0)</tt> = <tt>Rest 0<br>
Trans p (Rest 0)</tt> = <tt>Rest 0<br>
m :+: Rest 0</tt> = <tt>m</tt> = <tt>Rest 0 :+: m<br>
m :=: Rest 0</tt> = <tt>m</tt> = <tt>Rest 0 :=: m</tt>
</div>
<p>
<p>
<p>
<B>Exercise<br>
</B>Establish the validity of each of the above axioms.
<p>
<p>
<hr><body bgcolor="#ffffff"><i>The Haskore Tutorial</i><br><a href="index.html">top</a> <a href="Chords.html">back</a> <a href="related.html">next</a>
|
