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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
%%% NAME/LOGIN-ID Camil Staps / s4498062
%%% ACKNOWLEDGMENTS:
th_E: THEORY
BEGIN
%%%
%%% Standard development of iterative factorial-with-accumulator.
%%% Start with a "specification" of the factorial function.
%%%
fac(n:nat): RECURSIVE nat =
IF n = 0
THEN 1
ELSE fac(n-1) * n
ENDIF
MEASURE n
%%%
%%% A few simple facts about the factorial function.
%%%
thm_E_0: LEMMA (FORALL (k:nat): k>=1 IMPLIES fac(k) < fac(k+1))
thm_E_1: THEOREM (FORALL (k:nat): 1 <= fac(k))
thm_E_2: THEOREM (FORALL (k:nat): k <= fac(k))
%%%
%%% In tfac, below, all recursive calls are in the tail position. In operational terms,
%%% tfac "improves" fac because a no space is needed for a recursion stack. In other
%%% words, tfac is and instance of the "implementation model" for sequential execution.
%%%
tfac(n:nat, m:nat): RECURSIVE nat =
IF n = 0
THEN m
ELSE tfac(n - 1, m * n)
ENDIF
MEASURE n
%%%
%%% We should prove, though, that tfac is equivalent to fac. They are not "equal" because,
%%% for one thing, tfac takes two arguments and fac takes only one. In fact, tfac(n, m)
%%% only computes fac(n) when m = 1.
%%%
%%% However, in trying to prove this, we run into a problem...
%%% In the inductive case, we'll get something like this:
%%%
%%% [-1] fac(J) = tfac(J, 1)
%%% |------------------------
%%% [1] (J+1) * fac(J) = tfac(J, J+1)
%%%
%%% To complete the proof, we need to "distribute" J+1 outside fact. But attempting
%%% to prove this, for just "J+1" will fail. A _generalization_ is needed...
%%%
lemma_E_3: LEMMA (FORALL (m:nat, n:nat): tfac(m, n) = n * fac(m))
%%%
%%% On the strength of this lemma, we can prove the correctness of tfac.
th_E_4: THEOREM (FORALL (k:nat): fac(k) = tfac(k, 1))
%%%
%%% Below, we'll do the same standard development for iterative the Fibonacci function.
%%% Except this time, YOU have to find the appropriate lemma! Although there are several
%%% reasonable possibilities for the needed lemma, it is not easy to think of one.
%%%
%%% Remember that the lemma must GENERALIZE the desired result.
%%%
fib(n:nat): RECURSIVE nat =
(IF n = 0 THEN 1
ELSIF n = 1 THEN 1
ELSE fib(n - 1) + fib(n - 2)
ENDIF)
MEASURE n
%%%
%%% Tail-recursive version of fib.
%%%
tfib(n:nat, m:nat, p:nat): RECURSIVE nat =
(IF n = 0
THEN m
ELSE tfib(n - 1, p, p + m)
ENDIF)
MEASURE n
%%%
%%% YOU will need to discover a nontrivial lemma to prove thm.
%%% Place your lemma just below, before thm_E_6.
%%%
lem_E_Camil_2: LEMMA
(FORALL (i:nat, m:nat, p:nat):
tfib(i, m, p) =
IF i = 0 THEN m
ELSIF i = 1 THEN p
ELSE fib(i-2)*m + fib(i-1)*p
ENDIF)
thm_E_6: THEOREM
(FORALL (i:nat):
tfib(i, 1, 1) = fib(i))
END th_E
|
