The Haskore Tutorial
top back next

8  Equivalence of Literal Performances

A literal performance is one in which no aesthetic interpretation is given to a musical object. The function perform in fact yields a literal performance; aesthetic nuances must be expressed explicitly using note and phrase attributes.

There are many musical objects whose literal performances we expect to be equivalent. For example, the following two musical objects are certainly not equal as data structures, but we would expect their literal performances to be identical:

(m1 :+: m2) :+: (m3 :+: m4)
m1 :+: m2 :+: m3 :+: m4
Thus we define a notion of equivalence:

Definition:

Two musical objects m1 and m2 are equivalent, written m1 = m2, if and only if:
(forall imap,c) perform imap c m1 = perform imap c m2
where "=" is equality on values (which in Haskell is defined by the underlying equational logic).

One of the most useful things we can do with this notion of equivalence is establish the validity of certain transformations on musical objects. A transformation is valid if the result of the transformation is equivalent (in the sense defined above) to the original musical object; i.e. it is "meaning preserving."

The most basic of these transformation we treat as axioms in an algebra of music. For example:

Axiom
For any r1, r2, r3, r4, and m:

Tempo r1 r2 (Tempo r3 r4 m) = Tempo (r1*r3) (r2*r4) m

To prove this axiom, we use conventional equational reasoning (for clarity we omit imap and simplify the context to just dt):

Proof:

 
perform dt (Tempo r1 r2 (Tempo r3 r4 m))
= perform (r2*dt/r1) (Tempo r3 r4 m)       -- unfolding perform
= perform (r4*(r2*dt/r1)/r3) m             -- unfolding perform
= perform ((r2*r4)*dt/(r1*r3)) m           -- simple arithmetic
= perform dt (Tempo (r1*r3) (r2*r4) m)     -- folding perform

Here is another useful transformation and its validity proof (for clarity in the proof we omit imap and simplify the context to just (t,dt)):

Axiom
For any r1, r2, m1, and m2:

Tempo r1 r2 (m1 :+: m2) = Tempo r1 r2 m1 :+: Tempo r1 r2 m2

In other words, tempo scaling distributes over sequential composition.

Proof:

 
perform (t,dt) (Tempo r1 r2 (m1 :+: m2))
= perform (t,r2*dt/r1) (m1 :+: m2)                      -- unfolding perform
= perform (t,r2*dt/r1) m1 ++ perform (t',r2*dt/r1) m2   -- unfolding perform
= perform (t,dt) (Tempo r1 r2 m1) ++ 
          perform (t',dt) (Tempo r1 r2 m2)              -- folding perform
= perform (t,dt) (Tempo r1 r2 m1) ++ 
          perform (t'',dt) (Tempo r1 r2 m2)             -- folding dur
= perform (t,dt) (Tempo r1 r2 m1 :+: Tempo r1 r2 m2)    -- folding perform
where t'  = t + (dur m1)*r2*dt/r1
      t'' = t + (dur (Tempo r1 r2 m1))*dt

An even simpler axiom is given by:

Axiom
For any r and m:

Tempo r r m = m

In other words, unit tempo scaling is the identity.

Proof:

 
perform (t,dt) (Tempo r r m)
= perform (t,r*dt/r) m                       -- unfolding perform
= perform (t,dt) m                           -- simple arithmetic

Note that the above proofs, being used to establish axioms, all involve the definition of perform. In contrast, we can also establish theorems whose proofs involve only the axioms. For example, Axioms 1, 2, and 3 are all needed to prove the following:

Theorem
For any r1, r2, m1, and m2:

Tempo r1 r2 m1 :+: m2 = Tempo r1 r2 (m1 :+: Tempo r2 r1 m2)

Proof:

 
Tempo r1 r2 (m1 :+: Tempo r2 r1 m2)
= Tempo r1 r2 m1 :+: Tempo r1 r2 (Tempo r2 r1 m2)     -- by Axiom 1
= Tempo r1 r2 m1 :+: Tempo (r1*r2) (r2*r1) m2         -- by Axiom 2
= Tempo r1 r2 m1 :+: Tempo (r1*r2) (r1*r2) m2         -- simple arithmetic
= Tempo r1 r2 m1 :+: m2                               -- by Axiom 3
For example, this fact justifies the equivalence of the two phrases shown in Figure 9.

Equivalent Phrases
Figure 9: Equivalent Phrases

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).

Axiom
Tempo is multiplicative and Transpose is additive. That is, for any r1, r2, r3, r4, p, and m:

Tempo r1 r2 (Tempo r3 r4 m) = Tempo (r1*r3) (r2*r4) m
Trans p1 (Trans p2 m)
= Trans (p1+p2) m

Axiom
Function composition is commutative with respect to both tempo scaling and transposition. That is, for any r1, r2, r3, r4, p1 and p2:

Tempo r1 r2 . Tempo r3 r4 = Tempo r3 r4 . Tempo r1 r2
Trans p1 . Trans p2
= Trans p2 . Trans p1
Tempo r1 r2 . Trans p1
= Trans p1 . Tempo r1 r2

Axiom
Tempo scaling and transposition are distributive over both sequential and parallel composition. That is, for any r1, r2, p, m1, and m2:

Tempo r1 r2 (m1 :+: m2) = Tempo r1 r2 m1 :+: Tempo r1 r2 m2
Tempo r1 r2 (m1 :=: m2)
= Tempo r1 r2 m1 :=: Tempo r1 r2 m2
Trans p (m1 :+: m2)
= Trans p m1 :+: Trans p m2
Trans p (m1 :=: m2)
= Trans p m1 :=: Trans p m2

Axiom
Sequential and parallel composition are associative. That is, for any m0, m1, and m2:

m0 :+: (m1 :+: m2) = (m0 :+: m1) :+: m2
m0 :=: (m1 :=: m2)
= (m0 :=: m1) :=: m2

Axiom
Parallel composition is commutative. That is, for any m0 and m1:

m0 :=: m1 = m1 :=: m0

Axiom
Rest 0 is a unit for Tempo and Trans, and a zero for sequential and parallel composition. That is, for any r1, r2, p, and m:

Tempo r1 r2 (Rest 0) = Rest 0
Trans p (Rest 0)
= Rest 0
m :+: Rest 0
= m = Rest 0 :+: m
m :=: Rest 0
= m = Rest 0 :=: m

Exercise
Establish the validity of each of the above axioms.


The Haskore Tutorial
top back next