Não é bem assim: exploração de sistemas para verificar a precisão musical

Introdução

Tenho falado muito sobre a representação da música por meio de linguagens de programação. É um assunto popular, porque estimula a curiosidade mecânica do engenheiro, além de conectar-se com o universo musical.

E como funciona? Existem ambientes de codificação musical para diversas linguagens de programação. Duas das mais populares são o TidalCycles para Haskell e o Sonic Pi para Ruby no Raspberry Pi. Abaixo, mostro um exemplo usando a biblioteca de composição de Leipzig desenvolvido por mim. Como está escrito em Clojure, não há verificação de tipo.

(def row-row-row-your-boat
  (phrase [3/3 3/3 2/3 1/3 3/3]
          [  0   0   0   1   2]))

->> row-row-row-your-boat
  (canon (simple 4))
  (where :pitch (comp C major))
  (where :time (bpm 90))
  play)

Durações e afinações são representadas como literais de número inteiros e razões, o que pode ser um pouco complicado. A programação realmente desponta quando se trata de transformações musicais, como no exemplo acima, onde o fragmento original da melodia recebe um acompanhamento, sendo colocado na chave de Dó maior com um ritmo de 90 batidas por minuto.

Uma vez que os programadores veem o código musical, uma das reações mais comuns é perguntar se é possível usar sistemas de tipos para evitar músicas ruins. Este é um pensamento natural. Se a música pode ser vista como código, os erros musicais podem, de alguma forma, ser como erros de programação? E se esse for o caso, talvez possamos aplicar as técnicas que usamos na criação de programas para melhorar a forma como escrevemos músicas.

Em particular, há uma analogia óbvia entre o tipo de erro dos sistemas e os exemplos mais comuns de incoerência musical. Se a linguagem de programação puder garantir que não passe uma String para uma função que espera um Intenger, ela deve ser capaz de verificar se não executamos um F# em uma peça escrita em C maior, um campo harmônico sem acidentes.

Neste artigo, discutirei o que torna a música precisa e como podemos codificá-la em um sistema de tipos.

Prescritivismo

Há séculos os teóricos da música são fascinados pelo que faz a música ser precisa. Durante a maior parte desse tempo, operaram através de um quadro de prescritivismo musical, ou seja, avaliando a música quanto à conformidade com um conjunto de regras.

A metodologia historicamente dominante para chegar a essas regras pode ser resumida da seguinte forma:

• Examine o canon
• Extraia regularidades
• Formule-as como conjuntos de regras

Em seguida, podemos fazer a seguinte reivindicação:

Músicas que derivam destas regras estão corretas.

Por exemplo, uma regra de composição é que uma melodia saltando da sétima maior de um C até um B não é permitida. Essa abordagem produziu muitas informações valiosas. Existem regularidades genuinamente interessantes na música clássica, e generalizar nossas observações como conjuntos de regras nos ajuda a discutir fenômenos musicais.

Além disso, a adesão às regras não é uma má idéia para os alunos que aprendem o ofício. Fico feliz que as crianças que aprendem violino pratiquem a escala C e sempre que tocam um F#, o professor diz que cometeu um erro. Certamente existem contextos em que as noções prescritivas de música correta e incorreta são úteis.

No entanto, existem duas grandes falhas dessa maneira de definir o acerto musical.

Primeiro, as regras produzidas por esse processo são fortemente dependentes de qual música o teórico considera como canon. Um conjunto de dados tendencioso leva a inferências tendenciosas e a música clássica ocidental não é representativa da experiência musical da humanidade. Inferir regras baseadas na música de Bach e Mozart pode ser fascinante, mas não diz muito sobre música em geral.

Isso se torna especialmente complicado quando percebemos que os gêneros musicais geralmente estão fortemente associados a culturas e etnias específicas e que, ao priorizar um certo tipo de música, também priorizamos inadvertidamente um determinado tipo de pessoa. Em particular, a teoria musical acadêmica deve muito ao estudo da tradição euro clássica e prestou relativamente pouca atenção à música derivada da diáspora africana como blues, jazz, rock 'n' roll e hip hop. Confiar na teoria musical tradicional como fonte de correção pode levar a uma versão cultural do mesmo problema que levou os algoritmos de reconhecimento facial a funcionarem melhor para rostos brancos do que negros.

A segunda grande falha na construção de regras, extraindo e generalizando as regularidades existentes, é que ela é retrospectiva. A música é mais emocionante quando quebra as regras. Antes de Jimmy Page usar a distorção para efeito artístico, os engenheiros consideraram o corte do sinal durante a amplificação um defeito. Portanto, mesmo que as regularidades observadas sejam uma maneira útil de entender a música de hoje, elas são uma maneira terrível de julgar a música de amanhã.

