Clausal Language (ver. 5.81.21, by P.J. Voda, J. Komara, J. Kluka)

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. Course of Values Recursion.

Subsection. Course of Values Recursion with Substitution in Parameters.

Divisibility predicate.

x ∣ y \leftrightarrow \exists z y = x \cdot z

Greatest common divisor. Specification of the greatest common divisor function $\gcd (x, y)$ :

x \neq 0 \lor y \neq 0 \to \gcd (x, y) ∣ x \land \gcd (x, y) ∣ y

(x \neq 0 \lor y \neq 0) \land z ∣ x \land z ∣ y \to z ≦ \gcd (x, y)

Euclidean algorithm I. Find a course of values recursive definition of $\gcd (x, y)$ based on the property

x \neq 0 \land z ∣ x \to z ∣ y \leftrightarrow z ∣ y mod x

\gcd (x, y) = ?

Subsection. Course of Values Recursion with Measure.

Maximum.

\max (x, y) = x \leftarrow x ≧ y

\max (x, y) = y \leftarrow x < y

Euclidean algorithm II. Find a course of values recursive definition of $\gcd (x, y)$ based on the property

x < y \land z ∣ x \to z ∣ y \leftrightarrow z ∣ y \dot{-} x

[CL] Remark. Note that we have

x = 0 \lor y = 0 \to \gcd (x, y) = \max (x, y)

\gcd (x, y) = \max (x, y) \leftarrow x = 0

\gcd (x, y) = \max (x, y) \leftarrow x \neq 0 \land y = 0

\gcd (x, y) = ? \leftarrow x \neq 0 \land y \neq 0

Section. Iterative Recursion. See also in [1]:

the paragraph Fibonacci function in the section Primitive Recursion and
the paragraph Simulation of for-loops by recursion in the section Course of Values Recursion.

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

f_{0} = 0

f_{1} = 1

f_{n + 2} = f_{n + 1} + f_{n}

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

While-loop by primitive recursion with substitution in parameters.

g (n, a, b) = ?

Invariant:

g (n, f_{k + 1}, f_{k}) = f_{n + 1 + k}

f_{n} = ?

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

f_{0} = 0

f_{1} = 1

f_{2} = 2

f_{n + 3} = f_{n + 2} + f_{n + 1} + f_{n}

While-loop by primitive recursion with substitution in parameters.

g (n, a, b, c) = ?

Invariant:

g (n, f_{k + 2}, f_{k + 1}, f_{k}) = f_{n + 2 + k}

f_{n} = ?

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

f_{0} = 0

f_{1} = 1

f_{n + 2} = f_{n + 1} + f_{n} + n

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

For-loop by backward recursion with substitution in parameters.

g (i, n, a, b) = ?

Invariant:

i ≦ n \to g (i, n, f_{i + 1}, f_{i}) = f_{n + 1}

f_{n} = ?

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

f_{0} = 0

f_{1} = 1

f_{2} = 2

f_{n + 3} = f_{n + 2} + f_{n + 1} + f_{n} + n

For-loop by backward recursion with substitution in parameters.

g (i, n, a, b, c) = ?

Invariant:

i ≦ n \to g (i, n, f_{i + 2}, f_{i + 1}, f_{i}) = f_{n + 2}

f_{n} = ?