Last è un monoide gratuito?

Question

I monoidi liberi sono spesso considerati "list monoidi". Tuttavia, sono interessato ad altre possibili strutture che potrebbero darci monoidi liberi .

In primo luogo, esaminiamo la definizione di monoidi liberi . Non ho mai capito bene come sia possibile definire un monoide libero come una struttura che rispetta le leggi del monoide e nient'altro. Come dimostriamo che qualcosa non rispetta le regole ma sopra indicato? O è solo un'intuizione?

Comunque, parleremo di funtori. Se un monoide è gratuito , lo abbiamo ottenuto con un funtore gratuito . È ovvio che un elenco è abbastanza utile qui:

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

Tuttavia, se ne potrebbero inventare molti altri. Ad esempio, eccone uno per Lastdi Data.Monoid:

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

Quindi, questo funtore crea Lastun monoide libero ? Più in generale, se esiste un'istanza rispettosa della legge Monoid (T a), è Tun monoide libero ?

Answer 1

Ecco un modo per capire un monoide gratuito: se qualcuno ti dà un valore, quanto puoi dedurre da come è stato creato? Considera un monoide additivo di numeri naturali. Ti do un 7 e ti chiedo come l'ho preso. Avrei potuto aggiungere 4 + 3, o 3 + 4, o 2 + 5, ecc. Ci sono molte possibilità. Questa informazione è stata persa. Se invece ti do una lista [4, 3], sai che è stata creata da singleton [4]e [3]. Solo che forse c'era un'unità []coinvolta. Forse era [4]<>[3]<>[]o [4]<>[]<>[]<>[3]. Ma sicuramente non lo era [3]<>[4].

Con un elenco più lungo, [1, 2, 3]sono disponibili opzioni aggiuntive ([1]<>[2]) <> [3]o [1] <> ([2]<>[3]), più tutti i possibili inserimenti dell'elenco vuoto. Quindi le informazioni che perdi seguono le leggi unitarie e l'associatività, ma nient'altro . Un valore monoide libero ricorda come è stato creato, le leggi dell'unità modulo e l'associatività.

Answer 2

A titolo di esempio, prendiamo numeri interi non negativi, ad es 0,1,2,.... Quanti monoidi possiamo produrre?

Definizione di mempty = 0e (<>) = (+). Puoi facilmente provare che si tratta di un monoide.

Definizione di mempty = 1e (<>) = (*). Di nuovo, questo è un monoide (Dimostralo, è facile)

I due monoidi definiti sopra, sono chiamati monoidi additivi e moltiplicativi su numeri naturali. Sono diversi nella struttura, ad esempio, l'elemento 0nel monoide moltiplicativo, si comporta in modo totalmente diverso da qualsiasi altro elemento nel monoide additivo, quindi c'è qualcosa di interno ai numeri naturali, che rende questi monoidi diversi (mantieni questa affermazione fino al paragrafo successivo ).

Esiste un terzo monoide che possiamo creare, chiamiamolo concatenazione monoide.

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

Ad esempio, 3 <> mempty = 3e 3 <> 2 = 32. Si noti che il fatto che gli elementi siano numeri naturali non è rilevante qui. Se invece di Natural, prendiamo Rationals, o qualunque simbolo ti piaccia, il monoide sarebbe esattamente la stessa cosa. (* Leggi la nota in calce) Quindi, non c'è nulla di interno all'insieme sottostante che rende il monoide diverso dagli altri . Ecco perché il monoide è gratuito perché non dipende dalle regole aritmetiche dei Naturali, né da altre regole oltre a quelle monoide.

E questo è l'unico modo per costruire un monoide liberamente, non dipendente dalle regole interne dell'insieme sottostante. Ovviamente, la concatenazione è espressa come elenchi in haskell.

• Nota: l'unico aspetto importante è che condividono lo stesso numero di elementi. Ad esempio, il monoide libero con 3 elementi a, be csarebbe qualsiasi concatenazione arbitraria di quei tre, ma è possibile scegliere che cosa mai simbolo: 1, 2, 3o α, β, γ... e il monoide sarebbe la stessa cosa

Answer 3

Ecco un'altra legge che Lastsoddisfa:

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

Poiché soddisfa un'altra legge, non deve essere il Monoide libero.

Answer 4

In primo luogo, esaminiamo la definizione di monoidi liberi. Non ho mai capito bene come sia possibile definire un monoide libero come una struttura che rispetta le leggi del monoide e nient'altro. Come dimostriamo che qualcosa non rispetta le regole ma sopra indicato? O è solo un'intuizione?

Permettetemi di illustrare lo scopo dei monoidi liberi.

Se ti dico c'è un monoide, con alcuni elementi a, b, c, cosa si può dedurre da questo?

