Article

Parsimonious Types and Non-uniform Computation

Authors:

Kazushige TeruiAuthors Info & Claims

ICALP 2015: Proceedings, Part II, of the 42nd International Colloquium on Automata, Languages, and Programming - Volume 9135

Pages 350 - 361

https://doi.org/10.1007/978-3-662-47666-6_28

Published: 06 July 2015 Publication History

Abstract

We consider a non-uniform affine lambda-calculus, called parsimonious, and endow its terms with two type disciplines: simply-typed and with linear polymorphism. We show that the terms of string type into Boolean type characterize the class L/poly in the first case, and P/poly in the second. Moreover, we relate this characterization to that given by the second author in terms of Boolean proof nets, highlighting continuous affine approximations as the bridge between the two approaches to non-uniform computation.

References

[1]

Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 1632, 409---470 2000

Digital Library

[2]

Baillot, P., Terui, K.: Light types for polynomial time computation in lambda calculus. Inf. Comput. 2071, 41---62 2009

Digital Library

[3]

Bellantoni, S., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. Computational Complexity 2, 97---110 1992

Digital Library

[4]

Ehrhard, T., Regnier, L.: Differential interaction nets. Electr. Notes Theor. Comput. Sci. 123, 35---74 2005

Digital Library

[5]

Ehrhard, T., Regnier, L.: Uniformity and the taylor expansion of ordinary lambda-terms. Theor. Comput. Sci. 4032---3, 347---372 2008

Digital Library

[6]

Gaboardi, M., Péchoux, R.: Upper bounds on stream I/O using semantic interpretations. In: Grädel, E., Kahle, R. eds. CSL 2009. LNCS, vol. 5771, pp. 271---286. Springer, Heidelberg 2009

Digital Library

[7]

Ghica, D.R.: Geometry of synthesis: a structured approach to VLSI design. In: Proceedings of POPL, pp. 363---375 2007

Digital Library

[8]

Girard, J.Y.: Geometry of interaction I: Interpretation of system F. Proccedings of Logic Colloquium 1988, 221---260 1989

[9]

Girard, J.Y.: Light linear logic. Inf. Comput. 1432, 175---204 1998

Digital Library

[10]

Kfoury, A.J.: A linearization of the lambda-calculus and consequences. J. Log. Comput. 103, 411---436 2000

[11]

Leivant, D., Marion, J.Y.: Lambda calculus characterizations of poly-time. Fundam. Inform. 191/2 1993

Digital Library

[12]

Mazza, D.: An infinitary affine lambda-calculus isomorphic to the full lambda-calculus. In: Proceedings of LICS, pp. 471---480 2012

Digital Library

[13]

Mazza, D.: Non-uniform polytime computation in the infinitary affine lambda-calculus. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. eds. ICALP 2014, Part II. LNCS, vol. 8573, pp. 305---317. Springer, Heidelberg 2014

[14]

Mazza, D.: Simple parsimonious types and logarithmic space 2015, available on the author's web page

[15]

Melliès, P.A.: Asynchronous games 2: The true concurrency of innocence. Theor. Comput. Sci. 3582---3, 200---228 2006

Digital Library

[16]

Melliès, P.-A., Tabareau, N., Tasson, C.: An explicit formula for the free exponential modality of linear logic. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. eds. ICALP 2009, Part II. LNCS, vol. 5556, pp. 247---260. Springer, Heidelberg 2009

Digital Library

[17]

Ramyaa, R., Leivant, D.: Ramified corecurrence and logspace. Electr. Notes Theor. Comput. Sci. 276, 247---261 2011

Digital Library

[18]

Saurin, A.: Typing streams in the $$\Lambda \mu $$-calculus. ACM Trans. Comput. Log. 114 2010

Digital Library

[19]

Terui, K.: Proof nets and boolean circuits. In: Proceedings of LICS, pp. 182---191 2004

Digital Library

[20]

Vollmer, H.: Introduction to circuit complexity - a uniform approach. Texts in theoretical computer science. Springer 1999

Digital Library

Cited By

Accattoli BDal Lago UVanoni G(2021)The (In)Efficiency of interactionProceedings of the ACM on Programming Languages10.1145/34343325:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434332
Accattoli BDal Lago UVanoni GGabbrielli MAbel ACheney J(2020)The Machinery of InteractionProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414108(1-15)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414108
Hainry EMazza DPéchoux R(2020)Polynomial Time over the Reals with ParsimonyFunctional and Logic Programming10.1007/978-3-030-59025-3_4(50-65)Online publication date: 14-Sep-2020
https://dl.acm.org/doi/10.1007/978-3-030-59025-3_4
Show More Cited By

Parsimonious Types and Non-uniform Computation
1. Theory of computation

Recommendations

Qualified types for MLF
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

MLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Qualified types for MLF
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

MLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Boxy types: inference for higher-rank types and impredicativity
ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming

Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ICALP 2015: Proceedings, Part II, of the 42nd International Colloquium on Automata, Languages, and Programming - Volume 9135

July 2015

704 pages

ISBN:9783662476659

Editors:
Magnús M. Halldórsson
Reykjavik University, Reykjavik, Iceland
,
Kazuo Iwama
Kyoto University, Kyoto, Japan
,
Naoki Kobayashi
The University of Tokyo, Tokyo, Japan
,
Bettina Speckmann
Technische Universiteit Eindhoven, Eindhoven, The Netherlands

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 06 July 2015

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 04 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Accattoli BDal Lago UVanoni G(2021)The (In)Efficiency of interactionProceedings of the ACM on Programming Languages10.1145/34343325:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434332
Accattoli BDal Lago UVanoni GGabbrielli MAbel ACheney J(2020)The Machinery of InteractionProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414108(1-15)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414108
Hainry EMazza DPéchoux R(2020)Polynomial Time over the Reals with ParsimonyFunctional and Logic Programming10.1007/978-3-030-59025-3_4(50-65)Online publication date: 14-Sep-2020
https://dl.acm.org/doi/10.1007/978-3-030-59025-3_4
Seiller TKoskinen EGrohe MShankar N(2016)Interaction GraphsProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934568(427-436)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934568
Mazza DKoskinen EGrohe MShankar N(2016)Church Meets Cook and LevinProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934541(827-836)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934541

View Options

View options

Figures

Tables

Media

View Table of Conten