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/8/13

Y1 - 2008/8/13

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 -