David Sabel: Semantics of a Call-by-Need Lambda Calculus with McCarthy's amb for Program Equivalence

Zusammenfassung

Die Korrektheit von Programmtransformationen, wie sie in Compilern moderner Programmiersprachen verwendet werden, ist unabdingbar, da sie dem Programmierer Verlässlichkeit des Compilers gewährleistet und die Sicherheit der erstellten Programme erhöht.

Da nebenläufige und parallele Programmierung immer mehr an Bedeutung gewinnen, wird in diesem Vortrag über die Untersuchung eines nichtdeterministischen erweiterten call-by-need Lambda-Kalkül berichtet, der aufgrund seiner nebenläufigen Auswertung, die auch die Betrachtung von Fairness erfordert, als Modell einer nebenläufigen funktionalen Programmiersprache gesehen werden kann.

Neben rekursiven let-Ausdrücken, Datenkonstruktoren, case-Ausdrücken und seq zur sequentiellen Auswertung, enthält der Kalkül den nichtdeterministischen Operator amb. Angewendet auf zwei Argumente wählt dieser nichtdeterministisch eines der beiden Argumente, wobei er divergierende Argumente vermeiden muss. Der Operator kann implementiert werden, indem für beide Argumente eine nebenläufige Auswertung gestartet wird und der erste erhaltene Wert als Gesamtresultat übernommen wird.

Eine Programmtransformation ist korrekt, wenn sie die Programmgleichheit erhält. Als Gleichheitsbegriff dient hierbei kontextuelle Äquivalenz, d.h. zwei Programme sind gleich, wenn sie eingesetzt in allen beliebigen Programmen als Unterprogramm das gleiche Verhalten sowohl bezüglich may- als auch bezüglich must-Konvergenz aufweisen. Ein Programm ist may-konvergent, wenn es zu einer schwachen Kopfnormalform reduziert werden kann; es ist must-konvergent, wenn jeder Nachfolger bezüglich der Reduktion may-konvergent bleibt.

Neben Methoden und Techniken zum Nachweis der Korrektheit von Programmtransformationen wird im Vortrag eine abstrakte Maschine vorgestellt, die amb-Programme auswerten kann.

Folien vom Vortrag