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

research-article

Open access

Taylor subsumes Scott, Berry, Kahn and Plotkin

Authors:

Davide Barbarossa,

Giulio ManzonettoAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue POPL

Article No.: 1, Pages 1 - 23

https://doi.org/10.1145/3371069

Published: 20 December 2019 Publication History

Abstract

The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.

Supplementary Material

WEBM File (a1-barbarossa.webm)

Download
89.56 MB

References

[1]

Beniamino Accattoli. 2018. (In)Efficiency and Reasonable Cost Models. Electr. Notes Theor. Comput. Sci. 338 (2018), 23–43.

[2]

Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. 2018. Tight typings and split bounds. PACMPL 2, ICFP (2018), 94:1–94:30.

Digital Library

[3]

Davide Barbarossa and Giulio Manzonetto. 2019. About the power of Taylor expansion. 3rd International Workshop on Trends in Linear Logic and Applications.

[4]

Henk P. Barendregt. 1977. The type free lambda calculus. In Handbook of Mathematical Logic, J. Barwise (Ed.). Studies in Logic and the Foundations of Mathematics, Vol. 90. North-Holland, Amsterdam, 1091–1132.

[5]

Henk P. Barendregt. 1984. The lambda-calculus, its syntax and semantics (revised ed.). Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland.

[6]

Atilim Gunes Baydin, Barak A. Pearlmutter, Alexey Andreyevich Radul, and Jeffrey Mark Siskind. 2017. Automatic Differentiation in Machine Learning: a Survey. Journal of Machine Learning Research 18 (2017), 153:1–153:43. http: //jmlr.org/papers/v18/17- 468.html

[7]

Gérard Berry. 1978. Stable Models of Typed lambda-Calculi. In ICALP (Lecture Notes in Computer Science), Vol. 62. Springer, 72–89.

[8]

Richard Blute, J. Robin B. Cockett, and Robert A. G. Seely. 2006. Differential categories. Mathematical Structures in Computer Science 16, 6 (2006), 1049–1083.

Digital Library

[9]

Richard Blute, J. Robin B. Cockett, and Robert A. G. Seely. 2009. Cartesian differential categories. Theory and Applications of Categories 22, 23 (2009), 622–672.

[10]

Gérard Boudol. 1993. The Lambda-Calculus with Multiplicities (Abstract). In CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings (Lecture Notes in Computer Science), Eike Best (Ed.), Vol. 715. Springer, 1–6.

[11]

Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. 2012. A relational semantics for parallelism and nondeterminism in a functional setting. Ann. Pure Appl. Logic 163, 7 (2012), 918–934.

[12]

J. Robin B. Cockett and Geoff S. H. Cruttwell. 2014. Differential Structure, Tangent Structure, and SDG. Applied Categorical Structures 22, 2 (2014), 331–417.

[13]

J. Robin B. Cockett and Jean-Simon Lemay. 2019. Integral categories and calculus categories. Mathematical Structures in Computer Science 29, 2 (2019), 243–308.

[14]

Daniel de Carvalho. 2018. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science 28, 7 (2018), 1169–1203.

[15]

Thomas Ehrhard. 2002. On Köthe Sequence Spaces and Linear Logic. Mathematical Structures in Computer Science 12, 5 (2002), 579–623.

Digital Library

[16]

Thomas Ehrhard. 2012. Collapsing non-idempotent intersection types. In Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France (LIPIcs), Patrick Cégielski and Arnaud Durand (Eds.), Vol. 16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 259–273.

[17]

Thomas Ehrhard. 2018. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28, 7 (2018), 995–1060.

[18]

Thomas Ehrhard and Giulio Guerrieri. 2016. The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, James Cheney and Germán Vidal (Eds.). ACM, 174–187.

Digital Library

[19]

Thomas Ehrhard and Laurent Regnier. 2003. The differential lambda-calculus. Theor. Comput. Sci. 309, 1-3 (2003), 1–41.

Digital Library

[20]

Thomas Ehrhard and Laurent Regnier. 2006a. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In CiE (Lecture Notes in Computer Science), Vol. 3988. Springer, 186–197.

[21]

Thomas Ehrhard and Laurent Regnier. 2006b. Differential interaction nets. Theor. Comput. Sci. 364, 2 (2006), 166–195.

Digital Library

[22]

Thomas Ehrhard and Laurent Regnier. 2008. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci. 403, 2-3 (2008), 347–372.

Digital Library

[23]

