SE 504   Spring 2025
HW #5: Tail Recursion
Due: 4:00pm, Friday, April 11

1. Consider this tail recursive definition of function H : ℕ × ℕ → ℕ (where ℕ denotes the set of nonnegative integers):

H.m.n = { m max n   if m min n = 0
H.(m−1).(n−1)    otherwise

Using this definition, follow the standard procedure (as covered in lecture and on the relevant web page) by which to derive a program that satisfies the specification below (in which M and N are the inputs). Make sure that your program is appropriately annotated to include a loop invariant and bound function. You may assume that min and max are binary infix operators in our programming language. 

|[ con M, N : int;   { M,N ≥ 0 }
   var k : int;

   k := ?

   {Q: k = H.M.N }
]|

2. Consider this pseudo-tail recursive function definition, which describes a function having signature ℕ+ → ℕ (where ℕ denotes the set of nonnegative integers and ℕ+ denotes the set of positive integers):

G.n = { 0    if n=0
2 + G.(n−1)    otherwise (i.e., if n>0)

From this definition, use the procedure covered in lecture (and in the relevant web page) by which to derive a program that computes the function. That is, complete the program specified below, in which N is to be interpreted as being the input. Make sure that your program is appropriately annotated to include a loop invariant and bound function.

As an intermediate step, you should derive from the pseudo-tail recursive definition of G a (fully) tail recursive definition for function H (or G' if you prefer) such that (for every positive integer n) H.n.e = G.n, where e is the appropriate identity element. 

|[ con N : nat;  { N > 0 }
   var k : nat;

   k := ?

   {Q: k = G.N }
]|

3. Consider this pseudo-tail recursive function definition, which describes a function having signature ℕ × ℕ ⟶ ℕ

f.k.m = { 0    if k=0
f.(k/2).(2m)    if k≠0 ∧ isEven.k
m + f.(k-1).m    if ¬isEven.k

From this definition, use the procedure covered in class (and in the relevant web page) by which to derive a program that computes the function. That is, complete the specification below, in which K and M are to be interpreted as being the inputs.

As an intermediate step, you could derive from the pseudo-tail recursive definition of f a (fully) tail recursive definition for function f' such that (for all natural numbers k and m) f'.k.m.e = f.k.m, where e is the appropriate identity element.

If you don't recognize the function f upon first glance at its definition, you should recognize it sometime thereafter. 

|[ con K,M : int;  { K,M ≥ 0 }
   var z : int;

   z := ?

   {Q: z = f.K.M }
]|

4. (List Reversal)
The following introduces program constructs by which to manipulate lists.

You may make use of the following axioms and theorems.

For all  b:T  and  z,z1,z2 : list<T> :

Axiom 1: empty | z = z (empty: left identity of  | )
Axiom 2: z | empty = z (empty: right identity of  | )
Axiom 3: head.([b] | z) = b (definition of head)
Axiom 4: tail.([b] | z) = z (definition of tail)
Axiom 5: (z ≠ empty) ⇒ (z = [head.z] | tail.z) (universality of head/tail)
Axiom 6: ([b] | z1) | z2  =  [b] | (z1 | z2) (basis for associativity of |)
Theorem 1: (z1 | z2) | z3 = z1 | (z2 | z3) (associativity of  | )

Consider this pseudo-tail recursive function definition of Rev : list<T> → list<T>:

Rev.x = { empty   if x = empty
Rev.(tail.x)  |  [head.x]    otherwise

Using this definition, follow the standard procedure (as covered in lecture and in the relevant web page) by which to derive a program that satisfies the specification below (in which T stands for an arbitary data type). Make sure that your program is appropriately annotated to include a loop invariant and bound function.

As an intermediate step, from the given definition of function Rev you should derive a (fully) tail recursive definition for function Rev' such that (for all lists x) Rev'.x.empty = Rev.x.

Notice that in the recursive case of the definition, the application of Rev is the left operand of the catenate (or append, if you prefer) operator, not the right operand. This is the opposite of the template that we covered in lecture, which means that the roles being played by the two operands here are reversed, which you must take account of. 

|[ con X : list<T>;
   var z : list<T>;

   z := ?

   {Q': z = Rev'.X.empty }
   {Q: z = Rev.X }
]|