Missbrauch der Algebra von algebraischen Datentypen - warum funktioniert das?

Question

Der Ausdruck "algebraisch" für algebraische Datentypen sieht für jemanden mit einem Hintergrund in Mathematik sehr suggestiv aus. Lassen Sie mich versuchen zu erklären, was ich meine.

Nach der Definition der Grundtypen

• Produkt •
• Gewerkschaft +
• Singleton X
• Einheit 1

und die Verwendung der Abkürzung X² para X•X et 2X para X+X usw., können wir dann algebraische Ausdrücke für z. B. verknüpfte Listen definieren

data List a = Nil | Cons a (List a) L = 1 + X • L

und binäre Bäume:

data Tree a = Nil | Branch a (Tree a) (Tree a) T = 1 + X • T²

Nun ist mein erster Instinkt als Mathematiker, mit diesen Ausdrücken durchzudrehen und zu versuchen, zu lösen L et T . Ich könnte dies durch wiederholte Substitution erreichen, aber es scheint viel einfacher zu sein, die Notation fürchterlich zu missbrauchen und so zu tun, als könnte ich sie nach Belieben umstellen. Zum Beispiel für eine verknüpfte Liste:

L = 1 + X • L

(1 - X) • L = 1

L = 1 / (1 - X) = 1 + X + X² + X³ + ...

wobei ich die Potenzreihenentwicklung von 1 / (1 - X) auf völlig ungerechtfertigte Weise ein interessantes Ergebnis ableiten, nämlich dass ein L Typ ist entweder Nil oder er enthält 1 Element, oder er enthält 2 Elemente, oder 3, usw.

Noch interessanter wird es, wenn wir dies für binäre Bäume tun:

T = 1 + X • T²

X • T² - T + 1 = 0

T = (1 - (1 - 4 • X)) / (2 • X)

T = 1 + X + 2 • X² + 5 • X³ + 14 • X + ...

wiederum unter Verwendung der Potenzreihenentwicklung (die mit Wolfram Alpha ). Damit wird die (für mich) nicht offensichtliche Tatsache ausgedrückt, dass es nur einen Binärbaum mit einem Element gibt, 2 Binärbäume mit zwei Elementen (das zweite Element kann auf dem linken oder rechten Zweig liegen), 5 Binärbäume mit drei Elementen usw.

Meine Frage ist also: Was mache ich hier? Diese Operationen scheinen ungerechtfertigt zu sein (was genau ist eigentlich die Quadratwurzel eines algebraischen Datentyps?), aber sie führen zu sinnvollen Ergebnissen. Hat der Quotient zweier algebraischer Datentypen irgendeine Bedeutung in der Informatik, oder handelt es sich nur um einen Notationstrick?

Und, was vielleicht noch interessanter ist, ist es möglich, diese Ideen zu erweitern? Gibt es eine Theorie der Algebra der Typen, die z. B. beliebige Funktionen auf Typen zulässt, oder benötigen Typen eine Potenzreihendarstellung? Wenn man eine Klasse von Funktionen definieren kann, hat dann die Komposition von Funktionen irgendeine Bedeutung?

Answer 1

Die Algebra der kommunizierenden Prozesse (ACP) befasst sich mit ähnlichen Arten von Ausdrücken für Prozesse. Sie bietet Addition und Multiplikation als Operatoren für Auswahl und Abfolge, mit zugehörigen neutralen Elementen. Darauf aufbauend gibt es Operatoren für andere Konstrukte, wie Parallelität und Unterbrechung. Siehe http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes . Es gibt auch ein Papier online namens "A Brief History of Process Algebra".

Ich arbeite an der Erweiterung von Programmiersprachen mit ACP. Letzten April habe ich auf den Scala Days 2012 ein Forschungspapier vorgestellt, verfügbar unter http://code.google.com/p/subscript/

Auf der Konferenz habe ich einen Debugger vorgeführt, der eine parallele rekursive Spezifikation einer Tasche durchführt:

Beutel = A; (Beutel&a)

wobei A und a für Eingabe- und Ausgabeaktionen stehen; das Semikolon und das kaufmännische Und stehen für Reihenfolge und Parallelität. Sehen Sie sich das Video bei SkillsMatter an, das Sie über den vorherigen Link erreichen.

Eine Taschenspezifikation, die eher vergleichbar ist mit

L = 1 + X-L

wäre

B = 1 + X&B

ACP definiert Parallelität in Form von Auswahl und Reihenfolge unter Verwendung von Axiomen; siehe den Wikipedia-Artikel. Ich frage mich, was die Analogie für die Tasche wäre

L = 1 / (1-X)

Die Programmierung im ACP-Stil ist praktisch für Textparser und GUI-Controller. Spezifikationen wie

searchCommand = clicked(searchButton) + key(Enter)

cancelCommand = clicked(cancelButton) + key(Escape)

kann prägnanter geschrieben werden, indem man die beiden Verfeinerungen "clicked" und "key" implizit macht (wie es Scala mit Funktionen erlaubt). Daher können wir schreiben:

searchCommand = searchButton + Enter

cancelCommand = cancelButton + Escape

Die rechte Seite enthält nun Operanden, bei denen es sich um Daten und nicht um Prozesse handelt. Auf dieser Ebene ist es nicht notwendig zu wissen, durch welche impliziten Verfeinerungen diese Operanden zu Prozessen werden; sie würden nicht notwendigerweise zu Eingabeaktionen verfeinert; Ausgabeaktionen würden ebenfalls gelten, z. B. bei der Spezifikation eines Testroboters.

Prozesse erhalten auf diese Weise Daten als Begleiter; daher präge ich den Begriff "Item-Algebra".