Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

TL;DR

The paper studies encodings between sequential resource-aware computation and concurrent session-based interaction in the presence of non-determinism and failures. It defines a new resource lambda calculus with non-determinism and explicit failure, extends it with sharing, and then encodes the resulting system into a session-typed pi-calculus via a two-step encoding. The authors prove type preservation, operational correspondence, and success-sensitivity under Gorla/Kouzapas criteria, illustrating how resource absence or excess in sequential evaluation can be modeled as interaction protocols. This work bridges non-idempotent intersection-type reasoning in sequential settings with session-type protocols in concurrency, offering a formal pathway to reason about resource-aware programming across paradigms and informing the design of functional-concurrent languages with resource guarantees.

Abstract

We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of lambdafail into spi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in lambdafail via typed processes in spi. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.

Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

TL;DR

The paper studies encodings between sequential resource-aware computation and concurrent session-based interaction in the presence of non-determinism and failures. It defines a new resource lambda calculus with non-determinism and explicit failure, extends it with sharing, and then encodes the resulting system into a session-typed pi-calculus via a two-step encoding. The authors prove type preservation, operational correspondence, and success-sensitivity under Gorla/Kouzapas criteria, illustrating how resource absence or excess in sequential evaluation can be modeled as interaction protocols. This work bridges non-idempotent intersection-type reasoning in sequential settings with session-type protocols in concurrency, offering a formal pathway to reason about resource-aware programming across paradigms and informing the design of functional-concurrent languages with resource guarantees.

Abstract

We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of lambdafail into spi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in lambdafail via typed processes in spi. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.

Paper Structure

This paper contains 18 sections, 8 theorems, 24 equations, 5 figures.

Table of Contents

  1. Contributions
  2. Organization
  3. Overview of Key Ideas
  4. Non-determinism.
  5. Successful Reductions
  6. Explicit Failure.
  7. Typability and Well-formedness
  8. Controlling resources via sharing
  9. Encoding $\lambda^{\lightning}_{\oplus}\xspace$ into $\mathsf{s}\pi$.
  10. λ^↯_⊕: A λ-calculus with Non-Determinism and Failure
  11. Syntax
  12. Reduction Semantics
  13. Well-formed λ^↯_⊕-Expressions
  14. Intersection Types
  15. Well-formed Expressions (in )
  16. ...and 3 more sections

Key Result

Proposition 2.12

For all $\mathbb{N}$, $\mathbb{N}_1$, $\mathbb{N}_2$ in $\lambda^{\lightning}_{\oplus}\xspace$ s.t. $\mathbb{N} \longrightarrow \mathbb{N}_1$, $\mathbb{N} \longrightarrow \mathbb{N}_2$ with $\mathbb{N}_1 \neq \mathbb{N}_2$ then there exists $\mathbb{M}$ such that $\mathbb{N}_1 \longrightarrow \mathb

Figures (5)

  • Figure 1: Overview of our approach.
  • Figure 2: Reduction Rules for $\lambda^{\lightning}_{\oplus}\xspace$
  • Figure 3: Typing Rules for $\lambda_{\oplus}$
  • Figure 4: Well-Formed Rules for $\lambda^{\lightning}_{\oplus}$
  • Figure 5:

Theorems & Definitions (39)

  • Definition 2.1: Syntax of $\lambda^{\lightning}_{\oplus}$
  • Example 2.2
  • Definition 2.5: Set and Multiset of Free Variables
  • Definition 2.7: Head
  • Definition 2.8: Linear Head Substitution
  • Definition 2.9: Term and Expression Contexts
  • Example 2.11: Cont. Example \ref{['ex:terms']}
  • Example 2.12
  • Proposition 2.12: Diamond Property for $\lambda^{\lightning}_{\oplus}$
  • proof : Proof (Sketch)
  • ...and 29 more