Prüfung des Typensystems zur Überprüfung der Richtigkeit von Musik



Heute wird viel über die Präsentation von Musik in Programmiersprachen gesprochen, da dies einerseits eine interessante Aufgabe für Ingenieure ist und andererseits Teil der universellen Beschreibung von Musik ist.

Wie sieht es aus? Für viele Sprachen wurden Musikprogrammierumgebungen erstellt. Am beliebtesten sind TidalCycles für Haskell und Sonic Pi für Ruby auf dem Raspberry Pi. Es gibt auch ein Tool, das die Leipziger Komponistenbibliothek verwendet . Da es in Clojure geschrieben ist, fehlt es an Typprüfung.

(def row-row-row-your-boat
  (phrase [3/3 3/3 2/3 1/3 3/3]
          [  0   0   0   1   2]))

->> row-row-row-your-boat
  (canon (simple 4))
  (where :pitch (comp C major))
  (where :time (bpm 90))
  play)

Die Dauer und Tonhöhe von Tönen werden als Ganzzahlen und Literalkoeffizienten dargestellt, was nicht sehr praktisch ist. Wenn es um Musiktransformation geht, kann das Programmieren eine große Hilfe sein. Angenommen, im obigen Beispiel ist die Tonart auf die Tonart C-Dur eingestellt und das Tempo beträgt 90 Schläge pro Minute.

Wenn Programmierer Musikcode sehen, fragen sie meistens, ob es möglich ist, eine gefälschte Ausführung mit einem Typsystem zu verhindern. Faire Frage. Wenn Musik als Code dargestellt werden kann, können Fehler beim Schreiben von Musik als Programmierfehler angesehen werden? Und wenn ja, warum nicht den Prozess des Musikschreibens mit den Techniken verbessern, mit denen wir Programme schreiben?

Insbesondere gibt es eine offensichtliche Analogie zwischen Fehlern, die das Typsystem verhindern kann, und häufigen Fällen musikalischer Ungenauigkeit. Wenn Ihre Programmiersprache überprüfen kann, ob Sie eine Zeichenfolge an eine Funktion übergeben haben, die eine Zahl erwartet, kann sie überprüfen, ob Sie in einer in C-Dur geschriebenen Passage kein fis verwenden, dessen Schlüssel es keine Anzeichen von Veränderung gibt.

In diesem Artikel erfahren Sie, was Musik korrekt macht und wie sie mit einem Typensystem dargestellt werden kann.

Präskriptivismus


Theoretiker streiten sich seit Jahrhunderten darüber, was Musik richtig macht. Meistens arbeiten sie im Rahmen des musikalischen Preskriptivismus: Bewertung der Musik auf Einhaltung bestimmter Regeln.

Sie können die vorherrschende Methode zur Bildung von Regeln beschreiben:

  • Den Kanon lernen
  • Definition von Mustern
  • Formulieren sie als Regelwerk

Dann kann argumentiert werden, dass:

Musik, die diesen Regeln nicht entspricht, ist falsch.

Zum Beispiel besagt die Kompositionsregel, dass es nicht erlaubt ist, in der Melodie zu einem großen Septima von bis nach s zu springen. Dieser Ansatz hat zu zahlreichen wertvollen Erkenntnissen geführt. Klassische Musik hat äußerst interessante Muster, und eine Verallgemeinerung unserer Beobachtungen als Regelwerk hilft bei der Diskussion des Phänomens Musik.

Darüber hinaus ist das Befolgen der Regeln beim Beherrschen von Musikinstrumenten hilfreich. Es ist gut, wenn Lehrer Kinder korrigieren, die das Geigenspiel in C-Dur üben, aber in die Irre gehen. Es gibt Situationen, in denen es nützlich ist, sich an die Definitionen von korrekter und falscher Musik zu halten.

Dieser Ansatz hat jedoch zwei Hauptnachteile.

Erstens hängen die Regeln, die sich aus diesem Prozess ergeben, stark davon ab, was der Theoretiker als Kanon betrachtet. Die Verzerrung des Datensatzes führt zur Verzerrung der Schlussfolgerungen, und die westliche klassische Musik spiegelt nicht die gesamte musikalische Erfahrung der Menschheit wider. Das Erstellen von Regeln basierend auf der Musik von Bach und Mozart kann Spaß machen, aber sie werden Ihnen nicht zu viel über Musik im Allgemeinen erzählen.

