1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
\DOC REDEPTH_CONV
\TYPE {REDEPTH_CONV : conv -> conv}
\SYNOPSIS
Applies a conversion bottom-up to all subterms, retraversing changed ones.
\KEYWORDS
conversional.
\DESCRIBE
{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 `(\f x. (f x) + 1) (\y.y) 2`;;
val it : thm = |- (\f x. f x + 1) (\y. y) 2 = 2 + 1
}
\noindent Here, {BETA_CONV} is first applied successfully to the (beta-redex)
subterm:
{
`(\f x. (f x) + 1) (\y.y)`
}
\noindent This application reduces this subterm to:
{
`(\x. ((\y.y) x) + 1)`
}
\noindent {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`}.
\SEEALSO
DEPTH_CONV, ONCE_DEPTH_CONV, TOP_DEPTH_CONV, TOP_SWEEP_CONV.
\ENDDOC
|
