Формальные методы - часть 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)