Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 10, Issue 3, pp. 461-487: Abstract.

Axiomatic rewriting theory II: the [lgr][sgr]-calculus enjoys finite normalisation cones

P-A Melliès

Preuves, Programmes, Systèmes, CNRS EPJ-2025, Université Paris 7, Paris, France, E-mail: mellies@pps.jussieu.fr

Every needed strategy is normalizing in the [lgr]-calculus. Here, we extend the result to the [lgr][sgr]-calculus, a [lgr]-calculus with explicit substitutions. The extension requires considering rewriting systems with critical pairs, confluent or non-confluent, and developing for them a satisfactory theory of needed normalization. Our idea is to count for every term M the number of its normalizing paths, up to Lévy permutation equivalence. We deduce from standardization that every needed strategy normalizes when this number is finite. The number is zero or one in the [lgr]-calculus, and we show that it is finite in the [lgr][sgr]-calculus.

Keywords: rewriting theory, lambda calculus, explicit substitutions, strategies, critical pairs, normalization

  Full-Text PDF  (351 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2000.