Random Descent

摘要

We introduce a method for establishing that a reduction strategy is normalising and minimal, or dually, that it is perpetual and maximal, in the setting of abstract rewriting. While being complete, the method allows to reduce these global properties to the verification of local diagrams. We show its usefulness both by giving uniform proofs of some known results and by establishing new ones.