Positive Focusing is Directly Useful

TL;DR

This paper introduces the positive λ-calculus, a sharing-enabled λ-calculus with a compactness property that effectively models useful sharing for analyzing reasonable time cost models.

Contribution

It demonstrates that the positive λ-calculus captures the essence of useful sharing, advancing understanding of sharing techniques in λ-calculi.

Findings

Positive λ-calculus has a compactness property.

It effectively models useful sharing.

Supports analysis of time cost models.

Abstract

Recently, Miller and Wu introduced the positive $\lambda$-calculus, a call-by-value $\lambda$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive $\lambda$-calculus stands out among $\lambda$-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.