Um bom sistema de tipos de música deve evitar as duas armadilhas do prescritivismo. Não deve se basear em noções inadequadas ou tendenciosas de que música está correta. Mas, mais sutilmente, na tentativa de tornar estados inválidos irrepresentáveis, e não deve impossibilitar estados inovadores.

Descritivismo

A alternativa ao prescritivismo é o descritivismo. Enquanto o prescritivismo vê as regularidades musicais como leis a serem seguidas, o descritivismo as vê como padrões emergentes da prática real. Uma maneira descritivista de descobrir regras musicais pode ser algo como:

• Examinar um corpo de música;
• Extrair as tendências;
• Formulá-las como um modelo.

Em seguida, podemos afirmar o seguinte:

Músicas que se desviam do modelo, são incomuns.

Para fazer isso, precisamos de um bom modelo para estruturas musicais que possam representar o que é comum e incomum, e não apenas o que é certo ou errado. Uma abordagem útil é a adotada por David Huron no livro Sweet Anticipation. Huron apresenta uma teoria descritivista que, para os fins deste artigo, pode ser resumida em três axiomas principais:

1. A música é apreciada através da aprendizagem estatística;
2. A previsão precisa é encantadora.
3. A novidade evita que fiquemos entediados.

No exemplo prescritivista anterior, saltar de um C para um B é considerado ilegal, mas na teoria de Huron seria considerado altamente incomum. As pessoas que ouviram muita música ocidental aprenderiam que quando ouvem um C, é provável que a próxima nota seja outro C, uma nota mais baixa ou uma nota mais alta. O efeito de pular para o B mais alto surpreenderia os ouvintes, que poderiam interpretar negativamente.

Uma das consequências fascinantes da teoria de Huron é que compor música não é um exercício para maximizar nem minimizar a invenção. Em vez disso, a música dança entre a ordem e o caos, e a apreciação do público depende da capacidade do músico de equilibrar o choque do novo com a satisfação do esperado. Se realmente desejamos verificar a coerência de uma composição, precisamos nos certificar de que a música não fique muito longe da convenção, mas também não muito perto.

A tabela a seguir é uma análise estatística das tendências melódicas. Quadrados mais escuros representam resultados mais prováveis. A maneira de ler o quadro é escolher uma nota no eixo vertical e depois descobrir a probabilidade de que a nota escolhida seja seguida por cada nota no eixo horizontal. Por exemplo, 33,53% do tempo neste conjunto de dados, um "Re" é seguido por um "Do".

[Click na imagem para ampliá-la]

Os dados são adaptados das figuras do livro de Huron e baseiam-se em uma análise de mais de 250.000 pares de tons de músicas folclóricas alemãs no tom principal. Um corpus diferente, por exemplo, hip hop ou rock'n roll, produziria probabilidades diferentes.

Essas probabilidades podem ser representadas de maneira equivalente como bits de entropia, onde uma chance de 50% corresponde a um bit de entropia e uma chance de 25% corresponde a dois bits, etc. Para evitar a divisão por zero, modelei transições que nunca ocorrem no conjunto de dados como tendo uma chance de 1/100.000. Desta vez, os quadrados mais escuros representam transições mais raras em termos de entropia ou, em outras palavras, que se espera que ocorram com menos frequência. Por exemplo, um "Ré" seguido de um "Lá" corresponde a aproximadamente seis bits de entropia, ou uma chance de 1/64.

[Click na imagem para ampliá-la]

A representação da entropia torna mais natural agregar a surpresa de uma série de notas, onde cada transição de um tom para o outro recebe uma contagem de entropia e a surpresa da melodia como um todo soma cada transição.

Do -> Re -> Mi -> Fa = 2.20 + 2.71 + 5.94 = 10.85 bits
Do -> Ti -> Mi -> Fa = 2.48 + 7.43 + 5.94 = 15.85 bits

Essa é uma abordagem muito semelhante a um modelo oculto de Markov, mas em vez de gerar sequências de notas, usamos as probabilidades ponderadas para medir a ocorrência de uma determinada melodia.

Podemos notar que a transição de "Dó" para "Si" é de apenas 2,48 bits, o que parece contradizer minha afirmação anterior de que um salto de C para B é altamente incomum. Transições incomuns normalmente teriam cerca de 10 bits de entropia. A razão para essa inconsistência é que os dados de Huron não distinguem entre saltar seis notas de "Dó" para "Si" (muito incomum) e descer uma nota de "Dó" para um "Si" mais baixo (bastante comum). Se nossos dados nos permitissem separar os dois casos, nosso modelo mostraria "Dó", "Si", "Mi", "Fá" como ainda mais improvável em comparação com o comum, "Do", "Re", "Mi", "Fa".

Notas tipificadas

