💻 computer science

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

本文介绍了 Prismriver，这是一个通过形式化音乐理论来使可验证算法作曲成为可能、实现超越十二平均律调律的泛化、模拟对位法，并通过自定义 DSL 和 MusicXML 导出功能与标准音乐软件进行互操作的 Lean 4 库。

原作者： Leni Aniva, Claire Wang

发布于 2026-07-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Leni Aniva, Claire Wang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

不要将乐理想象成一本陈旧的、规定“该做什么、不该做什么”的规则手册，而要将其想象成一个巨大的、隐形的数学形状游乐场。几个世纪以来，音乐家们一直凭直觉在这些形状中嬉戏，但他们从未能够制造出一台能够“证明”这些形状是完美的机器人。这就是 Prismriver 的意义所在。它是一个构建在名为 Lean 4 的超智能计算机程序之内的全新数字工具箱，旨在将乐理转化为一场可验证的逻辑游戏。

把 Prismriver 想象成一个音乐的通用翻译器。在此之前，大多数计算机音乐工具都假设世界只有一种调音方式：标准的“十二平均律”（你在钢琴上看到的 12 个音符）。这就像假设世界上所有的语言都只有 26 个字母一样。Prismriver 打破了这一规则。它允许你发明任何你想要的音阶，甚至是带有“四分之一音”（钢琴键之间微小的音符）或“八度”不再是主要重复模式的音阶。这就像是给作曲家一个键盘，其按键可以拉伸、收缩或消失，而计算机仍然能够理解背后的数学原理。

“证明”游乐场

Prismriver 最酷的地方在于它处理音乐规则的方式。通常情况下，如果一位作曲家写了一首歌，我们只是听听看，然后说：“嗯，这听起来不错。”但在 Prismriver 中，你可以写一首歌，并要求计算机证明它遵循了规则。

想象你正在搭建一个积木塔。在过去，你只需堆叠它们并祈祷它们不会倒塌。有了 Prismriver，你拥有了一个神奇的检查员，在你在放下下一个积木之前，就会根据物理定律检查每一个积木的放置位置。如果你试图在一个需要“协和”积木（和谐的音符）的地方放置一个“不协和”积木（冲突的音符），计算机不仅会说“哎呀”，它还会阻止你并说：“此证明不完整。”

作者利用这一点来解决对位法（counterpoint）——一种将两个或多个旋律编织在一起的古老艺术。他们编写了一套严格的规则用于“第一类对位法”（一种特定的、适合初学者的旋律编织风格）。他们不仅仅是编写代码来制作音乐；他们编写代码来证明他们所创作的音乐遵循了规则。这就像是在写一个故事，其中的情节漏洞在数学上是不可能存在的。

“时空旅行”时钟

音乐发生在时间之中，而 Prismriver 有一种巧妙的处理方式。它没有通过计算从宇宙开始的每一个节拍（这会变得非常混乱）来计数，而是使用了一个“小节与偏移量”（bar and offset）系统。这就像一张地铁地图：你知道自己在哪一个站（小节），以及距离站台有多远（偏移量）。这使得移动整首歌的前后变得极其容易，而无需重新计算每一秒。它还允许“负偏移量”，这就像是音乐中的“前奏音”（pickup note），可以在正式下拍之前开始，这是作曲家们非常喜欢的技巧。

“乐高”语言

为了让它更易于上手，Prismriver 包含了一种看起来非常像 LilyPond（一种基于文本的记谱方式）的特殊语言。你可以输入类似 c'4（特定八度的一个 C 音）的内容，计算机能立即理解。但关键在于：Prismriver 可以获取你的文本，检查你的数学逻辑，然后将结果导出为一种通用的文件格式，即 MusicXML。这意味着你可以在这种高科技数学语言中作曲，证明它的完美性，然后将其导入到标准的音乐软件（如 MuseScore 或 LilyPond）中，在真实的乐器上演奏。这就像是在电子游戏中建造一艘宇宙飞船，证明其引擎工作正常，然后将蓝图导出到真实的工厂进行生产。

它“不是”什么（以及它目前还做不到什么）

了解 Prismriver 不是什么非常重要，这样我们才不会抱有过高的期望。

它不是神奇的歌曲生成器： 论文并未声称 Prismriver 能自动创作热门歌曲。它是一个用于算法作曲的工具，这意味着它帮助你编写歌曲的规则，但你（或你设计的特定算法）仍需决定旋律。
它目前还不具备视觉功能： 虽然它可以播放音乐，但论文明确指出，生成与音乐配套的视觉艺术属于“未来的研究工作”。所以，目前还没有跳舞的激光灯。
它并不局限于西方音乐： 虽然它能完美处理西方古典音乐，但作者谨慎地表示，它被设计得足够灵活，可以处理“异律音阶”（xenharmonic，非标准音阶），例如以“三度音”（tritave，即 3:1 的频率比）而非八度作为主要重复间隔的 Bohlen-Pierce 音阶。

核心结论

Prismriver 是一个形式化库（formalization library）。这是一个高级说法，意指它是一个经过验证的音乐数学工具集。作者已成功证明了传统的“二面体群”（dihedral group）数学（一种描述和弦旋转和翻转的复杂方式）在标准的十二平均律音乐中运行完美，并将其推广到了你可以想象的任何调律系统。

他们并没有解决“什么是美妙的歌曲”这个谜题，但他们建立了一个音乐理论的证明检查器。如果你想创作一首确保每一个音符都从数学上保证遵循对位法规则的歌曲，Prismriver 是第一个真正能说“是的，我已经检查过数学，这首歌是有效的”工具。它将音乐创作从一场“猜测与尝试”的游戏转变为一场“经过验证的逻辑”游戏，为未来计算机辅助创作不仅能被听到、而且能被“证明”的音乐打开了大门。

技术摘要：Prismriver

问题陈述

音乐理论受一套丰富的数学规则和对称性支配，这些规则可以用精确的数学语言来表达。然而，传统的数学音乐理论依赖于自然语言证明，这容易受到人为错误的影响，缺乏机械验证，并且无法在计算语境中复用研究结果。虽然现有的音乐理论形式化工作已经存在，但其中许多局限于特定的调律系统（如十二平均律），或者缺乏在统一框架内进行算法作曲与分析的能力。因此，需要一种能够支持任意调律系统、允许对音乐属性进行机器验证证明，并将这些证明与算法作曲及输入/输出功能集成的形式化方法。

方法论

作者提出了 Prismriver，这是一个基于 Lean 4 构建的音乐理论与算法作曲形式化库。Lean 既是函数式编程语言，也是交互式定理证明器，这使得该库能够定义音乐结构、证明关于它们的定理并生成音乐。

核心表示

抽象音阶与调律：
- Prismriver 将 PseudoScale（伪音阶）定义为一种没有限制的泛型音高类型 $P$ ，从而允许表示如实数频率等形式。
- Scale（音阶）被定义为一个配备了音程类型 $I$ 的音高类型 $P$ ，其中 $I$ 构成一个作用于 $P$ 上的阿贝尔加法群（即一个 $I$ -torsor）。这将音级（pitch classes）的概念推广到了超越标准十二音体系的范畴。
- 异质音律（Xenharmonic）支持： 该库容纳了非平均律调律、四分音（quartertones）以及具有非八度基本音程的音阶（例如具有三度音程 Tritave 的 Bohlen-Pierce 音阶）。它区分了增音/减音性质不同的音高（例如在十二平均律中声学等价的 $C\sharp$ 与 $D\flat$ ），这对于分析像五度相生律（Pythagorean tuning）这样的非平均律系统至关重要。
时间与音符：
- 时间被建模为一个有序阿贝尔加法群 $T$ 。
- 一个音符被定义为一个对 $(P, T)$ ，由一个音高和一个时长组成。
- 实现了一个 MeasuredTime 类型，它是整数（小节数）与有理数（小节内偏移量）的乘积，便于在不重新计算总拍数的情况下进行抢拍（pickups）和移位音乐的分析。
移调动作与二面体群：
- 该库推广了移调（transposition）和转位（inversion）的概念。它定义了一个 TransposeAction（移调动作），包括作用于任意音阶上的平移（ $r_i$ ）和反射（ $sr_{a,i}$ ）操作。
- 作者证明了在十二平均律下，这些广义的移调动作等价于二面体群 $D_{12}$ 在三和弦上的作用。这弥合了抽象群论与现有文献中特定西方音乐理论模型（如 [19]）之间的差距。
单子化作曲（Monadic Composition）：
- 算法作曲通过 CompositionT 单子进行处理。该单子追踪一个“当前时间”游标，并提供移动游标、添加事件（发音/表情）以及添加音符的原语。
- Score.foldlM 单子允许通过对正在进行的事件列表进行折叠来分析乐谱。
- 这些单子结构使得使用 Lean 的 LawfulMonad 类来验证作曲算法（例如，证明生成的对位法符合特定规则）成为可能。
输入/输出：
- DSL： 一个类 LilyPond 的领域特定语言（DSL）允许用户使用文本语法输入音乐。该 DSL 使用固定音高记谱而非相对记谱，以降低波动性。
- 导出： 乐谱被导出为 MusicXML（时间维度格式，并转换为分谱格式，以兼容 LilyPond 和 MuseScore 等工具）。
- 播放： #play 指令用于展开表达式并启动一个 Alda 进程进行交互式播放。

核心贡献

音乐理论的形式化： 一个在 Lean 4 中形式化了音高、变音记号、音阶、和弦、时长及声部的综合库。
广义调律兼容性： 支持异质音律音阶，包括非平均律调律系统以及具有非八度基本音程的音阶，超越了十二平均律的限制。
可证明的归约： 一个形式化证明，证明了在十二平均律下，广义移调动作等价于三和弦上的 $D_{12}$ 二面体群作用。
单子化算法作曲： 一个使用单子原语进行作曲与分析的框架，允许验证作曲算法（例如第一类对位法）。
互操作性： 集成了用于音乐输入的自定义 DSL 以及用于兼容外部音乐软件的 MusicXML 导出功能，同时支持通过 Alda 进行直接播放。

结果与实现

论文通过以下几种实现展示了 Prismriver 的效用：

对位作曲： 作者实现了一个**第一类对位法（first species counterpoint）**规则的子集。他们定义了关于和声与旋律音程、协和度以及特定约束（例如，无三全音转折点）的谓词。利用这些谓词，他们以程序化方式构建了对位法，并证明了生成的作品满足第一类对位法的规则。
和弦进行分析： 该库被用于从移调动作和和弦转位的角度分析帕赫贝尔《D大调卡农》的和弦进行，验证了广义二面体作用模型。
代码示例： 论文包含了显示音程定义、二面体群作用于三和弦的实现，以及使用作曲单子生成一段旋律（基于《Necrofantasia》）的代码片段。

意义

论文声称 Prismriver 为可验证的算法作曲与伴奏生成开启了大门。通过在证明辅助器中形式化音乐理论，作者实现了：

机械验证： 音乐证明中的错误可以被计算机检测到，消除了手工证明的低效性。
可重用性： 结果和原语可以在未来的证明和作曲中进行机械化的重用。
灵活性： 该库允许用户定义自定义调律系统和音乐原语，促进了一个不断增长且可重用的音乐形式化库的发展。
集成： 它架起了理论音乐分析与实际作曲工具之间的桥梁，使得生成可由标准软件播放的 MusicXML 成为可能。

作者将 Prismriver 定位为超越现有工具（如缺乏广义调律原语的 Lulu，以及受限于特定类型系统编码或调律系统的 HarmTrace 或 Mezzo）的一步。通过利用 Lean 的表达能力，Prismriver 提供了一个既能进行证明又能执行音乐理论的通用环境。