Обозначение Z: представление двумерного массива

Question

Я полный новичок в нотации Z. Мне нужно представить тип графа в Z. У меня есть идея использовать матрицу инцидентности, чтобы я мог легко перемещаться между узлами и ребрами.

Единственная проблема в том, что я не знаю, как задать матрицу инцидентности в Z. Я думаю, что мне нужен 2D-массив, но, просматривая справочный материал, доступный для записи Z, массивы обычно представлены с использованием seq. Есть ли другой способ указать многомерный массив?

Заранее спасибо.

Answer 1

Я думаю, что отношение между узлами было бы лучшим представлением для матрицы инцидентности. Предположим, что у нас есть тип узла:

 [node]

Тогда граф может быть смоделирован как отношение между узлами:

graph : node \rel node

Это будет ориентированный граф, потому что в графе может быть ребро n1->n2, но не n2->n1. Если вам нужен неориентированный граф, вы можете добавить еще одно ограничение:

graph\inv = graph

(Инверсия графа такая же, как и графа, т. Е. Если в графе n1->n2, то в графе также должно быть n2->n1.)

Если вы действительно хотите смоделировать матрицу инцидентности как многомерный массив, вы можете определить функцию, которая отображает позицию в массиве в целое число, например:

matrix: (node \cross node) \fun {0,1}

Отношение между двумя представлениями может быть выражено как:

\forall n1,n2:node @ (n1,n2)\in graph \iff graph( (n1,n2) ) = 1