TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Machkasova, Elena
T1  - A finite simulation method in a non-deterministic call-by-need calculus with letrec, constructors and case
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 32
N2  - The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus' semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as non-determinism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe's proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 32 
KW  - Lambda-Kalkül
KW  - Operationale Semantik
KW  - Programmiersprache
KW  - programming languages
KW  - simulation
KW  - lambda calculus
KW  - semantics
KW  - nondeterminism
Y1  - 2008
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/191
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-53630
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank32-finsim.pdf
IS  - Version: 12 Febr. 2008
EP  - 60
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  -