# Arlen Cox

Ramblings on my hobbies

## Building Your Own Synthesizer Part 1 – Getting Started

This is the start of a series of posts developing a MIDI (Musical Instrument Digital Interface) synthesizer.  For the sake of simplicity, we will start very simple and go from there.  The first synthesizer we will build will be a breath sensitive sine wave.  We will then develop that into a phase modulation synthesizer.

## Some Tools

Rather than developing a plugin that works with just VST or AU hosts, we are going to develop a standalone synthesizer.  Once you have a standalone synth that takes MIDI as input and produces samples, converting it to work as VST or AU should just be a matter of creating the wrappers.  We will discuss this conversion in a later entry in the series.

Since the goal is to make something useful across multiple platforms, we need a way to do real-time audio and MIDI in a cross platform way.  For this we turn to RtAudio and RtMidi.  These are two (compatible) libraries developed by Gary Scavone, who is a one of the original waveguide-based physical modelling researchers.

## Diving Into The Code

We will go over the code starting from the set up of MIDI and audio support. We will then go over the sound generation. Finally we will develop the MIDI control.

### Setting up and probing MIDI

#include<cstdlib>
#include<iostream>
#include "RtMidi.h"
#include "RtAudio.h"

using namespace std;

...

int main(int argc, char** argv)
{
RtMidiIn *midiin;
int nPorts;
// other declarations
...
try {
midiin = new RtMidiIn();
} catch ( RtError &error ) {
error.printMessage();
exit( EXIT_FAILURE );
}
nPorts = midiin->getPortCount();

if(argc != 2) {
// list inputs

string portName;
for(int i = 0; i < nPorts; i++) {
try {
portName = midiin->getPortName(i);
} catch ( RtError &error ) {
error.printMessage();
goto cleanup;
}
cout << "  Input port #d " << i+1 << ": " << portName << endl;
}
goto cleanup;
}

//open specified port
port = atoi(argv[1]) - 1;
if(port >= nPorts) {
cerr << "Invalid port number: " << port << endl;
goto cleanup;
}

midiin->openPort(port);
midiin->setCallback(&midicallback);
midiin->ignoreTypes(false, false, false);

// audio set up
...

cleanup:
delete midiin;
return 0;
}


The code starts by declaring a pointer for the midi input. We then initialize it and get the number of connected ports. If a port was not specified on the command line, we print out all of the ports and their corresponding names and then exit. getPortCount() gets the number of MIDI ports currently available on the computer. We can then use getPortName() to get the string representation of each port.

To open the selected port, we call openPort with the appropriate port number and then specify the callback routine that is responsible for handling MIDI messages. We also specify that no MIDI messages should be ignored.

In the case of an error, we want to delete the memory allocated for midiin, so we jump to the cleanup section and free the allocated memory. This is poor style and we will enhance it in a future version. This would be better handled with auto_ptr or by simply using static allocation.

### Setting up Audio

  unsigned sampleRate;
unsigned bufferFrames;
RtAudio dac;
RtAudio::StreamParameters parameters;


We then fill in the audio setup region:

  parameters.deviceId = dac.getDefaultOutputDevice();
parameters.nChannels = 2;
parameters.firstChannel = 0;

sampleRate = 44100;
bufferFrames = 128;

try {
dac.openStream(&parameters, NULL, RTAUDIO_FLOAT64, sampleRate, &bufferFrames, &sine_gen, NULL);
dac.startStream();
} catch(RtError& e) {
e.printMessage();
goto cleanup;
}


We get an output port and load it into the parameters structure. We also select that we are going to do stereo output and we select the zeroth index on the device. We also select a sample rate of 44100 Hz, which is compatible with most output devices and a buffer of 128 samples, which will produce an output delay of 128/44100 = ~3ms + MIDI delay + hardware buffering delay. This should keep the delay low enough that it is not too noticeable.

We then open the output stream and pass a callback function in that will be responsible for filling the buffer. If there is an error, we catch it, clean up and exit.

### MIDI processing

