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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
\DOC DEPTH_CONV
\TYPE {DEPTH_CONV : (conv -> conv)}
\SYNOPSIS
Applies a conversion repeatedly to all the sub-terms of a term, in bottom-up
order.
\KEYWORDS
conversional.
\DESCRIBE
{DEPTH_CONV c tm} repeatedly applies the conversion {c} to all the subterms of
the term {tm}, including the term {tm} itself. The supplied conversion is
applied repeatedly (zero or more times, as is done by {REPEATC}) to each
subterm until it fails. The conversion is applied to subterms in bottom-up
order.
\FAILURE
{DEPTH_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 {DEPTH_CONV} applies a conversion to all
subterms to which it applies:
{
#DEPTH_CONV BETA_CONV "(\x. (\y. y + x) 1) 2";;
|- (\x. (\y. y + x)1)2 = 1 + 2
}
\noindent Here, there are two beta-redexes in the input term, one of which
occurs within the other. {DEPTH_CONV BETA_CONV} applies beta-conversion to
innermost beta-redex {(\y. y + x) 1} first. The outermost beta-redex is then
{(\x. 1 + x) 2}, and beta-conversion of this redex gives {1 + 2}.
Because {DEPTH_CONV} applies a conversion bottom-up, the final result may still
contain subterms to which the supplied conversion applies. For example, in:
{
#DEPTH_CONV BETA_CONV "(\f x. (f x) + 1) (\y.y) 2";;
|- (\f x. (f x) + 1)(\y. y)2 = ((\y. y)2) + 1
}
\noindent the right-hand side of the result still contains a beta-redex,
because the redex {"(\y.y)2"} is introduced by virtue an application of
{BETA_CONV} higher-up in the structure of the input term. By contrast, in the
example:
{
#DEPTH_CONV BETA_CONV "(\f x. (f x)) (\y.y) 2";;
|- (\f x. f x)(\y. y)2 = 2
}
\noindent all beta-redexes are eliminated, because {DEPTH_CONV} repeats the
supplied conversion (in this case, {BETA_CONV}) at each subterm (in this case,
at the top-level term).
\USES
If the conversion {c} implements the evaluation of a function in logic, then
{DEPTH_CONV c} will do bottom-up evaluation of nested applications of it.
For example, the conversion {ADD_CONV} implements addition of natural number
constants within the logic. Thus, the effect of:
{
#DEPTH_CONV ADD_CONV "(1 + 2) + (3 + 4 + 5)";;
|- (1 + 2) + (3 + (4 + 5)) = 15
}
\noindent is to compute the sum represented by the input term.
\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 an argument happens to generate
a failure with string {`QCONV`}, the operation of {DEPTH_CONV} will be
unpredictable.
\SEEALSO
ONCE_DEPTH_CONV, REDEPTH_CONV, TOP_DEPTH_CONV.
\ENDDOC
|
