More Web Proxy on the site http://driver.im/

article

Open access

The complexity of interaction

Authors:

Stéphane Gimenez,

Georg MoserAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 1

Pages 243 - 255

https://doi.org/10.1145/2914770.2837646

Published: 11 January 2016 Publication History

Abstract

In this paper, we analyze the complexity of functional programs written in the interaction-net computation model, an asynchronous, parallel and confluent model that generalizes linear-logic proof nets. Employing user-defined sized and scheduled types, we certify concrete time, space and space-time complexity bounds for both sequential and parallel reductions of interaction-net programs by suitably assigning complexity potentials to typed nodes. The relevance of this approach is illustrated on archetypal programming examples. The provided analysis is precise, compositional and is, in theory, not restricted to particular complexity classes.

References

[1]

A. Asperti, C. Giovanetti, and A. Naletto. The bologna optimal higherorder machine. JFP, 6(6):763–810, 1996.

[2]

R. Atkey. Amortised resource analysis with separation logic. Logical Methods in Computer Science, 7(2), 2011.

[3]

M. Avanzini, U. Dal Lago, and G. Moser. Analysing the complexity of functional programs: Higher-order meets first-order, 2015.

Digital Library

[4]

P. Baillot and U. Dal Lago. Higher-order interpretations and program complexity. In Proc. 21th CSL, volume 16 of LIPIcs, pages 62–76, 2012.

[5]

P.v. Emde Boas. Machine models and simulation. In Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity (A), pages 1–66. MIT Press, 1990.

Digital Library

[6]

M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating runtime and size complexity analysis of integer programs. In Proc. 20th TACAS, volume 8413 of LNCS, pages 140–155, 2014.

[7]

M. Fernández, I. Mackie, S. Sato, and M. Walker. Recursive functions with pattern matching in interaction nets. ENTCS, 253(4):55–71, 2009.

Digital Library

[8]

D. Ghica and A. Smith. Bounded linear types in a resource semiring. In Proc. 23rd ESOP, volume 8410 of LNCS, pages 331–350, 2014.

[9]

S. Gimenez. Programmer, calculer et raisonner avec les réseaux de la logique linéaire. PhD thesis, 2009.

[10]

S. Gimenez and G. Moser. The complexity of interaction (long version). http://arxiv.org/abs/1511.01838.

[11]

S. Gimenez and G. Moser. The structure of interaction. In Proc. 22nd CSL, volume 23 of LIPIcs, pages 316–331, 2013.

[12]

J-Y. Girard, A. Scedrov, and P. Scott. Bounded linear logic: A modular approach to polynomial-time computability. TCS, 97(1):1–66, 1992.

Digital Library

[13]

G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In Proc. 19th POPL, pages 15–26. ACM Press, 1992.

Digital Library

[14]

G. Gonthier, M. Abadi, and J.-J. Lévy. Linear logic without boxes. In Proc. 7th LICS, pages 223–234. IEEE, 1992.

[15]

A. Hassan and S. Sato. Interaction nets with nested pattern matching. ENTCS, 203(1):79–92, 2008.

Digital Library

[16]

J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. TOPLAS, 34(3):14, 2012.

Digital Library

[17]

J. Hoffmann and Z. Shao. Automatic static cost analysis for parallel programs. In Proc. 24th ESOP, volume 9032 of LNCS, pages 132–157, 2015.

Digital Library

[18]

Y. Lafont. Interaction nets. In Proc. 17th POPL, pages 95–108. ACM, 1990.

Digital Library

[19]

Y. Lafont. Interaction combinators. IC, 137(1):69–101, 1997.

Digital Library

[20]

U. Dal Lago. Context semantics, linear logic, and computational complexity. TOCL, 10(4), 2009.

Digital Library

[21]

U. Dal Lago and B. Petit. Linear dependent types in a call-by-value scenario. Sci. Comput. Program., 84:77–100, 2014.

Digital Library

[22]

J. Lamping. An algorithm for optimal lambda calculus reduction. In Proc. 7th POPL, pages 16–30. ACM Press, 1990.

Digital Library

[23]

S. Lippi. Universal hard interaction for clockless computation: Dem Glücklichen schlägt keine Stunde! FI, 91(2):357–394, 2009.

Digital Library

[24]

The linear logic wiki: Fragments. http://llwiki.ens-lyon.fr/ mediawiki/index.php/Fragment.

[25]

I. Mackie. Interaction nets for linear logic. TCS, 247(1-2):83–140, 2000.

Digital Library

[26]

I. Mackie. Efficient lambda-evaluation with interaction nets. In Proc. 15th RTA, volume 3091 of LNCS, pages 155–169, 2004.

[27]

D. Mazza. Interaction Nets: Semantics and Concurrent Extensions. PhD thesis, 2006.

[28]

P.-A. Mellies. Functorial boxes in string diagrams. In Proc. 15th CSL, LNCS, pages 1–30, 2006.

Digital Library

[29]

M. Perrinel. On context semantics and interaction nets. In Proc. Joint 23rd CSL and 29th LICS, page 73. ACM, 2014.

Digital Library

[30]

J. S. Pinto. Parallel evaluation of interaction nets with mpine. In Proc. 12th RTA, volume 2051 of LNCS, pages 353–356, 2001.

Digital Library

[31]

M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proc. 26th CAV, volume 8559 of LNCS, pages 745–761, 2014.

Digital Library

[32]

P. Vasconcelos. Space Cost Analysis Using Sized Types. PhD thesis, School of Computer Science, University of St. Andrews, 2008.

[33]

L. Vaux. λ-calcul différentiel et logique classique: interactions combinatoires. PhD thesis, 2007.

Cited By

Castro-Perez DYoshida N(2020)CAMP: cost-aware multiparty session protocolsProceedings of the ACM on Programming Languages10.1145/34282234:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://doi.org/10.1145/3428223
Chatterjee KFu HGoharshady A(2019)Non-polynomial Worst-Case Analysis of Recursive ProgramsACM Transactions on Programming Languages and Systems10.1145/333998441:4(1-52)Online publication date: 12-Oct-2019
https://doi.org/10.1145/3339984
Chatterjee KFu HGoharshady A(2017)Non-polynomial Worst-Case Analysis of Recursive ProgramsComputer Aided Verification10.1007/978-3-319-63390-9_3(41-63)Online publication date: 13-Jul-2017
https://doi.org/10.1007/978-3-319-63390-9_3
Show More Cited By

Index Terms

The complexity of interaction
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

The complexity of interaction
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

In this paper, we analyze the complexity of functional programs written in the interaction-net computation model, an asynchronous, parallel and confluent model that generalizes linear-logic proof nets. Employing user-defined sized and scheduled types, ...
Differential interaction nets
Logic, language, information and computation

We introduce interaction nets for a fragment of the differential lambda-calculus and exhibit in this framework a new symmetry between the of course and the why not modalities of linear logic, which is completely similar to the symmetry between the ...
Interpreting a finitary pi-calculus in differential interaction nets

We propose and study a translation of a pi-calculus without sums nor recursion into an untyped version of differential interaction nets. We define a transition system of labeled processes and a transition system of labeled differential interaction nets. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 1

POPL '16

January 2016

815 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2914770

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2016
815 pages
ISBN:9781450335492
DOI:10.1145/2837614
General Chair:
Rastislav Bodik
UC Berkeley, USA
,
Program Chair:
Rupak Majumdar
MPI-SWS, Germany

Copyright © 2016 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: 11 January 2016

Published in SIGPLAN Volume 51, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

Austrian Science Fund

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
866
Total Downloads

Downloads (Last 12 months)214
Downloads (Last 6 weeks)42

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Castro-Perez DYoshida N(2020)CAMP: cost-aware multiparty session protocolsProceedings of the ACM on Programming Languages10.1145/34282234:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://doi.org/10.1145/3428223
Chatterjee KFu HGoharshady A(2019)Non-polynomial Worst-Case Analysis of Recursive ProgramsACM Transactions on Programming Languages and Systems10.1145/333998441:4(1-52)Online publication date: 12-Oct-2019
https://doi.org/10.1145/3339984
Chatterjee KFu HGoharshady A(2017)Non-polynomial Worst-Case Analysis of Recursive ProgramsComputer Aided Verification10.1007/978-3-319-63390-9_3(41-63)Online publication date: 13-Jul-2017
https://doi.org/10.1007/978-3-319-63390-9_3
Baillot PGhyselen A(2022)Types for Complexity of Parallel Computation in Pi-calculusACM Transactions on Programming Languages and Systems10.1145/349552944:3(1-50)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1145/3495529
Baillot PGhyselen A(2021)Types for Complexity of Parallel Computation in Pi-CalculusProgramming Languages and Systems10.1007/978-3-030-72019-3_3(59-86)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_3
Castro-Perez DYoshida N(2020)CAMP: cost-aware multiparty session protocolsProceedings of the ACM on Programming Languages10.1145/34282234:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428223
Chatterjee KFu HGoharshady A(2019)Non-polynomial Worst-Case Analysis of Recursive ProgramsACM Transactions on Programming Languages and Systems10.1145/333998441:4(1-52)Online publication date: 12-Oct-2019
https://dl.acm.org/doi/10.1145/3339984
Wang PFu HGoharshady AChatterjee KQin XShi WMcKinley KFisher K(2019)Cost analysis of nondeterministic probabilistic programsProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314581(204-220)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314581
Das AHoffmann JPfenning F(2018)Parallel complexity analysis with temporal session typesProceedings of the ACM on Programming Languages10.1145/32367862:ICFP(1-30)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236786
Das AHoffmann JPfenning F(2018)Work Analysis with Resource-Aware Session TypesProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209146(305-314)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209146
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Publication

Figures

Tables

Media

View Issue’s Table of Contents