Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)

TL;DR

This paper introduces a unified approach to prove factorization and normalization properties for call-by-name and call-by-value lambda calculi by leveraging linear logic-inspired calculus, simplifying proofs and extending robustness.

Contribution

It provides a single proof framework for factorization and normalization in both CbN and CbV calculi using the bang calculus and translation techniques.

Findings

Proves factorization and normalization for the bang calculus.

Transfers results to CbN and CbV via translations.

Framework remains robust with added operators and rules.

Abstract

In each variant of the lambda-calculus, factorization and normalization are two key-properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the lambda-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV. The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.