%%% 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