Warum ist der kleinste Fixpunkt (lfp) in der Programmanalyse wichtig?

11

Ich versuche, ein Gesamtbild über die Bedeutung des kleinsten Fixpunkts (lfp) in der Programmanalyse zu erhalten. Zum Beispiel scheint die abstrakte Interpretation die Existenz von lfp zu nutzen. Viele Forschungsarbeiten zur Programmanalyse konzentrieren sich auch stark darauf, den am wenigsten festgelegten Punkt zu finden.

In diesem Artikel in Wikipedia: Knaster-Tarski Theorem wird genauer erwähnt, dass lfp zur Definition der Programmsemantik verwendet wird.

Warum ist es wichtig? Jedes einfache Beispiel hilft mir. (Ich versuche ein großes Bild zu bekommen).

BEARBEITEN

Ich denke, mein Wortlaut ist falsch. Ich fordere die Bedeutung von lfp nicht heraus. Meine genaue Frage (Anfänger) lautet: Wie hilft die Berechnung von lfp bei der Programmanalyse? Zum Beispiel, warum / wie abstrakte Interpretation lfp verwendet? Was passiert, wenn im abstrakten Bereich kein LFP vorhanden ist?

Hoffentlich ist meine Frage jetzt konkreter.

RAM
quelle
@DW Dies ist eine Anfängerfrage in der Programmanalyse. Ich habe mich mehrmals diskutiert, bevor ich die Frage gestellt habe, ob sie zu vage aussieht. Was ich suche ist: Welche Rolle spielt lfp bei der Programmanalyse (Es ist sicher wichtig, aber wie?). Ich suche nach einer Antwort, die sich nicht mit vielen mathematischen Details befasst. Ich denke, der Wortlaut in meiner Frage ist auch nicht klar. Ich werde die Frage bearbeiten.
Ram
@ DW Ich stimme zu, dass dies möglicherweise keine gut recherchierte Frage ist. Wenn ich jedoch weiter Papiere lese, viele mathematische Details und ich verliere schnell das große Ganze. Konkreter erscheint mir dieses Papier [Erweiterung für Kontrollfluss] ( berkeleychurchill.com/research/papers/vmcai14.pdf ) sehr abstrakt. Es spricht direkt die Berechnung des kleinsten Fixpunkts an. Die meisten Arbeiten in der Programmanalyse scheinen sich in ähnlicher Weise mit dieser Frage zu befassen. Ich habe das große Ganze verloren. Ich bin froh zu wissen, warum es wichtig ist, lfp zu berechnen.
Ram

Antworten:

13

Jede Form der Rekursion oder Iteration in der Programmierung ist tatsächlich ein fester Punkt. Zum Beispiel wird eine whileSchleife durch die Gleichung charakterisiert

while b do c done  ≡  if b then (c ; while b do c done)

das heißt, das while b do c doneist eine Lösung Wder Gleichung

W  ≡  Φ(W)

wo Φ(x) ≡ if b then (c ; x). Aber was ist, wenn Φes viele Fixpunkte gibt? Welches entspricht der whileSchleife? Eine der grundlegenden Erkenntnisse der Programmiersemantik ist, dass dies der am wenigsten festgelegte Punkt ist.

Nehmen wir ein einfaches Beispiel, diesmal Rekursion. Ich werde Haskell benutzen. Die rekursive Funktion fdefiniert durch

f :: a -> a
f x = f x

ist die überall undefinierte Funktion, weil sie nur für immer läuft. Wir können diese Definition auf ungewöhnlichere Weise umschreiben (aber es funktioniert immer noch in Haskell) als

f :: a -> a
f = f

So fist ein Fixpunkt der Identitätsfunktion:

f ≡ id f

Aber jede Funktion ist ein fester Punkt von id. Unter der üblichen domänen-theoretischen Reihenfolge ist "undefiniert" das kleinste Element. Und in der Tat ist unsere Funktion fdie überall undefinierte Funktion.

