TY - GEN
T1 - Factorization and normalization, essentially
AU - Accattoli, Beniamino
AU - Faggian, Claudia
AU - Guerrieri, Giulio
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019/1/1
Y1 - 2019/1/1
N2 - λ-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems. In this paper we provide simple proof techniques for these theorems. Our starting point is a revisitation of Takahashi’s technique to prove factorization for head reduction. Our technique is both simpler and more powerful, as it works in cases where Takahashi’s does not. We then pair factorization with two other abstract properties, defining essential systems, and show that normalization follows. Concretely, we apply the technique to four case studies, two classic ones, head and the leftmost-outermost reductions, and two less classic ones, non-deterministic weak call-by-value and least-level reductions.
AB - λ-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems. In this paper we provide simple proof techniques for these theorems. Our starting point is a revisitation of Takahashi’s technique to prove factorization for head reduction. Our technique is both simpler and more powerful, as it works in cases where Takahashi’s does not. We then pair factorization with two other abstract properties, defining essential systems, and show that normalization follows. Concretely, we apply the technique to four case studies, two classic ones, head and the leftmost-outermost reductions, and two less classic ones, non-deterministic weak call-by-value and least-level reductions.
UR - https://www.scopus.com/pages/publications/85076707314
U2 - 10.1007/978-3-030-34175-6_9
DO - 10.1007/978-3-030-34175-6_9
M3 - Conference contribution
AN - SCOPUS:85076707314
SN - 9783030341749
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 159
EP - 180
BT - Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Proceedings
A2 - Lin, Anthony Widjaja
PB - Springer
T2 - 17th Asian Symposium on Programming Languages and Systems, APLAS 2019
Y2 - 1 December 2019 through 4 December 2019
ER -