Linearity in the non-deterministic call-by-value setting

TL;DR

This paper explores the linearity properties of a non-deterministic call-by-value lambda calculus, establishing a type system and translating it into System F to deepen understanding of linearity in such formalisms.

Contribution

It introduces a fine-grained type system for the non-deterministic call-by-value lambda calculus and relates it to linear logic through translation into System F.

Findings

Proves subject reduction and strong normalization.

Defines a type system capturing linearity.

Provides a translation into System F with pairs.

Abstract

We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting.