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
53
54
55
56
57
58
59
60
|
\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";;
|- (\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"}.
\COMMENTS
The implementation of this function uses failure to avoid rebuilding
unchanged subterms. That is to say, during execution the failure string
{`QCONV`} may be generated and later trapped. The behaviour of the function
is dependent on this use of failure. So, if the conversion given as argument
happens to generate a failure with string {`QCONV`}, the operation of
{REDEPTH_CONV} will be unpredictable.
\SEEALSO
DEPTH_CONV, ONCE_DEPTH_CONV, TOP_DEPTH_CONV.
\ENDDOC
|
