Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4

Resumen Técnico: Prismriver

Declaración del Problema

La teoría musical está regida por un rico conjunto de reglas matemáticas y simetrías que pueden expresarse en un lenguaje matemático preciso. Sin embargo, la teoría musical matemática tradicional se basa en pruebas de lenguaje natural, las cuales están sujetas al error humano, carecen de verificación mecánica y no permiten la reutilización de resultados en un contexto computacional. Si bien existen formalizaciones previas de la teoría musical, muchas están limitadas a sistemas de afinación específicos (como el temperamento igual de 12 tonos) o carecen de la capacidad de realizar composición y análisis algorítmico dentro de un marco unificado. Existe la necesidad de una formalización que soporte sistemas de afinación arbitrarios, permita pruebas de propiedades musicales verificadas por máquina e integre estas pruebas con la composición algorítmica y las capacidades de entrada/salida.

Metodología

Los autores presentan Prismriver, una biblioteca de formalización para la teoría musical y la composición algorítmica construida en Lean 4. Lean sirve tanto como lenguaje de programación funcional como probador de teoremas interactivo, lo que permite a la biblioteca definir estructuras musicales, probar teoremas sobre ellas y generar música.

Representaciones Centrales

1. Escalas Abstractas y Afinación:

   • Prismriver define una PseudoScale como un tipo de tono $P$ genérico sin restricciones, lo que permite representaciones como frecuencias de números reales.
   • Una Scale se define como un tipo de tono $P$ equipado con un tipo de intervalo $I$, donde $I$ forma un grupo abeliano aditivo que actúa sobre $P$ (un $I$-torsor). Esto generaliza el concepto de clases de tono más allá del sistema estándar de 12 tonos.
   • Soporte Xenharmónico: La biblioteca acomoda afinaciones de temperamento no igual, cuartos de tono y escalas con intervalos fundamentales distintos de la octava (por ejemplo, la escala Bohlen-Pierce con un tritave). Distingue entre tonos enarmónicos (por ejemplo, $C\sharp$ frente a $D\flat$) incluso si son acústicamente equivalentes en el temperamento igual de 12 tonos, lo cual es crucial para analizar sistemas de temperamento no igual como la afinación pitagórica.

2. Tiempo y Notas:

   • El tiempo se modela como un grupo abeliano aditivo ordenado $T$.
   • Una nota se define como un par $(P, T)$, que consiste en un tono y una duración.
   • Se implementa un tipo MeasuredTime como un producto de un entero (número de compás) y un número racional (desplazamiento dentro del compás), lo que facilita el análisis de anacrusas y desplazamientos musicales sin necesidad de recalcular los conteos totales de pulsos.

3. Acciones de Transposición y Grupos Diedros:

   • La biblioteca generaliza el concepto de transposición e inversión. Define una TransposeAction que incluye operaciones de traslación ($r_i$) y reflexión ($sr_{a,i}$) actuando sobre escalas arbitrarias.
   • Los autores demuestran que, bajo el temperamento igual de 12 tonos, estas acciones de transposición generalizadas son equivalentes a la acción del grupo diedro $D_{12}$ sobre las tríadas. Esto cierra la brecha entre la teoría de grupos abstracta y los modelos específicos de la teoría musical occidental encontrados en la literatura previa (por ejemplo, [19]).

4. Composición Monádica:

   • La composición algorítmica se gestiona mediante un monad CompositionT. Este monad rastrea un cursor de "tiempo actual" y proporciona primitivas para mover el cursor, añadir eventos (articulaciones) y añadir notas.
   • Un monad Score.foldlM permite el análisis de partituras mediante el plegado (folding) sobre listas de eventos en curso.
   • Estas estructuras monádicas permiten la verificación de algoritmos de composición (por ejemplo, demostrar que un contrapunto generado se adhiere a reglas específicas) utilizando la clase LawfulMonad de Lean.

5. Entrada/Salida:

   • DSL: Un Lenguaje de Dominio Específico (DSL) similar a LilyPong permite a los usuarios introducir música mediante sintaxis basada en texto. El DSL utiliza notación de tono fijo en lugar de notación relativa para reducir la volatilidad.
   • Exportación: Las partituras se exportan a MusicXML (formato basado en el tiempo, convertido a formato por partes para compatibilidad con herramientas como LilyPond y MuseScore).
   • Reproducción: La directiva #play elabora expresiones y lanza un proceso de Alda para la reproducción interactiva.

Principales Contribuciones

1. Formalización de la Teoría Musical: Una biblioteca exhaustiva que formaliza tonos, accidentales, escalas, acordes, duraciones y partes en Lean 4.
2. Compatibilidad de Afinación Generalizada: Soporte para escalas xenharmónicas, incluyendo sistemas de temperamento no igual y escalas con intervalos fundamentales distintos de la octava, yendo más allá de las limitaciones del temperamento igual de 12 tonos.
3. Reducción Probable: Una prueba formal que demuestra que, bajo el temperamento igual de 12 tonos, la acción de transposición generalizada es equivalente a la acción del grupo diedro $D_{12}$ sobre las tríadas.
4. Composición Algorítmica Monádica: Un marco para componer y analizar música utilizando primitivas monádicas, permitiendo la verificación de algoritmos de composición (por ejemplo, el contrapunto de primera especie).
5. Interoperabilidad: Integración de un DSL personalizado para la entrada de música y la exportación a MusicXML para la compatibilidad con software musical externo, junto con la reproducción directa vía Alda.

Resultados e Implementación

El artículo demuestra la utilidad de Prismriver a través de varias implementaciones:

• Composición de Contrapunto: Los autores implementaron un subconjunto de las reglas del contrapunto de primera especie. Definieron predicados para intervalos armónicos y melódicos, consonancia y restricciones específicas (por ejemplo, sin puntos de giro de tritono). Utilizando estos predicados, construyeron contrapuntos programáticamente y demostraron que las composiciones resultantes satisfacen las reglas del contrapunto de primera especie.
• Análisis de Progresión de Acordes: La biblioteca se utilizó para analizar la progresión de acordes de la Canon en Re de Pachelbel en términos de acciones de transposición e inversiones de acordes, validando el modelo de acción diedra generalizada.
• Ejemplos de Código: El documento incluye fragmentos de código que muestran la definición de intervalos, la implementación de la acción del grupo diedro sobre las tríadas y el uso del monad de composición para generar una melodía (basada en Necrofantasia).

Significancia

El artículo sostiene que Prismriver abre la puerta a la composición algorítmica y la generación de acompañamiento verificables. Al formalizar la teoría musical en un asistente de pruebas, los autores permiten:

• Verificación Mecánica: Los errores en las pruebas musicales pueden ser detectados por la computadora, eliminando las ineficiencias de las pruebas escritas a mano.
• Reutilización: Los resultados y las primitivas pueden ser reutilizados mecánicamente en futuras pruebas y composiciones.
• Flexibilidad: La biblioteca permite a los usuarios definir sistemas de afinación y primitivas musicales personalizadas, fomentando una biblioteca creciente y reutilizable de formalización musical.
• Integración: Cierra la brecha entre el análisis teórico de la música y las herramientas prácticas de composición, permitiendo la generación de MusicXML que puede ser reproducido por software estándar.

Los autores posicionan a Prismriver como un paso más allá de herramientas existentes como Lulu (que carece de primitivas de afinación generalizada) y HarmTrace o Mezzo (que están limitadas a sistemas de codificación de tipos o de afinación específicos). Al aprovechar el poder expresivo de Lean, Prismriver proporciona un entorno versátil donde la teoría musical puede ser tanto probada como ejecutada.