Evan Patterson zeigt, wie sich Gleichungen mit Diagrammen beweisen lassen
How to prove equations using diagrams, part 1
E-graphs sind Datenstrukturen, die Äquivalenzrelationen über Ausdrücken verwalten, doch was steckt abstrakt dahinter? Evan Patterson schlägt vor, Gleichungen als Diagramme in einer Kategorie darzustellen und ihre gültigen Umformungen über initiale Funktoren zu beschreiben. Diese bewahren die Lösungsmenge eines Gleichungssystems. Anhand einfacher Beispiele und eines Beweises für das Verkleben kommutierender Quadrate zeigt er, wie sich diagrammatisches Schließen mechanisch formulieren lässt.
Die Notation lässt das offensichtlich wahr erscheinen – das macht sie zu einer guten Notation! –, aber es braucht trotzdem einen Beweis.
- henearkr
Sehr interessant!!
Eine Kleinigkeit: Bei einem J-förmigen Diagramm D ist J die "Indexkategorie" oder das "Schema" von D, nicht die "Form", wie im Artikel geschrieben steht.
- boldslogan
Mann, ich bin vor kurzem über dieses Konzept von Funktor oder nicht-symbolischer Logik und so gestolpert. Hast du zufällig irgendwelche Vorschläge, was man sich anschauen könnte?