Mein Problem: Manipulation symbolischer Ausdrücke.
Ein symbolischer Ausdruck wird ausgehend von ganzzahligen Konstanten und Variablen mit Hilfe von Operatoren wie +, -, *, /, min, max erstellt. Genauer würde ich einen Ausdruck auf folgende Weise darstellen (Caml-Code):
%Vor%Ich stelle mir vor, dass ich für eine nützliche und effiziente Berechnung (z. B. a + b - a = 0 oder a + 1 & gt; a) eine normale Form haben und daran arbeiten muss. Die obige Darstellung wird wahrscheinlich nicht so gut funktionieren.
Kann mir jemand zeigen, wie ich das angehen soll? Ich brauche keinen Code. Das kann leicht geschrieben werden, wenn ich weiß wie. Links zu Artikeln, die Darstellungen für normale Formen und / oder Algorithmen für Konstruktion / Vereinfachung / Vergleich darstellen, würden ebenfalls hilfreich sein.
Wenn Sie von einer Ocaml-Bibliothek wissen, die dies tut, lassen Sie es mich wissen.
Wenn Sie Min
und Max
auslassen, sind normale Formen einfach: Sie sind Elemente des Bruchteils Ihrer Variablen, ich meine P[Vars]/Q[Vars]
wobei P
, Q
Polynome sind. Für Min und Max, ich weiß es nicht; Ich nehme an, der einfachste Weg ist, sie so zu betrachten, als ob / then / else testet, und sie an die Spitze Ihrer Ausdrücke zu treiben (Duplizierung von Dingen im Prozess), zum Beispiel würde P(Max(Q,R))
in P(if Q>R then Q else R)
und dann neu geschrieben werden in if Q>R then P(Q) else P(R)
.
Ich kenne zwei verschiedene Möglichkeiten, um normale Formen für Ihre Ausdrücke zu finden expr
:
Definieren Sie die Rewrite-Regeln expr -> expr
, die Ihrer Intuition entsprechen, und zeigen Sie, dass sie sich normalisieren. Das kann man tun, indem man die Gleichungen leitet, von denen man weiß, dass sie wahr sind: Von Add(a,Add(b,c)) = Add(Add(a,b),c)
wird entweder Add(a,Add(b,c)) -> Add(Add(a,b),c)
abgeleitet oder umgekehrt. Aber dann haben Sie ein Gleichungssystem, für das Sie Kirche-Rosser und Normalisierung zeigen müssen; schmutziges Geschäft in der Tat.
Nehmen Sie einen semantischeren Ansatz, indem Sie eine "Semantik" Ihrer Werte angeben: Ein Element in expr
ist wirklich eine Notation für ein mathematisches Objekt, das im Typ sem
lebt. Finden Sie eine geeignete (eindeutige) Repräsentation für Objekte von sem
, dann eine Auswertungsfunktion expr -> sem
, dann endlich (wenn Sie möchten, aber Sie müssen nicht für die Gleichheitsprüfung zum Beispiel) eine Bestätigung sem -> expr
. Die Zusammensetzung beider Transformationen wird Ihnen natürlich eine Normalisierungsprozedur geben, ohne sich zum Beispiel Gedanken über die Richtung des Add-Umschreibens machen zu müssen (irgendeine willkürliche Wahl wird natürlich von Ihrer Verdingungsfunktion herrühren). Zum Beispiel wäre der semantische Raum für polynomische Brüche etwa wie folgt:
.
%Vor%Natürlich ist das nicht immer so einfach. Ich sehe nicht richtig, welche Repräsentation einem semantischen Raum mit Min- und Max-Funktionen geben.
Edit: In Bezug auf externe Bibliotheken kenne ich keine und ich bin mir nicht sicher, ob es sie gibt. Sie sollten vielleicht nach Verbindungen zu anderer symbolischer Algebra-Software suchen, aber ich habe noch nichts davon gehört (vor ein paar Jahren gab es ein Jane Street Summer Project, aber ich bin mir nicht sicher, ob ein Ergebnis produziert wurde) > Wenn Sie das für eine Produktionsanwendung benötigen, sollten Sie vielleicht direkt daran denken, die Bindung selbst zu schreiben, z. zu Sage oder Maxima. Ich weiß nicht, wie es sein würde.
Der übliche Ansatz für ein solches Problem ist:
"a + 1 > a"
[Variable('a'); Plus; Number(1); GreaterThan; Variable('a')]
Max( Add( Var('a'), Const(1)), Var('a'))
Erstellen Sie eine Funktion, die den Syntaxbaum interpretieren kann, um Ihr Endergebnis zu erhalten
%Vor%Verzeiht die Syntax, ich habe Ocaml schon lange nicht mehr benutzt.
Über Bibliotheken erinnere ich mich nicht an irgendwelche Gedanken, aber es gibt sicherlich gute, die leicht verfügbar sind - das ist die Art von Aufgabe, die die FP-Gemeinschaft liebt.
Tags und Links algorithm ocaml symbolic-math