On the longest perpetual reductions in orthogonal expression reduction systems

AbstractWe study perpetual reductions in orthogonal (or conflict-free) fully extended expression reduction systems (OERS). ERS is a formalism for rewriting that subsumes term rewriting systems (TRSs) and the λ-calculus. We design a strategy that, for any given term t in a fully extended OERS, constructs a longest reduction starting from t if t is strongly normalizing and otherwise constructs an infinite reduction. We call this strategy a limit strategy. For a large class of OERSs a limit strategy is computable. The Conservation Theorem for fully extended OERSs follows easily from the properties of the strategy. We develop a method for computing the lengths of longest reductions in fully extended OERSs. For strongly persistent fully extended OERSs the algorithm does not require actual transformation of the input term. As a corollary, we get an algorithm for computing the lengths of longest developments in OERSs