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

• Type: Journal
• Year: 2015
• Where: RTA
• Authors: Giulio Guerrieri
• Keywords: RTA 2015, Theoretical Computer Science