Z符号法：表示二维数组

Question

我完全不了解Z符号。我需要在Z中表示一个图形类型。我的想法是使用关联矩阵，以便可以轻松自由地在节点和边之间遍历。

唯一的问题是，我不知道如何在Z中指定关联矩阵。我认为我需要一个二维数组，但是浏览可用于Z符号的参考资料时，数组通常使用序列(seq)来表示。是否有其他方法来指定多维数组？

提前致谢。

- MaXim

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

- danielp

---

Z-notation中的/rel是什么？ - Jut

如果某些节点没有关联的边，图形：节点\rel节点如何工作？ - Jut

"A \rel B"（LaTeX 语法）是指 A 和 B 之间所有关系的集合，即 "A <-> B"。 - danielp

以上解决方案（隐含地）假定集合node包含图的所有边。如果节点N没有关联的边，则在图中不会有左侧或右侧有N的对。但是，[node]将该集合声明为常量，因此您无法更改图中的边集。一种方法是定义一个包含所有可能边缘的常量[NODE]，并定义一个子集edges \subseteq NODE，其中graph：edges \rel edges。 - danielp