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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publication2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015
EditorsSantiago Escobar, David Sabel, Yuki Chiba, Naoki Nishida, Manfred Schmidt-Schauss
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages3-17
Number of pages15
Volume46
ISBN (Electronic)9783939897941
DOIs
Publication statusPublished - 1 Jan 2015
Event2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 - Warsaw, Poland
Duration: 2 Jul 2015 → …

Conference

Conference2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015
CountryPoland
CityWarsaw
Period2/07/15 → …

Keywords

  • (strong) normalization
  • Call-by-value
  • Confluence
  • Evaluation
  • Head reduction
  • Internal reduction
  • Lambda-calculus
  • Reduction strategy
  • Sequentialization
  • Sigma-reduction

ASJC Scopus subject areas

  • Geography, Planning and Development
  • Modelling and Simulation

Cite this

Guerrieri, G. (2015). Head reduction and normalization in a call-by-value lambda-calculus. In S. Escobar, D. Sabel, Y. Chiba, N. Nishida, & M. Schmidt-Schauss (Eds.), 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015 (Vol. 46, pp. 3-17). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/OASIcs.WPTE.2015.3

Head reduction and normalization in a call-by-value lambda-calculus. / Guerrieri, Giulio.

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015. ed. / Santiago Escobar; David Sabel; Yuki Chiba; Naoki Nishida; Manfred Schmidt-Schauss. Vol. 46 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. p. 3-17.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Guerrieri, G 2015, Head reduction and normalization in a call-by-value lambda-calculus. in S Escobar, D Sabel, Y Chiba, N Nishida & M Schmidt-Schauss (eds), 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015. vol. 46, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 3-17, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015, Warsaw, Poland, 2/07/15. https://doi.org/10.4230/OASIcs.WPTE.2015.3
Guerrieri G. Head reduction and normalization in a call-by-value lambda-calculus. In Escobar S, Sabel D, Chiba Y, Nishida N, Schmidt-Schauss M, editors, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015. Vol. 46. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2015. p. 3-17 https://doi.org/10.4230/OASIcs.WPTE.2015.3
Guerrieri, Giulio. / Head reduction and normalization in a call-by-value lambda-calculus. 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015. editor / Santiago Escobar ; David Sabel ; Yuki Chiba ; Naoki Nishida ; Manfred Schmidt-Schauss. Vol. 46 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. pp. 3-17
@inproceedings{5c74ee14669c4aecb8ebebe1b5194e45,
title = "Head reduction and normalization in a call-by-value lambda-calculus",
abstract = "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.",
keywords = "(strong) normalization, Call-by-value, Confluence, Evaluation, Head reduction, Internal reduction, Lambda-calculus, Reduction strategy, Sequentialization, Sigma-reduction",
author = "Giulio Guerrieri",
year = "2015",
month = "1",
day = "1",
doi = "10.4230/OASIcs.WPTE.2015.3",
language = "English",
volume = "46",
pages = "3--17",
editor = "Santiago Escobar and David Sabel and Yuki Chiba and Naoki Nishida and Manfred Schmidt-Schauss",
booktitle = "2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
address = "Germany",

}

TY - GEN

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

AU - Guerrieri, Giulio

PY - 2015/1/1

Y1 - 2015/1/1

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

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

KW - (strong) normalization

KW - Call-by-value

KW - Confluence

KW - Evaluation

KW - Head reduction

KW - Internal reduction

KW - Lambda-calculus

KW - Reduction strategy

KW - Sequentialization

KW - Sigma-reduction

UR - http://www.scopus.com/inward/record.url?scp=84938506744&partnerID=8YFLogxK

U2 - 10.4230/OASIcs.WPTE.2015.3

DO - 10.4230/OASIcs.WPTE.2015.3

M3 - Conference contribution

VL - 46

SP - 3

EP - 17

BT - 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015

A2 - Escobar, Santiago

A2 - Sabel, David

A2 - Chiba, Yuki

A2 - Nishida, Naoki

A2 - Schmidt-Schauss, Manfred

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -