## Abstract

We study an extension of Plotkin’s call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characteriza- tions of many semantic properties. We prove that this extended calculus is a conservative refinement of Plotkin’s one. In particular, the notions of solvability and potential valuability for this calculus coincide with those for Plotkin’s call-by-value lambda-calculus. The proof rests on a standardization theorem proved by generalizing Takahashi’s approach of parallel reductions to our set of reduction rules. The standardization is weak (i.e. redexes are not fully sequentialized) because of overlapping interferences between reductions.

Original language | English |
---|---|

Article number | 29 |

Journal | Logical Methods in Computer Science |

Volume | 13 |

Issue number | 4 |

Early online date | 22 Dec 2017 |

DOIs | |

Publication status | Published - 22 Dec 2017 |

## Keywords

- Call-by-value
- Head reduction
- Internal reduction
- Lambda-calculus
- Observational equivalence
- Parallel reduction
- Potential valuability
- Sequentialization
- Sigma- reduction
- Solv- ability
- Standard sequence
- Standardization

## ASJC Scopus subject areas

- Theoretical Computer Science
- General Computer Science