Guerrieri, Giulio and Paolini, Luca and Della Rocca, Simona Ronchi - Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus

lmcs:4162 - Logical Methods in Computer Science, December 22, 2017, Volume 13, Issue 4
Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus

Authors: Guerrieri, Giulio and Paolini, Luca and Della Rocca, Simona Ronchi

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 characterizations 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.


Source : oai:arXiv.org:1611.07255
DOI : 10.23638/LMCS-13(4:29)2017
Volume: Volume 13, Issue 4
Published on: December 22, 2017
Submitted on: December 22, 2017
Keywords: Computer Science - Logic in Computer Science,03B40, 68N18,F.3.2,D.3.1,F.4.1


Share

Consultation statistics

This page has been seen 268 times.
This article's PDF has been downloaded 98 times.