Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Node Replication: Theory And Practice

Delia Kesner, Loïc Peyrot, Daniel Ventura

TL;DR

This work introduces λR, a term-calculus for node replication that captures higher-order sharing by splitting values into skeletons and multiset MFEs. It provides an internal machinery to realize two evaluation strategies—call-by-name and a fully lazy call-by-need—through distance-based reductions and skeleton extraction, without relying on external meta-level definitions. A non-idempotent intersection type system is developed to give quantitative characterisations of termination and reduction length, and it is shown that name and fully lazy strategies are observationally equivalent using these type-theoretic tools. The results bridge Curry-Howard interpretations of deep inference with practical sharing mechanisms, offering a concise framework for implementing and reasoning about fully lazy sharing in functional languages and linking to prior work on explicit substitutions and graph-reduction formalisms.

Abstract

We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.

Node Replication: Theory And Practice

TL;DR

This work introduces λR, a term-calculus for node replication that captures higher-order sharing by splitting values into skeletons and multiset MFEs. It provides an internal machinery to realize two evaluation strategies—call-by-name and a fully lazy call-by-need—through distance-based reductions and skeleton extraction, without relying on external meta-level definitions. A non-idempotent intersection type system is developed to give quantitative characterisations of termination and reduction length, and it is shown that name and fully lazy strategies are observationally equivalent using these type-theoretic tools. The results bridge Curry-Howard interpretations of deep inference with practical sharing mechanisms, offering a concise framework for implementing and reasoning about fully lazy sharing in functional languages and linking to prior work on explicit substitutions and graph-reduction formalisms.

Abstract

We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.
Paper Structure (26 sections, 62 theorems, 42 equations, 5 figures)

This paper contains 26 sections, 62 theorems, 42 equations, 5 figures.

Table of Contents

  1. Introduction
  2. The Atomic Lambda-Calculus.
  3. Call-by-Name, Call-by-Value, Call-by-Need.
  4. Full laziness.
  5. Quantitative Types
  6. Contributions.
  7. A Calculus for Node Replication
  8. Syntax
  9. Operational semantics
  10. Levels
  11. Operational Properties
  12. Termination of $\rightarrow_{\mathtt{sub}}$
  13. Simulations
  14. Confluence
  15. Encoding Evaluation Strategies
  16. ...and 11 more sections

Key Result

Lemma 2.4

Let $x \neq z$, $t \in \mathtt{T}_{R}$ and $p \in \mathtt{T}_{P}$:

Figures (5)

  • Figure 1: Call-by-Name Strategy
  • Figure 2: Relation $\Downarrow^{\theta}$: Splitting Skeleton and MFEs in Big-Step Semantics
  • Figure 3: Relation $\rightarrow_{\mathtt{st}}$: Splitting Skeleton and MFEs in Small-Step Semantics
  • Figure 4: Call-by-Need Strategy
  • Figure 5: Typing System $\cap R$

Theorems & Definitions (132)

  • Example 2.1
  • Example 2.2
  • Example 2.3
  • Example 2.4
  • Lemma 2.4
  • proof
  • Lemma 2.4
  • proof
  • Lemma 3.1
  • proof
  • ...and 122 more