Qual é uma boa maneira de representar grupos livres?
É fácil representar magmas livres (árvores de folhas binárias), semigrupos gratuitos (listas não vazias) e monoides livres (listas), e não é difícil provar que eles realmente são o que afirmam ser. Mas grupos livres parecem muito mais complicados. Parece haver pelo menos duas abordagens para usar o método usualList (Either a)
representação:
Left a :: Right b :: ...
entãoNot (a = b)
e o contrário. Parece provável que seja um pouco difícil construí-los.Trabalhe sobre uma relação de equivalência que permita a inserção / exclusão arbitrária deLeft a :: Right a :: ...
pares (e vice-versa). Expressar essa relação parece terrivelmente complicado.Alguém tem uma ideia melhor?
EditarAcabei de perceber que a opção (1), que a única resposta usa, simplesmente não pode funcionar na configuração mais geral. Em particular, torna-se impossível definir a operação do grupo sem impor igualdade decidível!
Editar 2Eu deveria ter pensado no Google primeiro. Parece que Joachim Breitnerfiz isso na Agda alguns anos atrás, e a partir de sua descrição introdutória, parece que ele começou com a opção 1, mas finalmente escolheu a opção 2. Acho que vou tentar por conta própria e, se ficar muito travado, examinarei seu código.