Äquivalenz zweier Programme



  • Marthog schrieb:

    Ethon hat "endliche Eingabemenge" geschrieben und das funktioniert. Bei einem Programm, dass endlich viele Eingaben hat, kann man alle durchprobieren und so unter der Annahme, dass genug Speicher zur verfuegung steht, auf Gleichheit ueberpruefen.

    nur unter der Voraussetzung, dass beide Programme für alle Eingaben anhalten ➡ Halteproblem, wie schon erwähnt



  • Marthog schrieb:

    Ethon hat "endliche Eingabemenge" geschrieben und das funktioniert. Bei einem Programm, dass endlich viele Eingaben hat, kann man alle durchprobieren und so unter der Annahme, dass genug Speicher zur verfuegung steht, auf Gleichheit ueberpruefen.

    seit wann schlussfolgert "endliche eingabemenge" eine endliche laufzeit? 😕
    besser nochmals nachschlagen was das halteproblem ist.



  • freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡



  • Troll der Kenner schrieb:

    seit wann schlussfolgert "endliche eingabemenge" eine endliche laufzeit? 😕
    besser nochmals nachschlagen was das halteproblem ist.

    wenn man die Ausgabe vergleichen soll, muss es natuerlich eine geben. Damit ist auch nach der Voraussetzung klar, dass das Programm terminiert und aus sinnvollen Gruenden bringt es auch in akzeptabler Zeit ein Ergebnis.



  • Marthog schrieb:

    Troll der Kenner schrieb:

    seit wann schlussfolgert "endliche eingabemenge" eine endliche laufzeit? 😕
    besser nochmals nachschlagen was das halteproblem ist.

    wenn man die Ausgabe vergleichen soll, muss es natuerlich eine geben. Damit ist auch nach der Voraussetzung klar, dass das Programm terminiert und aus sinnvollen Gruenden bringt es auch in akzeptabler Zeit ein Ergebnis.

    Also nochmal langsam. Nur weil ich von einem Programm die Ausgabe haben will, terminiert dieses automatisch? Das ist ja nett 😉



  • Marthog schrieb:

    wenn man die Ausgabe vergleichen soll, muss es natuerlich eine geben. Damit ist auch nach der Voraussetzung klar, dass das Programm terminiert und aus sinnvollen Gruenden bringt es auch in akzeptabler Zeit ein Ergebnis.

    der threadersteller fragte aber wie man zwei programme vergleichen kann. wie zwei shorts miteinander verglichen werden sollte jedem hier klar sein.

    akzeptable zeit? schwammiger begriff. mein programm, das mit brute-force prueft, ob 2^127-1 eine primzahl ist, ist meiner meinung nach ebenso akzeptabel wie dasjenige, das den lucas-lehmer-test verwendet. wenn du keine fixe grenze fuer "akzeptabel" angeben kannst, ist deine aussage nichtig. wenn du eine angeben kannst, dann zeige ich dir mit dem heap-paradoxon, dass diese sinnlos und willkuerlich ist.



  • cooky451 schrieb:

    freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡

    doch nicht so easy, equal hat als dritten parameter first der zweiten sequenz, nicht last.



  • Da müsste man definieren was äquivalent ist.
    Wenn damit gemeint ist dass ein bestimmtes Eingabe-Tupel ein gewisses Ausgabe-Tupel erzeugt dann wird das mit dem Beweis nichts, siehe Halteproblem. Kann sicherlich ein Problem so verhunzen dass es in O(n!) anstatt O(n) läuft.



  • cooky451 schrieb:

    freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡

    Auf endlichen Eingabemengen gibt dieser Code bei mir das gleiche Resultat wie das Programm

    return reinretpret_cast<std::vector*>(61262)->empty();
    

    Sind die beiden Programme jetzt gleich oder war das jetzt Zufall?



  • equipotential schrieb:

    cooky451 schrieb:

    freakC++ schrieb:

    welche Methoden kennt ihr, um die Äquivalenz zweier Programme zu beweisen?

    return p1bytes.size() == p2bytes.size() && equal(p1bytes.begin(), p1bytes.end(), p2bytes.end());
    

    Easy peasy lemon squeezy. Zumindest für gleiche Programme. 🤡

    Auf endlichen Eingabemengen gibt dieser Code bei mir das gleiche Resultat wie das Programm

    return reinretpret_cast<std::vector*>(61262)->empty();
    

    Sind die beiden Programme jetzt gleich oder war das jetzt Zufall?

    Auf was willst du hinaus? Er hat nur den Quelltext auf Äquivalenz geprüft und das ist definitiv eine valide Möglichkeit Algorithmen auf Äquivalenz zu prüfen.

    Troll der Kenner schrieb:

    Ethon schrieb:

    Eine andere Möglichkeit wäre bei Programmen mit endlicher Eingabemenge und ohne Seiteneffekten sämtliche Eingabemöglichkeiten per Bruteforce zu probieren und den Output auf Äquivalenz zu prüfen. Der Eingabebereich muss natürlich limitiert sein. Das funktioniert für ein Programm, das 2 shorts entgegennimmt, nicht aber für ein Programm das 2 beliebige Strings entgegen nimmt.

    mit dieser methode kannst du nur semi-entscheiden ob sie gleich sind -> halteproblem.

    Theoretisch ja, praktisch aber mMn. nach ausreichend.



  • 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.

    funktioniert auch nur begrenzt (sofern man davon ausgeht dass computer fuer mathematische beweise nicht geeignet sind, was sie derzeit definitiv nicht sind). beispiel:

    //programm 1:
    double pi_square_div_6() //gibt pi^2/6 aus
    {
        //approximation mit einem big_float und summation der kehrwerte der quadrate der natuerlichen zahlen
    }
    //programm 2:
    double pi_square_div_6()
    {
        //monte-carlo-apporximation von pi mit einem zaehler + aes als zufallsquelle, dann / 6
    }
    //programm 3:
    double pi_square_div_6()
    {
        //numerische approximation an zeta(2)
    }
    

    dass die vom compiler generierten assembler-instruktionen in irgendeiner weise maschinell beweisbar zusammenhaengen wage ich sehr zu bezweifeln.

    fuer simple aufgaben ist diese herangehensweise allerdings interessant, da fallen mir spontan spannende faelle fuer rekursiv / iterativ ein (mit zyklischen graphen / flussdiagrammen). maschinell iterativen c++-code in eine rekursive form bringen? koestlich!



  • Ethon schrieb:

    Auf was willst du hinaus? Er hat nur den Quelltext auf Äquivalenz geprüft und das ist definitiv eine valide Möglichkeit Algorithmen auf Äquivalenz zu prüfen.

    Sein Code war UB, meiner auch.
    Ich wollte hinaus, dass nur weil der Code einmal etwas ausgibt, er das nächste mal etwas völlig anderes ausgeben kann, warum auch immer (UB, rand(), externe Abhängigkeit, etc.).

    Ethon schrieb:

    Troll der Kenner schrieb:

    Ethon schrieb:

    Eine andere Möglichkeit wäre bei Programmen mit endlicher Eingabemenge und ohne Seiteneffekten sämtliche Eingabemöglichkeiten per Bruteforce zu probieren und den Output auf Äquivalenz zu prüfen. Der Eingabebereich muss natürlich limitiert sein. Das funktioniert für ein Programm, das 2 shorts entgegennimmt, nicht aber für ein Programm das 2 beliebige Strings entgegen nimmt.

    mit dieser methode kannst du nur semi-entscheiden ob sie gleich sind -> halteproblem.

    Theoretisch ja, praktisch aber mMn. nach ausreichend.

    Man kann mit dieser Methode maximal beweisen, dass sie nicht gleich sind (wenn sie terminieren ein unterschiedliches Resultat ergeben), noch dass sie gleich sind (selbst wenn sie das gleiche Resultat ausspucken, sie könnten mit Wahrscheinlichkeit von 10^-80 ein falsches Resultat liefern).


  • Mod

    equipotential schrieb:

    Man kann mit dieser Methode maximal beweisen, dass sie nicht gleich sind (wenn sie terminieren ein unterschiedliches Resultat ergeben), noch dass sie gleich sind (selbst wenn sie das gleiche Resultat ausspucken, sie könnten mit Wahrscheinlichkeit von 10^-80 ein falsches Resultat liefern).

    Wenn wir vom theoretischen Idealbild ausgehen, dann ist die Maschine streng deterministisch. Diese Faktoren, die in diesem Beispiel dafuer sorgen, dass manchmal etwas anderes rauskommen kann, sind ein versteckter Teil der Eingabemenge.



  • 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?



  • Was ist denn der Graph eines Algorithmus?

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



  • 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.



  • 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.



  • 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.



  • 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.



  • 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%.


Anmelden zum Antworten