Die Situation ist kompliziert, wenn Sie feststellen, dass Musikgenres häufig stark mit bestimmten Kulturen und ethnischen Gruppen verbunden sind und dass Sie durch die Priorisierung bestimmter Arten von Musik bestimmte Arten von Menschen unabsichtlich priorisieren. In der akademischen Musiktheorie wird beispielsweise dem Studium der klassischen europäischen Traditionen viel Aufmerksamkeit geschenkt und der Musik, die aus der Diaspora von Einwanderern aus Afrika stammt, relativ wenig Aufmerksamkeit geschenkt: Blues, Jazz, Rock and Roll und Hip Hop. Wenn wir die Korrektheit von Musik anhand der traditionellen Theorie bewerten, kann dies zu einer kulturologischen Version des Problems führen, wenn Gesichtserkennungsalgorithmen bei Kaukasiern besser funktionieren als bei Negern.

Der zweite große Nachteil beim Erstellen von Regeln durch Identifizieren und Verallgemeinern von Mustern besteht darin, dass wir uns auf diese Weise immer auf die Vergangenheit konzentrieren. Und Musik begeistert am meisten, wenn sie gegen die Regeln verstößt. Bevor Jimmy Page den Verzerrungseffekt nutzte , betrachteten die Ingenieure das Abschneiden des Signals während der Verstärkung als Defekt. Und obwohl die aufgedeckten Muster helfen, moderne Musik zu verstehen, sind sie für die Bewertung zukünftiger Musik völlig ungeeignet.

Ein gutes Typensystem für Musik sollte beide beschriebenen Fallen des Preskriptivismus vermeiden. Es sollte nicht auf inakzeptablen oder subjektiven Kriterien für korrekte Musik basieren. Gleichzeitig sollte das Typsystem nicht versuchen , fehlerhafte Zustände nicht darstellbar zu machen , sondern das Auftreten neuer Zustände nicht beeinträchtigen.

Deskriptivismus


Eine Alternative zum Preskriptivismus ist der Deskriptivismus. Wenn im ersten Fall musikalische Muster als verbindliche Regeln betrachtet werden, dann werden sie im zweiten Fall als Muster betrachtet, die im Laufe der Praxis gebildet werden. Ein beschreibender Ansatz zum Studium musikalischer Regeln sieht folgendermaßen aus:

  • Den Körper der Musik erkunden
  • Trends erkennen
  • Wir formulieren sie in Form eines Modells

Es kann argumentiert werden, dass:

Vom Modell abweichende Musik ist ungewöhnlich.

Dazu brauchen wir ein gutes Modell musikalischer Strukturen, das eher das Gewöhnliche oder das Ungewöhnliche als das Richtige oder das Falsche beschreiben kann. David Huron bietet in seinem Buch Sweet Anticipation eine beschreibende Theorie an, die auf drei Schlüsselaspekte reduziert werden kann:

  • Musik wird durch statistisches Training bewertet
  • Sie sind mit der richtigen Prognose zufrieden
  • Neuheit lässt Sie nicht langweilen

In unserem vorherigen präskriptiven Beispiel wird das Springen von einer Note zu C als Fehler angesehen. Und nach der Theorie von Huron wird dies sehr ungewöhnlich sein. Diejenigen, die viel westliche Musik gehört haben, werden feststellen, dass die nächste Note, wenn sie eine Note hören, meistens eine andere Note oder eine Note ist, die einen oder einen Schritt höher oder niedriger klingt. Ein Sprung zum B wird das Publikum überraschen, und sie können dies negativ bewerten.

Eine der merkwürdigen Konsequenzen von Hurons Theorie ist, dass das Schreiben von Musik keine Übung zur Maximierung oder Minimierung von Fiktion ist. Musik balanciert an der Grenze zwischen Ordnung und Chaos, und der Ort der Zuhörer hängt von der Fähigkeit des Musikers ab, den Schock der Neuheit mit der Zufriedenheit des Empfangens des Erwarteten in Einklang zu bringen. Wenn Sie die Richtigkeit der Komposition wirklich überprüfen möchten, müssen Sie sicherstellen, dass sie nicht zu weit von akzeptierten Traditionen entfernt ist, diese aber auch nicht zu streng einhält.

Das Folgende sind Daten aus einer statistischen Analyse melodischer Trends. Dunkle Farben zeigen wahrscheinlichere Ergebnisse an. Wählen Sie eine Linie mit einer der Noten aus und finden Sie darauf eine Zelle mit einer Note, die eher Ihrer Wahl folgt - der dunkel hervorgehobene Schnittpunkt mit der Spalte einer anderen Note. Zum Beispiel wird in diesem Datensatz in 33,53% der Fälle nach der Notiz die Notiz erneut angezeigt.


