Infinitary lambda calculi from a linear perspective

DOI10.1145/2933575.2934505zbMATH Open1394.03027arXiv1604.08248OpenAlexW2531157181MaRDI QIDQ4635902FDOQ4635902

Ugo Dal Lago

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: We introduce a linear infinitary $lambda$-calculus, called $ellLambd{a}_{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 $ellLambd{a}_{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 $ellLambda$ built around the principles of $mathsfSLL$ and $mathsf4LL$. Interestingly, it enjoys confluence, contrarily to what happens in ordinary infinitary $lambda$-calculi.

Full work available at URL: https://arxiv.org/abs/1604.08248

Recommendations

• scientific article; zbMATH DE number 919545
• Applications of infinitary lambda calculus
• A functorial bridge between the infinitary affine lambda-calculus and linear logic
• An Infinitary Model of Linear Logic
• Infinite \(\lambda\)-calculus and types

zbMATH Keywords

linear logiclambda calculusinfinitary rewriting

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cited In (13)

• Title not available (Why is that?)
• Implicit computation complexity in higher-order programming languages
• Title not available (Why is that?)
• Confluence of the coinductive \(\lambda\)-calculus
• Infinite \(\lambda\)-calculus and types
• Applications of infinitary lambda calculus
• A construction of one-point bases in extended lambda calculi
• Title not available (Why is that?)
• An Alpha-Corecursion Principle for the Infinitary Lambda Calculus
• Title not available (Why is that?)
• A classical linear \(\lambda\)-calculus
• Polynomial time over the reals with parsimony
• Title not available (Why is that?)

This page was built for publication: Infinitary lambda calculi from a linear perspective

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635902)