The theory of call-by-value solvability
| Autor: | Beniamino Accattoli, Giulio Guerrieri |
|---|---|
| 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), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), University of Bath [Bath] |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.855-885. ⟨10.1145/3547652⟩ |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3547652 |
| Popis: | International audience; The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|