Examen del sistema de tipos para verificar la exactitud de la música.



Hoy, se habla mucho sobre la presentación de la música usando lenguajes de programación, porque por un lado es una tarea interesante para los ingenieros, y por otro lado es parte de la descripción universal de la música.

Cómo se ve? Para muchos idiomas, se han creado entornos de programación musical. Los más populares son TidalCycles para Haskell y Sonic Pi para Ruby on the Raspberry Pi. También hay una herramienta que utiliza la biblioteca de compositores de Leipzig . Como está escrito en Clojure, carece de verificación de tipo.

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

La duración y el tono de los sonidos se representan como enteros y coeficientes literales, lo que no es muy conveniente. Cuando se trata de la transformación de la música, la programación puede ser de gran ayuda. Digamos, en el ejemplo anterior, la clave se establece en la clave de Do mayor y el tempo es de 90 latidos por minuto.

Cuando los programadores ven el código de música, a menudo preguntan si es posible evitar la ejecución falsa utilizando un sistema de tipos. Buena pregunta. Si la música se puede representar como código, ¿pueden los errores de escritura musical considerarse errores de programación? Y si es así, ¿por qué no mejorar el proceso de escribir música usando las técnicas que usamos para escribir programas?

En particular, existe una analogía obvia entre los errores que el sistema de tipos puede prevenir y los casos comunes de imprecisión musical. Si su lenguaje de programación puede verificar si pasó una cadena a una función que espera obtener un número, entonces puede verificar que no use f-sharp en un pasaje escrito en Do mayor, cuya clave no hay signos de alteración.

En este artículo, descubriremos qué hace que la música sea correcta y cómo se puede representar mediante un sistema de tipos.

Prescriptivismo


Los teóricos han estado discutiendo durante siglos sobre lo que hace que la música sea correcta. Con mayor frecuencia, operan dentro del marco del prescriptivismo musical: evaluando la música para el cumplimiento de algún conjunto de reglas.

Puede describir la metodología dominante para la formación de reglas:

  • Aprendiendo el canon
  • Definición de patrones
  • Formulandolos como un conjunto de reglas

Entonces se puede argumentar que:

La música que no cumple con estas reglas es incorrecta.

Por ejemplo, la regla de composición establece que no está permitido saltar a una gran septima de a a s en la melodía. Este enfoque ha llevado a numerosos hallazgos valiosos. La música clásica tiene patrones extremadamente interesantes, y una generalización de nuestras observaciones como un conjunto de reglas ayuda a discutir el fenómeno de la música.

Además, seguir las reglas es útil al dominar instrumentos musicales. Es bueno cuando los maestros corrigen a los niños que practican tocar el violín en do mayor, pero se extravían. Hay situaciones en las que es útil adherirse a las definiciones de música correcta e incorrecta.

Sin embargo, este enfoque tiene dos desventajas principales.

Primero, las reglas que surgen de este proceso dependen en gran medida de lo que el teórico considere canon. El sesgo del conjunto de datos conduce al sesgo de las conclusiones, y la música clásica occidental no refleja toda la experiencia musical de la humanidad. Crear reglas basadas en la música de Bach y Mozart puede ser divertido, pero no te contarán demasiado sobre la música en general.

La situación se complica cuando te das cuenta de que los géneros musicales a menudo están fuertemente asociados con ciertas culturas y grupos étnicos, y que al priorizar ciertos tipos de música, priorizas inconscientemente a ciertos tipos de personas. Por ejemplo, en la teoría académica de la música, se presta mucha atención al estudio de las tradiciones europeas clásicas y relativamente poca a la música que se origina en las diásporas de inmigrantes de África.: blues, jazz, rock and roll y hip hop. Si evaluamos la corrección de la música a través de la teoría tradicional, esto puede conducir a una versión culturológica del problema cuando los algoritmos de reconocimiento facial funcionan mejor con los caucásicos que con los negros.

El segundo gran inconveniente de crear reglas al identificar y generalizar patrones es que de esta manera siempre nos enfocaremos en el pasado. Y la música emociona más cuando rompe las reglas. Antes de que Jimmy Page utilizara el efecto de distorsión , los ingenieros consideraron cortar la señal durante la amplificación como un defecto. Y aunque los patrones revelados ayudan a comprender la música moderna, sin embargo, son completamente inadecuados para evaluar la música futura.

Un buen sistema de tipos para la música debería evitar las dos trampas de prescriptivismo descritas. No debe basarse en criterios inaceptables o subjetivos para la música correcta. Al mismo tiempo, tratando de hacer que los estados erróneos no sean representables , el sistema de tipos no debe interferir con la aparición de nuevos estados.

Descriptivismo


Una alternativa al prescriptivismo es el descriptivismo. Si en el primer caso los patrones musicales se consideran reglas vinculantes, en el segundo se consideran patrones que se forman en el curso de la práctica. Un enfoque descriptivo para el estudio de las reglas musicales se ve así:

  • Explorando el cuerpo de la música
  • Identificar tendencias
  • Los formulamos en forma de modelo.

Es posible argumentar que:

La música que se desvía del modelo es inusual.

Para hacer esto, necesitamos un buen modelo de estructuras musicales que pueda describir lo ordinario o lo inusual, en lugar de lo correcto o incorrecto. David Huron, en su libro Sweet Anticipation, ofrece una teoría descriptiva que puede reducirse a tres aspectos clave:

  • La música se clasifica a través del entrenamiento estadístico
  • Estás satisfecho con el pronóstico correcto
  • La novedad no te deja aburrirte

En nuestro ejemplo prescriptivista anterior, saltar de una nota a C se considera un error. Y de acuerdo con la teoría de Huron, esto será muy inusual. Aquellos que han escuchado mucho la música occidental descubrirán que cuando escuchan una nota, la siguiente nota a menudo será otra, o una nota un sonido más alto o más bajo. Saltar a la B sorprenderá a la audiencia, y pueden tomar esto negativamente.

Una de las curiosas consecuencias de la teoría de Huron es que escribir música no es un ejercicio para maximizar o minimizar la ficción. La música se equilibra en el límite entre el orden y el caos, y la ubicación de los oyentes depende de la capacidad del músico para equilibrar el impacto de la novedad con la satisfacción de recibir lo esperado. Si realmente desea verificar la corrección de la composición, deberá asegurarse de que no se aleje demasiado de las tradiciones aceptadas, pero que tampoco las observe de manera demasiado estricta.

Los siguientes son datos de un análisis estadístico de tendencias melódicas. Los colores más oscuros indican resultados más probables. Seleccione una línea con una de las notas y encuentre en ella una celda con una nota que sea más probable que siga la elegida: la intersección resaltada en la oscuridad con la columna de otra nota. Por ejemplo, en este conjunto de datos en el 33.53% de los casos después de que la nota vuelve a aparecer.


Estos datos están tomados del libro de Huron, son el resultado del análisis de más de 250,000 pares de tonos de canciones populares germánicas en general. Otro conjunto de datos, por ejemplo, hip-hop o rock and roll, demostrará diferentes probabilidades.

Todas estas probabilidades se pueden representar de manera equivalente como bits de entropía: una probabilidad del 50% corresponde a un bit, una probabilidad del 25% a dos bits, etc. Para evitar dividir por cero, suponemos que para las transiciones que nunca ocurren en el conjunto de datos, la probabilidad es 1/100 000. Ahora el color más oscuro muestra las transiciones que son más caras en términos de entropía, es decir, menos probable. Por ejemplo, para re después es igual a 6 bits de entropía, es decir, tiene una probabilidad de 1/64.


La representación en forma de entropía nos ayuda a combinar la sorpresa de una serie de notas en las que cada transición de un sonido a otro es un contador de entropía, con la sorpresa de toda la melodía como la suma de las transiciones.

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

Esto es muy similar al modelo oculto de Markov , pero en lugar de generar cadenas de notas, usamos probabilidades ponderadas para estimar la probabilidad de una melodía.

