Technische Samenvatting: Prismriver

Probleemstelling

Muziektheorie wordt beheerst door een rijke set wiskundige regels en symmetrieën die in een precieze wiskundige taal kunnen worden uitgedrukt. Traditionele wiskundige muziektheorie leunt echter op natuurlijke taalbewijzen, die onderhevig zijn aan menselijke fouten, geen mechanische verificatie missen en niet toelaten om resultaten te hergebruiken in een computationele context. Hoewel er eerdere formalisaties van muziektheorie bestaan, zijn veel daarvan beperkt tot specifieke stemmingen (zoals de 12-toons gelijkzwevende temperatuur) of ontbreekt het hen aan het vermogen om algoritmische compositie en analyse binnen een verenigd kader uit te voeren. Er is behoefte aan een formalisering die ondersteuning biedt voor willekeurige stemmingen, machine-verifieerbare bewijzen van muzikale eigenschappen toestaat en deze bewijzen integreert met algoritmische compositie en input/output-mogelijkheden.

Methodologie

De auteurs presenteren Prismriver, een formaliseringsbibliotheek voor muziektheorie en algoritmische compositie gebouwd in Lean 4. Lean dient zowel als een functionele programmeertaal als een interactieve stellingbewijzer, wat het mogelijk maakt om de bibliotheek te gebruiken voor het definiëren van muzikale structuren, het bewijzen van stellingen over deze structuren en het genereren van muziek.

Kernrepresentaties

1. Abstracte toonladders en stemming:

   • Prismriver definieert een PseudoScale als een generiek toonhoogtetype $P$ zonder restricties, wat representaties zoals frequenties van reële getallen mogelijk maakt.
   • Een Scale wordt gedefinieerd als een toonhoogtetype $P$ uitgerust met een intervaltype $I$, waarbij $I$ een abelse optellende groep vormt die op $P$ werkt (een $I$-torsor). Dit generaliseert het concept van toonklassen voorbij het standaard 12-toons systeem.
   • Xenharmonische ondersteuning: De bibliotheek faciliteert niet-gelijkzwevende stemmingen, kwarttonen en toonladders met fundamentele intervallen die afwijken van de octaaf (bijv. de Bohlen-Pierce schaal met een tritave). Het maakt onderscheid tussen enharmonische toonhoogtes (bijv. $C\sharp$ versus $D\flat$), zelfs als deze akoestisch equivalent zijn in de 12-toons gelijkzwevende temperatuur, wat cruciaal is voor de analyse van niet-gelijkzwevende systemen zoals de pythagoreïsche stemming.

2. Tijd en Noten:

   • Tijd wordt gemodelleerd als een geordende abelse optellende groep $T$.
   • Een noot wordt gedefinieerd als een paar $(P, T)$, bestaande uit een toonhoogte en een duur.
   • Een MeasuredTime type is geïmplementeerd als een product van een geheel getal (maatnummer) en een rationaal getal (offset binnen de maat), wat analyse van maatstrepen en verschuivende muziek vergemakkelijkt zonder het totale aantal tellen opnieuw te hoeven berekenen.

3. Transpositie-acties en Dihedrale Groepen:

   • De bibliotheek generaliseert het concept van transpositie en inversie. Het definieert een TransposeAction die translatie ($r_i$) en reflectie ($sr_{a,i}$) operaties bevat die op willekeurige toonladders werken.
   • De auteurs bewijzen dat onder de 12-toons gelijkzwevende temperatuur, deze gegeneraliseerde transpositie-acties equivalent zijn aan de actie van de dihedrale groep $D_{12}$ op drieklanken. Dit overbrugt de kloof tussen abstracte groepentheorie en specifieke westerse muziektheoretische modellen zoals gevonden in de literatuur (bijv. [19]).

4. Monadische Compositie:

   • Algoritmische compositie wordt afgehandeld via een CompositionT monaad. Deze monaad houdt een "huidige tijd"-cursor bij en biedt primitieven om de cursor te bewegen, gebeurtenissen (articulaties) toe te voegen en noten toe te voegen.
   • Een Score.foldlM monaad maakt de analyse van partituren mogelijk door over lijsten van lopende gebeurtenissen te itereren (folding).
   • Deze monadische structuren maken de verificatie van compositie-algoritmen (bijv. bewijzen dat een gegenereerde contrapunt voldoet aan specifieke regels) mogelijk met behulp van de Lean LawfulMonad klasse.

