A finite simulation method in a non-deterministic call-by-need lambda-calculus with letrec, constructors, and case

Manfred Schmidt-Schauss, Elena Machkasova

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationRewriting Techniques and Applications - 19th International Conference, RTA 2008, Proceedings
Pages321-335
Number of pages15
DOIs
StatePublished - Aug 13 2008
Event19th International Conference on Rewriting Techniques and Applications, RTA 2008 - Hagenberg, Austria
Duration: Jul 15 2008Jul 17 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5117 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Conference on Rewriting Techniques and Applications, RTA 2008
Country/TerritoryAustria
CityHagenberg
Period7/15/087/17/08

Fingerprint

Dive into the research topics of 'A finite simulation method in a non-deterministic call-by-need lambda-calculus with letrec, constructors, and case'. Together they form a unique fingerprint.

Cite this