На этом шаге мы рассмотрим. некоторые важные свойства функций.
Более подробно остановимся на свойствах важных функций, которые называются элементарными селекторами и предназначены для построения и анализа списков:
(1) head (x:y), y ∈ List 0(A) => x∈A; (2) y ∈ List(A), y ≠ [] => (head y)∈A; (3) tail (x:y) => y∈List(A); (4) y ∈ List(A), y ≠ [] => (tail y)∈List(A); (5) head (x:y):tail (x:y) => (x:y); (6) init y = (reverse.tail.reverse) y, y∈List(A); (7) init y = reverse $ tail $ reverse y, y∈List(A); (8) last y = (head.reverse) y, y∈List(A); (9) take m y ++ drop m y => y, m∈N, y∈List(A).
Замечание для знатоков теории комбинаторов.
S(B(++) (take m)) (drop m) y => y, m∈N, y∈List(A).
На следующем шаге мы рассмотрим несколько демонстрационных примеров.
