Demo Counterpoint Analysis and Synthesis
summary
An Agda library encodes first‑species counterpoint as high‑level constraints compiled to a tiny expression language and solved via an SMT backend (SBV via a Haskell FFI). It analyzes Beethoven exercises, flags consonance and motion violations, reproduces Haydn’s correction by changing F5→A5, and synthesizes three missing notes (one solution uses B rather than A). Adding constraints to maximize independence yields six instances of contrary motion and one leap. The pipeline is Agda library → SMT solver and runs quickly.
AI-written summary · about
chapters (16)
- 0:00Start
- 1:24Rules of First Species Counterpoint
- 2:44Motion Rules
- 5:24Interface
- 7:50Motion Constraints
- 9:07Violations of Consonants
- 9:53First Species Constraints
- 10:50Overview
- 11:23Layers of Abstraction
- 11:42Intermediate Layer
- 12:23Symbolic Module
- 14:04Counterpoint Rules
- 15:07Low Level Expression Language
- 16:14Synthesis Using the Smt Solver
- 18:48Constraints
- 20:31Future Work
related talks
01h 33mComposition Intuition II
33mProgram Synthesis Using Example Propagation
51mThe Hills Are Alive With the Sound of Comonads
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
27mHaskell equations, thirty-eight years later
42mFunctional interpreters and you
34mThe Monoiad: an epic poem on monoids
27mA Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware