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 |
Funding
Key words and phrases: call-by-value, standardization, sequentialization, observational equivalence, sigma-reduction, head reduction, parallel reduction, internal reduction, standard sequence, lambda-calculus, solvability, potential valuability. ∗ This paper is a revised and extended version of [GPR15], invited for the special issue of TLCA 2015. This work has been supported by LINTEL TO Call1 2012 0085, a Research Project funded by the “Com-pagnia di San Paolo”, and by the A*MIDEX project (ANR-11-IDEX-0001-02) funded by the “Investissements d’Avenir” French Government program, managed by the French National Research Agency (ANR).
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