合金谓词演算后期制作

Question

由于我是合金新手，这很可能是一个简单的问题。我已经阅读了在线教程，现在正在阅读软件抽象，修订版。在第 34 页，页面底部有一个示例：

r' = {b:B, a:A, c:C | a->b->c in r}

文本说这定义了 B->A->C 的新关系。我看不出这个语句是如何实现 r' 的明确顺序的。

Answer 1

这是集合推导的属性

• {a: A | somePredicate1[a]} 是 A 类型，并返回一个集合，其中包含 somePredicate1 所持有的所有原子；
• {a: A, b: B | somePredicate2[a, b]} 是 A->B 类型，并返回一个包含所有 a->b 元组的关系，其中 somePredicate2 持有；
• 等等

集合理解的语法基本上由两部分组成（1）类型声明（在| 字符之前），以及（2）必须为返回集合中的每个元素保留的谓词。