The MIDI processing routine updates global variables that dictate the sound that will be generated. Therefore, we introduce some global variables:

double phase;
double deltaphase;
double delta;
double amplitude;


The phase variable stores the current phase of the waveform that is being played. The deltaphase variable dicates how much change in phase there will be per sample. The delta variable dictates how much time passes per sample and amplitude is the volume parameter for the waveform.

Using phases instead of time keeps the sound pop-free. If you output sin(2*pi*f*t), you’ll get the correct frequency, but when you change the f value, the output sample may have been high and now it will be low, thus causing a very short, high frequency sound, which is a pop. Using the phase avoids this the frequency changes the rate at which we update the phase, rather than the actual f value.

unsigned breath;
unsigned note;

void midicallback(double deltatime, vector<unsigned char> *message, void *userData) {
//unsigned nBytes = message->size();
/*for(unsigned i = 0; i < nBytes; i++)
std::cout << "Byte " << i << " = " << (int)message->at(i) << ", ";
if(nBytes > 0)
std::cout << "stamp = " << deltatime << std::endl;*/

switch((*message)[0] & 0xF0) {
case 0x80: // note off
//amplitude = 0.0;
cout << "Note off: " << (unsigned)((*message)[1]) << endl;
break;
case 0x90: // note on
{
if((*message)[2] == 0)
break;
(*message)[1] -= 12;
float freq = midiToFreq[(*message)[1]];
deltaphase = 2.0*M_PI*(double)freq*delta;
breath = (*message)[2];
amplitude = (double)(*message)[2]/127.0;
note = (*message)[1];
cout << "Note on: " << (unsigned)((*message)[1]) << " " << (double)freq << " " << (unsigned)((*message)[2]) << endl;
}
break;
case 0xB0: // controller change
switch((*message)[1]) {
case 2: // breath controller
if(breath == 0)
break;
breath = (*message)[2];
cout << "Breath: " << (unsigned)((*message)[2]) << endl;
amplitude = (double)(*message)[2]/127.0;

break;
default:
break;
}
break;
case 0xE0: // pitch bend
{
int bend_amount = ((*message)[2] << 7) + (*message)[1];
bend_amount -= 8192;
cout << "Pitch Bend: " << bend_amount << endl;
float bend = (float)bend_amount/8192.0/8.0+1.0;
float freq = midiToFreq[note]*bend;
deltaphase = 2.0*M_PI*(double)freq*delta;
}
break;
default: // throw it away
break;
}
}


Now we generate the appropriate parameters from the MIDI messages. We ignore the channel for our prototype as it does not actually make a difference and could just complicate using the synth. We do this by bitwise anding the first byte of the message by 0xF0. The lower four bits of the first byte are the channel, so this will force all channels to be channel zero.

Based on the value of the first byte we know mostly what the message is. A 0x80 message indicates note off. A 0x90 message indicates note on, a 0xB0 message indicates controller change (which we use for breath pressure) and 0xE0 indicates pitch bend.

One of the catches with this is that a note on message can also indicate note off. If the velocity is zero, this means note off. Additionally, legato is created by sending the next note on before the previous note off. If you’re not careful to handle this you may get some strange behavior. We handle it by checking to see if the velocity field (byte 2) is 0 before handling note on. If it is zero, we simply break out and don’t do anything. As the note start and stops are dictated by the breath pressure rather than the note on and off messages, we don’t have to properly handle note off.

We convert the midi note value (byte 1 of a note on message) into a frequency using a look up table that can be generated by the following python program:

a = 440.0

s = a/(2.**(69./12))
def fofm(m):
return s*2**(m/12.)

for x in xrange(128):
print "%f," % (fofm(x))


It generates a mapping of MIDI notes to their corresponding frequencies. We use the frequency to compute the deltaphase value and an initial breath pressure value. This is to work around a bug in the controller where it generates breath pressure messages before note on messages. Therefore, we ignore all messages after a pressure of 0 is reached until a note on is received. We must set the pressure at this point or we won’t get any sound until the next breath pressure message is sent, which may never happen.

The rest of this handling is in the controller change code. If the breath pressure value was already 0, we ignore all breath controller changes until the breath pressure is already non-zero. It is set to a non-zero value by the note on code.

Pitch bend simply multiplies the frequency by the value received from the pitch bend message. The value is received as [pitch bend, lsb, msb]. We join the msb and lsb into a single 14 bit number and subtract 8192 to make 0 mean that there is no pitch bend. We scale this value and center it around 1 so that when we multiply it by the frequency we get an appropriately modified frequency value.

### Sound Generation

We decided to support two different waveforms. A sine wave produces a mellow tone, while a sawtooth produces a hard buzz sound common to synthesizers. These sounds are generated by the following code:

double saw(double phase) {
return 1.0/M_PI*phase-1.0;
}

int sine_gen(void* outputBuffer, void* inputBuffer, unsigned nBufferFrames, double streamTime, RtAudioStreamStatus status, void* userData)
{
if(status)
cout << "Stream underflow detected!" << endl;

double* buffer = (double *)outputBuffer;

for(unsigned i = 0; i < nBufferFrames; ++i) {

//double val = amplitude*sin(phase);
double val = amplitude*saw(phase);
*buffer++ = val;
*buffer++ = val;
phase += deltaphase;
if(phase > 2.0*M_PI)
phase -= 2.0*M_PI;
}

return 0;
}


We see that we iterate through all of the possible frames and output samples accordingly. Since the output buffer is an array of double precision floating point numbers and because we know that the two channels are interleaved, we compute the value (val) and then place it into both channels. Also, to maximize precision, we subtract 2*Pi from the phase whenever it gets larger than 2*Pi.

### Bugs and Deficiencies

Currently we are not preserving the pitch bend from note to note. This means that if you maintain a bend and start a new note, it won’t have the bend applied. Also, the code is incredibly unclean and hacky, though it does work well with my EWI-USB. In the next version, we will create a nice interface for handling MIDI and audio output from our synthesizer and we will make a better version of the same synthesizer.

Written by arlencox

November 21, 2010 at 9:42 pm

Posted in Uncategorized

## Proving Implication as a Disjunction in Coq

with one comment

In classical logic there is an equivalence between implication and disjunction:

$\forall P,Q. \; (P \rightarrow Q) \leftrightarrow (\neg P \vee Q)$

A simple proof of this is by case analysis:

P Q P -> Q ~P | Q
F F T T
F T T T
T F F F
T T T T

Let’s prove this in Coq using a partial case analysis.

The first trick is that we need to use the law of excluded middle, which says $\neg P \vee P$ must be a tautology. This is not true in all logics, but in classical logic it is true, so we will use it for our proof.

Coq < Axiom excluded_middle: forall P: Prop, P \/ ~P.
excluded_middle is assumed


Next, we declare our section and state the theorem we wish to prove.

Coq < Section implication.
Coq < Theorem impl: forall P Q: Prop, (P -> Q) <-> (~P \/ Q).
1 subgoal

============================
forall P Q : Prop, P -> Q <-> ~ P \/ Q


We introduce the variable P.

impl < intro P.
1 subgoal

P : Prop
============================
forall Q : Prop, P -> Q <-> ~ P \/ Q


We introduce the variable Q.

impl < intro Q.
1 subgoal

P : Prop
Q : Prop
============================
P -> Q <-> ~ P \/ Q


Because we have a bi-implication, we must split it into two single implications. We do this using the split tactic, which now gives us two subgoals. There is a subgoal for each direction.

impl < split.
2 subgoals

P : Prop
Q : Prop
============================
(P -> Q) -> ~ P \/ Q

subgoal 2 is:
~ P \/ Q -> P -> Q


Working on the top subgoal first, we see an implication. Just like before, we introduce any antecedents into the hypothesis section.

impl < intro HPQ.
2 subgoals

P : Prop
Q : Prop
HPQ : P -> Q
============================
~ P \/ Q

subgoal 2 is:
~ P \/ Q -> P -> Q


