Last is a free monoid?

Question

Os monóides livres são freqüentemente considerados como "monóides de lista". No entanto, estou interessado em outras estruturas possíveis que podem nos dar monóides livres .

Em primeiro lugar, examinemos a definição de monóides livres . Nunca entendi muito bem como é possível definir um monóide livre como uma estrutura que obedece às leis do monóide e nada mais. Como podemos provar que algo não obedece a regras, mas afirmado acima? Ou isso é apenas uma intuição?

De qualquer forma, vamos falar sobre functores. Se algum monóide é gratuito , nós o obtemos com um functor gratuito . É óbvio que uma lista é muito útil aqui:

free :: Set -> Mon
free a = ([a], (++), [])

No entanto, um pode surgir com vários outros. Por exemplo, aqui é um para Lastde Data.Monoid:

freeLast :: Set -> Mon
freeLast a = (Last a, (<>) :: Last a -> Last a -> Last a, Last Nothing) 

Então, este functor faz Lastum monóide livre ? De forma mais geral, se houver uma instância que cumpre a lei para Monoid (T a), é Tum monóide livre ?

Answer 1

Esta é uma maneira de entender um monóide livre: se alguém lhe der um valor, quanto você pode deduzir sobre como ele foi criado? Considere um monóide aditivo de números naturais. Eu te dou um 7 e pergunto como o consegui. Eu poderia ter adicionado 4 + 3, ou 3 + 4, ou 2 + 5, etc. Existem muitas possibilidades. Esta informação foi perdida. Se, por outro lado, eu der uma lista [4, 3], você sabe que foi criada a partir de singletons [4]e [3]. Exceto que talvez houvesse uma unidade []envolvida. Talvez fosse [4]<>[3]<>[]ou [4]<>[]<>[]<>[3]. Mas definitivamente não era [3]<>[4].

Com uma lista mais longa,, [1, 2, 3]você tem opções adicionais ([1]<>[2]) <> [3], ou [1] <> ([2]<>[3]), mais todas as inserções possíveis da lista vazia. Portanto, a informação que você perde segue as leis de unidade e associatividade, mas nada mais . Um valor monóide livre lembra como foi criado, as leis da unidade do módulo e a associatividade.

Answer 2

Por exemplo, vamos pegar números inteiros não negativos, ou seja 0,1,2,.... Quantos monoides podemos fazer?

Definindo mempty = 0e (<>) = (+). Você pode provar facilmente que este é um monóide.

Definindo mempty = 1e (<>) = (*). Novamente, este é um monóide (prove, é fácil)

Os dois monóides definidos acima são chamados de monóides aditivos e multiplicativos sobre os números naturais. Eles são diferentes na estrutura, por exemplo, o elemento 0no monóide multiplicativo, se comporta totalmente diferente de qualquer outro elemento no monóide aditivo, portanto, há algo interno aos números naturais, que torna esses monóides diferentes (mantenha esta afirmação até o próximo parágrafo )

Existe um terceiro monóide que podemos criar, vamos chamá-lo de monóide de concatenação .

Definindo mempty = no-actione (<>) = glue one integer beside the other.

Por exemplo, 3 <> mempty = 3e 3 <> 2 = 32. Observe que o fato de que os elementos são números naturais não é relevante aqui. Se em vez de Natural, tomarmos Racionais, ou quaisquer símbolos que você goste, o monóide seria exatamente a mesma coisa. (* Ler nota de rodapé) Portanto, não há nada interno no conjunto subjacente que torne o monóide diferente dos outros . Por isso, o monóide é gratuito porque não depende das regras aritméticas dos Naturais, nem de qualquer outra regra além das monóides.

E esta é a única maneira de construir um monóide livremente, não dependendo das regras internas do conjunto subjacente. Obviamente, a concatenação é expressa como listas em haskell.

• Nota: a única parte importante é que eles compartilham o mesmo número de elementos. Por exemplo, o monoid livre com 3 elementos a, be cseria qualquer concatenação arbitrária daqueles três, mas você pode escolher o que sempre símbolo: 1, 2, 3ou α, β, γ... eo monoid seria a mesma coisa

Answer 3

Aqui está outra lei que Lastsatisfaz:

forall (t :: Type) (x, y :: t).
  Last (Just x) <> Last (Just y) === Last (Just y)

Uma vez que satisfaz outra lei, não deve ser o Monóide livre.

Answer 4

Em primeiro lugar, examinemos a definição de monóides livres. Nunca entendi muito bem como é possível definir um monóide livre como uma estrutura que obedece às leis do monóide e nada mais. Como podemos provar que algo não obedece a regras, mas afirmado acima? Ou isso é apenas uma intuição?

Deixe-me ilustrar o propósito dos monóides livres.

Se eu te disser que há um monoid, com alguns elementos a, b, c, o que você pode deduzir a partir disso?

• Podemos encontrar mais elementos do que monoid escrevendo expressões envolvendo os geradores a , b, ce as operações monoid (+)e 0(aka. (<>)E mempty). (cf. Definição 1, na segunda metade desta resposta.)
• Podemos usar as leis monoidais para provar que algumas expressões denotam o mesmo elemento: podemos provar equações como ((a + 0) + b) = (a + b). (Definição 2.) Na verdade, as equações podemos provar com apenas que o conhecimento são equações que detêm em qualquer monoid, para quaisquer valores a, b, c. (Teorema 1)

E as equações que não podemos provar apenas com as leis monóides? Por exemplo, não podemos provar (a + b) = (b + a). Mas também não podemos provar sua negação (a + b) /= (b + a), se apenas conhecermos as leis monoidais. O que isso significa? Acontece que essa equação é válida em alguns monóides (por exemplo, monóides comutativos), mas não em outros: por exemplo, escolha um monóide onde x + y = ypara quase todos xe y(este é o Lastmonóide em Haskell), se escolhermos distinto ae b, então (a + b) /= (b + a).

Mas esse foi apenas um exemplo. O que podemos dizer em geral sobre as equações que não podemos provar apenas com as leis monoidais? As ofertas monoide livre uma resposta definitiva, de fato, um contra-exemplo universal: equações improváveis são falsas na monoid livre (gerados por a, b, c). Em outras palavras, podemos provar uma equação e = fusando apenas as leis do monóide se e somente se for verdadeira no monóide livre (ênfase em "se"). (Teorema 2.) Isso corresponde à intuição de que o monóide livre "apenas obedece às leis do monóide e nada mais".

Então, esse functor torna o Last um monóide livre? De forma mais geral, se houver uma instância obediente à lei para Monóide (T a), T é um monóide livre?

O Lastmonóide não é gratuito porque torna as equações mais verdadeiras do que você pode realmente provar puramente a partir das leis do monóide. Veja outra resposta :

forall (t :: Type) (x, y :: t).
  Last (Just x) <> Last (Just y) === Last (Just y)

---

Aqui está um esboço de como formalizar o acima.

Definição 1. O conjunto de expressões monoidais gerados pelo (alguns símbolos atômicos) A, B, Cé definido pela gramática:

e ::=
  | A | B | C   -- generators
  | e + e       -- binary operation (<>)
  | 0           -- identity (mempty)

Dado qualquer "monoid adequado", ou seja, um monoid (M, (+), 0)com alguns elementos escolhidos a, b, cem M(que não tem que ser distinto), uma expressão edenota um elemento eval eem M.

Definição 2. Uma equação é um par de expressões escritas e ~ f. O conjunto de equações prováveis é o menor conjunto de equações ("menor" quando ordenado por inclusão) satisfazendo o seguinte:

1. Ele inclui as leis monoid: (e + 0) ~ e, (0 + e) ~ e, ((e + f) + g) ~ (e + (f + g))são demonstráveis.
2. É uma relação de equivalência (ver um conjunto de tuplas como uma relação): por exemplo, para reflexividade, e ~ eé demonstrável.
3. É uma relação de congruência: se e ~ fé provável, então (g + e) ~ (g + f)e (e + g) ~ (f + g)são prováveis.

(A ideia dessa definição é que a afirmação " e ~ fé demonstrável" é válida se e somente se puder ser deduzida pela "aplicação" dessas regras. "Conjunto menor" é um método convencional para formalizar isso.

A definição de "equações prováveis" pode parecer arbitrária. Essas são as regras certas para definir "provabilidade"? Por que essas três regras em particular? Notavelmente, a regra de congruência pode não ser óbvia em uma primeira tentativa de dar tal definição. Este é o ponto dos seguintes teoremas, solidez e completude. Adicione uma regra (não redundante) e perderemos a solidez. Remova uma regra e perderemos a integridade.

Teorema 1. (Solidez) Se e ~ ffor demonstrável, então eval e = eval fem qualquer "monóide adequado" M.

Teorema 2. (integralidade) Se e ~ fnão é demonstrável, então suas denotações diferem em F, eval e /= eval fonde Fé o monoid livre gerado pelo A, B, C.

(Solidez é muito mais fácil de provar do que completude. Exercícios para o leitor.)

Este teorema da completude é uma caracterização do monóide livre: qualquer outro monóide Fque mantém a afirmação do teorema verdadeira é isomórfico ao monóide livre (tecnicamente, isso requer completude e uma suposição de que a função de denotação eval : Expr -> Mé sobrejetiva). É por isso que podemos dizer "o monóide livre" em vez de "o monóide de listas"; essa prática é mais precisa em contextos onde a representação não importa ("até o isomorfismo").

Na verdade, completude é trivial se você definir "o monóide livre" como o quociente de expressões monoidais pela relação de equivalência " _ ~ _é demonstrável". O trabalho árduo reside, na verdade, em uma prova separada, de que esse monóide é isomórfico ao monóide de listas.