Mateusz Pyzik - Call-By-Name Is Just Call-By-Value with Delimited Control

entics:10502 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII -
Call-By-Name Is Just Call-By-Value with Delimited ControlArticle

Authors: Mateusz Pyzik

    Delimited control operator shift0 exhibits versatile capabilities: it can express layered monadic effects, or equivalently, algebraic effects. Little did we know it can express lambda calculus too! We present $ \Lambda_\$ $, a call-by-value lambda calculus extended with shift0 and control delimiter $ \$ $ with carefully crafted reduction theory, such that the lambda calculus with beta and eta reductions can be isomorphically embedded into $ \Lambda_\$ $ via a right inverse of a continuation-passing style translation. While call-by-name reductions of lambda calculus can trivially simulate its call-by-value version, we show that addition of shift0 and $ \$ $ is the golden mean of expressive power that suffices to simulate beta and eta reductions while still admitting a simulation back. As a corollary, calculi $ \Lambda\mu_v $, $ \lambda_\$ $, $ \Lambda_\$ $ and $ \lambda $ all correspond equationally.

    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: January 19, 2023
    Submitted on: December 19, 2022
    Keywords: Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 109 times.
    This article's PDF has been downloaded 107 times.