Joerg Endrullis ; Dimitri Hendriks ; Jan Willem Klop ; Andrew Polonsky - Discriminating Lambda-Terms Using Clocked Boehm Trees

lmcs:880 - Logical Methods in Computer Science, May 28, 2014, Volume 10, Issue 2 - https://doi.org/10.2168/LMCS-10(2:4)2014
Discriminating Lambda-Terms Using Clocked Boehm Trees

Authors: Joerg Endrullis ORCID-iD; Dimitri Hendriks ; Jan Willem Klop ; Andrew Polonsky

    As observed by Intrigila, there are hardly techniques available in the lambda-calculus to prove that two lambda-terms are not beta-convertible. Techniques employing the usual Boehm Trees are inadequate when we deal with terms having the same Boehm Tree (BT). This is the case in particular for fixed point combinators, as they all have the same BT. Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model P-omega of lambda-calculus, and hence valid with respect to BT-equality but nevertheless the terms are beta-inconvertible. To prove such beta-inconvertibilities, we employ `clocked' BT's, with annotations that convey information of the tempo in which the data in the BT are produced. Boehm Trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda-terms. The corresponding equality is strictly intermediate between beta-convertibility and Boehm Tree equality, the equality in the model P-omega. An analogous approach pertains to Levy-Longo and Berarducci Trees. Our refined Boehm Trees find in particular an application in beta-discriminating fixed point combinators (fpc's). It turns out that Scott's equation BY = BYS is the key to unlocking a plethora of fpc's, generated by a variety of production schemes of which the simplest was found by Boehm, stating that new fpc's are obtained by postfixing the term SI, also known as Smullyan's Owl. We prove that all these newly generated fpc's are indeed new, by considering their clocked BT's. Even so, not all pairs of new fpc's can be discriminated this way. For that purpose we increase the discrimination power by a precision of the clock notion that we call `atomic clock'.


    Volume: Volume 10, Issue 2
    Published on: May 28, 2014
    Accepted on: June 25, 2015
    Submitted on: January 21, 2011
    Keywords: Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Clock Semantics for Lambda Calculus; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 2300162793
    • Lazy Productivity; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 2300156514
    • A Term Rewriting Perspective on Program Termination; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 2300161683

    2 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 401 times.
    This article's PDF has been downloaded 234 times.