A call-by-need lambda-calculus with locally bottom-avoiding choice: context lemma and correctness of transformations
- We present a higher-order call-by-need lambda calculus enriched with constructors, case-expressions, recursive letrec-expressions, a seq-operator for sequential evaluation and a non-deterministic operator amb that is locally bottom-avoiding. We use a small-step operational semantics in form of a single-step rewriting system that defines a (nondeterministic) normal order reduction. This strategy can be made fair by adding resources for bookkeeping. As equational theory we use contextual equivalence, i.e. terms are equal if plugged into any program context their termination behaviour is the same, where we use a combination of may- as well as must-convergence, which is appropriate for non-deterministic computations. We show that we can drop the fairness condition for equational reasoning, since the valid equations w.r.t. normal order reduction are the same as for fair normal order reduction. We evolve different proof tools for proving correctness of program transformations, in particular, a context lemma for may- as well as mustconvergence is proved, which restricts the number of contexts that need to be examined for proving contextual equivalence. In combination with so-called complete sets of commuting and forking diagrams we show that all the deterministic reduction rules and also some additional transformations preserve contextual equivalence.We also prove a standardisation theorem for fair normal order reduction. The structure of the ordering <=c a is also analysed: Ω is not a least element, and <=c already implies contextual equivalence w.r.t. may-convergence.
Author: | David SabelORCiDGND, Manfred Schmidt-SchaußORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-344265 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/sabel/frank-24-ambcalcV3.pdf |
Parent Title (English): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 24 |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (24 [v.3]) |
Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik |
Place of publication: | Frankfurt am Main |
Document Type: | Working Paper |
Language: | English |
Date of Publication (online): | 2008/02/19 |
Date of first Publication: | 2008/02/19 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2014/07/08 |
Issue: | Version: 19 Febr. 2008 |
Page Number: | 78 |
Last Page: | 78 |
HeBIS-PPN: | 344383083 |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Licence (German): | Deutsches Urheberrecht |