Positive Focusing is Directly Useful
Beniamino Accattoli, Jui-Hsuan Wu
TL;DR
This work studies the positive λ-calculus $\lambda_{\mathtt pos}$, which imposes a compactness constraint to capture the core of useful sharing in a sharing-based, open, call-by-value setting. By developing an Open Value Substitution Calculus ($\lambda_{\mathsf{o}vsc}$) and a core reduction $\rightarrow_{o\mathtt{core}}$, the authors prove a postponement/factorization theorem that reduces reduction to a core part containing only directly useful steps and a non-useful remainder. They then construct a translation $\llbracket \cdot \rrbracket$ from $\lambda_{\mathsf{o}vsc}$ to an explicit open positive calculus $\lambda_{\mathsf{o}x pos}$, showing that core reductions simulate in the target calculus and that core normal forms map to normal forms, establishing termination equivalence. The results yield a principled framework for reasonable time cost models and point toward efficient implementations and optimizations, as well as potential extensions to call-by-need evaluation.
Abstract
Recently, Miller and Wu introduced the positive $λ$-calculus, a call-by-value $λ$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive $λ$-calculus stands out among $λ$-calculi with sharing for a compactness property related to the sharing of variables. We show that -- thanks to compactness -- the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models.