Resource approximation for the $λμ$-calculus

TL;DR

This work develops a resource-aware approximation framework for the $\lambda\mu$-calculus by adapting Ehrhard–Regnier's Taylor expansion to a qualitative setting. It defines a resource $\lambda\mu$-calculus with bags, linear substitutions, and a robust reduction theory, proving strong normalization and confluence. A qualitative Taylor expansion $\mathcal{T}$ is then introduced, yielding a nontrivial, sensible $\lambda\mu$-theory $=_\tau$ via $M=_\tau N$ iff $\mathrm{NF}\mathcal{T}(M)=\mathrm{NF}\mathcal{T}(N)$, together with Monotonicity and a simulation property that links term reductions to resource approximants. Applying this approximation theory yields the Stability property and the Perpendicular Lines Property, which in turn imply the non-representability of parallel-or in $\lambda\mu$. The results demonstrate that resource approximation can meaningfully extend to classical control languages and provide a foundation for further study of Böhm-like notions, differential extensions, and connections to Krivine’s realizability.

Abstract

The $λμ$-calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not satisfy Böhm's Theorem and it lacks the corresponding notion of approximation. On the contrary, we show that Ehrhard and Regnier's Taylor expansion can be easily adapted, thus providing a resource conscious approximation theory. This produces a sensible $λμ$-theory with which we prove some advanced properties of the $λμ$-calculus, such as Stability and Perpendicular Lines Property, from which the impossibility of parallel computations follows.

Figures (7)

• Figure 1: Definition of linear substitution
• Figure 2: Definition of linear named application
• Figure 3: Notable diagrams of Proposition \ref{['lamu-prop:lamu^+Confl']}, point (1), subcase $t=(\mu\alpha.{}_{\beta}|{s}|)[\vec{u}]$, $\mathbb{T} = \mu\alpha.\langle {}_{\beta}|{s}| \rangle^+_\alpha[\vec{u}]$, $s=\mu\gamma.{}_{\eta}|{s'}|$, $\alpha\neq\beta$.
• Figure 4: Notable diagrams of Proposition \ref{['lamu-prop:lamu^+Confl']}, point (1), subcase $t=(\mu\alpha.{}_{\beta}|{s}|)[\vec{u}]$, $\mathbb{T} = \mu\alpha.\langle {}_{\beta}|{s}| \rangle^+_\alpha[\vec{u}]$, $s=\mu\gamma.{}_{\eta}|{s'}|$,$\alpha=\beta,\gamma\neq\eta,\eta=\alpha$.
• Figure 5: Notable diagrams of Proposition \ref{['lamu-prop:lamu^+Confl']}, point (1), subcase $t=(\mu\alpha.{}_{\beta}|{s}|)[\vec{u}]$, $\mathbb{T} = \mu\alpha.\langle {}_{\beta}|{s}| \rangle^+_\alpha[\vec{u}]$, $s=\mu\gamma.{}_{\eta}|{s'}|$,$\alpha=\beta,\gamma\neq\eta,\eta\neq\alpha$.

Theorems & Definitions (107)

• Definition 1.1
• Definition 1.2
• Theorem 1.3
• proof
• Lemma 1.4
• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5