REDEPTH_CONV : conv -> conv

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 CONDITIONS

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 `(\f x. (f x) + 1) (\y.y) 2`;;
  val it : thm = |- (\f x. f x + 1) (\y. y) 2 = 2 + 1

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`.