Résumé Technique : Prismriver

Énoncé du Problème

La théorie musicale est régie par un riche ensemble de règles mathématiques et de symétries qui peuvent être exprimées dans un langage mathématique précis. Cependant, la théorie musicale mathématique traditionnelle repose sur des preuves en langage naturel, lesquelles sont sujettes à l'erreur humaine, manquent de vérification mécanique et ne permettent pas la réutilisation des résultats dans un contexte computationnel. Bien que des formalisations de la théorie musicale existent, beaucoup sont limitées à des systèmes d'accordage spécifiques (tels que le tempérament égal à 12 tons) ou manquent de la capacité d'effectuer de la composition et de l'analyse algorithmiques au sein d'un cadre unifié. Il existe un besoin pour une formalisation qui supporte des systèmes d'accordage arbitraires, permette des preuves mécaniquement vérifiées de propriétés musicales, et intègre ces preuves à la composition algorithmique et aux capacités d'entrée/sortie.

Méthodologie

Les auteurs présentent Prismriver, une bibliothèque de formalisation pour la théorie musicale et la composition algorithmique construite en Lean 4. Lean sert à la fois de langage de programmation fonctionnelle et de prouveur de théorèmes interactif, permettant à la bibliothèque de définir des structures musicales, de prouver des théorèmes à leur sujet et de générer de la musique.

Représentations Fondamentales

1. Échelles Abstraites et Accordage :

   • Prismriver définit une PseudoScale comme un type de hauteur $P$ générique sans restrictions, permettant des représentations comme des fréquences de nombres réels.
   • Une Scale est définie comme un type de hauteur $P$ équipé d'un type d'intervalle $I$, où $I$ forme un groupe additif abélien agissant sur $P$ (un $I$-torsor). Cela généralise le concept de classes de hauteurs au-delà du système standard de 12 tons.
   • Support Xenharmonique : La bibliothèque accommode les accordages non égaux, les quarts de ton, et les échelles avec des intervalles fondamentaux autres que l'octave (par exemple, l'échelle de Bohlen-Pierce avec un tritave). Elle distingue les hauteurs enharmoniques (par exemple, $C\sharp$ vs $D\flat$) même si elles sont acoustiquement équivalentes dans le tempérament égal à 12 tons, ce qui est crucial pour analyser les systèmes de tempérament non égaux comme l'accordage pythagoricien.

2. Temps et Notes :

   • Le temps est modélisé comme un groupe additif abélien ordonné $T$.
   • Une note est définie comme une paire $(P, T)$, consistant en une hauteur et une durée.
   • Un type MeasuredTime est implémenté comme un produit d'un entier (numéro de mesure) et d'un nombre rationnel (décalage au sein de la mesure), facilitant l'analyse des anacoles et des décalages musicaux sans recalculer le compte total des temps.

3. Actions de Transposition et Groupes Diédraux :

   • La bibliothèque généralise le concept de transposition et d'inversion. Elle définit une TransposeAction qui inclut des opérations de translation ($r_i$) et de réflexion ($sr_{a,i}$) agissant sur des échelles arbitraires.
   • Les auteurs prouvent que sous le tempérament égal à 12 tons, ces actions de transposition généralisées sont équivalentes à l'action du groupe diédral $D_{12}$ sur les triades. Cela comble le fossé entre la théorie des groupes abstraite et les modèles spécifiques de la théorie musicale occidentale trouvés dans la littérature antérieure (par exemple, [19]).

4. Composition Monadique :

   • La composition algorithmique est gérée via un monade CompositionT. Ce monade suit un curseur de "temps actuel" et fournit des primitives pour déplacer le curseur, ajouter des événements (articulations) et ajouter des notes.
   • Une structure Score.foldlM permet l'analyse des partitions en effectuant un repli (fold) sur des listes d'événements en cours.
   • Ces structures monadiques permettent la vérification d'algorithmes de composition (par exemple, prouver qu'un contrepoint généré respecte des règles spécifiques) en utilisant la classe LawfulMonad de Lean.

5. Entrée/Sortie :

   • DSL : Un langage de domaine spécifique (DSL) de type LilyPond permet aux utilisateurs de saisir de la musique via une syntaxe textuelle. Le DSL utilise une notation de hauteur fixe plutôt qu'une notation relative pour réduire la volatilité.
   • Exportation : Les partitions sont exportées en MusicXML (format temporel, converti en format par partie pour la compatibilité avec des outils comme LilyPond et MuseScore).
   • Lecture : La directive #play élabore les expressions et lance un processus Alda pour une lecture interactive.

Contributions Clés

1. Formalisation de la Théorie Musicale : Une bibliothèque complète formalisant les hauteurs, les altérations, les échelles, les accords, les durées et les parties en Lean 4.
2. Compatibilité d'Accordage Généralisée : Support des échelles xenharmoniques, incluant les systèmes de tempérament non égaux et les échelles avec des intervalles fondamentaux autres que l'octave, dépassant les limitations du tempérament égal à 12 tons.
3. Réduction Prouvable : Une preuve formelle démontrant que sous le tempérament égal à 12 tons, l'action de transposition généralisée est équivalente à l'action du groupe diédral $D_{12}$ sur les triades.
4. Composition Algorithmique Monadique : Un cadre pour composer et analyser la musique en utilisant des primitives monadiques, permettant la vérification d'algorithmes de composition (par exemple, le contrepoint de premier espèce).
5. Interopérabilité : Intégration d'un DSL personnalisé pour la saisie musicale et l'exportation MusicXML pour la compatibilité avec des logiciels de musique externes, ainsi qu'une lecture directe via Alda.

Résultats et Implémentation

L'article démontre l'utilité de Prismriver à travers plusieurs implémentations :

• Composition de Contrepoint : Les auteurs ont implémenté un sous-ensemble des règles du contrepoint de premier espèce. Ils ont défini des prédicats pour les intervalles harmoniques et mélodiques, la consonance, et des contraintes spécifiques (par exemple, pas de points de retournement de triton). En utilisant ces prédicats, ils ont construit des contrepoints de manière programmatique et ont prouvé que les compositions résultantes respectent les règles du contrepoint de premier espèce.
• Analyse de Progression d'Accords : La bibliothèque a été utilisée pour analyser la progression d'accords du Canon en Ré de Pachelbel en termes d'actions de transposition et d'inversions d'accords, validant le modèle d'action diédrale généralisée.
• Exemples de Code : L'article inclut des extraits de code montrant la définition d'intervalles, l'implémentation de l'action du groupe diédral sur les triades, et l'utilisation du monade de composition pour générer une mélodie (basée sur Necrofantasia).

Signification

L'article affirme que Prismriver ouvre la voie à la composition et l'accompagnement algorithmiques vérifiables. En formalisant la théorie musicale dans un assistant de preuve, les auteurs permettent :

• Vérification Mécanique : Les erreurs dans les preuves musicales peuvent être détectées par l'ordinateur, éliminant l'inefficacité des preuves manuscrites.
• Réutilisabilité : Les résultats et les primitives peuvent être mécaniquement réutilisés dans de futures preuves et compositions.
• Flexibilité : La bibliothèque permet aux utilisateurs de définir des systèmes d'accordage et des primitives musicales personnalisés, favorisant une bibliothèque croissante et réutilisable de formalisations musicales.
• Intégration : Elle comble le fossé entre l'analyse théorique de la musique et les outils de composition pratique, permettant la génération de MusicXML qui peut être joué par des logiciels standards.

Les auteurs positionnent Prismriver comme une étape au-delà des outils existants comme Lulu (qui manque de primitives d'accordage généralisées) et HarmTrace ou Mezzo (qui sont limités par des encodages de types ou des systèmes d'accordage spécifiques). En exploitant la puissance expressive de Lean, Prismriver fournit un environnement polyvalent où la théorie musicale peut être à la fois prouvée et exécutée.