Es posible que haya notado que la transición de la nota a C es de solo 2.48 bits, aunque a primera vista esto contradice el hecho de que la transición de C a C se describió anteriormente como muy inusual. Muy a menudo, las transiciones inusuales son de aproximadamente 10 bits de entropía. La razón de la discrepancia es que los datos de Huron no distinguen entre un salto de seis notas de a a si (muy inusual) y una transición de una nota a un si más bajo (una situación bastante común). Si los datos nos permiten separar estos dos casos, el modelo mostrará que la cadena pre-si-mi-fa sonará aún más poco convencional que la pre-re-mi-fa.

Notas escritas


Idealmente, un sistema de tipos ayuda a los programadores a tomar las decisiones correctas y elimina la posibilidad de errores. Una buena analogía musical es el solfeo. Si no tienes educación musical, entonces podrías familiarizarte con el solfeo en la canción Do-Re-Mi del musical The Sound of Music . Cada nota de una octava tiene su propio nombre, y cualquier nota fuera de la tonalidad del nombre no tiene:

  1. Para (nota más baja de este conjunto)
  2. Re
  3. Mi
  4. F
  5. sal
  6. La
  7. Si
  8. Para (ahora una octava más alta)

Este sistema permite a los músicos adherirse a las notas correctas, establece un mini-idioma que prohíbe tocar notas fuera de la tecla seleccionada. Hay infinitas frecuencias entre d y re, pero no se reproducen dentro del solfeo.

Esto se puede representar fácilmente en el código como datos de tipo algebraico:

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

Ahora puede definir funciones musicales que no permiten notas fuera de las teclas. Por ejemplo, esta función repite una nota n veces:

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

Con esta definición, la repetición triple de una nota re es una expresión que se entenderá fácilmente en el campo musical. Una repetición triple de un filo agudo es un error de verificación de tipo, porque el filo agudo no es un valor de tipo Solfege.

Esto nos da un cierto tipo de seguridad. Nuestro sistema nos permite evitar las notas incorrectas, pero aún así no protege contra combinaciones incorrectas de notas. Si jugáramos en Do mayor, no jugaríamos F fuerte, pero podríamos jugar C, luego saltar a una gran septima con una nota B, lo cual está prohibido por las reglas de composición (tradicionales). Tal verificación de tipo contextual es posible, pero requiere un enfoque más complejo.

Transiciones Mecanografiadas


La biblioteca Mezzo Haskell utiliza tipos relacionados para verificar la corrección musical. La descripción dice que esta es una "prueba muy estricta para la música", la biblioteca puede verificar el cumplimiento de varias reglas de composición, y no solo la tonalidad. En Mezzo, el siguiente código se compila porque la melodía pre-re-mi-fa consiste en los intervalos permitidos:

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

Pero si rompemos la regla que prohíbe saltar de a a si, entonces Mezzo no compilará dicho código:

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

Es genial que Mezzo incluso señale un problema:

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_’

Puede parecer que el sueño de presentar música incorrecta como errores de tipo se ha hecho realidad. Pero a veces surgen situaciones incómodas. Cuando el autor de la biblioteca codificó el preludio de Chopin, resultó que varias veces el compositor no siguió las reglas tradicionales:

El trabajo se transcribió casi por completo, pero a veces fue necesario omitir algunas notas, porque crearon los intervalos prohibidos a los que Mezzo señaló.

Usted puede preguntar, ¿quién se comprometió a prohibirlo? Si a Chopin no se le permite hablar sobre lo que está permitido en la música occidental y lo que no, ¿entonces quién?

El problema es que, aunque Mezzo puede tener en cuenta el contexto, la estimación de tipo sigue siendo una tarea de elección binaria. O bien todas las notas son correctas y el trabajo se compila, ya sea que una de las notas se elimine y el trabajo no se compile. Y a pesar de que Mezzo le permite elegir reglas de composición, la decisión de aplicar o no la regla es global. Si desactiva la regla porque alguna decisión musical viola el acuerdo habitual, entonces cancelará la verificación de otras partes del trabajo.

Entropía mecanografiada


