-
Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines
Authors:
Małgorzata Biernacka,
Dariusz Biernacki,
Sergueï Lenglet,
Piotr Polesiuk,
Damien Pous,
Alan Schmitt
Abstract:
We present fully abstract encodings of the call-by-name and call-by-value $λ$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $λ$-calculus side -- normal-form bisimilarity, applicative bisimilarity, and contextual equivalence -- that we internalize into abstract machines in order to prove full abstraction of the encodi…
▽ More
We present fully abstract encodings of the call-by-name and call-by-value $λ$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $λ$-calculus side -- normal-form bisimilarity, applicative bisimilarity, and contextual equivalence -- that we internalize into abstract machines in order to prove full abstraction of the encodings. We also demonstrate that this technique scales to the $λμ$-calculus, i.e., a standard extension of the $λ$-calculus with control operators.
△ Less
Submitted 2 July, 2024; v1 submitted 13 May, 2022;
originally announced May 2022.
-
Automating the Functional Correspondence between Higher-Order Evaluators and Abstract Machines
Authors:
Maciej Buszka,
Dariusz Biernacki
Abstract:
The functional correspondence is a manual derivation technique transforming higher-order evaluators into the semantically equivalent abstract machines. The transformation consists of two well-known program transformations: translation to continuation-passing style that uncovers the control flow of the evaluator and Reynolds's defunctionalization that generates a first-order transition function. Ev…
▽ More
The functional correspondence is a manual derivation technique transforming higher-order evaluators into the semantically equivalent abstract machines. The transformation consists of two well-known program transformations: translation to continuation-passing style that uncovers the control flow of the evaluator and Reynolds's defunctionalization that generates a first-order transition function. Ever since the transformation was first described by Danvy et al. it has found numerous applications in connecting known evaluators and abstract machines, but also in discovering new abstract machines for a variety of $λ$-calculi as well as for logic-programming, imperative and object-oriented languages.
We present an algorithm that automates the functional correspondence. The algorithm accepts an evaluator written in a dedicated minimal functional meta-language and it first transforms it to administrative normal form, which facilitates program analysis, before performing selective translation to continuation-passing style, and selective defunctionalization. The two selective transformations are driven by a control-flow analysis that is computed by an abstract interpreter obtained using the abstracting abstract machines methodology, which makes it possible to transform only the desired parts of the evaluator. The article is accompanied by an implementation of the algorithm in the form of a command-line tool that allows for automatic transformation of an evaluator embedded in a Racket source file and gives fine-grained control over the resulting machine.
△ Less
Submitted 16 August, 2021;
originally announced August 2021.
-
An Abstract Machine for Strong Call by Value
Authors:
Małgorzata Biernacka,
Dariusz Biernacki,
Witold Charatonik,
Tomasz Drab
Abstract:
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $λ$-calculus. It is derived using Danvy et al.'s functional correspondence from Crégut's KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation function akin to Filinski and Rohde's, (2) modifying the resulting normalizer so that it implements the right-to-left call-by…
▽ More
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $λ$-calculus. It is derived using Danvy et al.'s functional correspondence from Crégut's KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation function akin to Filinski and Rohde's, (2) modifying the resulting normalizer so that it implements the right-to-left call-by-value function application, and (3) constructing the functionally corresponding abstract machine.
This new machine implements a reduction strategy that subsumes the fireball-calculus variant of call by value studied by Accattoli et al. We describe the strong strategy of the machine in terms of a reduction semantics and prove the correctness of the machine using a method based on Biernacka et al.'s generalized refocusing. As a byproduct, we present an example application of the machine to checking term convertibility by discriminating on the basis of their partially normalized forms.
△ Less
Submitted 15 September, 2020;
originally announced September 2020.
-
Bisimulations for Delimited-Control Operators
Authors:
Dariusz Biernacki,
Sergueï Lenglet,
Piotr Polesiuk
Abstract:
We present a comprehensive study of the behavioral theory of an untyped $λ$-calculus extended with the delimited-control operators shift and reset. To that end, we define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We consider different styles of bisimilarities (namely applicative, normal-form, and enviro…
▽ More
We present a comprehensive study of the behavioral theory of an untyped $λ$-calculus extended with the delimited-control operators shift and reset. To that end, we define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We consider different styles of bisimilarities (namely applicative, normal-form, and environmental) within a unifying framework, and we give several examples to illustrate their respective strengths and weaknesses. We also discuss how to extend this work to other delimited-control operators.
△ Less
Submitted 23 May, 2019; v1 submitted 23 April, 2018;
originally announced April 2018.
-
Proving Soundness of Extensional Normal-Form Bisimilarities
Authors:
Dariusz Biernacki,
Serguei Lenglet,
Piotr Polesiuk
Abstract:
Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in $λ$-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of…
▽ More
Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in $λ$-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of $η$-expansion and usually relies on ad hoc proof methods which depend on the language. In this paper we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding up to context technique are sound. We illustrate our technique with three calculi: the call-by-value $λ$-calculus, the call-by-value $λ$-calculus with the delimited-control operators shift and reset, and the call-by-value $λ$-calculus with the abortive control operators call/cc and abort. In the first two cases, there was previously no sound up to context technique validating the $η$-law, whereas no theory of normal-form bisimulations for a calculus with call/cc and abort has been presented before. Our results have been fully formalized in the Coq proof assistant.
△ Less
Submitted 28 March, 2019; v1 submitted 31 October, 2017;
originally announced November 2017.
-
Logical relations for coherence of effect subtyping
Authors:
Dariusz Biernacki,
Piotr Polesiuk
Abstract:
A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article we present heterogeneous, biorthogonal, step-indexed logical relations for establishing the coherenc…
▽ More
A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article we present heterogeneous, biorthogonal, step-indexed logical relations for establishing the coherence of coercion semantics of programming languages with subtyping. To illustrate the effectiveness of the proof method, we develop a proof of coherence of a type-directed, selective CPS translation from a typed call-by-value lambda calculus with delimited continuations and control-effect subtyping. The article is accompanied by a Coq formalization that relies on a novel shallow embedding of a logic for reasoning about step-indexing.
△ Less
Submitted 29 January, 2018; v1 submitted 25 October, 2017;
originally announced October 2017.
-
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
Authors:
Andrés Aristizábal,
Dariusz Biernacki,
Sergueï Lenglet,
Piotr Polesiuk
Abstract:
We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented…
▽ More
We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented using Madiot et al.'s framework that allows for smooth integration and composition of up-to techniques facilitating bisimulation proofs. We also generalize the framework in order to express environmental bisimulations that support equivalence proofs of evaluation contexts representing continuations. This change leads to a novel and powerful up-to technique enhancing bisimulation proofs in the presence of control operators.
△ Less
Submitted 18 September, 2017; v1 submitted 29 November, 2016;
originally announced November 2016.
-
Environmental Bisimulations for Delimited-Control Operators
Authors:
Dariusz Biernacki,
Sergueï Lenglet
Abstract:
We present a theory of environmental bisimilarity for the delimited-control operators {\it shift} and {\it reset}. We consider two different notions of contextual equivalence: one that does not require the presence of a top-level control delimiter when executing tested terms, and another one, fully compatible with the original CPS semantics of shift and reset, that does. For each of them, we devel…
▽ More
We present a theory of environmental bisimilarity for the delimited-control operators {\it shift} and {\it reset}. We consider two different notions of contextual equivalence: one that does not require the presence of a top-level control delimiter when executing tested terms, and another one, fully compatible with the original CPS semantics of shift and reset, that does. For each of them, we develop sound and complete environmental bisimilarities, and we discuss up-to techniques.
△ Less
Submitted 16 September, 2013;
originally announced September 2013.
-
Proving termination of evaluation for System F with control operators
Authors:
Małgorzata Biernacka,
Dariusz Biernacki,
Sergueï Lenglet,
Marek Materzok
Abstract:
We present new proofs of termination of evaluation in reduction semantics (i.e., a small-step operational semantics with explicit representation of evaluation contexts) for System F with control operators. We introduce a modified version of Girard's proof method based on reducibility candidates, where the reducibility predicates are defined on values and on evaluation contexts as prescribed by the…
▽ More
We present new proofs of termination of evaluation in reduction semantics (i.e., a small-step operational semantics with explicit representation of evaluation contexts) for System F with control operators. We introduce a modified version of Girard's proof method based on reducibility candidates, where the reducibility predicates are defined on values and on evaluation contexts as prescribed by the reduction semantics format. We address both abortive control operators (callcc) and delimited-control operators (shift and reset) for which we introduce novel polymorphic type systems, and we consider both the call-by-value and call-by-name evaluation strategies.
△ Less
Submitted 5 September, 2013;
originally announced September 2013.
-
Normal Form Bisimulations for Delimited-Control Operators
Authors:
Dariusz Biernacki,
Serguei Lenglet
Abstract:
We define a notion of normal form bisimilarity for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarit…
▽ More
We define a notion of normal form bisimilarity for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.
△ Less
Submitted 28 February, 2012; v1 submitted 27 February, 2012;
originally announced February 2012.
-
Applicative Bisimulations for Delimited-Control Operators
Authors:
Dariusz Biernacki,
Serguei Lenglet
Abstract:
We develop a behavioral theory for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. For this calculus, we discuss the possible observable behaviors and we define an applicative bisimilarity that characterizes contextual equivalence. We then compare the applicative bisimilarity and the CPS equivalence, a relation on terms often used in studies…
▽ More
We develop a behavioral theory for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. For this calculus, we discuss the possible observable behaviors and we define an applicative bisimilarity that characterizes contextual equivalence. We then compare the applicative bisimilarity and the CPS equivalence, a relation on terms often used in studies of control operators. In the process, we illustrate how bisimilarity can be used to prove equivalence of terms with delimited-control effects.
△ Less
Submitted 4 January, 2012;
originally announced January 2012.
-
An Operational Foundation for Delimited Continuations in the CPS Hierarchy
Authors:
Malgorzata Biernacka,
Dariusz Biernacki,
Olivier Danvy
Abstract:
We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constru…
▽ More
We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.
△ Less
Submitted 8 December, 2005; v1 submitted 8 August, 2005;
originally announced August 2005.
