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
|
\DOC SCANL_CONV
\TYPE {SCANL_CONV : conv -> conv}
\SYNOPSIS
Computes by inference the result of applying a function to elements of a list.
\KEYWORDS
conversion, list.
\DESCRIBE
{SCANL_CONV} takes a conversion {conv} and a term {tm} in the following form:
{
SCANL f e0 [x1;...xn]
}
\noindent It returns the theorem
{
|- SCANL f e0 [x1;...xn] = [e0; e1; ...;en]
}
\noindent where {ei} is the result of applying the function {f} to
the result of the previous iteration and the current element, i.e.,
{ei = f e(i-1) xi}. The iteration starts from the left-hand side (the
head) of the list.
The user supplied conversion {conv} is used to derive a theorem
{
|- f e(i-1) xi = ei
}
\noindent which is used in the next iteration.
\FAILURE
{SCANL_CONV conv tm} fails if {tm} is not of the form described above,
or failure occurs when evaluating {conv "f e(i-1) xi"}.
\EXAMPLE
To sum the elements of a list and save the result at each step, one can evaluate
{
SCANL_CONV ADD_CONV "SCANL $+ 0 [1;2;3]";;
}
\noindent which returns the following theorem:
{
|- SCANL $+ 0[1;2;3] = [0;1;3;6]
}
\noindent In general, if the function {f} is an explicit lambda abstraction
{(\x x'. t[x,x'])}, the conversion should be in the form
{
((RATOR_CONV BETA_CONV) THENC BETA_CONV THENC conv'))
}
\noindent where {conv'} applied to {t[x,x']} returns the theorem
{
|-t[x,x'] = e''.
}
\SEEALSO
SCANR_CONV, FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV.
\ENDDOC
|
