On equivalences and standardization in a non-deterministic call-by-need lambda calculus

The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in an extended lambda-calculus LS with case, constructors, seq, let, and choice, with a simple set of reduction rules; and to argue that an approximation calculus LA is equivalent to LS w.r.t. the contextual preorder, which enables the proof tool of simulation. Unfortunately, a direct proof appears to be impossible. The correctness proof is by defining another calculus L comprising the complex variants of copy, case-reduction and seq-reductions that use variable-binding chains. This complex calculus has well-behaved diagrams and allows a proof of correctness of transformations, and that the simple calculus LS, the calculus L, and the calculus LA all have an equivalent contextual preorder.

Metadaten
Verfasserangaben:	Manfred Schmidt-Schauß ORCiD GND, Matthias Mann
URN:	urn:nbn:de:hebis:30:3-344517
URL:	http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank31-approxcalc-v3.pdf
Titel des übergeordneten Werkes (Englisch):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 31
Schriftenreihe (Bandnummer):	Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (31 [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):	18.09.2009
Datum der Erstveröffentlichung:	18.09.2009
Veröffentlichende Institution:	Universitätsbibliothek Johann Christian Senckenberg
Datum der Freischaltung:	08.07.2014
Auflage:	Rev. version, 18. September 2008
Seitenzahl:	27
HeBIS-PPN:	365995592
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

Open Access