Формальные методы - часть 4
2. Списки типов – это последовательность значений одного типа списка list Т, могут быть конечным списком типов Тk и неконечными списком типов T n . в качестве структур данных типа списку может быть бинарное дерево, в котором есть голова (head) и сын ( tail), следует за ним в списке и хвост. Операциями для списка является операция hd взятия первого элемента списка, т.е. головы и операция tl – хвоста остальные элементы.
Функция Caddr (I) = L Þ tail Þtail Þ Head выбирает из списка I –элемент. Индекс элемента помогает выбрать нужный элемент списка Index(I, idx) = L (idx) =
while (Ø is null(idx))do((L Þ tail ÞL) Ñdec(idx)) L Þ Head. Для определения количества элементов в списке выполняется функция
len (L) = (ld Ñ null (result))
while (L Þ) do (( L Þ tail Þ tail ÞL) Ñ inc (result))
result Þ
Элемент списка находится так:
elem (L) = (ld Ñ empty (result))
while (L Þ) do (( L Þ tail ÞL) Ñ
( result ( LÞ head Þ) Þ elem ) Þ result)
result Þ.
Аналогично можно представить функции конкатенации, преобразование типов данных, добавления элемента в голову и хвост списка и др.
3. Отображение – это структура (map), которая ставит в соответствие значениям одного типа значение другого типа. С другой стороны, отображение является бинарным отношением декартового произведения двух множеств, как совокупности двухкомпонентных пар, в которой первый компонент arg содержит элементы аргументов отображения, а другой компонент res соответствующие элементы значений этого отображения.
В языке представлены разные допустимые операции над отображениями: наложение, объединение, композиция, срез и др. Среди этих видов отношений рассмотрим только композицию отображений.(m1, m2).
(ld Ñ (compose (m1, m2) Þ m)) apply (m, elem)