Strong Call-by-Value is Reasonable, Implosively
| Autor: | Andrea Condoluci, Claudio Sacerdoti Coen, Beniamino Accattoli |
|---|---|
| Přispěvatelé: | Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion (PARTOUT), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Tweag I/O, Department of Computer Science and Engineering [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Accattoli B., Condoluci A., Sacerdoti Coen C., ANR-16-CE40-0004,COCA_HOLA,Modèles de coût pour les analyses de complexité des langages de programmation d'ordre supérieur(2016) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
FOS: Computer and information sciences
Evaluation strategy Computer Science - Logic in Computer Science Theoretical computer science Logarithm Computer science 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 0102 computer and information sciences 16. Peace & justice 01 natural sciences Time cost Abstract machine Exponential function Logic in Computer Science (cs.LO) Turing machine symbols.namesake Quadratic equation 010201 computation theory & mathematics symbols lambda calculus call-by-value reduction machines explicit substitutions Overhead (computing) 0101 mathematics ComputingMilieux_MISCELLANEOUS |
| Zdroj: | 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-14, ⟨10.1109/LICS52264.2021.9470630⟩ LICS |
| DOI: | 10.1109/LICS52264.2021.9470630⟩ |
| Popis: | Whether the number of beta-steps in the lambda-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate problem, which depends on the notion of evaluation strategy. Since the nineties, it is known that weak (that is, out of abstractions) call-by-value evaluation is a reasonable strategy while L\'evy's optimal parallel strategy, which is strong (that is, it reduces everywhere), is not. The strong case turned out to be subtler than the weak one. In 2014 Accattoli and Dal Lago have shown that strong call-by-name is reasonable, by introducing a new form of useful sharing and, later, an abstract machine with an overhead quadratic in the number of beta-steps. Here we show that also strong call-by-value evaluation is reasonable for time, via a new abstract machine realizing useful sharing and having a linear overhead. Moreover, our machine uses a new mix of sharing techniques, adding on top of useful sharing a form of implosive sharing, which on some terms brings an exponential speed-up. We give examples of families that the machine executes in time logarithmic in the number of beta-steps. Comment: Technical report associated to a LICS 2021 paper |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|