TY - GEN
T1 - A finite simulation method in a non-deterministic call-by-need lambda-calculus with letrec, constructors, and case
AU - Schmidt-Schauss, Manfred
AU - Machkasova, Elena
PY - 2008
Y1 - 2008
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 preorder, 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.
AB - 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 preorder, 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.
UR - http://www.scopus.com/inward/record.url?scp=48949085521&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=48949085521&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-70590-1_22
DO - 10.1007/978-3-540-70590-1_22
M3 - Conference contribution
AN - SCOPUS:48949085521
SN - 3540705880
SN - 9783540705888
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 321
EP - 335
BT - Rewriting Techniques and Applications - 19th International Conference, RTA 2008, Proceedings
T2 - 19th International Conference on Rewriting Techniques and Applications, RTA 2008
Y2 - 15 July 2008 through 17 July 2008
ER -