Cited By
View all- Dal Lago U(2022)Implicit computation complexity in higher-order programming languagesMathematical Structures in Computer Science10.1017/S0960129521000505(1-17)Online publication date: 15-Mar-2022
Algebras and coalgebras in the light affine Lambda calculus
Abstract
Algebra and coalgebra are widely used to model data types in functional programming languages and proof assistants. Their use permits to better structure the computations and also to enhance the expressivity of a language or of a proof system. Interestingly, parametric polymorphism à la System F provides a way to encode algebras and coalgebras in strongly normalizing languages without losing the good logical properties of the calculus. Even if these encodings are sometimes unsatisfying because they provide only limited forms of algebras and coalgebras, they give insights on the expressivity of System F in terms of functions that we can program in it. With the goal of contributing to a better understanding of the expressivity of Implicit Computational Complexity systems, we study the problem of defining algebras and coalgebras in the Light Affine Lambda Calculus, a system characterizing the complexity class FPTIME. This system limits the computational complexity of programs but it also limits the ways we can use parametric polymorphism, and in general the way we can write our programs. We show here that while the restrictions imposed by the Light Affine Lambda Calculus pose some issues to the standard System F encodings, they still permit to encode some form of algebra and coalgebra. Using the algebra encoding one can define in the Light Affine Lambda Calculus the traditional inductive types. Unfortunately, the corresponding coalgebra encoding permits only a very limited form of coinductive data types. To extend this class we study an extension of the Light Affine Lambda Calculus by distributive laws for the modality §. This extension has been discussed but not studied before.
References
[1]
A. Asperti. Light affine logic. In LICS ’98, pages 300–308. IEEE, 1998.
[2]
A. Asperti and L. Roversi. Intuitionistic light affine logic. ACM TOCL, 3(1):137–175, 2002.
[3]
P. Baillot and U. Dal Lago. Higher-Order Interpretations and Program Complexity. In CSL’12, volume 16, pages 62–76. LIPIcs, 2012.
[4]
P. Baillot and D. Mazza. Linear logic by levels and bounded time complexity. TCS, 411(2):470–503, 2010.
[5]
P. Baillot and K. Terui. Light types for polynomial time computation in lambda-calculus. In LICS ’04, pages 266–275. IEEE, 2004.
[6]
P. Baillot, M. Gaboardi, and V. Mogbil. A polytime functional language from light linear logic. In ESOP’10, volume 6012 of LNCS. Springer, 2010.
[7]
S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the poly-time functions. Comp. Complexity, 2:97–110, 1992.
[8]
M. J. Burrell, R. Cockett, and B. F. Redmond. Pola: a language for PTIME programming. In LCC’09, 2009.
[9]
S. Cook and A. Urquhart. Functional interpretations of feasibly constructive arithmetic. STOC ’89, pages 107–112. ACM, 1989.
[10]
H. Férée, E. Hainry, M. Hoyrup, and R. Péchoux. Interpretation of stream programs: characterizing type 2 polynomial time complexity. In ISAAC’10, pages 291–303. Springer, 2010.
[11]
P. Freyd. Structural polymorphism. TCS, 115(1):107–129, 1993.
[12]
M. Gaboardi and R. Péchoux. Upper bounds on stream I/O using semantic interpretations. In CSL ’09, volume 5771 of LNCS, pages 271 – 286. Springer, 2009.
[13]
M. Gaboardi and R. Péchoux. Global and local space properties of stream programs. In FOPARA’09, volume 6324 of LNCS, pages 51 – 66. Springer, 2010.
[14]
M. Gaboardi and S. Ronchi Della Rocca. A soft type assignment system for λ-calculus. In CSL ’07, volume 4646 of LNCS, pages 253– 267. Springer, 2007.
[15]
M. Gaboardi, J.-Y. Marion, and S. Ronchi Della Rocca. Soft linear logic and polynomial complexity classes. In LSFA 2007, volume 205 of ENTCS, pages 67–87. Elsevier.
[16]
M. Gaboardi, J.-Y. Marion, and S. Ronchi Della Rocca. A logical account of PSPACE. In POPL’08. ACM, 2008.
[17]
M. Gaboardi, L. Roversi, and L. Vercelli. A by-level analysis of Multiplicative Exponential Linear Logic. In MFCS’09, volume 5734 of LNCS, pages 344 – 355. Springer, 2009.
[18]
H. Geuvers. Inductive and coinductive types with iteration and recursion. In Types for Proofs and Programs, pages 193–217. 1992.
[19]
J. Girard. The Blind Spot: Lectures on Logic. European Mathematical Society, 2011. ISBN 9783037190883.
[20]
J.-Y. Girard. Linear logic. TCS, 50:1–102, 1987.
[21]
J.-Y. Girard. Light linear logic. Information and Computation, 143(2): 175–204, 1998.
[22]
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge university press, 1989.
[23]
T. Hagino. A typed lambda calculus with categorical type constructors. In Category Theory and Computer Science, volume 283, pages 140–57. LNCS, 1987.
[24]
P. Hájek. Arithmetical hierarchy and complexity of computation. TCS, 8:227–237, 1979.
[25]
M. Hofmann. Programming languages capturing complexity classes. ACM SIGACT News, 31(1):31–42, 2000.
[26]
B. Jacobs and J. Rutten. A tutorial on (co) algebras and (co) induction. EATCS, 62:222–259, 1997.
[27]
Y. Lafont. Soft linear logic and polynomial time. TCS, 318(1-2):163– 180, 2004.
[28]
U. D. Lago and P. Baillot. On light logics, uniform encodings and polynomial time. MSCS’06, 16(4):713–733, 2006.
[29]
D. Leivant and R. Ramyaa. Implicit complexity for coinductive data: a characterization of corecurrence. In DICE’12, volume 75 of EPTCS, pages 1–14, 2012.
[30]
D. Leivant and R. Ramyaa. The computational contents of ramified corecurrence. In FOSSACS, 2015. To appear.
[31]
R. Matthes. Monotone (co)inductive types and positive fixed-point types. ITA, 33(4/5):309–328, 1999.
[32]
F. Maurel. Nondeterministic light logics and NP-time. In TLCA ’03, volume 2701 of LNCS, pages 241–255. Springer, 2003.
[33]
D. Mazza. Non-uniform polytime computation in the infinitary affine lambda-calculus. In ICALP’14, pages 305–317, 2014.
[34]
A. S. Murawski and C. L. Ong. On an interpretation of safe recursion in light affine logic. TCS, 318(1-2):197–223, 2004.
[35]
B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
[36]
R. Ramyaa and D. Leivant. Ramified corecurrence and logspace. ENTCS, 276(0):247 – 261, 2011. MFPS’11.
[37]
J. C. Reynolds and G. Plotkin. On functors expressible in the polymorphic typed lambda calculus. Information and Computation, 105 (1):1–29, 1993.
[38]
L. Roversi and L. Vercelli. Safe recursion on notation into a light logic by levels. In DICE’10, pages 63–77, 2010.
[39]
U. Schöpp. Stratified bounded affine logic for logarithmic space. In LICS ’07, pages 411–420, Washington, DC, USA, 2007. IEEE.
[40]
K. Terui. Light affine lambda calculus and polytime strong normalization. In LICS ’01, pages 209–220. IEEE, 2001.
[41]
P. Wadler. Recursive types for free! Technical report, University of Glasgow, 1990.
[42]
G. C. Wraith. A note on categorical datatypes. In CTCS, volume 389 of LNCS, pages 118–127. Springer, 1993.
Index Terms
- Algebras and coalgebras in the light affine Lambda calculus
Recommendations
Algebras and coalgebras in the light affine Lambda calculus
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional ProgrammingAlgebra and coalgebra are widely used to model data types in functional programming languages and proof assistants. Their use permits to better structure the computations and also to enhance the expressivity of a language or of a proof system. ...
Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus
Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like ...
Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus
Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2015
436 pages
August 2015436 pages
Copyright © 2015 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 29 August 2015
Published in SIGPLAN Volume 50, Issue 9
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 252Total Downloads
- Downloads (Last 12 months)4
- Downloads (Last 6 weeks)2
Reflects downloads up to 02 Mar 2025
Other Metrics
Citations
Cited By
View all- Dal Lago U(2022)Implicit computation complexity in higher-order programming languagesMathematical Structures in Computer Science10.1017/S0960129521000505(1-17)Online publication date: 15-Mar-2022
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in