Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, Alan Schmitt

TL;DR

The paper addresses faithfully encoding the call-by-name and call-by-value $\lambda$-calculus into the minimal higher-order process calculus $HOcore$, despite its lack of name restriction. It fixes the evaluation strategy and internalizes three core notions of equivalence—normal-form bisimilarity, applicative bisimilarity, and contextual equivalence—via extended abstract machines (KAM/CK and their nf/bisimilarity variants) and then translates these machines into $HOcore$, proving full abstraction in each case. The technique scales to the $\lambda\mu$-calculus with control operators by extending the machines and translations accordingly, including handling of continuations and named binders. This shows that a compact process calculus with a finite set of hidden names suffices to faithfully encode essential operational and observational aspects of $\lambda$-calculus, including continuation-related features, and points toward automated derivations and cross-pollination with process-calculus proof techniques.

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 encodings. We also demonstrate that this technique scales to the $λμ$-calculus, i.e., a standard extension of the $λ$-calculus with control operators.

Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines

TL;DR

The paper addresses faithfully encoding the call-by-name and call-by-value -calculus into the minimal higher-order process calculus , despite its lack of name restriction. It fixes the evaluation strategy and internalizes three core notions of equivalence—normal-form bisimilarity, applicative bisimilarity, and contextual equivalence—via extended abstract machines (KAM/CK and their nf/bisimilarity variants) and then translates these machines into , proving full abstraction in each case. The technique scales to the -calculus with control operators by extending the machines and translations accordingly, including handling of continuations and named binders. This shows that a compact process calculus with a finite set of hidden names suffices to faithfully encode essential operational and observational aspects of -calculus, including continuation-related features, and points toward automated derivations and cross-pollination with process-calculus proof techniques.

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 encodings. We also demonstrate that this technique scales to the -calculus, i.e., a standard extension of the -calculus with control operators.
Paper Structure (31 sections, 22 theorems, 79 equations, 13 figures)

This paper contains 31 sections, 22 theorems, 79 equations, 13 figures.

Table of Contents

  1. Introduction
  2. The Calculus HOcore
  3. Encoding the Krivine Abstract Machine
  4. Definition of the KAM
  5. Translation into HOcore
  6. Normal-Form Bisimilarity
  7. Normal-Form Bisimilarity
  8. Abstract Machine
  9. Translation into HOcore
  10. Operational Correspondence and Full Abstraction
  11. Applicative Bisimilarity
  12. The KAM and Behavioral Equivalences
  13. Argument Generation for the Applicative Bisimilarity
  14. Translation into HOcore
  15. Internalizing Contextual Equivalence
  16. ...and 16 more sections

Key Result

Theorem 3.1

In the forward direction, if $C \mapsto^{*} C'$, then $\left\ldbrack C \right\rdbrack \mathrel{\xRightarrow{\hbox{\scriptsize $\tau$}}} \left\ldbrack C' \right\rdbrack$. In the backward direction, if $\left\ldbrack C \right\rdbrack \mathrel{\xRightarrow{\hbox{\scriptsize $\tau$}}} P$, then there exi

Figures (13)

  • Figure 1: HOcore LTS
  • Figure 2: NFB Machine
  • Figure 3: Translation of the NFB machine into HOcore
  • Figure 4: AB machine: argument generation
  • Figure 5: Example of argument generation
  • ...and 8 more figures

Theorems & Definitions (52)

  • Definition 2.1
  • Definition 2.2
  • Theorem 3.1
  • proof
  • Corollary 3.2
  • proof
  • Theorem 3.3
  • proof
  • Definition 4.1
  • Example 4.2
  • ...and 42 more