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

Literature.

Chapter. Programs Operating on Lists.

Section. Operations on Lists.

Map. Given the function $f (x)$ , define the function ${Map}_{f} (x)$ such that

L {Map}_{f} (x) = L (x)

i < L (x) \to {Map}_{f} (x) [i] = f (x [i])

Verify your implementation!

{Map}_{f} (0) = 0

{Map}_{f} (v, w) = f (v), {Map}_{f} (w)

L {Map}_{f} (x) = L (x)

i < L (x) \to {Map}_{f} (x) [i] = f (x [i])

Zip and unzip. (bonus 1 1/2 points) Define the functions $Zip (x, y)$ and $Unzip (z)$ such that

L (x) = L (y) \to L Zip (x, y) = L (x)

L (x) = L (y) \land i < L (x) \to Zip (x, y) [i] = x [i], y [i]

and

L (x) = L (y) \to Unzip Zip (x, y) = x, y

Verify your implementations!

Zip (x, y) = ?

Unzip (z) = ?

L (x) = L (y) \to L Zip (x, y) = L (x)

L (x) = L (y) \land i < L (x) \to Zip (x, y) [i] = x [i], y [i]

L (x) = L (y) \to Unzip Zip (x, y) = x, y

Take and drop. (bonus 2 points) Define the functions $Take (n, x)$ and $Drop (n, x)$ such that

n ≦ L (x) \to L Take (n, x) = n

n ≦ L (x) \to \exists y x = Take (n, x) \oplus y

and

n ≦ L (x) \to L Drop (n, x) = L (x) \dot{-} n

n ≦ L (x) \to \exists y x = y \oplus Drop (n, x)

Verify your implementations!

Take (n, x) = ?

Drop (n, x) = ?

n ≦ L (x) \to L Take (n, x) = n

n ≦ L (x) \to \exists y x = Take (n, x) \oplus y

n ≦ L (x) \to L Drop (n, x) = L (x) \dot{-} n

n ≦ L (x) \to \exists y x = y \oplus Drop (n, x)

Interval. (bonus 1 point) Define the function $[m .. n)$ such that

L ([m .. n)) = n \dot{-} m

i < n \dot{-} m \to [m .. n) [i] = m + i

Verify your implementation!

[m .. n) = ?

L ([m .. n)) = n \dot{-} m

i < n \dot{-} m \to [m .. n) [i] = m + i

Exercise. (bonus 1/2 point) Prove

k ≦ m \land m ≦ n \to [k .. m) \oplus [m .. n) = [k .. n)

k ≦ m \land m ≦ n \to [k .. m) \oplus [m .. n) = [k .. n)

List minimum. Define the function $Minl (x)$ such that

x \neq 0 \to Minl (x) &CLin; x

x \neq 0 \land a &CLin; x \to Minl (x) ≦ a

Verify your implementations!

Minl (v, 0) = v

Minl (v, w) = \min (v, Minl (w)) \leftarrow w \neq 0

x \neq 0 \to Minl (x) &CLin; x

x \neq 0 \land a &CLin; x \to Minl (x) ≦ a

List maximum. (bonus 1 point) Define the function $Maxl (x)$ such that

x \neq 0 \to Maxl (x) &CLin; x

x \neq 0 \land a &CLin; x \to a ≦ Maxl (x)

Verify your implementations!

Maxl (x) = ?

x \neq 0 \to Maxl (x) &CLin; x

x \neq 0 \land a &CLin; x \to a ≦ Maxl (x)

Deleting elements from lists. (bonus 1/2 point) Define the function $Delall (a, x)$ such that

b &CLin; Delall (a, x) \leftrightarrow b &CLin; x \land b \neq a

Verify your implementation!

Delall (a, x) = ?

b &CLin; Delall (a, x) \leftrightarrow b &CLin; x \land b \neq a

Filter. (bonus 1/2 point) Given the predicate $A$ , define the function ${Filter}_{A} (x)$ such that

a &CLin; {Filter}_{A} (x) \leftrightarrow a &CLin; x \land A (a)

Verify your implementation!

{Filter}_{A} (x) = ?

a &CLin; {Filter}_{A} (x) \leftrightarrow a &CLin; x \land A (a)

Multiplicity. (bonus 1 point) Define the function $#_{a} (x)$ such that

#_{a} (b, 0) = (a =_{*} b)

#_{a} (x \oplus y) = #_{a} (x) + #_{a} (y)

Verify your implementation!

Remark. The $x =_{*} y$ is the characteristic function of the binary equality predicate $x = y$ and it is defined in the module Maux*.

#_{a} (x) = ?

#_{a} (b, 0) = (a =_{*} b)

#_{a} (x \oplus y) = #_{a} (x) + #_{a} (y)

List union. (bonus 1 point) Define the function $⋃ x$ such that

⋃ (x, 0) = x

⋃ (x \oplus y) = ⋃ x \oplus ⋃ y

Verify your implementation!

⋃ x = ?

⋃ (x, 0) = x

⋃ (x \oplus y) = ⋃ x \oplus ⋃ y