Conv.REDEPTH

STRUCTURE

SYNOPSIS

Applies a conversion bottom-up to all subterms, retraversing changed ones.

DESCRIPTION

REDEPTH_CONV c tm applies the conversion c repeatedly to all subterms of the term tm and recursively applies REDEPTH_CONV c to each subterm at which c succeeds, until there is no subterm remaining for which application of c succeeds.

More precisely, REDEPTH_CONV c tm repeatedly applies the conversion c to all the subterms of the term tm, including the term tm itself. The supplied conversion c is applied to the subterms of tm in bottom-up order and is applied repeatedly (zero or more times, as is done by REPEATC) to each subterm until it fails. If c is successfully applied at least once to a subterm, t say, then the term into which t is transformed is retraversed by applying REDEPTH_CONV c to it.

FAILURE

REDEPTH_CONV c tm never fails but can diverge if the conversion c can be applied repeatedly to some subterm of tm without failing.

EXAMPLE

The following example shows how REDEPTH_CONV retraverses subterms:

   - REDEPTH_CONV BETA_CONV (Term `(\f x. (f x) + 1) (\y.y) 2`);
   val it = |- (\f x. (f x) + 1)(\y. y)2 = 2 + 1 : thm

Here, BETA_CONV is first applied successfully to the (beta-redex) subterm:

   (\f x. (f x) + 1) (\y.y)

This application reduces this subterm to:

   (\x. ((\y.y) x) + 1)

REDEPTH_CONV BETA_CONV is then recursively applied to this transformed subterm, eventually reducing it to (\x. x + 1). Finally, a beta-reduction of the top-level term, now the simplified beta-redex (\x. x + 1) 2, produces 2 + 1.

COMMENTS

The implementation of this function uses failure to avoid rebuilding unchanged subterms. That is to say, during execution the exception QConv.UNCHANGED may be generated and later trapped. The behaviour of the function is dependent on this use of failure. So, if the conversion given as an argument happens to generate the same exception, the operation of REDEPTH_CONV will be unpredictable.

SEEALSO

DEPTH_CONV, ONCE_DEPTH_CONV, TOP_DEPTH_CONV