• Treffer 5 von 5
Zurück zur Trefferliste

A finite simulation method in a non-deterministic call-by-need calculus with letrec, constructors and case

  • The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus’ semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as nondeterminism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe’s proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.

Volltext Dateien herunterladen

Metadaten exportieren

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Manfred Schmidt-SchaußORCiDGND, Elena Machkasova
URN:urn:nbn:de:hebis:30:3-344298
URL:http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank32-finsim-v2.pdf
Titel des übergeordneten Werkes (Englisch):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 32
Schriftenreihe (Bandnummer):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (32 [v.2])
Verlag:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
Verlagsort:Frankfurt am Main
Dokumentart:Arbeitspapier
Sprache:Englisch
Datum der Veröffentlichung (online):23.07.2009
Datum der Erstveröffentlichung:23.07.2009
Veröffentlichende Institution:Universitätsbibliothek Johann Christian Senckenberg
Datum der Freischaltung:08.07.2014
GND-Schlagwort:Programmiersprache; Lambda-Kalkül; Operationale Semantik
Ausgabe / Heft:Version: 23 Juli 2009
Seitenzahl:60
Letzte Seite:60
HeBIS-PPN:344379698
Institute:Informatik und Mathematik / Informatik
DDC-Klassifikation:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Lizenz (Deutsch):License LogoDeutsches Urheberrecht