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 ; 31
N2  - The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in a an extended lambda-calculus with case, constructors, seq, let, and choice, with a simple set of reduction rules. Unfortunately, a direct proof appears to be impossible. The correctness proof is by defining another calculus comprising the complex variants of copy, case-reduction and seq-reductions that use variablebinding chains. This complex calculus has well-behaved diagrams and allows a proof that of correctness of transformations, and also that the simple calculus defines an equivalent contextual order.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 31 
Y1  - 2007
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/510
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-50344
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank31-approxcalc.pdf
IS  - Version: 15 August 2007
EP  - 26
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  -