Diese Daten stammen aus dem Buch Huron und sind das Ergebnis der Analyse von mehr als 250.000 Tonpaaren aus germanischen Volksliedern in Dur. Eine andere Reihe von Daten, beispielsweise Hip-Hop oder Rock'n'Roll, zeigt unterschiedliche Wahrscheinlichkeiten.

Alle diese Wahrscheinlichkeiten können äquivalent als Entropiebits dargestellt werden: Eine Wahrscheinlichkeit von 50% entspricht einem Bit, eine Wahrscheinlichkeit von 25% bis zwei Bits usw. Um eine Division durch Null zu vermeiden, nehmen wir an, dass für Übergänge, die niemals im Datensatz auftreten, die Wahrscheinlichkeit 1/100 000 beträgt. Jetzt zeigt die dunklere Farbe Übergänge, die in Bezug auf die Entropie teurer sind - das heißt weniger wahrscheinlich. Zum Beispiel hat re after gleich 6 Bit Entropie, das heißt, es hat eine Wahrscheinlichkeit von 1/64.


Die Darstellung in Form von Entropie hilft uns, die Überraschung aus einer Reihe von Noten zu kombinieren, in denen jeder Übergang von einem Klang zum anderen ein Entropiezähler ist, wobei die Überraschung aus der gesamten Melodie die Summe der Übergänge ist.

 ->  ->  ->  = 2,20 + 2,71 + 5,94 = 10,85 
 ->  ->  ->  = 2,48 + 7,43 + 5,94 = 15,85 

Dies ist dem Hidden- Markov-Modell sehr ähnlich , aber anstatt Notenfolgen zu generieren, verwenden wir gewichtete Wahrscheinlichkeiten, um die Wahrscheinlichkeit einer Melodie abzuschätzen.

Sie haben vielleicht bemerkt, dass der Übergang von Note zu C nur 2,48 Bit beträgt, obwohl dies auf den ersten Blick der Tatsache widerspricht, dass der Übergang von C zu C oben als sehr ungewöhnlich beschrieben wurde. Am häufigsten sind ungewöhnliche Übergänge ungefähr 10 Bit Entropie. Der Grund für die Diskrepanz ist, dass die Huron-Daten nicht zwischen einem Sprung von sechs Noten von zu nach Si (sehr ungewöhnlich) und einem Übergang von einer Note zu zu einem niedrigeren Si (eine ziemlich häufige Situation) unterscheiden. Wenn die Daten es uns ermöglichen, diese beiden Fälle zu trennen, zeigt das Modell, dass die Pre-Si-Mi-Fa-Kette noch unkonventioneller klingt als die Pre-Re-Mi-Fa-Kette.

Eingeschriebene Notizen


Im Idealfall hilft ein Typsystem Programmierern, die richtigen Entscheidungen zu treffen, und eliminiert die Möglichkeit von Fehlern. Eine gute musikalische Analogie ist Solfeggio. Wenn Sie keine musikalische Ausbildung haben, können Sie Solfeggio auf dem Song Do-Re-Mi aus dem Musical The Sound of Music kennenlernen . Jede Note einer Oktave hat einen eigenen Namen, und jede Note außerhalb der Tonalität des Namens hat nicht:

  1. Bis (niedrigste Note aus diesem Satz)
  2. Re
  3. Mi.
  4. F.
  5. Salz
  6. La
  7. Si
  8. Bis (jetzt eine Oktave höher)

Dieses System ermöglicht es Musikern, sich an die richtigen Noten zu halten. Es legt eine Minisprache fest, die das Spielen von Noten außerhalb der ausgewählten Taste verbietet. Es gibt unendlich viele Frequenzen zwischen d und re, aber sie werden nicht im Solfeggio reproduziert.

Dies kann im Code leicht als algebraische Typdaten dargestellt werden:

data Solfege = Do | Re | Mi | Fa | So | La | Ti

Jetzt können Sie Musikfunktionen definieren, die keine Noten außerhalb der Tasten zulassen. Diese Funktion wird beispielsweise n- mal eine Note wiederholt :

repeat : Nat -> Solfege -> List Solfege
repeat 0 s = [s]
repeat n s = s :: repeat (n - 1) s

Mit dieser Definition ist die dreifache Wiederholung einer Note ein Ausdruck, der im musikalischen Bereich leicht zu verstehen ist. Eine dreifache Wiederholung einer scharfen Schärfe ist ein Typprüfungsfehler, da die scharfe Schärfe kein Typwert ist Solfege.

