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

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 $4LL$. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary $\lambda$-calculi.