-
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.
-
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.
-
Faithful (meta-)encodings of programmable strategies into term rewriting systems
Authors:
Horatiu Cirstea,
Serguei Lenglet,
Pierre-Etienne Moreau
Abstract:
Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and rewriting strategies are used to con- trol their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific…
▽ More
Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and rewriting strategies are used to con- trol their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, estab- lished termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. We show that the encoding of strategies into term rewriting systems can be easily adapted to handle many-sorted signa- tures and we use a meta-level representation of terms to reduce the size of the encodings. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; experiments in Tom show that applying our encoding leads to performances comparable to the native Tom strategies.
△ Less
Submitted 26 November, 2017; v1 submitted 24 May, 2017;
originally announced May 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.
-
Expansion for Universal Quantifiers
Authors:
Sergueï Lenglet,
J. B. Wells
Abstract:
Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the lambda-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g., intersection introduc…
▽ More
Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the lambda-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g., intersection introduction) until enough information has been gathered to make the right decision. Furthermore, these choices can be equivalent to inserting uses of such typing rules at deeply nested positions in a typing derivation, without needing to actually inspect or modify (or even have) the typing derivation. Expansion has in recent years become simpler due to the use of expansion variables (e.g., in System E).
This paper extends expansion and expansion variables to systems with forall-quantifiers. We present System Fs, an extension of System F with expansion, and prove its main properties. This system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future.
△ Less
Submitted 5 January, 2012;
originally announced January 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.