Dies gibt uns eine bestimmte Art von Sicherheit. Unser System ermöglicht es uns , die falschen Noten zu vermeiden, aber es schützt noch nicht vor Fehl Kombinationen von Noten. Wenn wir in C-Dur spielen würden, würden wir nicht Fis spielen, aber wir könnten C spielen und dann zu einer großen Septima auf einer B-Note springen, was nach (traditionellen) Kompositionsregeln verboten ist. Eine solche kontextbezogene Typprüfung ist möglich, erfordert jedoch einen komplexeren Ansatz.

Typisierte Übergänge


Die Mezzo Haskell-Bibliothek verwendet verwandte Typen, um die musikalische Korrektheit zu überprüfen. Die Beschreibung besagt, dass dies ein "sehr strenger Test für Musik" ist. Die Bibliothek kann überprüfen, ob verschiedene Kompositionsregeln eingehalten werden und nicht nur die Tonalität. In Mezzo wird der folgende Code kompiliert, da die Pre-Re-Mi-Fa-Melodie aus den zulässigen Intervallen besteht:

comp = defScore $ start $ melody :| c :| d :| e :| f :>> g

Wenn wir jedoch gegen die Regel verstoßen, die das Springen von nach nach si verbietet, wird Mezzo einen solchen Code nicht kompilieren:

comp = defScore $ start $ melody :| c :| b :| e :| f :>> g

Es ist großartig, dass Mezzo sogar auf ein Problem hinweist:

Major sevenths are not permitted in melody: C and B
In the first argument of ‘(:|)’, namely ‘melody :| c :| b’
In the first argument of ‘(:|)’, namely ‘melody :| c :| b :| e’
In the first argument of ‘(:>>)’, namely
    ‘melody :| c :| b :| e :| f_’

Es scheint, dass der Traum, falsche Musik als Typfehler darzustellen, wahr geworden ist. Aber manchmal entstehen unangenehme Situationen. Als der Autor der Bibliothek Chopins Auftakt verschlüsselte, stellte sich heraus, dass der Komponist bei mehreren Gelegenheiten nicht den traditionellen Regeln folgte:

Das Werk wurde fast vollständig transkribiert, aber manchmal war es notwendig, ein paar Notizen zu überspringen, weil sie die von Mezzo angegebenen verbotenen Intervalle erzeugten.

Sie fragen sich vielleicht, wer sich verpflichtet hat, es zu verbieten? Wenn Chopin nicht darüber sprechen darf, was in der westlichen Musik zulässig ist und was nicht, wer dann?

Das Problem ist, dass Mezzo zwar den Kontext berücksichtigen kann, die Typschätzung jedoch eine binäre Auswahlaufgabe bleibt. Entweder sind alle Notizen korrekt und die Arbeit wird kompiliert, unabhängig davon, ob eine der Notizen ausgeknockt ist und die Arbeit nicht kompiliert wurde. Und trotz der Tatsache, dass Sie in Mezzo Kompositionsregeln auswählen können, ist die Entscheidung, die Regel anzuwenden oder nicht anzuwenden, global. Wenn Sie die Regel deaktivieren, weil eine musikalische Entscheidung gegen die übliche Vereinbarung verstößt, brechen Sie die Überprüfung anderer Teile des Werks ab.

Typisierte Entropie


Eine Möglichkeit, musikalische Schreibregeln zu brechen oder zu umgehen, besteht darin, die Übergänge zwischen Noten in Bezug auf Ähnlichkeit nach Hurons Rat zu modellieren. Anstatt einen bestimmten Übergang für richtig oder falsch zu erklären, können Sie die Entropie berechnen, die die Überraschung des Publikums über die Paarungskombinationen von Noten widerspiegelt.

Der folgende Code ist in der abhängigen typisierten Funktionssprache Idris geschrieben . Im Code wird überprüft, ob die den Regeln entsprechende Melodie mit to beginnt und mit salt endet und dass der Pfad zwischen diesen Noten 8-16 Bit Entropie erzeugt. Zuerst müssen Sie den Typ bestimmen Melody, der unsere Darstellung der Melodie mit einer bestimmten Ähnlichkeit oder Größe der Entropie widerspiegelt. Dieser Typ hat drei Konstruktoren:

  • Pure: Reflektiert die Erstellung einer Melodie aus einer einzelnen Note mit einem oberen und unteren Entropiepegel von Null.
  • (>>=): nimmt zwei Melodien und addiert ihre Entropiegrenzen mit den Kosten für den Wechsel von einer Note am Ende der ersten Melodie zu einer Note am Ende der zweiten.
  • Relax: nimmt eine Melodie und erweitert ihre Entropiegrenzen.

