Textdokument
Semantik eines verzögert auswertenden Lambdakalküls mit McCarthy’s amb für Programmäquivalenz
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Dateien
Zusatzinformation
Datum
2009
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik
Zusammenfassung
In diesem Beitrag werden die Ergebnisse der Untersuchung eines verzögert-auswertenden Lambdakalküls höherer Ordnung mit case-Ausdrücken, rekursivem let-rec, einem seq-Operator und einem nichtdeterministischen Divergenz-vermeidenden Operatoramb dargestellt. Als Gleichheitsbegriff wird kontextuelle Äquivalenzbzgl. einer May- und Must-Konvergenz verwendet. Mithilfe syntaktischer Methoden wird die Korrektheit von Programmtransformationen nachgewiesen und die Korrektheit von Übersetzungenuntersucht.U.a.werden ein Kontextlemma, ein Standardisierungstheorem und die Gültigkeit einer endlichen Simulation gezeigt.