¶Abstract

Weak reduction relations in the λ-calculus are characterized by the rejection of the so-called ξ-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 λ-reduction.

In this work, we attack the problem of algorithmically computing normal forms for λwk, the λ-calculus with weak λ-reduction. We do so by first contrasting it with other weak systems, arguing that their notion of reduction is not strong enough to compute λwk-normal forms. We observe that some aspects of weak λ-reduction prevent us from normalizing λwk directly, thus devise a new, better-behaved weak calculus λex, and reduce the normalization problem for λw to that of λex. We finally define type systems for both calculi and apply Normalization by Evaluation to λex, obtaining a normalization proof for λwk as a corollary. We formalize all our results in Agda, a proof-assistant based on intensional Martin-Löf Type Theory.

¶BiBTeX

@InProceedings{sestini:LIPIcs.TYPES.2018.6,
  author =	{Sestini, Filippo},
  title =	{{Normalization by Evaluation for Typed Weak lambda-Reduction}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.6},
  URN =		{urn:nbn:de:0030-drops-114101},
  doi =		{10.4230/LIPIcs.TYPES.2018.6},
  annote =	{Keywords: normalization, lambda-calculus, reduction, term-rewriting, Agda}
}