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

Literature.

[1] J. Komara. Recursive Functions. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Lecture Notes in Theory of Computability. 2001.
[3] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
[4] I. Korec. Úvod do teórie algoritmov. Skriptá MFF UK, 1981.

[CL] CL-TeX.

[CL] Remark. Below use the non-strict version of the function $D$ from the module Standard; it plays the role of if-then-else construct.

Chapter. Declarative Programming.

Section. The Realm of Discrimination.

Discrimination on constant patterns.

Exercise. Find a simple closed form of the following clausal definition:

{fib}_{0} = 0

{fib}_{1} = 1

{fib}_{n} = {fib}_{n \dot{-} 1} + {fib}_{n \dot{-} 2} \leftarrow n \neq 0 \land n \neq 1

Solution.

{fib}_{n} = ?

Dichotomy discrimination.

Exercise. Find a simple closed form of the following clausal definition:

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

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

Solution.

\max (x, y) = ?

Exercise. Find a simple closed form of the following clausal definition:

x \div y = 0 \leftarrow y \neq 0 \land x < y

x \div y = (x \dot{-} y) \div y + 1 \leftarrow y \neq 0 \land x ≧ y

Note that by default

x \div 0 = 0

Solution.

x \div y = ?

Trichotomy discrimination.

Exercise. Find a simple closed form of the following clausal definition:

\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) = \gcd (x, y \dot{-} x) \leftarrow x \neq 0 \land y \neq 0 \land x < y

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

\gcd (x, y) = \gcd (x \dot{-} y, y) \leftarrow x \neq 0 \land y \neq 0 \land x > y

Solution.

\gcd (x, y) = ?

Discrimination on monadic patterns.

Exercise. Find a simple closed form of the following clausal definition:

x^{0} = 1

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

Solution.

x^{y} = ?

Exercise. Find a simple closed form of the following clausal definition:

A (0, y) = y + 1

A (x + 1, 0) = A (x, 1)

A (x + 1, y + 1) = A (x, A (x + 1, y))

Solution.

A (x, y) = ?

Discrimination on pair patterns.

Exercise. Find a simple closed form of the following clausal definition:

{∣ 0 ∣}_{p} = 0

{∣ v, w ∣}_{p} = {∣ v ∣}_{p} + {∣ w ∣}_{p} + 1

Solution.

{∣ x ∣}_{p} = ?

Exercise. Find a simple closed form of the following clausal definition:

Zip (0, 0) = 0

Zip ((v_{1}, w_{1}), v_{2}, w_{2}) = (v_{1}, v_{2}), Zip (w_{1}, w_{2})

Solution.

Zip (x, y) = ?