TY  - UNPD
A1  - Sabel, David
A1  - Schmidt-Schauß, Manfred
T1  - A call-by-need lambda-calculus with locally bottom-avoiding choice: context lemma and correctness of transformations
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 24
N2  - 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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 24 [v.2] 
Y1  - 2006
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34425
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344253
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/sabel/frank-24-ambcalcV2.pdf
IS  - Version: 31 Juli 2006
EP  - 78
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
CY  - Frankfurt am Main
ER  -