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, which is locally bottom-avoiding. We use a small-step operational semantics in form of a normal order reduction. As equational theory we use contextual equivalence, i.e. terms are equal if plugged into an arbitrary program context their termination behaviour is the same. We use a combination of may- as well as must-convergence, which is appropriate for non-deterministic computations. We evolve different proof tools for proving correctness of program transformations. We provide a context lemma for may- as well as must- convergence 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 keep contextual equivalence. In contrast to other approaches our syntax as well as semantics does not make use of a heap for sharing expressions. Instead we represent these expressions explicitely via letrec-bindings.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 24 
Y1  - 2006
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2829
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-25758
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/sabel/frank-24-ambcalc.pdf
IS  - Version: 13 Januar 2006
EP  - 67
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -