Literature.

• [1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.

• [2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

Chapter. Numeric Programs.

Section. Iterative Recursion.

Exercise. Find an efficient, tail recursive implementation of the function:

Your solution should simulate the following while-loop by primitive recursion with substitution in parameters:

def f(n):
    if n == 0:
        return 0
    else:
        n,a,b = n-1,1,0
        while n != 0:
            n,a,b = n-1,a+b,a
        return a

Verify your implementation.

While-loop by primitive recursion with substitution in parameters.

Prove

Exercise. Find a similar tail recursive implementation of the function:

While-loop by primitive recursion with substitution in parameters.

Exercise. Find an efficient, tail recursive implementation of the function:

Your solution should simulate the following for-loop by backward recursion with substitution in parameters:

def f(n):
    if n == 0:
        return 0
    else:
        n,a,b = n-1,1,0
        for i in range(0,n):
            a,b = a+b+i,a
        return a

Verify your implementation.

For-loop by backward recursion with substitution in parameters.

Prove

Exercise. (1 point) Find a similar tail recursive implementation of the function:

For-loop by backward recursion with substitution in parameters.