Auf Anfrage hinzugefügt: In den Kommentaren fragte OP nach der Teilreihenfolge für Semantikschleifen while(Sie haben angenommen, es sei ein Gitter, aber es muss nicht sein). Eine allgemeinere Frage ist die domänen-theoretische Interpretation einer prozeduralen Sprache, die Variablen manipulieren kann und die grundlegenden Kontrollstrukturen (Bedingungen und Schleifen) aufweist. Es gibt verschiedene Möglichkeiten, dies zu tun, je nachdem, was genau Sie erfassen möchten. Um die Dinge einfach zu halten, nehmen wir an, dass wir eine feste Anzahl globaler Variablennx1,,xndass das Programm lesen und aktualisieren kann und sonst nichts (keine E / A oder Ausnahmen oder Zuweisung neuer Variablen). In diesem Fall kann ein Programm als Transformation des Anfangszustands der Variablen in den Endzustand oder als undefinierter Wert angesehen werden, wenn das Programm zyklisch abläuft. Wenn also jede Variable ein Element einer Menge , entspricht ein Programm einer Zuordnung : für jede Anfangskonfiguration der Variablen wird das Programm entweder divergieren und , oder es wird beendet und den Endzustand erzeugt, der ein Element von . Die Menge aller Zuordnungen ist eine Domäne:V.V.nV.n{}}(v1,,vn)V.nV.nV.nV.n{}}

  • V.n{}}V.nV.nV.n{}}
  • while true do skip done
  • Jede zunehmende Sequenz hat ein Supremum

Nur um Ihnen eine Vorstellung davon zu geben, wie dies funktioniert, die Semantik des Programms

x_1 := e

(v1,,vn)V.nvee(v1,,vn)(ve,v2,,vn)

Andrej Bauer
quelle
1
+1 für das while-Beispiel. Ich bin jedoch etwas verwirrt. But what if Φ has many fixed points?Während ich die Fixpunktgleichung verstehe, ist in diesem Zusammenhang W \ in L? Wie definieren wir hier Gitter? Ich freue mich über Ihre weitere Ausarbeitung.
Ram
Im obigen Kommentar verwende ich "L", um für ein Gitter (oder einen Poset) zu stehen
Ram
Ich habe die Antwort geändert.
Andrej Bauer
Danke für das Update. Ich schätze es besonders, weil es mir eine andere Sicht auf das Betrachten von Programmen gab. Ich lese jetzt "Fixpunkttheorie" aus "Semantik mit Anwendungen: Eine formale Einführung" von Nielson, die die Ansicht über die Konstruktion eines Gitters aus Teilfunktionen für die IMP-Sprache vervollständigte.
Ram
6

Hier ist die Intuition: Die kleinsten Fixpunkte helfen Ihnen bei der Analyse von Schleifen.

Bei der Programmanalyse wird das Programm ausgeführt, wobei jedoch einige Details der Daten abstrahiert werden. Das ist alles gut. Die Abstraktion hilft dabei, die Analyse schneller durchzuführen als das eigentliche Ausführen des Programms, da Sie Aspekte ignorieren können, die Sie nicht interessieren. So funktioniert beispielsweise die abstrakte Interpretation: Sie simuliert im Grunde die Ausführung des Programms, verfolgt jedoch nur Teilinformationen über den Status des Programms.

Das Knifflige ist, wenn Sie zu einer Schleife kommen. Die Schleife könnte viele, viele Male ausgeführt werden. Normalerweise möchten Sie nicht, dass Ihre Programmanalyse alle diese Iterationen der Schleife ausführen muss, da die Programmanalyse dann lange dauert ... oder möglicherweise nicht einmal beendet wird. Hier verwenden Sie also einen am wenigsten festen Punkt. Der am wenigsten festgelegte Punkt kennzeichnet im Grunde genommen, was Sie mit Sicherheit sagen können, wird nach Beendigung der Schleife wahr sein, wenn Sie nicht wissen, wie oft die Schleife iteriert.

Dafür wird der am wenigsten feste Punkt verwendet. Da in allen Programmen Schleifen vorhanden sind, werden in der gesamten Programmanalyse die kleinsten Fixpunkte verwendet. Kleinste Fixpunkte sind wichtig, da Schleifen überall sind und es wichtig ist, Schleifen analysieren zu können.

Übrigens sind Rekursion und gegenseitige Rekursion nur eine andere Form der Schleife - daher werden auch sie mit einem am wenigsten festen Punkt behandelt.

DW
quelle