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
    CountryAustria
    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