Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Type Theory for the Working Mathematical Music Theorist

Drew Flieder

TL;DR

The work identifies a gap in mathemusical reasoning caused by heavy categorical encodings and introduces a type-theoretic symbolic language that preserves semantic rigor via categorical semantics. It develops signatures, typing judgments, and higher-order constructs, then connects these syntactic tools to topos-based semantics and internal language concepts. The framework is then applied to voice-leading spaces, showing how to specify their type, semantics, and transformations within a unified language, including both group-action and homotopy-based interpretations. This approach promises greater conceptual transparency and flexibility for modeling musically meaningful structures while remaining faithful to formal foundations, with broad potential for future theory-building in mathematical music theory.

Abstract

Many formal languages of contemporary mathematical music theory -- particularly those employing category theory -- are powerful but cumbersome: ideas that are conceptually simple frequently require expression through elaborate categorical constructions such as functor categories. This paper proposes a remedy in the form of a type-theoretic symbolic language that enables mathematical music theorists to build and reason about musical structures more intuitively, without relinquishing the rigor of their categorical foundations. Type theory provides a syntax in which elements, functions, and relations can be expressed in simple terms, while categorical semantics supplies their mathemusical interpretation. Within this system, reasoning itself becomes constructive: propositions and proofs are treated as objects, yielding a framework in which the formation of structures and the reasoning about them take place within the same mathematical language. The result is a concise and flexible formalism that restores conceptual transparency to mathemusical thought and supports new applications, illustrated here through the theory of voice-leading spaces.

Type Theory for the Working Mathematical Music Theorist

TL;DR

The work identifies a gap in mathemusical reasoning caused by heavy categorical encodings and introduces a type-theoretic symbolic language that preserves semantic rigor via categorical semantics. It develops signatures, typing judgments, and higher-order constructs, then connects these syntactic tools to topos-based semantics and internal language concepts. The framework is then applied to voice-leading spaces, showing how to specify their type, semantics, and transformations within a unified language, including both group-action and homotopy-based interpretations. This approach promises greater conceptual transparency and flexibility for modeling musically meaningful structures while remaining faithful to formal foundations, with broad potential for future theory-building in mathematical music theory.

Abstract

Many formal languages of contemporary mathematical music theory -- particularly those employing category theory -- are powerful but cumbersome: ideas that are conceptually simple frequently require expression through elaborate categorical constructions such as functor categories. This paper proposes a remedy in the form of a type-theoretic symbolic language that enables mathematical music theorists to build and reason about musical structures more intuitively, without relinquishing the rigor of their categorical foundations. Type theory provides a syntax in which elements, functions, and relations can be expressed in simple terms, while categorical semantics supplies their mathemusical interpretation. Within this system, reasoning itself becomes constructive: propositions and proofs are treated as objects, yielding a framework in which the formation of structures and the reasoning about them take place within the same mathematical language. The result is a concise and flexible formalism that restores conceptual transparency to mathemusical thought and supports new applications, illustrated here through the theory of voice-leading spaces.

Paper Structure

This paper contains 55 sections, 2 theorems, 181 equations, 2 figures.

Table of Contents

  1. Introduction and Motivation
  2. A Symbolic Lingua Franca for Mathematical Music Theorists
  3. Reasoning as Constructive
  4. Structure of the Paper
  5. The Type-Theoretic Machinery
  6. Signatures
  7. Terms, Contexts, and Typing Judgments
  8. Terms
  9. Contexts
  10. Typing Judgments
  11. The Classifying Category of a Signature
  12. Musical Examples of Typing Judgments
  13. Typing Judgments for Data Types
  14. Typing Judgments for Propositions
  15. Type Constructors
  16. ...and 40 more sections

Key Result

Proposition 4.1

For a category $\Sigma_\mathsf{VLS}\text{-}\mathbf{Str}(\mathcal{E})$ of $\Sigma_\mathsf{VLS}$-structures, an objective transformation of a voice-leading space is induced by an automorphism $h : M \to N$ in $\Sigma_\mathsf{VLS}\text{-}\mathbf{Str}(\mathcal{E})$.

Figures (2)

  • Figure 1: The inductive structure of the list $[a, b, c]$ represented as nested $\mathsf{sup}$-applications, where each subtree corresponds to the tail of the list above it.
  • Figure 2: A rhythm tree with root duration $9.5$ subdivided into proportional branches. Each branching node represents a rational proportional factor, which may itself branch further.

Theorems & Definitions (28)

  • Definition 2.1: Signature
  • Example 2.1: Signature of a group
  • Definition 2.2: Classifying Category
  • Example 2.2: Constructing intervals
  • Example 2.3: Building chords
  • Example 2.4: Scale membership
  • Example 2.5: Functional harmony
  • Example 2.6: Dominance depends on context
  • Example 2.7: MIDI note
  • Example 2.8: Pitch or rest
  • ...and 18 more