5. Input/Output:

   • DSL: Een LilyPond-achtige Domain Specific Language (DSL) stelt gebruikers in staat muziek in te voeren met behulp van tekstgebaseerde syntaxis. De DSL gebruikt vaste toonhoogte-notatie in plaats van relatieve notatie om volatiliteit te verminderen.
   • Export: Partituren worden geëxporteerd naar MusicXML (tijd-gebaseerd formaat, geconverteerd naar part-gebaseerd formaat voor compatibiliteit met tools zoals LilyPond en MuseScore).
   • Playback: De #play directive evalueert expressies en start een Alda proces voor interactieve weergave.

Belangrijkste Bijdragen

1. Formalisering van Muziektheorie: Een uitgebreide bibliotheek die toonhoogtes, accidenten, toonladders, akkoorden en partijen formaliseert in Lean 4.
2. Gegeneraliseerde Stemmingscompatibiliteit: Ondersteuning voor xenharmonische toonladders, inclusief niet-gelijkzwevende stemmingen en toonladders met fundamentele intervallen andere dan het octaaf, waarmee de beperkingen van de 12-toons gelijkzwevende temperatuur worden overstegen.
3. Bewijsbaar Reductie: Een formeel bewijs dat aantoont dat onder de 12-toons gelijkzwevende temperatuur de gegeneraliseerde transpositie-actie equivalent is aan de $D_{12}$ dihedrale groep-actie op drieklanken.
4. Monadische Algoritmische Compositie: Een framework voor het componeren en analyseren van muziek met behulp van monadische primitieven, waardoor de verificatie van compositie-algoritmen (bijv. eerste soort contrapunt) mogelijk wordt.
5. Interoperabiliteit: Integratie van een aangepaste DSL voor muziekinvoer en MusicXML-export voor compatibiliteit met externe muzieksoftware, naast directe weergave via Alda.

Resultaten en Implementatie

Het artikel demonstreert het nut van Prismriver door middel van verschillende implementaties:

• Contrapunt Compositie: De auteurs hebben een subset van de regels voor eerste soort contrapunt geïmplementeerd. Ze hebben predicaten gedefinieerd voor harmonische en melodische intervallen, consonantie en specifieke beperkingen (bijv. geen tritonus draaipunten). Met behulp van deze predicaten hebben ze programmatisch contrapunt geconstrueerd en bewezen dat de resulterende composities voldoen aan de regels van het eerste soort contrapunt.
• Akkoordprogressie Analyse: De bibliotheek werd gebruikt om de akkoordprogressie van Pachelbel's Canon in D te analyseren in termen van transpositie-acties en akkoordinversies, wat het gegeneraliseerde dihedrale actiemodel valideert.
• Codevoorbeelden: Het paper bevat codefragmenten die de definitie van intervallen laten zien, de implementatie van de dihedrale groep-actie op drieklanken, en het gebruik van de compositie-monaad om een melodie te genereren (gebaseerd op Necrofantasia).

Betekenis

Het artikel stelt dat Prismriver de deur opent naar verifieerbare algoritmische compositie en begeleidingsgeneratie. Door muziektheorie in een bewijsassistent te formaliseren, stellen de auteurs gebruikers in staat tot:

• Mechanische Verificatie: Fouten in muzikale bewijzen kunnen door de computer worden gedetecteerd, wat de inefficiënties van handgeschreven bewijzen elimineert.
• Herbruikbaarheid: Resultaten en primitieven kunnen mechanisch worden hergebruikt in toekomstige bewijzen en composities.
• Flexibiliteit: De bibliotheek stelt gebruikers in staat om aangepaste stemmingen en muzikale primitieven te definiëren, wat een groeiende, herbruikbare bibliotheek van muziekformalisering bevordert.
• Integratie: Het overbrugt de kloof tussen theoretische muziekanalyse en praktische compositietools, waardoor de generatie van MusicXML mogelijk is die gespeeld kan worden door standaardsoftware.

De auteurs positioneren Prismriver als een stap verder dan bestaande tools zoals Lulu (die een gebrek heeft aan gegeneraliseerde stemmingprimitieven) en HarmTrace of Mezzo (die beperkt zijn tot specifieke type-systeem encodings of stemmingen). Door de expressieve kracht van Lean te benutten, biedt Prismriver een veelzijdige omgeving waarin muziektheorie zowel bewezen als uitgevoerd kan worden.