合金中的不相交联合和笛卡尔积答案

【问题标题】：disjoint union and Cartesian product in Alloy合金中的不相交联合和笛卡尔积
【发布时间】：2014-12-06 16:52:57
【问题描述】：

我在 Alloy 中有两个集合理解谓词（一元），如下所示：

pred A (o : Object){ .. } 

pred B (o : Object) { ..}

我想定义谓词，其中一个是不相交并集，另一个是 A 和 B 的笛卡尔积。

PS：要定义它们的并集和交集，我可以定义以下谓词：

pred Union(o : Object){
    A[o] or B[o]
}

pred Inter(o:Object){
  A[o] and B[o]
}

我想获得笛卡尔积和不相交联合的类似谓词。

谢谢

【问题讨论】：

标签： alloy

【解决方案1】：

您可能混淆了谓词的概念和集合的概念。你有很好的伙伴（弗雷格就是其中之一），但事实证明这很危险。

表达式o in A[o] 和o in B[o] 应该引发类型错误，因为如果A 和B 是谓词，那么表达式A[o] 和B[o] 应该评估为真或假，而不是哪个集合可以想象成为会员。

如果你想要一个谓词 U，当 A 或 B 或两者都对那个对象为真时，它对一个对象为真，那么你想要类似的东西

pred U[o : Object] { A[o] or B[o] }

如果你想要一个排他性的分离——我假设这就是你所说的分离联合的意思——那么

pred X[o : Object] { (A[o] and not B[o]) or (B[o] and not A[o]) }

如果你想要 A、B 和 X 为真的集合，那么你想写

{ o : Object | A[o] } 
{ o : Object | B[o] } 
{ o : Object | X[o] }

其中第三个当然可以写

{ o : Object | (A[o] and not B[o]) or (B[o] and not A[o]) }

集合理解表示法（同样，我鼓励您阅读相关文档）也可以处理元组集合；满足 A 和 B 的对象集的笛卡尔积可以这样写：

{ a, b : Object | A[a] and B[b] }

【讨论】：

我更正了工会和国米机构。在我的应用程序中，我将集合视为一元谓词是有原因的。拖车集和笛卡尔积的不相交并集呢？我怎样才能把它们写成谓词？
@qartal，如果“不相交联合”的意思不是答案中描述的排他性分离，那么您可能需要定义您的意思。笛卡尔积也可以使用推导式表达；我再次建议您阅读文档中的理解。
不相交联合是指here 描述的操作。请让我知道您要查看笛卡尔积的文件是什么？你是说合金书（软件抽象）？
我并不是要推荐一段具体的文章供你阅读； Software Abstractions 确实讨论了理解，我怀疑 Web 上的 Alloy 教程和参考资料也讨论了。如果在阅读并考虑了此处给出的推导式示例后，您无法弄清楚如何表达不相交的并集，我会感到非常惊讶。

【解决方案2】：

这是我正在寻找的解决方案：

A 和 B 的笛卡尔积定义为 A * B = {(a,b) | a 在 A 中，b 在 B 中}。因此，将其放入带有集合理解表达式的 Alloy 语法如下：

pred ACartesB(o1:Object, o2: Object){
    A[o1] and B[o2]
}

A 和 B 的不相交并集定义为 A+B= {(a,1) union (b,2) | a 在 A 中，b 在 B 中}。 1和2是区分A+B中A和B相同元素的指标。因此，将其放在合金上下文中将如下所示：

pred AdisjUnionB(o:Object, i: Int){
    (A[o] and i=1) or (B[o] and i=2)
}

PS：我们假设我们的签名中有sig Object {}。

【讨论】：