Call-by-value and call-by-need lambda-calculi are defined using the distinguished syntactic category of values. In theoretical studies, values are variables and abstractions. In more practical works, values are usually defined simply as abstractions. This paper shows that practical values lead to a more efficient process of substitution—for both call-by-value and call-by-need—once the usual hypothesis for implementations hold (terms are closed, reduction does not go under abstraction, and substitution is done in micro steps, replacing one variable occurrence at the time). Namely, the number of substitution steps becomes linear in the number of β-redexes, while theoretical values only provide a quadratic bound.

Accattoli, B., Sacerdoti Coen, C. (2014). On the value of variables. Berlin : Springer Berlin Heidelberg [10.1007/978-3-662-44145-9_3].

On the value of variables

ACCATTOLI, BENIAMINO;SACERDOTI COEN, CLAUDIO
2014

Abstract

Call-by-value and call-by-need lambda-calculi are defined using the distinguished syntactic category of values. In theoretical studies, values are variables and abstractions. In more practical works, values are usually defined simply as abstractions. This paper shows that practical values lead to a more efficient process of substitution—for both call-by-value and call-by-need—once the usual hypothesis for implementations hold (terms are closed, reduction does not go under abstraction, and substitution is done in micro steps, replacing one variable occurrence at the time). Namely, the number of substitution steps becomes linear in the number of β-redexes, while theoretical values only provide a quadratic bound.
2014
Logic, Language, Information and Computation
36
50
Accattoli, B., Sacerdoti Coen, C. (2014). On the value of variables. Berlin : Springer Berlin Heidelberg [10.1007/978-3-662-44145-9_3].
Accattoli, B.; Sacerdoti Coen, C.
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/519735
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact