Äquivalenz zweier Programme

Columbo

Was ist denn der Graph eines Algorithmus?

Ich denke er könnte etwas wie den Configuration Graph einer TM meinen die den Algo berechnet.

Ethon

Jester schrieb:

Ethon schrieb:

Beweisen? Könntest du höchstens wenn du den Graphen des Algorithmus auf elementare Basisoperationen herunterbrichst, vereinfachst und für diesen zeigst dass er isomorph ist.

Klingt ja interessant. Was ist denn der Graph eines Algorithmus? Und auf welchen Äquivalenzbegriff bezieht sich das?

Ich würde den Kontrollfluss des Algorithmus als gerichteten Graphen abbilden.
Davor natürlich Transformationen durchführen damit logisch äquivalente aber syntaktisch verschiedene Sprachkonstrukte den selben Graphen ergeben. Akso wohl auch grundlegende Optimierungen durchführen.

unsigned sum(unsigned n) {
    unsigned x = 0;
    for(unsigned z = 1; z < n; ++z) {
        x += z;
    }
    return x;
}

unsigned sum2(unsigned m) {
    unsigned foo;
    foo = 0;
    while(m) {
        foo += m;
        --m;
    }
    return foo;
}

Sollte man so wohl als äquivalent erkennen können.

icarus2

Ethon schrieb:

Davor natürlich Transformationen durchführen damit logisch äquivalente aber syntaktisch verschiedene Sprachkonstrukte den selben Graphen ergeben.

Und wie sollen diese Transformationen konkret aussehen? Ich meine jetzt nicht bloss fuer ein konkrets Beispiel, sondern im allgemeinen Fall. Das wirst du nicht hinbekommen.

Wie bereits erwaehnt ist die Aequivalenz von zwei Programmen allgemein nicht entscheidbar - angenommen wir hatten einen Algorithmus A, der die Aequivalenz von zwei Programmen ueberprueft, dann kann man das Halteproblem ganz einfach auf A reduzieren. In diesem Zusammenhang ist auch der Satz von Rice interessant.

Bashar

Dass das nicht allgemein funktioniert, ist doch klar, deshalb das Wort "man könnte höchstens"... Wenn man es für eine möglichst große Klasse von Spezialfällen machen will, ist die Idee aber gar nicht so schlecht, das Programm in eine möglichst kanonische Form zu überführen und dann gleiche Programme als äquivalent zu bezeichnen. Ich weiß nicht, ob das wirklich praktikabel ist, aber auf einer gewissen Ebene ist das mit dem, was ein optimierender Compiler macht, vergleichbar.

icarus2

Hatte das "hoechstens" ueberlesen, dachte er wolle das im allgemeinen Fall machen.

Es ist allerdings ein ziemlich grosser Unterschied ob man als Input zwei Programme bekommt und entscheiden muss, ob die Programme aequivalent sind, oder ob man entscheiden muss ob eine konkrete Transformation (bei einem optimierenden Compiler eine Optimierung) in einem aequivalenten Programm resultiert. Letzteres scheint ja in der Praxis ziemlich gut zu funktionieren.

volkard

Ethon schrieb:

Jester schrieb:

Ethon schrieb:

Beweisen? Könntest du höchstens wenn du den Graphen des Algorithmus auf elementare Basisoperationen herunterbrichst, vereinfachst und für diesen zeigst dass er isomorph ist.

Klingt ja interessant. Was ist denn der Graph eines Algorithmus? Und auf welchen Äquivalenzbegriff bezieht sich das?

Ich würde den Kontrollfluss des Algorithmus als gerichteten Graphen abbilden.
Davor natürlich Transformationen durchführen damit logisch äquivalente aber syntaktisch verschiedene Sprachkonstrukte den selben Graphen ergeben. Akso wohl auch grundlegende Optimierungen durchführen.
unsigned sum(unsigned n) {
    unsigned x = 0;
    for(unsigned z = 1; z < n; ++z) {
        x += z;
    }
    return x;
}
unsigned sum2(unsigned m) {
    unsigned foo;
    foo = 0;
    while(m) {
        foo += m;
        --m;
    }
    return foo;
}
Sollte man so wohl als äquivalent erkennen können.

Also mit -O3 compilieren und die asm-Ausgabe vergleichen.

Jo. Nur ist damit quasi keinem geholfen.

unsigned sum3(unsigned n) {
    return n*(n-1)/2;
}

Siehst ja hier im Forum, wie unterschiedlich die Lösungen für einfache Aufgaben sind. Sagen wir mal, 10% der Funktionen sind so, daß zu erwarten ist, daß Der Syntaxbaumvergleicher keine Äquivalenz erkennt. Macht bei sagen wie mal 7 Funktionen im Programm eine Erwartung von <50%, daß der er es packt.

Hier übrigens sind sum3 und sum nicht aquivalent, wegen ein paar Eingaben, wo der op* überläuft. Außer, wenn so Eingaben als Fehleingaben abgelehnt werden, dann erst wären die Progs wieder gleich.
Was uns dazu führt, daß zwei ansonsten aquivalente Progs allein wegen anderer Fehleingabentests unterschiedlich sind, der eine erlaubt Mehrwertsteuern <50%, der andere nur >=0% und <100%.

volkard schrieb:

unsigned sum3(unsigned n) {
    return n*(n-1)/2;
}

kleiner vorzeichenfehler. :p

volkard

Troll der Kenner schrieb:

volkard schrieb:
unsigned sum3(unsigned n) {
    return n*(n-1)/2;
}
kleiner vorzeichenfehler. :p

Nö, denn ich hab sum2 nachprogrammiert und nicht sum. Die beiden sind nämlich schon total verschieden.

Jester

@Ethon: was ist mit meiner anderen Frage?

volkard schrieb:

Nö, denn ich hab sum2 nachprogrammiert und nicht sum. Die beiden sind nämlich schon total verschieden.

hoppla, ich hab' übersehen, dass die beiden nicht gleich sind (inklusiv / exklusiv). hab' Ethon blind vertraut. entschuldigung volkard!