data Melody : (Solfege, Solfege) -> (Nat, Nat) -> Type where

  Pure  : x -> Melody (x, x) (0, 0)

  (>>=) : Melody (w, x) (low, high) ->
          (() -> Melody (y, z) (low2, high2)) ->
          Melody (w, z) (cost x y + low + low2, cost x y + high + high2)

  Relax : Melody (x, y) (low + dl, high) ->
          Melody (x, y) (low, high + dh)

Diese Typdefinition ist komplizierter, aber dank dieser Definition kann Idris eine Melodie in Notation komponieren do, und der Compiler verfolgt für uns die Grenzen der Entropie. Hier ist die relevante Melodie mit den geringen Kosten aller Übergänge:

conventional : Melody (Do, So) (8, 16)
conventional = Relax $ do
  Pure Do
  Pure Re
  Pure Mi
  Pure Fa
  Pure So

Die folgende Melodie entspricht nicht den Regeln, da sie zu einer großen Septima springt. In Mezzo ist dies entweder verboten oder Sie müssen die Regel vollständig deaktivieren. Hier haben wir nur die Grenzen der Komplexität der Melodie erweitert, sodass sie in den Bereich von 8 bis 24 Entropiebits passt:

unconventional : Melody (Do, So) (8, 24)
unconventional = Relax $ do
  Pure Do
  Pure Ti
  Pure Mi
  Pure Fa
  Pure So

Wenn Melody (Do, So) (8, 24)wir stattdessen einen Typ zuweisen würden, der nicht den Regeln der Melodie entspricht Melody (Do, So) (8, 16), würde er nicht kompiliert!

Das Neue an diesem Ansatz ist, dass Sie verstehen können, wenn die Musik zu langweilig wird. Wenn die Entropie der Melodie die Untergrenze nicht erreicht, wird ein Typfehler erzeugt. Wenn Sie also einer Melodie, die den Regeln entspricht, einen Typ zuweisen, Melody (Do, So) (16, 24)wird dieser ebenfalls nicht kompiliert, da seine Entropie die Untergrenze nicht erreicht. Dies inspiriert uns zum Vertrauen in die Huron-Theorie, wonach es für Menschen zu schwierig sein wird, Musik zu hören, die zu ungewöhnlich oder unvorhersehbar ist.

Im entarteten Fall erhöhen Übergänge zwischen Noten innerhalb der Tonart die Entropie nicht, und Übergänge außerhalb der Tonart führen zu einer willkürlich starken Zunahme der Entropie. Dann ist es ratsam, zu einer binären Auswertung zurückzukehren, bei der jede Note ohne Zwischenstatus als erlaubt oder verboten betrachtet wird.

Wichtig, aber schwer zu überprüfen


Das Überprüfen von Musiktypen ist schwierig, da es schwierig ist, die Richtigkeit der Musik zu bestimmen. Wenn wir die Definition der musikalischen Korrektheit nicht mathematisch genau modellieren können, können wir sie nicht auf das Typensystem übertragen. Selbst wenn wir unser Verständnis authentisch formalisieren können, müssen wir uns anstrengen und ein leistungsfähiges Typsystem anwenden, damit der Compiler die Melodie angemessen bewerten kann. Dies ist jedoch mit einigen Definitionen und einigen vereinfachenden Annahmen möglich.

Ist das nur Neugier? Könnte sein. Es ist unwahrscheinlich, dass die Musikindustrie bald ein Typensystem einführt, um Kompositionsfehler zu vermeiden. Wenn uns das Studium des Rechnens im Bereich der Musik dabei helfen wird, unterschiedlich zu bewerten, was für fast alle von uns eine so wichtige Rolle spielt, dann rechtfertigt dies allein alle Bemühungen.

Vielleicht nicht weniger wichtig ist die Tatsache, dass Musik nur einer der Bereiche ist, in denen Korrektheit wichtig, aber schwer zu überprüfen ist. Je aktiver die soziale und kulturelle Sphäre mit Hilfe der Programmierung automatisiert wird, desto häufiger treten Situationen auf, in denen es schwierig ist, die für die Menschen entscheidende Antwort zu bewerten. Nehmen Sie die Verwendung eines Computerprogramms , das , wie lange einzusperren entscheidet . Die Richtigkeit der verhängten Strafen hängt von komplexen Kompromissen zwischen Kosten und Wahrscheinlichkeiten ab. Wenn wir die Logik der Entscheidungsfindung durch das System nicht verfolgen können, wie können wir dann die Fairness des Ergebnisses bewerten?

Jedes Mal, wenn wir undurchsichtige Entscheidungsprozesse automatisieren, müssen wir uns fragen: „Woher wissen wir, dass das System ordnungsgemäß funktioniert?“

All Articles