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

Literature.

Chapter. Numeric Programs.

Section. Primitive Recursion.

Summation. The following component contains a primitive recursive definition of the summation function $\sum_{i = 0}^{n} i$ :

\sum_{i = 0}^{0} i = 0

\sum_{i = 0}^{n + 1} i = \sum_{i = 0}^{n} i + n + 1

\sum_{i = 0}^{n} i = 0 \leftarrow n = 0

\sum_{i = 0}^{n} i = \sum_{i = 0}^{n ∸ 1} i + n \leftarrow n \neq 0

Factorial. Define by primitive recursion the factorial function $n!$ :

0! = 1

(n + 1)! = (n + 1) \cdot n!

n! = ?

Exponentiation. Define by primitive recursion the exponentiation function $x^{y}$ :

x^{0} = 1

x^{y + 1} = x \cdot x^{y}

x^{y} = ?

Section. Course of Values Recursion.

Fibonacci sequence. Specification of the function ${fib}_{n}$ computing the $n$ -th element of the Fibonacci sequence:

{fib}_{0} = 0

{fib}_{1} = 1

{fib}_{n + 2} = {fib}_{n + 1} + {fib}_{n}

Find a course of values recursive definition of ${fib}_{n}$ .

{fib}_{n} = ? \leftarrow n = 0

{fib}_{n} = ? \leftarrow n \neq 0 \land n = 1

{fib}_{n} = ? \leftarrow n \neq 0 \land n \neq 1

Integer division. Specification of the integer division function $x \div y$ :

x \div 0 = 0

y \neq 0 \to \exists r (x = x \div y \cdot y + r \land r < y)

Find a course of values recursive definition of $x \div y$ .

x \div y = ?

Remainder. Specification of the remainder function $x mod y$ :

x mod 0 = 0

y \neq 0 \to \exists q (x = q \cdot y + x mod y \land x mod y < y)

Find a course of values recursive definition of $x mod y$ .

x \mod y = ?

Subsection. Course of Values Recursion with Substitution in Parameters.

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.

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