Isabelle Buch Übung 2.11: Ausdrücke Polynom Form Transforming

Question

meine Frage bezüglich Übung 2.11 in dem Buch Beton Semantics (http://concrete-semantics.org/):

arithmetische Ausdrücke in einer Variablen über ganze Zahlen definieren (Typ int) als Datentyp:

datatype exp = Var | Const int | Add exp exp | Mult exp exp 

definieren einer Funktion, so dass eval :: exp => int => inteval e x e bei der Wert x auswertet. Ein Polynom kann als eine Liste von Koeffizienten dargestellt werden, beginnend mit der Konstante. Zum Beispiel repräsentiert [4, 2, -1, 3] das Polynom 4+2x-x^2+3x^3.

Definieren Sie eine Funktion evalp :: int list => int => int dass der angegebene Wert ein Polynom in auswertet. Definieren Sie eine Funktion coeffs :: exp => int list, die einen Ausdruck in ein Polynom umwandelt. Dies kann zusätzliche Funktionen erfordern. Beweisen Sie, dass coeffs den Wert des Ausdrucks erhält: evalp (coeffs e) x = eval e x.

--- Ende

Es ist alles ziemlich einfach, bis Sie zu coeffs bekommen. Wir müssten uns mit Ausdrücken wie (X + X)*(2*X + 3*X*X) beschäftigen, die rekursiv unter Verwendung eines Verteilungsgesetzes bis zu ihrer polynomischen Form von unten nach oben expandiert werden müssen. Der resultierende Ausdruck könnte immer noch so etwas wie (X*X + X*2*X + 3*X*X + 4*X*X*X) sein, so dass es notwendig ist, die Produktbegriffe zu normalisieren (so wird zB X*2*X zu 2*X*X), sammle zusammen wie Begriffe und ordne sie schließlich in der Reihenfolge des zunehmenden Grades an! Das scheint mir wesentlich komplizierter zu sein als die bisherigen Übungen. Ich frage mich, ob ich etwas vermisse oder übermäßig verkompliziere.

Answer 1

Ich denke, diese Übung ist wesentlich einfacher als Sie denken. Sie können eine einzige primitiv-rekursive Funktion coeffs schreiben, die die Aufgabe erfüllt: die Koeffizienten Var sind [0,1], die Koeffizienten Const c sind [c]. Wenn Sie zwei Unterausdrücke haben und deren Koeffizienten kennen, können Sie diese beiden Koeffizientenlisten in einer einzigen Liste für Addition/Multiplikation kombinieren.

Dafür sollten Sie idealerweise zwei Hilfsfunktionen add_coeffs und mult_coeffs schreiben, die zwei Koeffizientenlisten addieren und multiplizieren. (Letztere werden wahrscheinlich Gebrauch des ehemaligen machen)

Sie beweisen müssen, dass add_coeffs und mult_coeffs das Richtige tun (w.r.t. eval und evalp). Die resultierenden Lemmas machen auch gute [simp] Regeln.

Die Beweise sind alle einfache Induktionen, wo jeder Fall automatisch ist.

Als allgemeine Regel gilt: Eine gute Definition macht oft den Unterschied zwischen einem langen und langwierigen Beweis und einem direkten oder sogar vollständig automatischen Beweis. Eine langatmige Erweiterung zu machen und dann Summanden usw. zu gruppieren, wie Sie es in Ihrer Frage vorgeschlagen haben, wird sicherlich zu einem langwierigen Beweis führen.

Natürlich ist die Methode, die ich in dieser Antwort vorgeschlagen habe, nicht sehr effizient, aber wenn Sie Dinge in einem Theorembeweiser tun möchten, ist Effizienz in der Regel kein großes Anliegen - Sie wollen Dinge einfach und elegant und zugänglich sein zu schönen Beweisen.Wenn Sie effizienten Code benötigen, können Sie Ihre nette und einfache abstrakte Formulierung später zu etwas effizienterem entwickeln und Äquivalenz zeigen.