article

Optimizing optimal reduction: A type inference algorithm for elementary affine logic

Authors:

Simone MartiniAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 7, Issue 2

Pages 219 - 260

https://doi.org/10.1145/1131313.1131315

Published: 01 April 2006 Publication History

Abstract

We propose a type inference algorithm for lambda terms in elementary affine logic (EAL). The algorithm decorates the syntax tree of a simple typed lambda term and collects a set of linear constraints. The result is a parametric elementary type that can be instantiated with any solution of the set of collected constraints.We point out that the typeability of lambda terms in EAL has a practical counterpart, since it is possible to reduce any EAL-typeable lambda terms with the Lamping's abstract algorithm obtaining a substantial increase of performances.We show how to apply the same techniques to obtain decorations of intuitionistic proofs into linear logic proofs.

References

[1]

Asperti, A. 1998. Light affine logic. In Proceedings of 13th Symposium on Logic in Computer Science (Indianapolis, IN). IEEE Computer Society, 300--308.]]

Digital Library

[2]

Asperti, A., Coppola, P., and Martini, S. 2000. (Optimal) duplication is not elementary recursive. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 00, Boston, MA). ACM Press, 96--107.]]

Digital Library

[3]

Asperti, A. and Guerrini, S. 1998. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, vol. 45. Cambridge University Press.]]

Digital Library

[4]

Baillot, P. 2002. Checking polynomial time complexity with types. In Proceedings of 2nd IFIP International Conference on Theoretical Computer Science (TCS 2002, Montréal, Qué.) vol. 223. Kluwer, 370--382.]]

Digital Library

[5]

Baillot, P. 2003. Type inference for polynomial time complexity via constraints on words. Tech. rep., Laboratoire d'Informatique de Paris Nord, Université Paris 13, Institut Galilée.]]

[6]

Benton, N., Bierman, G., de Paiva, V., and Hyland, M. 1993. A term calculus for intuitionistic linear logic. In Typed Lambda Calculus and Applications. In Proceedings of the 1st International Conference, (TLCA'93, Utrecht), M. Benzen and J. Groote, eds. Lecture Notes in Computer Science, vol. 664. Springer, 75--90.]]

Digital Library

[7]

Coppola, P. and Martini, S. 2001. Typing lambda terms in elementary logic with linear constraints. In Typed Lambda Calculi and Applications, 5th International Conference, (TLCA 2001, Krakow), S. Abramsky, ed. Lecture Notes in Computer Science, vol. 2044. Springer, 76--90.]]

Digital Library

[8]

Coppola, P. and Rocca, S. R. D. 2003. Principal typing in elementary affine logic. In Typed Lambda Calculi and Applications, 6th International Conference, (TLCA 2003, Valencia) M. Hofmann, ed. Lecture Notes in Computer Science, vol. 2701. Springer, 90--104.]]

[9]

Danos, V. and Joinet, J.-B. 2003. Linear logic and elementary time. Inf. Comput. 183, 1, 123--137.]]

Digital Library

[10]

Danos, V., Joinet, J.-B., and Schellinx, H. 1995. On the linear decoration of intuitionistic derivations. Archive Math. Logic 33, 387--412.]]

[11]

Girard, J.-Y. 1998. Light linear logic. Inf. Comput. 204, 2, 143--175.]]

Digital Library

[12]

Kathail, V. K. 1990. Optimal interpreters for lambda-calculus based functional programming languages. Ph.D. thesis, MIT.]]

[13]

Lamping, J. 1990. An algorithm for optimal lambda calculus reduction. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, (POPL '90, San Francisco) ACM Press, 16--30.]]

Digital Library

[14]

Lévy, J.-J. 1980. Optimal reductions in the lambda-calculus. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley, eds. Academic Press, London, 159--191.]]

[15]

Mairson, H. G. 1992. A simple proof of a theorem of Statman. Theor. Comput. Sci. 103, 2, 387--394.]]

Digital Library

[16]

Prawitz, D. 1965. Natural Deduction. Almqvist & Wiksell.]]

[17]

Roversi, L. 1992. A compiler from Curry-typed λ-terms to linear-λ-terms. In Theoretical Computer Science: Proceedings of the 4th Italian Conference World Scientific, L'Aquila (Italy), 330--344.]]

[18]

