graph - Z 表示法：二维数组的表示

Question

我是 Z 表示法的完整初学者。我需要在 Z 中表示一个图类型。我的想法是使用关联矩阵，以便我可以轻松地在节点和边之间自由遍历。

唯一的问题是，我不知道如何在 Z 中指定关联矩阵。我认为我需要一个 2D 数组，但是通过可用于 Z 表示法的参考资料，数组通常使用 seq 表示。还有另一种方法来指定多维数组吗？

提前致谢。

Answer 1

我认为节点之间的关系将是关联矩阵的更好表示。假设我们有一个类型节点：

 [node]

然后可以将图建模为节点之间的关系：

graph : node \rel node

这将是一个有向图，因为图中可能有一条边 n1->n2，但没有 n2->n1。如果您需要一个无向图，您可以添加进一步的限制：

graph\inv = graph

（graph的倒数与graph相同，即如果n1->n2 in graph，那么n2->n1也一定在graph中。）

如果您真的想将关联矩阵建模为多维数组，您可以定义一个从数组中的位置映射到整数的函数，例如：

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

两种表示之间的关系可以表示为：

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