These are some points of reference and notes from the book the haskell school of music chapter one.
1.3 Computation by Calculation
By Example
3 * (9 + 5)
3 * 14
⇒ 42 ⇒
Definition
= x * y + z simple x y z
Invocation
3 9 5 simple
Calculation
3 9 5
simple ⇒ 3 * (9 + 5) -- example of unfolding
⇒ 3 * 14
⇒ 42
So we can write simple 3 9 5 ⟹ 42
Which should be read as:
simple 3 9 5 evaluates to 42
-- reads e evaluates to v e ⟹ v
This stuff is imlortant because musical programs usually have some kind of mathematical basis. Proof by calculation might be a tool used to connect problem specs with implementations. This may seem tedious but can be rewarding due to the confidence in the program and the ability to rule out errors earlier.
Exercise 1.1
Write out the calculation of: simple (simple 2 3 4) 5 6
2 3 4) 5 6
simple (simple ⇒ simple (3 * (9 + 5)) 5 6
⇒ simple (3 * 14) 5 6
⇒ simple (42) 5 6
⇒ 42 * (5 + 6)
⇒ 42 * 11
⇒ 462
Exercise 1.2
Prove by calculation that: simple (a - b) a b ⟹ a² - b²
- b) a b
simple (a ⇒ (a - b) * (a + b)
⇒ a² + ab - ab - b²
⇒ a² - b²