Thomas Ehrhard and Christine Tasson. 2019. Probabilistic call by push value. Logical Methods in Computer Science 15, 1 (2019).

[24]

Jörg Endrullis and Roel C. de Vrijer. 2008. Reduction Under Substitution. In Rewriting Techniques and Applications, 19th International Conference, RTA 2008 (Lecture Notes in Computer Science), Andrei Voronkov (Ed.), Vol. 5117. Springer, 425–440.

[25]

Sabrina Fiege, Andrea Walther, Kshitij Kulshreshtha, and Andreas Griewank. 2018. Algorithmic differentiation for piecewise smooth functions: a case study for robust optimization. Optimization Methods and Software 33, 4-6 (2018), 1073–1088.

[26]

Marcelo P. Fiore, Nicola Gambino, J. Martin E. Hyland, and Glynn Winskel. 2007. The cartesian closed bicategory of generalised species of structures. J. London Maths. Soc 77 (2007), 203–220.

[27]

Jean Goubault-Larrecq. 2019. A Probabilistic and Non-Deterministic Call-by-Push-Value Language. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. IEEE, 1–13.

[28]

Andreas Griewank, Richard Hasenfelder, Manuel Radons, Lutz Lehmann, and Tom Streubel. 2018. Integrating Lipschitzian dynamical systems using piecewise algorithmic differentiation. Optimization Methods and Software 33, 4-6 (2018), 1089–1107.

[29]

Giulio Guerrieri and Giulio Manzonetto. 2018. The Bang Calculus and the Two Girard’s Translations. In Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018. (EPTCS), Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco (Eds.), Vol. 292. 15–30.

[30]

Martin Hyland. 1975. A syntactic characterization of the equality in some models for the λ-calculus. Journal London Mathematical Society (2) 12(3) (1975), 361–370.

[31]

Bart Jacobs and Jan Rutten. 1997. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62 (1997), 62–222.

[32]

Gilles Kahn and Gordon D. Plotkin. 1978. Domaines Concrets. Technical Report 333. Rapport INRIA-LABORIA.

[33]

Emma Kerinec, Giulio Manzonetto, and Michele Pagani. 2018. Revisiting Call-by-value Böhm trees in light of their Taylor expansion. CoRR abs/1809.02659 (2018). Accepted in Logical Methods in Computer Science.

[34]

Dexter Kozen and Alexandra Silva. 2017. Practical coinduction. Mathematical Structures in Computer Science 27, 7 (2017), 1132–1152.

[35]

Jan Kuper. 1995. Proving the Genericity Lemma by Leftmost Reduction is Simple. In RTA (Lecture Notes in Computer Science), Vol. 914. Springer, 271–278.

[36]

Ugo Dal Lago and Thomas Leventis. 2019. On the Taylor Expansion of Probabilistic lambda-terms. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. (LIPIcs), Herman Geuvers (Ed.), Vol. 131. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 13:1–13:16.

[37]

Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. and Applic. 46, 3 (2012), 413–450.

[38]

Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. 2013. Weighted Relational Models of Typed LambdaCalculi. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. IEEE Computer Society, 301–310.

Digital Library

[39]

Soren B. Lassen. 1999. Bisimulation in Untyped Lambda Calculus: Böhm Trees and Bisimulation up to Context. Electr. Notes Theor. Comput. Sci. 20 (1999), 346–374.

[40]

Thomas Leventis. 2018. Probabilistic Böhm Trees and Probabilistic Separation. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 649–658.

Digital Library

[41]

Paul Blain Levy. 2006. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation 19, 4 (2006), 377–414.

Digital Library

[42]

Stefania Lusin and Antonino Salibra. 2004. The Lattice of Lambda Theories. J. Log. Comput. 14, 3 (2004), 373–394.

Digital Library

[43]

Giulio Manzonetto. 2009. A General Class of Models of H ∗ . In Mathematical Foundations of Computer Science 2009, 34th International Symposium, MFCS 2009, Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009. Proceedings (Lecture Notes in Computer Science), Rastislav Královic and Damian Niwinski (Eds.), Vol. 5734. Springer, 574–586.

Digital Library

[44]

Giulio Manzonetto and Domenico Ruoppolo. 2014. Relational Graph Models, Taylor Expansion and Extensionality. Electr. Notes Theor. Comput. Sci. 308 (2014), 245–272.

Digital Library

[45]

Rob P. Nederpelt, J. Herman. Geuvers, and Roel C. de Vrijer (Eds.). 1994. Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, Vol. 133. North-Holland, Amsterdam.

[46]