Now we have a difficulty. We need to state that if P is true, Q must be true and thus the goal is true. If P is not true, then the goal is true. This split on the cases of P is dependent on the law of excluded middle. Therefore, we must destruct based on the excluded_middle axiom we stated at the beginning using the variable P.

impl < destruct (excluded_middle P).
3 subgoals

P : Prop
Q : Prop
HPQ : P -> Q
H : P
============================
~ P \/ Q

subgoal 2 is:
~ P \/ Q
subgoal 3 is:
~ P \/ Q -> P -> Q


Now we have three subgoals to prove. We split the first subgoal into two, where we assume P in one and ~P in the other. Like we did in the modus tollens proof, we will use P and P -> Q to prove Q.

impl < generalize (HPQ H).
3 subgoals

P : Prop
Q : Prop
HPQ : P -> Q
H : P
============================
Q -> ~ P \/ Q

subgoal 2 is:
~ P \/ Q
subgoal 3 is:
~ P \/ Q -> P -> Q


Like before, this is a two step process, where a new antecedent is introduced to the goal and we must use the intro tactic to place that into the hypothesis.

impl < intro HQ.
3 subgoals

P : Prop
Q : Prop
HPQ : P -> Q
H : P
HQ : Q
============================
~ P \/ Q

subgoal 2 is:
~ P \/ Q
subgoal 3 is:
~ P \/ Q -> P -> Q


Now, we select which disjunct we are going to prove. Since we now have Q, we’ll prove that disjunct. We select it by using the right or left tactic. In this case we use right.

impl < right.
3 subgoals

P : Prop
Q : Prop
HPQ : P -> Q
H : P
HQ : Q
============================
Q

subgoal 2 is:
~ P \/ Q
subgoal 3 is:
~ P \/ Q -> P -> Q


Now the proof is trivial. Our goal is equal to that of one of our hypotheses. We could state exact HQ, but we’ll cheat a little here. Coq can determine which one matches if we simply use the assumption tactic. This finishes the first subgoal.

impl < assumption.
2 subgoals

P : Prop
Q : Prop
HPQ : P -> Q
H : ~ P
============================
~ P \/ Q

subgoal 2 is:
~ P \/ Q -> P -> Q


The ~P case is trivial because we just need to select the appropriate disjunct. This time it is the left disjunct.

impl < left.
2 subgoals

P : Prop
Q : Prop
HPQ : P -> Q
H : ~ P
============================
~ P

subgoal 2 is:
~ P \/ Q -> P -> Q


We complete the first direction of the bi-implication using assumption like above. We now will move on to the other direction.

impl < assumption.
1 subgoal

P : Prop
Q : Prop
============================
~ P \/ Q -> P -> Q


First, we introduce the antecedents to the hypothesis.

impl < intro HNPQ.
1 subgoal

P : Prop
Q : Prop
HNPQ : ~ P \/ Q
============================
P -> Q

impl < intro HP.
1 subgoal

P : Prop
Q : Prop
HNPQ : ~ P \/ Q
HP : P
============================
Q


Now we must prove this for two cases. If ~P is true or if Q is true. This is a case split. We use the tactic case to make two subgoals, one where ~P is true and one where Q is true.

impl < case HNPQ.
2 subgoals

P : Prop
Q : Prop
HNPQ : ~ P \/ Q
HP : P
============================
~ P -> Q

subgoal 2 is:
Q -> Q


We introduce the generated antecedent to our hypothesis and we show that we now have a contradiction, completing the first case.

impl < intro HNP.
2 subgoals

P : Prop
Q : Prop
HNPQ : ~ P \/ Q
HP : P
HNP : ~ P
============================
Q

subgoal 2 is:
Q -> Q

1 subgoal

P : Prop
Q : Prop
HNPQ : ~ P \/ Q
HP : P
============================
Q -> Q


Finally, we prove the last case, which is trivial since we simply must prove that Q -> Q. We introduce Q to the hypothesis and then use the assumption tactic to complete the proof.

impl < intro HQ.
1 subgoal

P : Prop
Q : Prop
HNPQ : ~ P \/ Q
HP : P
HQ : Q
============================
Q

impl < assumption.
Proof completed.


Written by arlencox

November 7, 2010 at 5:51 pm

Posted in coq

Tagged with

## Proving Modus Tollens in Coq

Modus Tollens is quite similar to Modus Ponens except that it proves the contrapositive of the implication:

$\forall p, q. \; \neg q \wedge (p \rightarrow q) \rightarrow \neg p$

If $p \rightarrow q$, we know two things: modus ponens says that if $p$ is true, then $q$ must be true. Modus tollens says that if $q$ is false, then $p$ must be false.

We can prove modus tollens by assuming that $q$ is false and that $p \rightarrow q$ is true. Since $(p \rightarrow q) \leftrightarrow (\neg p \vee q)$, if $q$ is false, $p$ must be false, completing the proof.

Similar to what we did for Modus Ponens, we prove Modus Tollens in Coq. First we present the theorem to Coq. Coq shows the entire theorem as the goal.

Coq < Section Modus_tollens.

Coq < Theorem MT: forall P Q: Prop, ~Q /\ (P -> Q) -> ~P.
1 subgoal

============================
forall P Q : Prop, ~ Q /\ (P -> Q) -> ~ P


Next, we introduce three hypotheses from the forall and from the antecedent of the implication:

MT < intro P.
1 subgoal
P : Prop
============================
forall Q : Prop, ~ Q /\ (P -> Q) -> ~ P

MT < intro Q.
1 subgoal
P : Prop
Q : Prop
============================
~ Q /\ (P -> Q) -> ~ P

MT < intro HNQPQ.
1 subgoal
P : Prop
Q : Prop
HNQPQ : ~ Q /\ (P -> Q)
============================
~ P


Exactly like we did for Modus Ponens, we split the conjunction in the hypothesis into two hypotheses:

MT < destruct HNQPQ as [HNQ HPQ].
1 subgoal
P : Prop
Q : Prop
HNQ : ~ Q
HPQ : P -> Q
============================
~ P


This is where we have to do something different. We’re effectively moving the not P from the right hand side of the implication to the left hand side (negating it in the process) and introducing it as a hypothesis. Now we have P in our hypothesis, but we’re trying to prove false as our goal, so we need to use contradiction in the hypothesis to do so.

MT < intro HP.
1 subgoal
P : Prop
Q : Prop
HNQ : ~ Q
HPQ : P -> Q
HP : P
============================
False


We can find the required contradiction by using P and P -> Q along with modus ponens to show that Q must also by a hypothesis. It is introduced as an antecedent the the previous goal.

MT < generalize (HPQ HP).
1 subgoal
P : Prop
Q : Prop
HNQ : ~ Q
HPQ : P -> Q
HP : P
============================
Q -> False


We can then introduce Q as a new hypothesis because it is on the left hand side of the implication. This produces a contraction because we have both Q and ~Q in the hypothesis.

MT < intro HQ.
1 subgoal
P : Prop
Q : Prop
HNQ : ~ Q
HPQ : P -> Q
HP : P
HQ : Q
============================
False


We declare the contradiction and thus complete the proof.

MT < contradiction.
Proof completed.


Written by arlencox

November 3, 2010 at 6:49 pm

Posted in Uncategorized

## Proving Modus Ponens in Coq

with one comment

Recently, I have been learning how to use theorem provers.  Coq has been my tool of choice because of its clean syntax and relatively good (but still terrible) documentation.  It seems to be quite a powerful tool, but it is quite difficult to use.

When I am proving theorems, I apply a series of tactics.  Consider Modus Ponens:

$\forall p, q. \; p \wedge (p \rightarrow q) \rightarrow q$

If $p$ is false or if $p \rightarrow q$ is false, this equation is trivially true (hypothesis/antecedent is false).  So we only need to consider the cases where p is true and $p \rightarrow q$ is true.  Since $p$ is true, in order for $p \rightarrow q$ to be true, $q$ must be true.  Therefore $q$ is true.

So how do we do this proof in Coq?

First, we start a section.  It names a number of theorems.  We decided to call this Modus_ponens.

Coq < Section Modus_ponens.


Next, we declare the theorem.  We declare P and Q as propositional variables.  Note that this creates a goal for us to prove.  Our hypotheses are stated above the ====== line and our goal is stated below line.

Coq < Theorem MP: forall P Q: Prop, P /\ (P -> Q) -> Q.
1 subgoal

============================
forall P Q : Prop, P /\ (P -> Q) -> Q


We introduce our first hypothesis. While it wasn’t stated above, P must be a propositional variable. We can safely introduce it as a hypothesis since the quantification is only over propositional variables. Any variable that is not propositional need not be considered.

MP < intro P.
1 subgoal

P : Prop
============================
forall Q : Prop, P /\ (P -> Q) -> Q


We introduce Q to the hypotheses exactly as we did with P.

MP < intro Q.
1 subgoal

P : Prop
Q : Prop
============================
P /\ (P -> Q) -> Q


If the antecedent of the implication is false, the goal is trivially true. Therefore, we only consider the case where the antecedent is true. Therefore, we can add it to our hypotheses.

MP < intro HPPQ.
1 subgoal

P : Prop
Q : Prop
HPPQ : P /\ (P -> Q)
============================
Q


Since we now have P /\ (P -> Q) in our hypotheses, we should be able to complete the proof, but we can’t do anything with this hypothesis. It is a compound hypothesis. Therefore, we must break it down into two separate hypothesis. We will call these hypotheses HP and HPQ corresponding to hypothesis of P and hypothesis of P -> Q. The destruct command will split a conjunction in the hypothesis into two hypotheses.

MP < destruct HPPQ as [HP HPQ].
1 subgoal

P : Prop
Q : Prop
HP : P
HPQ : P -> Q
============================
Q


Now that we have all the hypotheses that we need, we can complete the proof. First, since we have that P -> Q, if we have P, we have Q. So we apply P -> Q to our current goal. This gives us a new goal of P.

MP < apply HPQ.
1 subgoal

P : Prop
Q : Prop
HP : P
HPQ : P -> Q
============================
P


Since our goal is P and we have a P in our hypothesis, we can finish the proof by saying that the goal is exactly HP.

MP < exact HP.
Proof completed.


Written by arlencox

October 30, 2010 at 1:27 am

Posted in Uncategorized

## A First Post/Test of WordPress

After not getting very far with Blogger, I’ve decided to give WordPress a try. If it’s good, maybe I’ll move to a real server.

Blogger had several problems that I hope WordPress will resolve:

1. Image support was terrible. Blogger always placed images poorly and it’s mandatory poor integration with Picasaweb was more than pitiful.  Blogger always places inserted pictures at the top of the page. Relocating these to their proper location is an exercise in frustration, at best. Why couldn’t it insert the picture where the cursor is?  Blogger forces pictures to be uploaded to Picasaweb. Since I use and like picasaweb, you might think that this wouldn’t be a problem, but I can’t add pictures already in picasaweb to my blog. I have to reupload them through the horrid Blogger interface.
2. Blogger lacks Math and code support. Hopefully WordPress will allow me to insert and properly format math and source code from a variety of obscure languages.

To prove that WordPress is at least improved over Blogger, here is some math:

$A \wedge B \wedge C \Rightarrow D$

Also, here is some source code:

let _ =
print_endline "Hello World!"


An Image:

Photo from a Rockies vs. Dodgers game.

This is a picture I took at a recent Rockies vs Dodgers game.

Fortunately, WordPress correctly inserted it where the cursor was.  It improves upon Blogger in every way, apparently.

Written by arlencox

September 28, 2010 at 5:38 am

Posted in Uncategorized

## Hello world!

with one comment

Welcome to WordPress.com. This is your first post. Edit or delete it and start blogging!

Written by arlencox

September 28, 2010 at 5:29 am

Posted in Uncategorized