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. 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. 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) ∸ 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) ∸ n

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

Interval. Define the function $[m .. n)$ such that

L ([m .. n)) = n ∸ m

i < n ∸ m \to [m .. n) [i] = m + i

Verify your implementation!

[m .. n) = ?

L ([m .. n)) = n ∸ m

i < n ∸ m \to [m .. n) [i] = m + i

Exercise. 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) ϵ x

x \neq 0 \land a ϵ 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) ϵ x

x \neq 0 \land a ϵ x \to Minl (x) ≦ a

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

x \neq 0 \to Maxl (x) ϵ x

x \neq 0 \land a ϵ x \to a ≦ Maxl (x)

Verify your implementations!

Maxl (x) = ?

x \neq 0 \to Maxl (x) ϵ x

x \neq 0 \land a ϵ x \to a ≦ Maxl (x)

Deleting elements from lists. Define the function $Delall (a, x)$ such that

b ϵ Delall (a, x) \leftrightarrow b ϵ x \land b \neq a

Verify your implementation!

Delall (a, x) = ?

b ϵ Delall (a, x) \leftrightarrow b ϵ x \land b \neq a

Filter. Given the predicate $A$ , define the function ${Filter}_{A} (x)$ such that

a ϵ {Filter}_{A} (x) \leftrightarrow a ϵ x \land A (a)

Verify your implementation!

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

a ϵ {Filter}_{A} (x) \leftrightarrow a ϵ x \land A (a)

Multiplicity. 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. 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