Perpetuality and Uniform Normalization

10 years 7 months ago
Perpetuality and Uniform Normalization
We de ne a perpetual one-step reduction strategy which enables one to construct minimal (w.r.t. Levy's ordering 2 on reductions) in nite reductions in Conditional Orthogonal Expression Reduction Systems. We use this strategy to derive two characterizations of perpetual redexes, i.e., redexes whose contractions retain the existence of in nite reductions. These characterizations generalize existing related criteria for perpetuality of redexes. We give a number of applications of our results, demonstrating their usefulness. In particular, we prove equivalence of weak and strong normalization (the uniform normalization property) for various restricted -calculi, which cannot be derived from previously known perpetuality criteria.
Zurab Khasidashvili, Mizuhito Ogawa
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1997
Where ALP
Authors Zurab Khasidashvili, Mizuhito Ogawa
Comments (0)