Sintesi Tecnica: Prismriver

Problematica

La teoria musicale è governata da un ricco insieme di regole matematiche e simmetrie che possono essere espresse in un preciso linguaggio matematico. Tuttavia, la teoria musicale matematica tradizionale si basa su dimostrazioni in linguaggio naturale, che sono soggette all'errore umano, mancano di verifica meccanica e non permettono il riutilizzo dei risultati in un contesto computazionale. Sebbene esistano formalizzazioni precedenti della teoria musicale, molte sono limitate a sistemi di intonazione specifici (come il temperamento equabile a 12 toni) o mancano della capacità di eseguire composizione algoritmica e analisi all'interno di un framework unificato. È necessaria una formalizzazione che supporti sistemi di intonazione arbitrari, permetta dimostrazioni verificate meccanicamente di proprietà musicali e integri queste dimostrazioni con la composizione algoritmica e le capacità di input/output.

Metodologia

Gli autori presentano Prismriver, una libreria di formalizzazione per la teoria musicale e la composizione algoritmica costruita in Lean 4. Lean funge sia da linguaggio di programmazione funzionale che da dimostratore di teoremi interattivo, consentendo alla libreria di definire strutture musicali, dimostrare teoremi su di esse e generare musica.

Rappresentazioni Core

1. Scale Astratte e Intonazione:

   • Prismriver definisce una PseudoScale come un tipo di pitch $P$ generico senza restrizioni, permettendo rappresentazioni come frequenze di numeri reali.
   • Una Scale è definita come un tipo di pitch $P$ dotato di un tipo di intervallo $I$, dove $I$ forma un gruppo additivo abeliano che agisce su $P$ (un torsore $I$). Questo generalizza il concetto di classi di pitch oltre il sistema standard a 12 toni.
   • Supporto Xenharmonico: La libreria accoglie intonazioni non a temperamento equabile, quarti di tono e scale con intervalli fondamentali diversi dall'ottava (ad esempio, la scala Bohlen-Pierce con un tritavo). Distingue tra pitch enarmonici (ad esempio, $C\sharp$ vs. $D\flat$) anche se acusticamente equivalenti nel temperamento equabile a 12 toni, il che è cruciale per l'analisi di sistemi di intonazione non equabili come l'intonazione pitagorica.