Na melhor das hipóteses, os sistemas de tipos oferecem suporte aos programadores, orientando-os para decisões de codificação válidas e eliminando a possibilidade de erros. Um bom exemplo análogo ao musical é o solfège. Mesmo se nunca tivemos educação formal musical, provavelmente já conhecemos a música Dó-Ré-Mi do musical The Sound of Music. Cada nota da oitava recebe seu próprio nome e qualquer nota fora do campo harmônico não tem um nome:

1. Dó (A nota mais baixa da escala)
2. Ré
3. Mi
4. Fá
5. Sol
6. Lá
7. Si
8. Dó (Desta vez uma oitava acima)

Este sistema orienta os músicos para as notas corretas, definindo um mini idioma que impossibilita a expressão de notas fora da escala escolhida. Existem infinitas frequências entre "Dó" e "Ré", mas, em solfège, são inexistentes.

Isso pode ser facilmente expresso em um código com um tipo de dados algébrico:

 data Sollfege = Do | Re | Mi | Fa | Sol | La | Si 

Isso nos permite definir funções musicais em que não há a possibilidade de notas fora da escala, por exemplo, essa que repete a mesma nota n vezes:

repeat : Nat -> Solfege -> List Solfege
repeat 0 s = [s]
repeat n s = s :: repeat (n - 1) s

Com essa definição, repeat 3 Re é uma expressão que pode ser facilmente entendida no domínio musical, enquanto repeat 3 F# é um erro de verificação de tipo, porque F# não é um valor do tipo Solfege.

Isso nos dá um certo grau de segurança na tipificação. Nosso sistema de tipos pode nos ajudar a evitar notas inválidas, mas ainda não pode nos proteger de combinações inválidas. Se estivermos tocando uma escala de C maior, nunca tocaremos um F#, mas ainda assim podemos tocar um C, depois saltaremos um sétimo maior para um B, o que é proibido pelas regras de composição convencionais. Esse tipo de verificação de tipo contextual é possível, mas requer uma abordagem mais sofisticada.

Transições tipificadas

Mezzo, uma biblioteca Haskell de Dima Samoz, usa tipos dependentes para verificar se a música está precisa. O README do Mezzo o descreve como um "verificador ortográfico musical muito rigoroso" e pode verificar uma variedade de regras de composição além da simples segurança de notas. Em Mezzo, isso é compilado porque a melodia C, D, E, F é composta por intervalos legais:

comp = defScore $ start $ melody :| c :| d :| e :| f :>> g

No entanto, quando violamos a regra de saltar de C para B, Mezzo intervém. O código a seguir não é compilado:

comp = defScore $ start $ melody :| c :| b :| e :| f :>> g

Em uma conquista notável, Mezzo é até mesmo capaz de identificar o problema:

Major sevenths are not permitted in melody: C and B
In the first argument of ‘(:|)’, namely ‘melody :| c :| b’
In the first argument of ‘(:|)’, namely ‘melody :| c :| b :| e’
In the first argument of ‘(:>>)’, namely
    ‘melody :| c :| b :| e :| f_’

Isso pode parecer a realização de um sonho de tornar a música imprecisa em um erro de tipo, mas ainda existem problemas ocasionais. Quando Samoz codificou o Prelude de Chopin no Mezzo, descobriu que em algumas ocasiões o compositor não seguiu as regras convencionais:

"A peça pode ser quase totalmente transcrita, no entanto, ocasionalmente, precisava deixar algumas notas de fora, pois criavam intervalos proibidos, apontados pelo Mezzo."

Podemos perguntar quem está fazendo a proibição aqui. Se Chopin não tem permissão para dizer o que é e o que não é permitido na música clássica ocidental, a quem é permitido?

O problema aqui é que, embora o Mezzo possa levar em consideração o contexto, um julgamento de tipo ainda é uma opção binária. As notas estão todas corretas e a peça é compilada, ou uma nota está deslocada e a peça não é compilada. Portanto, enquanto o Mezzo fornece controle sobre quais regras de composição estão ativas, a decisão de usar ou não uma regra é global. Se desativarmos uma regra porque possui um efeito artístico específico que quebra as convenções comuns, abandonamos a verificação de outras partes da composição.

Entropia tipificada

Uma maneira de modelar a quebra ou flexão de regras musicais em tipos é seguir o Huron e modelar as mudanças entre as notas em termos de probabilidade. Em vez de uma certa transição ser permitida ou não, a combinação pode receber uma pontuação de entropia que representa o quão surpreendente esse par de notas seria para um ouvinte.

O código a seguir foi escrito na linguagem de programação funcional de tipo dependente Idris. Ele confirma que conventional é uma melodia que começa em "Dó" e termina em "Si", e que o caminho percorrido entre essas notas gera entre 8 e 16 bits de entropia. Primeiro, precisamos definir um tipo de melodia que capture a noção com um certo valor de probabilidade ou entropia. Este tipo possui três construtores:

• Pure, que representa a criação de uma melodia de uma única nota com uma entropia superior e inferior vinculada a zero.
• (>>=), que representa compor duas melodias adicionando os limites de entropia juntamente com o valor de transição da nota no final da primeira melodia para a nota no início da segunda.
• Relax,que representa tomar uma melodia e relaxar os limites de entropia.

data Melody : (Solfege, Solfege) -> (Nat, Nat) -> Type where

  Pure  : x -> Melody (x, x) (0, 0)

  (>>=) : Melody (w, x) (low, high) ->
          (() -> Melody (y, z) (low2, high2)) ->
          Melody (w, z) (cost x y + low + low2, cost x y + high + high2)

  Relax : Melody (x, y) (low + dl, high) ->
          Melody (x, y) (low, high + dh)

Essa definição de tipo é um pouco complicada, mas uma vez que a tenhamos, podemos usar a notação do do Idris para sequenciar uma melodia e o compilador do Idris rastreará os limites da entropia. Aqui está uma melodia convencional, onde todas as transições têm baixo custo:

conventional : Melody (Do, So) (8, 16)
conventional = Relax $ do
  Pure Do
  Pure Re
  Pure Mi
  Pure Fa
  Pure So

dia não é convencional porque salta na sétima maior, que em Mezzo teria que ser proibida ou a regra desativada completamente. Aqui, apenas expandimos os limites de complexidade da melodia para ter entre 8 e 24 bits de entropia:

unconventional : Melody (Do, So) (8, 24)
unconventional = Relax $ do
  Pure Do
  Pure Ti
  Pure Mi
  Pure Fa
  Pure So

Se em vez de Melody (Do, So) (8, 24) tivéssemos atribuído à melodia não convencional o tipo Melody (Do, So) (8, 16), ela não teria sido compilada!

A novidade dessa abordagem é que também captura músicas que são muito chatas. Se a entropia da melodia for insuficiente para atender ao limite inferior, será gerado um erro de tipo. Portanto, se a melodia convencional tivesse recebido o tipo Melody (Do, So) (16, 24), também não seria compilada, pois a entropia dessa melodia cai abaixo do limite inferior. Isso nos permite ser fiéis à percepção de Huron de que os ouvintes têm dificuldade em ouvir música que é muito surpreendente ou muito previsível.

No caso de usar essa abordagem, as transições para outras notas na escala recebem um valor de entropia igual a zero e as transições para as notas fora da escala recebem um valor de entropia arbitrariamente grande. Nesse caso, recuperamos efetivamente a abordagem de julgamento do tipo binário, em que uma nota é legal ou ilegal, sem uma área de meio termo.

Importante mas difícil de verificar

A verificação de tipo de música é algo complexo porque é difícil definir o que é uma música precisa. Se não podemos modelar nossa noção de correção musical de maneira precisa e matemática, não podemos codificá-la em um sistema de tipos. Mesmo se formos capazes de formalizar o entendimento de maneira autêntica, é preciso algum esforço combinado com sistemas de tipos poderosos para chegar ao ponto em que o compilador é um juiz adequado da composição. No entanto, com algumas determinações e algumas suposições simplificadoras, é possível.

Isso é apenas uma curiosidade? Possivelmente. É improvável que a indústria da música empregue sistemas de tipos a qualquer momento, como forma de evitar erros de composição. Mas explorar o aspecto computacional da música pode nos dar uma nova maneira de apreciar algo que tem tanto significado na vida de quase todo mundo, então isso justifica o empreendimento.

Mas talvez igualmente importante, a música é apenas um domínio em que a exatidão é importante e difícil de ser verificada. Quanto mais a programação é usada para automatizar domínios sociais e culturais, mais frequentemente ocorrem situações em que uma resposta é difícil de ser avaliada, porém tem uma importância crucial para o ser humano. Considere usar um programa de computador para decidir quanto tempo manter uma pessoa na prisão. A correção de uma decisão de sentença envolve uma compensação complexa de valores e probabilidades, e se não podemos seguir o raciocínio do sistema, como sabemos que o resultado foi justo?

Sempre que automatizamos o raciocínio difuso, precisamos nos perguntar: Como sabemos que esse sistema está correto?

Sobre o autor

Chris Ford começou a fazer música com códigos para compensar sua falta de técnica no piano. Somente mais tarde percebeu que a programação oferece uma visão profunda das estruturas musicais. Nos últimos anos, Chris palestrou muitas vezes apresentando teoria musical ao público de programação, cobrindo tópicos que incluem música clássica européia, teoria da complexidade, jazz, polirritmos da África Central e sistemas de afinação. É o chefe de tecnologia da ThoughtWorks Spain e vive e trabalha em Barcelona.