TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Mann, Matthias
T1  - On equivalences and standardization in a non-deterministic call-by-need lambda calculus
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik
N2  - 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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 31 [v.2] 
Y1  - 2007
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34450
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344508
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank31-approxcalc-v2.pdf
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
CY  - Frankfurt am Main
ER  -