Una forma de romper o eludir las reglas de mecanografía musical es modelar las transiciones entre notas en términos de similitud según el consejo de Huron. En lugar de declarar una transición particular correcta o incorrecta, puede calcular la cantidad de entropía que refleja la sorpresa de la audiencia por las combinaciones de notas combinadas.

El siguiente código está escrito en el lenguaje funcional tipeado dependiente Idris . En el código, se verifica que la melodía correspondiente a las reglas comienza con ay termina con sal y que el camino entre estas notas genera 8-16 bits de entropía. Primero debe determinar el tipo Melodyque refleja nuestra representación de la melodía con cierta similitud o magnitud de entropía. Este tipo tiene tres constructores:

  • Pure: Refleja la creación de una melodía a partir de una sola nota, con un nivel de entropía superior e inferior igual a cero.
  • (>>=): toma dos melodías y suma sus límites de entropía con el costo de cambiar de una nota al final de la primera melodía a una nota al final de la segunda.
  • Relax: toma una melodía y expande sus límites de entropía.

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)

Esta definición de tipo es más complicada, pero gracias a ella, Idris puede componer una melodía usando notación do, y el compilador rastreará los límites de la entropía por nosotros. Aquí está la melodía relevante con el bajo costo de todas las transiciones:

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

La siguiente melodía no cumple con las reglas, ya que salta a una gran septima. En Mezzo, estará prohibido o deberá deshabilitar completamente la regla. Aquí solo expandimos los límites de la complejidad de la melodía para que se ajuste al rango de 8-24 bits de entropía:

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

Si, en cambio Melody (Do, So) (8, 24), asignamos un tipo que no se ajusta a las reglas de la melodía Melody (Do, So) (8, 16), ¡entonces no se compilaría!

La novedad del enfoque es que le permite comprender cuándo la música se vuelve demasiado aburrida. Si la entropía de la melodía no alcanza el límite inferior, se genera un error de tipo. Entonces, si asigna un tipo a una melodía que cumpla con las reglas, Melody (Do, So) (16, 24)entonces tampoco se compilará, porque su entropía no alcanza el límite inferior. Esto nos inspira con fe en la teoría de Huron, según la cual será demasiado difícil para las personas escuchar música que es demasiado inusual o impredecible.

En el caso degenerado, las transiciones entre notas dentro de la clave no aumentan la entropía, y las transiciones fuera de la clave dan un aumento arbitrariamente grande en la entropía. Entonces es aconsejable volver a una evaluación binaria, en la que cada nota se considerará permitida o prohibida, sin ningún estado intermedio.

Importante pero difícil de verificar


Verificar los tipos de música es difícil porque es difícil determinar la exactitud de la música. Si no podemos modelar matemáticamente con precisión la definición de corrección musical, entonces no podemos transferirla al sistema de tipos. Incluso si podemos formalizar auténticamente nuestra comprensión, tendremos que hacer un esfuerzo y aplicar un sistema de tipo potente para que el compilador pueda evaluar adecuadamente la melodía. Sin embargo, esto es posible con alguna definición y algunos supuestos simplificadores.

¿Es esto solo curiosidad? Tal vez. Es poco probable que la industria de la música adopte pronto un sistema de tipos para evitar errores de composición. Pero si el estudio de la informática en el campo de la música nos ayudará a evaluar de manera diferente lo que juega un papel tan importante en la vida de casi todos nosotros, entonces esto solo justifica todos los esfuerzos.

Quizás no menos importante es el hecho de que la música es solo una de las áreas donde la corrección es importante, pero difícil de verificar. Cuanto más activamente se automatiza la esfera social y cultural con la ayuda de la programación, más a menudo surgen situaciones en las que es difícil evaluar la respuesta, que es crucial para las personas. Tome el uso de un programa de computadora que decida cuánto tiempo encarcelar . La exactitud de las oraciones impuestas depende de complejas compensaciones entre costos y probabilidades, y si no podemos rastrear la lógica de la toma de decisiones por parte del sistema, ¿cómo podemos evaluar la equidad del resultado?

Cada vez que automatizamos procesos opacos de toma de decisiones, debemos preguntarnos: "¿Cómo sabemos que el sistema funciona correctamente?"

All Articles