Michele Pagani, Peter Selinger, and Benoît Valiron. 2014. Applying quantitative semantics to higher-order quantum computing. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 647–658.

Digital Library

[47]

Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. 2017. Essential and relational models. Mathematical Structures in Computer Science 27, 5 (2017), 626–650.

[48]

Gordon D. Plotkin. 1974. The lambda-Calculus is ω-Incomplete. Journal of Symbolic Logic 39, 2 (1974), 313–317.

[49]

Gordon D. Plotkin. 1975. Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci. 1, 2 (1975), 125–159.

[50]

Dana S. Scott. 1972. Continuous lattices. In Toposes, Algebraic Geometry and Logic (Lecture Notes in Mathematics), Lawvere (Ed.), Vol. 274. Springer, 97–136.

[51]

Richard Statman and Henk Barendregt. 1999. Applications of Plotkin-Terms: Partitions and Morphisms for Closed Terms. J. Funct. Program. 9, 5 (1999), 565–575.

Digital Library

[52]

Masako Takahashi. 1994. A Simple Proof of the Genericity Lemma. In Logic, Language and Computation (Lecture Notes in Computer Science), Vol. 792. Springer, 117–118.

[53]

Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. 2018. Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. In LICS. ACM, 889–898.

[54]

Dirk van Daalen. 1980. The Language Theory of Automath. Ph.D. thesis. Technical University Eindhoven. Large parts of the thesis, including the treatment of reduction under substitution, have been reproduced in [ Nederpelt et al. 1994 ].

[55]

Lionel Vaux. 2009. The algebraic lambda calculus. Mathematical Structures in Computer Science 19, 5 (2009), 1029–1059.

Digital Library

[56]

Lionel Vaux. 2019. Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors. Logical Methods in Computer Science Volume 15, Issue 3 (2019).

[57]

Christopher P. Wadsworth. 1976. The Relation Between Computational and Denotational Properties for Scott’s D ∞ -Models of the Lambda-Calculus. SIAM J. Comput. 5, 3 (1976), 488–521.

[58]

Sebastian F. Walter and Lutz Lehmann. 2013. Algorithmic differentiation in Python with AlgoPy. J. Comput. Science 4, 5 (2013), 334–344.

Cited By

Arrial VGuerrieri GKesner DSobocinski PLago UEsparza J(2024)Genericity Through StratificationProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662113(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662113
Kerjean MPédrot PSobocinski PLago UEsparza J(2024)δ is for DialecticaProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662106(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662106
Accattoli BLancelot A(2024)Light GenericityFoundations of Software Science and Computation Structures10.1007/978-3-031-57231-9_2(24-46)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57231-9_2
Show More Cited By

Index Terms

Taylor subsumes Scott, Berry, Kahn and Plotkin
1. Theory of computation
  1. Logic
    1. Linear logic
  2. Models of computation
    1. Computability
      1. Lambda calculus

Recommendations

Taylor Expansion, Finiteness and Strategies
Abstract
We examine some recent methods introduced to extend Ehrhard and Regnier's result on Taylor expansion: infinite linear combinations of approximants of a lambda-term can be normalized while keeping all coefficients finite. The methods considered ...
Relational Graph Models, Taylor Expansion and Extensionality

We define the class of relational graph models and study the induced order- and equational- theories. Using the Taylor expansion, we show that all λ-terms with the same Böhm tree are equated in any relational graph model. If the model is moreover ...
The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
1,361
Total Downloads

Downloads (Last 12 months)136
Downloads (Last 6 weeks)16

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Arrial VGuerrieri GKesner DSobocinski PLago UEsparza J(2024)Genericity Through StratificationProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662113(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662113
Kerjean MPédrot PSobocinski PLago UEsparza J(2024)δ is for DialecticaProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662106(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662106
Accattoli BLancelot A(2024)Light GenericityFoundations of Software Science and Computation Structures10.1007/978-3-031-57231-9_2(24-46)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57231-9_2
Kerjean MLemay J(2023)Taylor Expansion as a Monad in Models of DiLL2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175753(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175753
Clairambault POlimpieri FPaquet H(2023)From Thin Concurrent Games to Generalized Species of Structures2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175681(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175681
Ehrhard T(2023)Coherent differentiationMathematical Structures in Computer Science10.1017/S0960129523000129(1-52)Online publication date: 28-Apr-2023
https://doi.org/10.1017/S0960129523000129
Barbarossa D(2022)Resource approximation for the λμ-calculusProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3532469(1-12)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3532469

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents