Minimality in a Linear Calculus with Iteration

Gödel’s System T is an extremely powerful calculus: essentially anything that we want to compute can be expressed [3]. A linear variant of this well-known calculus, called System L, was introduced in [1], and shown to be every bit as expressive as System T. The novelty of System L is that it is based on the linear λ-calculus, and all duplication and erasing can be done through an encoding using the iterator. There are many well-known, and well-understood, strategies for reduction in the (pure) λ-calculus. When investigating deeper into the structure of terms, we get a deeper understanding of reduction. For instance, calculi with explicit resource management or explicit substitution allow a finer control over reduction. In a similar way, System L splits the usual λ in two different constructs: a binder, able to generate a substitution, and an iterator able to erase or copy its argument. This entails a finer control of these fundamentally different issues, which are intertwined in the λ-calculus. Having a calculus which offers at the same time a lot of freedom in reduction and a lot of information about resources makes it an ideal framework to start a fresh attempt at studying reduction strategies in λ-calculi. We present a first step towards a thorough study of reduction strategies for System L. I