Infinitary $\lambda$-Calculi from a Linear Perspective (Long Version)

TL;DR

This paper introduces a linear infinitary lambda calculus with two exponential modalities, enabling both terminating and productive computations over infinite structures, and demonstrates its properties and applications.

Contribution

It presents a novel linear infinitary lambda calculus with dual modalities, unifying finitary and coinductive computation, and analyzes its properties and fragments.

Findings

Embeds infinitary applicative lambda calculus

Allows restriction to terminating or productive computations

Achieves confluence in a fragment, unlike traditional infinitary lambda calculi

Abstract

We introduce a linear infinitary $\lambda$-calculus, called $\ell\Lambda_{\infty}$, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted coinductively. The obtained calculus embeds the infinitary applicative $\lambda$-calculus and is universal for computations over infinite strings. What is particularly interesting about $\ell\Lambda_{\infty}$, is that the refinement induced by linear logic allows to restrict both modalities so as to get calculi which are terminating inductively and productive coinductively. We exemplify this idea by analysing a fragment of $\ell\Lambda$ built around the principles of $\mathsf{SLL}$ and $\mathsf{4LL}$. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary $\lambda$-calculi.