On generic context lemmas for lambda calculi with sharing
- This paper proves several generic variants of context lemmas and thus contributes to improving the tools for observational semantics of deterministic and non-deterministic higher-order calculi that use a small-step reduction semantics. The generic (sharing) context lemmas are provided for may- as well as two variants of must-convergence, which hold in a broad class of extended process- and extended lambda calculi, if the calculi satisfy certain natural conditions. As a guide-line, the proofs of the context lemmas are valid in call-by-need calculi, in callby-value calculi if substitution is restricted to variable-by-variable and in process calculi like variants of the π-calculus. For calculi employing beta-reduction using a call-by-name or call-by-value strategy or similar reduction rules, some iu-variants of ciu-theorems are obtained from our context lemmas. Our results reestablish several context lemmas already proved in the literature, and also provide some new context lemmas as well as some new variants of the ciu-theorem. To make the results widely applicable, we use a higher-order abstract syntax that allows untyped calculi as well as certain simple typing schemes. The approach may lead to a unifying view of higher-order calculi, reduction, and observational equality.
Verfasserangaben: | Manfred Schmidt-SchaußORCiDGND, David SabelORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-344287 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-27_v3.pdf |
Titel des übergeordneten Werkes (Englisch): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 27 |
Schriftenreihe (Bandnummer): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (27 [v.3]) |
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): | 19.06.2008 |
Datum der Erstveröffentlichung: | 19.06.2008 |
Veröffentlichende Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Datum der Freischaltung: | 08.07.2014 |
Freies Schlagwort / Tag: | context lemma; functional programming languages; lambda calculus; observational semantics |
Ausgabe / Heft: | Version: 19 Juni 2008 |
Seitenzahl: | 36 |
Letzte Seite: | 36 |
HeBIS-PPN: | 344379663 |
Institute: | Informatik und Mathematik / Informatik |
DDC-Klassifikation: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Lizenz (Deutsch): | Deutsches Urheberrecht |