在合金中对二元关系使用集合理解

Question

我有以下签名：

sig Id, Grade {}

sig Foo {
    result : Id -> Grade
}

现在我想创建一个函数，它接收一个 foo 变量并返回所有关联的 Foo -> Grade 关系：

fun results[ id : Id ]: Foo -> Grade {
    //return all Foo->Grade binary relationships such that "id -> grade" in Foo.result
}

即

所以如果“结果”关系是这样的：

(foo0, id0, grade0)
(foo0, id1, grade0)
(foo0, id2, grade1)
(foo1, id0, grade2)
(foo1, id3, grade3)
(foo2, id0, grade0)

我运行函数“results[id0]”我会得到：

(foo0, grade0)
(foo1, grade2)
(foo2, grade0)

现在我想我会使用某种集合推导，但问题是集合推导仅适用于一元集，而不适用于二元集。

Answer 1

现在我想我会使用某种集合推导，但问题是集合推导只适用于一元集，而不是二元集。

第一次正确（是的，使用集合推导），第二次不太正确（集合推导在关系上工作得很好）。请参阅语言参考的第 B.8 节，或软件抽象的第 3.5.5 节。

尝试这样的事情（未检查！）：

fun results[ id : Id ]: Foo -> Grade {
/* return all Foo->Grade binary relationships
   such that "id -> grade" in Foo.result */
   { f : Foo, g : Grade 
     | f -> id -> g in result } 
   /* not Foo.result, that was a slip */
}

可能有一种聪明的方法可以在没有理解的情况下编写所需的集合，只需使用框连接和点连接，但如果有的话，目前它正在躲避我。我得到的最接近的是

{ f : Foo, g : Grade | f.result.g = id }