Open Access

Christopher Stamm

• Wir haben ein Softwaresystem entwickelt, das in der Lage ist, Beschreibungen von Termersetzungssystemen höherer Ordnung, deren Reduktionsregeln auf einer strukturellen operationalen Semantik basieren, einzulesen und zu interpretieren. Das System ist dabei fähig, Reduktionskontexte für die Redexsuche zu benutzen, die entweder vom Benutzer definiert werden können oder automatisch anhand der strikten Positionen berechnet werden. Außerdem dürfen Kontexte und spezielle Definitionen für Term-Mengen, die wir Domains nennen, in den Reduktionsregeln verwendet werden. Mit dem resultierenden Reduktionssystem-Format können wir somit nicht nur den „lazy“ Lambda-Kalkül, den Call-by-Value Lambda-Kalkül und verwandte, um Konstruktoren und Fallunterscheidungen erweiterte Kalküle, wie die in Kapitel 4 vorgestellten Kernsprachen KFP und PCF, darstellen, sondern auch den (in Abschnitt 4.3 vorgestellten) Call-by-Need Lambda-Kalkül, welcher sich durch die Verwendung von Kontexten innerhalb der Regeln deutlich von den anderen Kalkülen abhebt. Allerdings hält sich der Call-by-Need Lambda-Kalkül damit nicht an das in Kapitel 5 vorgestellte GDSOS-Format, das u.a. sicherstellt, dass Bisimulation eine Kongruenz ist. Wir haben dabei in Abschnitt 5.3.3 bewiesen, dass sich ein GDSOS-Reduktionssystem in ein äquivalentes strukturiertes Auswertungssystem nach Howe übersetzen lässt. Unser System ist in der Lage, die GDSOS-Bedingungen zu prüfen und gibt eine Warnung aus, falls eine der nötigen Bedingungen nicht erfüllt ist (wobei aus dieser auch gleich der Grund des Verstoßes hervorgeht). Wie wir gesehen haben, ist unser System nicht nur befähigt, die einzelnen Reduktionsschritte für kleinere Bespiele ordnungsgemäß auszuführen, sondern es ist durchaus in der Lage, auch aufwendigere KFP-Ausdrücke, wie in unserem Quicksort- Beispiel, auszuwerten.