Infinitary lambda calculi from a linear perspective

DOI10.1145/2933575.2934505MaRDI QIDQ4635902zbMATH OpenOpenAlexFDO

Authors 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)

Full work available at URL https://arxiv.org/abs/1604.08248, https://hal.inria.fr/hal-01400883/file/main%20%281%29.pdf

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)

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.

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

Cited in

(16)

• scientific article; zbMATH DE number 1523050 (Why is no real title available?)
• scientific article; zbMATH DE number 1841833 (Why is no real title available?)
• A functorial bridge between the infinitary affine lambda-calculus and linear logic
• Implicit computation complexity in higher-order programming languages
• scientific article; zbMATH DE number 919545 (Why is no real title available?)
• Confluence of the coinductive \(\lambda\)-calculus
• Infinite \(\lambda\)-calculus and types
• Strict ideal completions of the lambda calculus
• Applications of infinitary lambda calculus
• A construction of one-point bases in extended lambda calculi
• scientific article; zbMATH DE number 759438 (Why is no real title available?)
• An Alpha-Corecursion Principle for the Infinitary Lambda Calculus
• A classical linear \(\lambda\)-calculus
• scientific article; zbMATH DE number 6712184 (Why is no real title available?)
• Polynomial time over the reals with parsimony
• An infinitary affine lambda-calculus isomorphic to the full lambda-calculus

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)