Weighted Refinement Types for Counterpoint Composition
summary
Proposes weighted refinement types that attach a numeric weight to each predicate (use -∞ for forbidden rules) and implements a type system for first‑species counterpoint where a melody is a nonempty list of pitch/interval pairs, bar rules yield W1, adjacency rules yield W2, and total score is the sum; examples show minus‑infinity for dissonance/direct fifths and small penalties for chromatic or repeated notes, and the system successfully ranks correct > acceptable > broken.
AI-written summary · about
chapters (20)
- 0:00Weighted refinement types intro
- 2:29Weighted refinement types for music
- 3:11Species counterpoint basics
- 6:12Representing counterpoint with types
- 8:23Typing rules for correctness
- 9:49Evaluating counterpoint examples
- 11:15Future work in counterpoint
- 12:43Conclusion from music
- 13:50Q&A
- 14:11Counterpoint rules questions
- 15:17Benefits of weighted types
- 16:19Global counterpoint rules
- 18:09Applying to other music styles
- 19:14Configuring weights
- 20:16Evaluating musical works
- 22:08Species complexity and scoring
- 23:52Elaborating weighting scheme
- 24:54Integration with software
- 26:20Realistic counterpoint rules
- 27:23Closing remarks