Girard's Paradox as Structure Music
summary
A system called Soundproof converts a Girard paradox proof term from lambda pi (bidirectional, de Bruijn indices) into a hierarchical call tree that maps node variants to short melodies, rendered with the Rust library fundsp. Time is split by fractional-weighting and depth is scaled (depths reach ~20), producing a 40‑minute synthesized piece that makes the paradox’s circular structure audible. Output is coherent but non‑normalizing; reduction dynamics are not yet implemented and remain future work.
AI-written summary · about
chapters (12)
- 0:00Structure music introduction
- 1:03Paradoxes as concept art
- 2:51Girard's Paradox in type theory
- 4:17Encoding in Soundproof
- 6:23Proof terms to sound trees
- 8:56Proof structures to music
- 12:17Time and depth scaling
- 14:01Sounds for proof nodes
- 15:46Context-aware sound selectors
- 17:14Normalized vs annotated terms
- 18:54Future work
- 19:18Q&A
related talks
32mScala, Sound, and Structure - Composing Music through FP
42mKolmogorov music
21mPrismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4
42mAfrican Polyphony & Polyrhythm
43mThe Butcherbird Combinator
25mDemo: A Geometric Approach to Generate Musical Rhythmic Patterns in Haskell
42mSounds of Structure - Music Modelling with ADT's
16mDemo: Functional Sound Design