eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
6:1
6:17
10.4230/LIPIcs.TYPES.2018.6
article
Normalization by Evaluation for Typed Weak lambda-Reduction
Sestini, Filippo
1
Functional Programming Laboratory, University of Nottingham, United Kingdom
Weak reduction relations in the lambda-calculus are characterized by the rejection of the so-called xi-rule, which allows arbitrary reductions under abstractions. A notable instance of weak reduction can be found in the literature under the name restricted reduction or weak lambda-reduction.
In this work, we attack the problem of algorithmically computing normal forms for lambda-wk, the lambda-calculus with weak lambda-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute lambda-wk-normal forms. We observe that some aspects of weak lambda-reduction prevent us from normalizing lambda-wk directly, thus devise a new, better-behaved weak calculus lambda-ex, and reduce the normalization problem for lambda-w to that of lambda-ex. We finally define type systems for both calculi and apply Normalization by Evaluation to lambda-ex, obtaining a normalization proof for lambda-wk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.6/LIPIcs.TYPES.2018.6.pdf
normalization
lambda-calculus
reduction
term-rewriting
Agda