Roversi, L. 1998. A Polymorphic language which is typable and poly-step. In Proceedings of the 4th Asian Computing Science Conference (ASIAN'98, Manila). Lecture Notes in Computer Science, vol. 1538. Springer Verlag, 43--60.]]

[19]

Schellinx, H. 1994. The noble art of linear decorating. Ph.D. thesis, Institute for Logic, Language and Computation, University of Amsterdam.]]

Cited By

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
https://doi.org/10.1017/S0960129521000505
Madet ADe Schreye DJanssens GKing A(2012)A polynomial time λ-calculus with multithreading and side effectsProceedings of the 14th symposium on Principles and practice of declarative programming10.1145/2370776.2370785(55-66)Online publication date: 19-Sep-2012
https://dl.acm.org/doi/10.1145/2370776.2370785
Madet AAmadio R(2011)An elementary affine λ-calculus with multithreading and side effectsProceedings of the 10th international conference on Typed lambda calculi and applications10.5555/2021953.2021968(138-152)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.5555/2021953.2021968
Show More Cited By

Index Terms

Optimizing optimal reduction: A type inference algorithm for elementary affine logic
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Light logics and optimal reduction: Completeness and complexity

Typing of lambda-terms in elementary and light affine logic (EAL and LAL, respectively) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, respectively) proof-nets admits a guaranteed polynomial (...
Phase semantics and decidability of elementary affine logic
Logic, semantics and theory of programming

Light, elementary and soft linear logics are formal systems derived from Linear Logic, enjoying remarkable normalization properties. In this paper, we prove decidability of Elementary Affine Logic, EAL. The result is obtained by semantical means, first ...
The decidability of the intensional fragment of classical linear logic

Intensional classical linear logic (MELL) is proved decidable.Intensional interlinear logic (RLL) is proved decidable.We adapt Kripke's method used to prove decidability for some relevance logics.The semi-relevant RLL emerges as a logic superior to MELL ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 7, Issue 2

April 2006

221 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/1131313

Issue’s Table of Contents

Copyright © 2006 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 ACM 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: 01 April 2006

Published in TOCL Volume 7, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
293
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

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
https://doi.org/10.1017/S0960129521000505
Madet ADe Schreye DJanssens GKing A(2012)A polynomial time λ-calculus with multithreading and side effectsProceedings of the 14th symposium on Principles and practice of declarative programming10.1145/2370776.2370785(55-66)Online publication date: 19-Sep-2012
https://dl.acm.org/doi/10.1145/2370776.2370785
Madet AAmadio R(2011)An elementary affine λ-calculus with multithreading and side effectsProceedings of the 10th international conference on Typed lambda calculi and applications10.5555/2021953.2021968(138-152)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.5555/2021953.2021968
Baillot PCoppola PDal Lago U(2011)Light logics and optimal reductionInformation and Computation10.1016/j.ic.2010.10.002209:2(118-142)Online publication date: 1-Feb-2011
https://dl.acm.org/doi/10.1016/j.ic.2010.10.002
Madet AAmadio R(2011)An Elementary Affine λ-Calculus with Multithreading and Side EffectsTyped Lambda Calculi and Applications10.1007/978-3-642-21691-6_13(138-152)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21691-6_13
Baillot PHofmann MKutsia TSchreiner WFernández M(2010)Type inference in intuitionistic linear logicProceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming10.1145/1836089.1836118(219-230)Online publication date: 26-Jul-2010
https://dl.acm.org/doi/10.1145/1836089.1836118
Baillot PMazza D(2010)Linear logic by levels and bounded time complexityTheoretical Computer Science10.1016/j.tcs.2009.09.015411:2(470-503)Online publication date: 1-Jan-2010
https://dl.acm.org/doi/10.1016/j.tcs.2009.09.015
Baillot PTerui K(2009)Light types for polynomial time computation in lambda calculusInformation and Computation10.1016/j.ic.2008.08.005207:1(41-62)Online publication date: 1-Jan-2009
https://dl.acm.org/doi/10.1016/j.ic.2008.08.005
Baillot P(2007)From proof-nets to linear logic type systems for polynomial time computingProceedings of the 8th international conference on Typed lambda calculi and applications10.5555/1770203.1770205(2-7)Online publication date: 26-Jun-2007
https://dl.acm.org/doi/10.5555/1770203.1770205
Baillot PCoppola PLago U(2007)Light Logics and Optimal ReductionProceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.2007.27(421-430)Online publication date: 10-Jul-2007
https://dl.acm.org/doi/10.1109/LICS.2007.27
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents