Demo: The Reduction of Girard’s Paradox as Music
summary
Translates the reduction behavior of Girard’s paradox into sound by extending Soundproof from single-term rendering to reduction-based translation, implemented in Rust + funddsp. The system reduces large lambda-pi terms (thousands–tens of thousands of nodes), maps nodes to 4,096 frequency buckets (64 for live), and chooses call-by-name stepping with even frequency division and time scaled to change size. Multithreaded translation and bucketing make long-running reductions audible and feasible in live performance.
AI-written summary · about
chapters (12)
- 0:00Translating Girard’s Paradox into music
- 1:55Choosing a paradox for structure
- 3:00Girard’s Paradox in dependent type theory
- 5:10Soundproof: translating proofs into music
- 6:56Mapping proofs to sound trees
- 9:05Melody-based approach limitations
- 11:37Redesigning for paradoxical growth
- 14:04Frequency and time division choices
- 16:33Evaluating variations with combinatorial testing
- 17:56Final aesthetic and technical balance
- 19:42Performance challenges and optimization
- 21:52Live setup and real-time rendering
related talks
43mThe Butcherbird Combinator
01h 02mprogrammingLanguage as Language;
18mMachines that Judge Us
27mScheme Pearl: Quantum Continuations
13mFabObscura: Computational Design and Fabrication for Interactive Barrier-Grid Animations
37mRendering performance inside out
26mPrincipled algorithm, data structure and system design for Processing-in-Memory (PIM)”
05mLive Voice Transformations For Web Conferencing Using The Browser