Head reduction and normalization in a call-by-value lambda-calculus

4 years 10 months ago
Head reduction and normalization in a call-by-value lambda-calculus
Recently, a standardization theorem has been proven for a variant of Plotkin’s call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this result was based on a partitioning between head and internal reductions. We study the head normalization for this call-by-value calculus with sigma-reductions and we relate it to the weak evaluation of original Plotkin’s call-by-value lambda-calculus. We give also a (non-deterministic) normalization strategy for the call-by-value lambda-calculus with sigma-reductions. 1998 ACM Subject Classification D.3.1 Formal Definitions and Theory, F.3.2 Semantics of Programming Language, F.4.1 Mathematical Logic, F.4.2 Grammars and Other Rewriting Systems. Keywords and phrases sequentialization, lambda-calculus, sigma-reduction, call-by-value, head reduction, internal reduction, (strong) normalization, evaluation, confluence, reduction strategy. Digital Object Identifier 10.4230/OASIcs.WPTE.2015.3
Giulio Guerrieri
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where RTA
Authors Giulio Guerrieri
Comments (0)