Mirroring Call-By-Need, or Values Acting Silly - Laboratoire d'informatique de l'X (LIX)
Communication Dans Un Congrès Année : 2024

Mirroring Call-By-Need, or Values Acting Silly

Résumé

Call-by-need evaluation for the λ-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need - that is, its operational equivalence with call-by-name - showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
Fichier principal
Vignette du fichier
LIPIcs.FSCD.2024.23.pdf (983.53 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
licence

Dates et versions

hal-04837722 , version 1 (13-12-2024)

Licence

Identifiants

Citer

Beniamino Accattoli, Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. FSCD 2024 - 9th International Conference on Formal Structures for Computation and Deduction, Jul 2024, Tallin, Estonia. ⟨10.4230/LIPIcs.FSCD.2024.23⟩. ⟨hal-04837722⟩
0 Consultations
0 Téléchargements

Altmetric

Partager

More