Ist Last ein freies Monoid?
Die freien Monoide werden oft als "Listenmonoide" angesehen. Ich interessiere mich jedoch für andere mögliche Strukturen, die uns freie Monoide geben könnten .
Lassen Sie uns zunächst die Definition der freien Monoide durchgehen . Ich habe nie ganz verstanden, wie es möglich ist, ein freies Monoid als eine Struktur zu definieren , die sich an monoide Gesetze hält und sonst nichts. Wie beweisen wir, dass etwas keine Regeln einhält, sondern die oben genannten? Oder ist das nur eine Intuition?
Wie auch immer, wir werden Funktoren sprechen. Wenn ein Monoid frei ist , haben wir es mit einem kostenlosen Funktor bekommen . Es ist offensichtlich, dass eine Liste hier sehr nützlich ist:
free :: Set -> Mon
free a = ([a], (++), [])
Man könnte sich jedoch mehrere andere einfallen lassen. Zum Beispiel ist hier ein für Lastvon Data.Monoid:
freeLast :: Set -> Mon
freeLast a = (Last a, (<>) :: Last a -> Last a -> Last a, Last Nothing)
Macht dieser Funktor Lastein freies Monoid ? Im Allgemeinen, wenn es eine gesetzestreue Instanz für gibt Monoid (T a), ist Tein freies Monoid ?
Antworten
Hier ist eine Möglichkeit, ein freies Monoid zu verstehen: Wenn Ihnen jemand einen Wert gibt, wie viel können Sie daraus ableiten, wie es geschaffen wurde? Betrachten Sie ein additives Monoid natürlicher Zahlen. Ich gebe dir eine 7 und frage dich, wie ich es bekommen habe. Ich hätte 4 + 3 oder 3 + 4 oder 2 + 5 usw. hinzufügen können. Es gibt viele Möglichkeiten. Diese Informationen gingen verloren. Wenn ich Ihnen andererseits eine Liste gebe [4, 3], wissen Sie, dass sie aus Singletons [4]und erstellt wurde [3]. Nur dass vielleicht eine Einheit []beteiligt war. Vielleicht war es [4]<>[3]<>[]oder [4]<>[]<>[]<>[3]. Aber das war es definitiv nicht [3]<>[4].
Bei einer längeren Liste haben [1, 2, 3]Sie zusätzliche Optionen ([1]<>[2]) <> [3]oder [1] <> ([2]<>[3])sowie alle möglichen Einfügungen der leeren Liste. Die Informationen, die Sie verlieren, folgen also den Einheitsgesetzen und der Assoziativität, aber sonst nichts . Ein freier Monoidwert erinnert sich an seine Entstehung, Modulo-Einheitsgesetze und Assoziativität.
Nehmen wir zum Beispiel nicht negative Ganzzahlen, dh 0,1,2,.... Wie viele Monoide können wir machen?
Definieren mempty = 0und (<>) = (+). Sie können leicht beweisen, dass dies ein Monoid ist.
Definieren mempty = 1und (<>) = (*). Auch dies ist ein Monoid (Beweisen Sie, es ist einfach)
Die beiden oben definierten Monoide werden als additive und multiplikative Monoide über natürliche Zahlen bezeichnet. Sie haben eine unterschiedliche Struktur, zum Beispiel 0verhält sich das Element im multiplikativen Monoid völlig anders als jedes andere Element im additiven Monoid. Daher haben natürliche Zahlen etwas Inneres, das diese Monoide anders macht (halten Sie diese Behauptung bis zum nächsten Absatz aufrecht ).
Es gibt ein drittes Monoid, das wir erstellen können. Nennen wir es Verkettungsmonoid .
Definieren mempty = no-actionund (<>) = glue one integer beside the other.
Als Beispiel 3 <> mempty = 3und 3 <> 2 = 32. Beachten Sie, dass die Tatsache, dass Elemente natürliche Zahlen sind, hier nicht relevant ist. Wenn wir anstelle von Natural Rationals oder andere Symbole verwenden, die Sie mögen, wäre das Monoid genau dasselbe. (* Fußnote lesen) Daher gibt es nichts Inneres in der zugrunde liegenden Menge, was das Monoid von anderen unterscheidet . Deshalb ist das Monoid frei, weil es weder von den arithmetischen Regeln der Naturals noch von anderen Regeln außer den monoiden Regeln abhängt.
Und dies ist die einzige Möglichkeit, ein Monoid frei zu bauen, unabhängig von den inneren Regeln der zugrunde liegenden Menge. Natürlich wird die Verkettung als Liste in Haskell ausgedrückt.
- Hinweis: Das einzig wichtige Bit ist, dass sie die gleiche Anzahl von Elementen gemeinsam haben. Zum Beispiel das freie Monoid mit 3 Elementen
a,bundcwäre jede beliebige Verkettung dieser drei, aber Sie können wählen , was auch immer Symbol:1,2,3oderα,β,γ... und das Monoid würde die gleiche Sache
Hier ist ein anderes Gesetz, das Lasterfüllt:
forall (t :: Type) (x, y :: t).
Last (Just x) <> Last (Just y) === Last (Just y)
Da es einem anderen Gesetz entspricht, darf es nicht das freie Monoid sein.
Lassen Sie uns zunächst die Definition der freien Monoide durchgehen. Ich habe nie ganz verstanden, wie es möglich ist, ein freies Monoid als eine Struktur zu definieren, die sich an monoide Gesetze hält und sonst nichts. Wie beweisen wir, dass etwas keine Regeln einhält, sondern die oben genannten? Oder ist das nur eine Intuition?
Lassen Sie mich den Zweck freier Monoide veranschaulichen.
Wenn ich Ihnen sagen , es ist ein Monoid, mit einigen Elementen a, b, c, was kann man daraus ableiten?
- Wir können mehr Elemente dieser Monoid finden durch Ausdrücke , die die Schreib Generatoren
a,b,cund die Monoid Operationen(+)und0(aka.(<>)Undmempty). (vgl. Definition 1 in der zweiten Hälfte dieser Antwort.) - Wir können die Monoidgesetze verwenden, um zu beweisen, dass einige Ausdrücke dasselbe Element bezeichnen: Wir können Gleichungen wie beweisen
((a + 0) + b) = (a + b). (Definition 2.) In der Tat Gleichungen wir nur mit diesem Wissen unter Beweis stellen können , sind Gleichungen , die halten in jedem Monoid, für alle Wertea,b,c. (Satz 1.)
Was ist mit Gleichungen, die wir nicht nur aus den monoiden Gesetzen beweisen können? Zum Beispiel können wir nicht beweisen (a + b) = (b + a). Aber wir können seine Negation auch nicht beweisen (a + b) /= (b + a), wenn wir nur die monoiden Gesetze kennen. Was bedeutet das? Es stellt sich heraus, dass diese Gleichung in einigen Monoiden (z. B. kommutativen Monoiden) gilt, in anderen jedoch nicht: Wählen Sie beispielsweise ein Monoid, wo x + y = yfür fast alle xund y(dies ist das LastMonoid in Haskell), wenn wir ein unterschiedliches aund bdann wählen (a + b) /= (b + a).
Das war aber nur ein Beispiel. Was können wir allgemein über Gleichungen sagen, die wir nicht nur aus den monoiden Gesetzen beweisen können? Die freie Monoid bietet eine definitive Antwort in der Tat ein universelles Gegenbeispiel : unbeweisbar Gleichungen falsch sind in der freien Monoid (erzeugt durch a, b, c). Mit anderen Worten, wir können eine Gleichung e = fnur dann unter Verwendung der Monoidgesetze beweisen, wenn sie im freien Monoid wahr ist (Betonung auf "wenn"). (Satz 2.) Dies entspricht der Intuition, dass das freie Monoid "nur die Monoidgesetze einhält und sonst nichts".
Macht dieser Funktor Last zu einem freien Monoid? Wenn es eine gesetzestreue Instanz für Monoid (T a) gibt, ist T allgemein ein freies Monoid?
Das LastMonoid ist nicht frei, weil es mehr Gleichungen wahr macht, als Sie tatsächlich nur aus den Monoidgesetzen beweisen können. Siehe andere Antwort :
forall (t :: Type) (x, y :: t).
Last (Just x) <> Last (Just y) === Last (Just y)
Hier ist eine Skizze, wie man das Obige formalisiert.
Definition 1. Der Satz von monoidal Ausdrücke von (einigen Atom Symbole) erzeugt A, B, Cwird durch die Grammatik definiert:
e ::=
| A | B | C -- generators
| e + e -- binary operation (<>)
| 0 -- identity (mempty)
Jede „geeignete monoid“ gegeben, das, ein monoid heißt (M, (+), 0)mit einigen ausgewählten Elementen a, b, cin M( , die nicht eindeutig sein müssen), ein Ausdruck ebezeichnet ein Element eval ein M.
Definition 2. Eine Gleichung ist ein geschriebenes Ausdruckspaar e ~ f. Der Satz nachweisbarer Gleichungen ist der kleinste Satz von Gleichungen ("kleinste", wenn durch Einbeziehung geordnet), der Folgendes erfüllt:
- Es umfasst die Monoid Gesetze:
(e + 0) ~ e,(0 + e) ~ e,((e + f) + g) ~ (e + (f + g))beweisbar sind. - Es ist eine Äquivalenzbeziehung (Betrachtung einer Reihe von Tupeln als Beziehung): Zum Beispiel für Reflexivität
e ~ eist nachweisbar. - Es ist eine Kongruenzbeziehung: Wenn
e ~ fes dann beweisbar ist(g + e) ~ (g + f)und(e + g) ~ (f + g)beweisbar ist.
(Die Idee dieser Definition ist, dass die Behauptung " e ~ fbeweisbar" genau dann gilt, wenn sie durch "Anwenden" dieser Regeln abgeleitet werden kann. "Kleinste Menge" ist eine herkömmliche Methode, um dies zu formalisieren.)
Die Definition von "nachweisbaren Gleichungen" mag willkürlich erscheinen. Sind das die richtigen Regeln, um "Beweisbarkeit" zu definieren? Warum gerade diese drei Regeln? Insbesondere ist die Kongruenzregel bei einem ersten Versuch, eine solche Definition zu geben, möglicherweise nicht offensichtlich. Dies ist der Punkt der folgenden Sätze, Solidität und Vollständigkeit. Fügen Sie eine (nicht redundante) Regel hinzu, und wir verlieren die Solidität. Entfernen Sie eine Regel, und wir verlieren die Vollständigkeit.
Satz 1. (Solidität) Wenn e ~ fnachweisbar, dann eval e = eval fin jedem "geeigneten Monoid" M.
Satz 2. (Vollständigkeits) Wenn e ~ fist nicht beweisbar, dann ihre Benennungen unterscheiden sich in F, eval e /= eval fwo Fdie freie Monoid erzeugt durch A, B, C.
(Solidität ist viel einfacher zu beweisen als Vollständigkeit. Übungen für den Leser.)
Dieser Vollständigkeitssatz ist eine Charakterisierung des freien Monoids: Jedes andere Monoid F, das die Aussage des Satzes wahr hält, ist isomorph zum freien Monoid (technisch erfordert dies sowohl Vollständigkeit als auch die Annahme, dass die Bezeichnungsfunktion eval : Expr -> Msurjektiv ist). Deshalb können wir "das freie Monoid" anstelle von "das Monoid der Listen" sagen; Diese Praxis ist am genauesten in Kontexten, in denen die Darstellung keine Rolle spielt ("bis zum Isomorphismus").
In der Tat ist die Vollständigkeit trivial, wenn Sie "das freie Monoid" als den Quotienten monoidaler Ausdrücke durch die Äquivalenzbeziehung " _ ~ _ist beweisbar" definieren. Die harte Arbeit beruht tatsächlich auf einem separaten Beweis, dass dieses Monoid isomorph zum Monoid von Listen ist.