Prismriver
A Music formalization library and DSL in Lean 4 for:
- Formalization of music theory including pitches, accidentals, scales, chords, durations, parts
- Algorithmic analysis (e.g. key estimation) and composition (counterpoint)
- Mathematical modeling of music
- Lilypond compatible music syntax
Structure
Tuning and Scale
Scales are handled in Scale.lean and
Classical.lean. We do not distinguish between
tuning systems and scales. A PseudoScale is a list of pitches. A Scale is a
list of pitches with a fundamental interval. This flexibility handles
xenharmonic tuning systems that are not based on Western music theory. Equal
temperament is a scale. A Tuning system maps one scale to another. For
example, under the equal temperament tuning system, C♯ and D♭ are enharmonic.
Classical.lean handles Western Classical
music. Each pitch is the combination of a name (Hep), an accidental, and an
octave, with the octave being the fundamental interval. An interval has a letter
distance and a semitone distance. We can transpose a note using arithmetic
operations + and -. In some sense, the intervals form a group action on
pitches. This also recalls properties of affine spaces.
Whether an interval is consonant or dissonant is dependent on the physical
properties of the instrument and this varies across cultures, and hence the
choice of consonant intervals is left as free parameters in composition
algorithms. We still provide convenient shortcuts such as p5 or ma6 for
intervals.
Time
We handle time, the other axis of music, in
Time.lean. To allow arbitrary musical sequences,
the most general form of time only consists of an instance type I and a
duration type D. MeasuredTime is a representation based on bars and rational
offsets. This abstraction is out of consideration of flexibility. The time as
written on paper may not exactly match the time of performance.
Composition and Analysis
Score contains an implementation of music scores. Each score is a list of ordered events along time instances.
In Composition, we implemented algorithmic composition of counterpoints.
Syntax and Playback
A LilyPond-like DSL is provided in Syntax.lean.
Prismriver supports playback using Alda. Alda is optional, but it is necessary for playing music.
This command plays the first 5 notes of Necrofantasia
import Prismriver
#play ♩[e4 c'4 b4 d4 e2]
Contributing
Every commit must pass through pre-commit hooks. Install prek (provided in
shell.nix), and run
prek install
See roadmap (need to be compiled with Typst).
Contributors and Acknowledgments
References