• Possiamo trovare più elementi di questa monoid scrivendo espressioni che coinvolgono i generatori a , b, ce le operazioni monoide (+)e 0(aka. (<>)E mempty). (cfr. definizione 1, nella seconda metà di questa risposta.)
• Possiamo usare le leggi dei monoidi per dimostrare che alcune espressioni denotano lo stesso elemento: possiamo dimostrare equazioni come ((a + 0) + b) = (a + b). (Definizione 2.) In effetti, le equazioni possiamo dimostrare con un solo che la conoscenza sono equazioni che tengono in alcun monoide, per tutti i valori a, b, c. (Teorema 1.)

E le equazioni che non possiamo provare solo con le leggi dei monoidi? Ad esempio, non possiamo provare (a + b) = (b + a). Ma non possiamo nemmeno provare la sua negazione (a + b) /= (b + a), se conosciamo solo le leggi del monoide. Cosa significa? Si scopre che l'equazione vale in alcuni monoidi (ad esempio, monoidi commutativi), ma non in altri: per esempio, scegli un monoide dove x + y = yper quasi tutti xe y(questo è il Lastmonoide in Haskell), se scegliamo distinti ae b, allora (a + b) /= (b + a).

Ma quello era solo un esempio. Cosa possiamo dire in generale delle equazioni che non possiamo dimostrare solo con le leggi monoide? Le offerte monoide libero una risposta definitiva, infatti, un controesempio universale: equazioni indimostrabili sono false nel monoide libero (generato da a, b, c). In altre parole, possiamo provare un'equazione e = fusando solo le leggi del monoide se e solo se è vera nel monoide libero (enfasi su "se"). (Teorema 2.) Ciò corrisponde all'intuizione che il monoide libero "si attiene solo alle leggi del monoide e nient'altro".

Quindi, questo funtore rende Last un monoide gratuito? Più in generale, se esiste un'istanza rispettosa della legge per Monoid (T a), T è un monoide libero?

Il Lastmonoide non è libero perché rende vere più equazioni di quelle che puoi effettivamente dimostrare puramente dalle leggi del monoide. Vedi altra risposta :

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

---

Ecco uno schizzo di come formalizzare quanto sopra.

Definizione 1. L'insieme di espressioni monoidali generati da (alcuni simboli atomiche) A, B, Cè definito dalla grammatica:

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

Dato un "monoid adatto", vale a dire, un monoide (M, (+), 0)con alcuni elementi scelti a, b, cin M(che non devono essere distinti), espressione edenota un elemento eval ea M.

Definizione 2. Un'equazione è una coppia di espressioni, scritte e ~ f. L'insieme di equazioni dimostrabile è il più piccolo insieme di equazioni ("più piccolo" se ordinato per inclusione) che soddisfa quanto segue:

1. Esso comprende le leggi monoid: (e + 0) ~ e, (0 + e) ~ e, ((e + f) + g) ~ (e + (f + g))sono dimostrabili.
2. È una relazione di equivalenza (vedere un insieme di tuple come una relazione): ad esempio, per la riflessività, e ~ eè dimostrabile.
3. È una relazione di congruenza: se e ~ fè dimostrabile allora (g + e) ~ (g + f)e (e + g) ~ (f + g)sono dimostrabili.

(L'idea di questa definizione è che l'affermazione " e ~ fè dimostrabile" vale se e solo se può essere dedotta "applicando" quelle regole. "Insieme più piccolo" è un metodo convenzionale per formalizzarlo.)

La definizione di "equazioni dimostrabili" può sembrare arbitraria. Sono queste le regole giuste per definire la "provabilità"? Perché queste tre regole in particolare? In particolare, la regola di congruenza potrebbe non essere ovvia in un primo tentativo di dare una tale definizione. Questo è il punto dei seguenti teoremi, correttezza e completezza. Aggiungi una regola (non ridondante) e perderemo la validità. Rimuovi una regola e perdiamo la completezza.

Teorema 1. (Solidità) Se e ~ fè dimostrabile, allora eval e = eval fin qualsiasi "monoide adatto" M.

Teorema 2. (completezza) Se e ~ fnon è dimostrabile, allora le loro denotazioni differiscono F, eval e /= eval fdove Fè il monoide libero generato da A, B, C.

(La validità è molto più facile da dimostrare della completezza. Esercizi per il lettore.)

Questo teorema di completezza è una caratterizzazione del monoide libero: qualsiasi altro monoide Fche mantiene l'affermazione del teorema vera è isomorfo al monoide libero (tecnicamente, ciò richiede sia completezza che l'assunzione che la funzione di denotazione eval : Expr -> Msia suriettiva). Questo è il motivo per cui possiamo dire "il monoide libero" invece di "il monoide delle liste"; quella pratica è più accurata in contesti in cui la rappresentazione non ha importanza ("fino all'isomorfismo").

In effetti, la completezza è banale se si definisce "il monoide libero" come il quoziente di espressioni monoidali dalla relazione di equivalenza " _ ~ _è dimostrabile". Il duro lavoro risiede in realtà in una dimostrazione separata, che questo monoide è isomorfo al monoide delle liste.