合金の述語計算後のポストプロダクション

Question

私は合金に慣れていないので、これはおそらく簡単な質問です。私はオンラインのチュートリアルを終わり、改訂版ソフトウェアアブストラクションを読んでいます。

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

テキストこれはB-> A-> Cの新しい関係を定義することを言う：34ページ、ページの下部にある例があります。私はr 'の明示的な順序がこのステートメントによってどのように達成されるかは分かりません。

Answer 1

それはセットの理解のプロパティ

• {a: A | somePredicate1[a]}はタイプAであり、somePredicate1が成立するために、すべての原子を含むセットを返します。
• {a: A, b: B | somePredicate2[a, b]}はA->Bであり、すべてa->bのタプルを含む関係を返します。somePredicate2が成り立ちます。

にセット理解の構文は基本的に2つの部分で構成さ

ので、（1）（|文字の前）の宣言を入力して、返されたセットのすべての要素のために保持しなければならない（2）述語。