Resumo Técnico: Prismriver

Declaração do Problema

A teoria musical é governada por um rico conjunto de regras matemáticas e simetrias que podem ser expressas em linguagem matemática precisa. No entanto, a teoria musical matemática tradicional baseia-se em provas de linguagem natural, que estão sujeitas ao erro humano, carecem de verificação mecânica e não permitem o reuso de resultados em um contexto computacional. Embora existam formalizações anteriores da teoria musical, muitas são limitadas a sistemas de afinação específicos (como o temperamento igual de 12 tons) ou carecem de capacidade para realizar composição e análise algorítmica dentro de um framework unificado. Há uma necessidade de uma formalização que suporte sistemas de afinação arbitrários, permita provas mecanicamente verificáveis de propriedades musicais e integre essas provas com composição algorítmica e capacidades de entrada/saída.

Metodologia

Os autores apresentam o Prismriver, uma biblioteca de formalização para teoria musical e composição algorítmica construída em Lean 4. O Lean serve tanto como uma linguagem de programação funcional quanto como um provador de teoremas interativo, permitindo que a biblioteca defina estruturas musicais, prove teoremas sobre elas e gere música.

Representações Principais

1. Escalas Abstratas e Afinação:

   • O Prismriver define uma PseudoScale como um tipo de pitch $P$ genérico sem restrições, permitindo representações como frequências de números reais.
   • Uma Scale é definida como um tipo de pitch $P$ equipado com um tipo de intervalo $I$, onde $I$ forma um grupo aditivo abeliano que atua sobre $P$ (um $I$-torsor). Isso generaliza o conceito de classes de altura além do sistema padrão de 12 tons.
   • Suporte Xenharmônico: A biblioteca acomoda afinações de temperamento não igual, quartos de tom e escalas com intervalos fundamentais diferentes da oitava (por exemplo, a escala Bohlen-Pierce com um tritave). Ela distingue entre pitches enarmônicos (ex: $C\sharp$ vs. $D\flat$) mesmo que sejam acusticamente equivalentes no temperamento igual de 12 tons, o que é crucial para analisar sistemas de temperamento não igual como a afinação pitagórica.

2. Tempo e Notas:

   • O tempo é modelado como um grupo aditivo abeliano ordenado $T$.
   • Uma nota é definida como um par $(P, T)$, consistindo em um pitch e uma duração.
   • Um tipo MeasuredTime é implementado como um produto de um número inteiro (número do compasso) e um número racional (deslocamento dentro do compasso), facilitando a análise de anacroses e deslocamentos de música sem recalcular contagens totais de batidas.

3. Ações de Transposição e Grupos Diedrais:

   • A biblioteca generaliza os conceitos de transposição e inversão. Ela define uma TransposeAction que inclui operações de translação ($r_i$) e reflexão ($sr_{a,i}$) atuando sobre escalas arbitrárias.
   • Os autores provam que, sob o temperamento igual de 12 tons, essas ações de transposição generalizadas são equivalentes à ação do grupo diedral $D_{12}$ sobre tríades. Isso estabelece a ponte entre a teoria de grupos abstrata e modelos específicos da teoria musical ocidental encontrados na literatura anterior (ex: [19]).

4. Composição Monádica:

   • A composição algorítmica é tratada via um monad CompositionT. Este monad rastreia um cursor de "tempo atual" e fornece primitivas para mover o cursor, adicionar eventos (articulações) e adicionar notas.
   • Um monad Score.foldlM permite a análise de partituras ao realizar o fold sobre listas de eventos em andamento.
   • Essas estruturas monádicas permitem a verificação de algoritmos de composição (ex: provar que um contraponto gerado adere a regras específicas) usando a classe LawfulMonad do Lean.

5. Entrada/Saída:

   • DSL: Uma Linguagem de Domínio Específico (DSL) semelhante ao LilyPond permite que usuários insiram música usando sintaxe baseada em texto. A DSL utiliza notação de pitch fixo em vez de notação relativa para reduzir a volatilidade.
   • Exportação: As partituras são exportadas para MusicXML (formato baseado em tempo, convertido para formato baseado em partes para compatibilidade com ferramentas como LilyPond e MuseScore).
   • Reprodução: A diretiva #play elabora expressões e inicia um processo Alda para reprodução interativa.

Contribuições Principais

1. Formalização da Teoria Musical: Uma biblioteca abrangente que formaliza pitches, acidentes, escalas, acordes, durações e partes em Lean 4.
2. Compatibilidade de Afinação Generalizada: Suporte para escalas xenharmônicas, incluindo sistemas de temperamento não igual e escalas com intervalos fundamentais diferentes da oitava, indo além das limitações do temperamento igual de 12 tons.
3. Redução Provável: Uma prova formal demonstrando que, sob o temperamento igual de 12 tons, a ação de transposição generalizada é equivalente à ação do grupo diedral $D_{12}$ sobre tríades.
4. Composição Algorítmica Monádica: Um framework para compor e analisar música usando primitivas monádicas, permitindo a verificação de algoritmos de composição (ex: contraponto de primeira espécie).
5. Interoperabilidade: Integração de uma DSL customizada para entrada de música e exportação MusicXML para compatibilidade com softwares de música externos, além de reprodução direta via Alda.

Resultados e Implementação

O artigo demonstra a utilidade do Prismriver através de várias implementações:

• Composição de Contraponto: Os autores implementaram um subconjunto das regras de contraponto de primeira espécie. Eles definiram predicados para intervalos harmônicos e melódicos, consonância e restrições específicas (ex: sem pontos de virada de trítono). Usando esses predicados, eles construíram contrapontos programaticamente e provaram que as composições resultantes satisfazem as regras do contraponto de primeira espécie.
• Análise de Progressão de Acordes: A biblioteca foi utilizada para analisar a progressão de acordes de Canon in D de Pachelbel em termos de ações de transposição e inversões de acordes, validando o modelo de ação diedral generalizada.
• Exemplos de Código: O artigo inclui trechos de código mostrando a definição de intervalos, a implementação da ação do grupo diedral sobre tríades e o uso do monad de composição para gerar uma melodia (baseada em Necrofantasia).

Significância

O artigo afirma que o Prismriver abre as portas para a composição algorítmica e geração de acompanhamento verificáveis. Ao formalizar a teoria musical em um assistente de prova, os autores permitem:

• Verificação Mecânica: Erros em provas musicais podem ser detectados pelo computador, eliminando as ineficiências de provas manuscritas.
• Reusabilidade: Resultados e primitivas podem ser mecanicamente reutilizados em futuras provas e composições.
• Flexibilidade: A biblioteca permite que usuários definam sistemas de afinação e primitivas musicais customizados, fomentando uma biblioteca crescente e reutilizável de formalização musical.
• Integração: Une a análise teórica da música com ferramentas práticas de composição, permitindo a geração de MusicXML que pode ser tocado por softwares padrão.

Os autores posicionam o Prismriver como um passo além de ferramentas existentes como o Lulu (que carece de primitivas de afinação generalizadas) e o HarmTrace ou Mezzo (que são limitados a tipos específicos de codificação ou sistemas de afinação). Ao aproveitar o poder expressivo do Lean, o Prismriver fornece um ambiente versátil onde a teoria musical pode ser tanto provada quanto executada.