Sciweavers

Share
RTA
2015
Springer

Leftmost Outermost Revisited

3 years 6 months ago
Leftmost Outermost Revisited
We present an elementary proof of the classical result that the leftmost outermost strategy is normalizing for left-normal orthogonal rewrite systems. Our proof is local and extends to hyper-normalization and weakly orthogonal systems. Based on the new proof, we study basic normalization, i.e., we study normalization if the set of considered starting terms is restricted to basic terms. This allows us to weaken the left-normality restriction. We show that the leftmost outermost strategy is hyper-normalizing for basically left-normal orthogonal rewrite systems. This shift of focus greatly extends the applicability of the classical result, as evidenced by the experimental data provided. 1998 ACM Subject Classification F.4.2 Grammars and Other Rewriting Systems Keywords and phrases term rewriting, strategies, normalization Digital Object Identifier 10.4230/LIPIcs.RTA.2015.209
Nao Hirokawa, Aart Middeldorp, Georg Moser
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where RTA
Authors Nao Hirokawa, Aart Middeldorp, Georg Moser
Comments (0)
books