2. Tempo e Note:

   • Il tempo è modellato come un gruppo additivo ordinato abeliano $T$.
   • Una nota è definita come una coppia $(P, T)$, composta da un pitch e una durata.
   • È implementato un tipo MeasuredTime come prodotto di un intero (numero di battuta) e un numero razionale (offset all'interno della battuta), facilitando l'analisi di misure di sbarramento (pickups) e spostamenti musicali senza ricalcolare il conteggio totale dei battiti.

3. Azioni di Trasposizione e Gruppi Diedrali:

   • La libreria generalizza i concetti di trasposizione e inversione. Definisce una TransposeAction che include operazioni di traslazione ($r_i$) e riflessione ($sr_{a,i}$) che agiscono su scale arbitrarie.
   • Gli autori dimostrano che, sotto il temperamento equabile a 12 toni, queste azioni di trasposizione generalizzate sono equivalenti all'azione del gruppo diedrale $D_{12}$ sulle triadi. Questo colma il divario tra la teoria dei gruppi astratta e i modelli specifici della teoria musicale occidentale presenti nella letteratura precedente (ad esempio, [19]).

4. Composizione Monadica:

   • La composizione algoritmica è gestita tramite una monade CompositionT. Questa monade traccia un cursore del "tempo corrente" e fornisce primitive per muovere il cursore, aggiungere eventi (articolazioni) e aggiungere note.
   • Una monade Score.foldlM permette l'analisi degli spartiti effettuando il fold su liste di eventi in corso.
   • Queste strutture monadiche consentono la verifica degli algoritmi di composizione (ad esempio, dimostrare che un contrappunto generato aderisce a regole specifiche) utilizzando la classe LawfulMonad di Lean.

5. Input/Output:

   • DSL: Un linguaggio di dominio specifico (DSL) simile a LilyPond permette agli utenti di inserire musica usando una sintassi testuale. Il DSL utilizza la notazione del pitch fisso piuttosto che la notazione relativa per ridurre la volatilità.
   • Export: Gli spartiti sono esportati in MusicXML (formato temporale, convertito in formato per singola parte per la compatibilità con strumenti come LilyPond e MuseScore).
   • Riproduzione: La direttiva #play elabora le espressioni e avvia un processo Alda per la riproduzione interattiva.

Contributi Chiave

1. Formalizzazione della Teoria Musicale: Una libreria completa che formalizza pitch, accidenti, scale, accordi e parti in Lean 4.
2. Compatibilità di Intonazione Generalizzata: Supporto per scale xenharmoniche, inclusi sistemi di intonazione non a temperamento equabile e scale con intervalli fondamentali diversi dall'ottava, andando oltre i limiti del temperamento equabile a 12 toni.
3. Riduzione Dimostrabile: Una dimostrazione formale che mostra come, sotto il temperamento equabile a 12 toni, l'azione di trasposizione generalizzata sia equivalente all'azione del gruppo diedrale $D_{12}$ sulle triadi.
4. Composizione Algoritmica Monadica: Un framework per comporre e analizzare musica usando primitive monadiche, permettendo la verifica di algoritmi di composizione (ad esempio, il contrappunto di prima specie).
5. Interoperabilità: Integrazione di un DSL personalizzato per l'input musicale ed esportazione in MusicXML per la compatibilità con software musicali esterni, insieme alla riproduzione diretta tramite Alda.

Risultati e Implementazione

Il documento dimostra l'utilità di Prismriver attraverso diverse implementazioni:

• Composizione di Contrappunto: Gli autori hanno implementato un sottoinsieme delle regole del contrappunto di prima specie. Hanno definito predicati per gli intervalli armonici e melodici, la consonanza e vincoli specifici (ad esempio, nessun punto di svolta di tritono). Utilizzando questi predicati, hanno costruito contrappunti programmaticamente e dimostrato che le composizioni risultanti soddisfano le regole del contrappunto di prima specie.
• Analisi delle Progressioni di Accordi: La libreria è stata utilizzata per analizzare la progressione di accordi del Canone in Re di Pachelbel in termini di azioni di trasposizione e inversioni di accordi, validando il modello dell'azione diedrale generalizzata.
• Esempi di Codice: Il documento include snippet di codice che mostrano la definizione di intervalli, l'implementazione dell'azione del gruppo diedrale sulle triadi e l'uso della monade di composizione per generare una melodia (basata su Necrofantasia).

Significato

Il documento sostiene che Prismriver apre la strada alla composizione algoritmica e alla generazione di accompagnamento verificabili. Formalizzando la teoria musicale in un assistente alla dimostrazione, gli autori consentono:

• Verifica Meccanica: Gli errori nelle dimostrazioni musicali possono essere rilevati dal computer, eliminando le inefficienze delle dimostrazioni scritte a mano.
• Riutilizzabilità: I risultati e le primitive possono essere meccanicamente riutilizzati in future dimostrazioni e composizioni.
• Flessibilità: La libreria consente agli utenti di definire sistemi di intonazione e primitive musicali personalizzati, favorendo una libreria crescente e riutilizzabile di formalizzazione musicale.
• Integrazione: Colma il divario tra l'analisi teorica della musica e gli strumenti pratici di composizione, permettendo la generazione di MusicXML che può essere eseguito da software standard.

Gli autori posizionano Prismriver come un passo oltre strumenti esistenti come Lulu (che manca di primitive di intonazione generalizzate) e HarmTrace o Mezzo (che sono limitati a specifici encoding di sistemi di tipo o sistemi di intonazione). Sfruttando la potenza espressiva di Lean, Prismriver fornisce un ambiente versatile dove la teoria musicale può essere sia dimostrata che eseguita.