graph - Z 符号 : Representation of a 2D array

Question

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

唯一的问题是，我不知道如何指定 Z 中的关联矩阵。我认为我需要一个二维数组，但通过查看可用于 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