ampersand-rules

在Ampersand模型（ADL）中，规则（RULE）、约束（constraint）、不变量（invariant）、过程规则（process rule）、ENFORCE规则或自动化规则（automated rule）均基于关系代数（relation algebra）进行定义与推理。以下从关系代数的语言出发，系统解释这些概念的含义、作用及相互推导逻辑，适用于回答诸如“解释此规则”“此约束有何作用”“leg deze regel uit”等问题，或当用户粘贴一条RULE并询问其含义时。 --- ### 1. **规则（RULE）** 在Ampersand中，一条规则形如： ``` RULE MyRule : r |- s ``` 这表示：**关系 r 蕴含关系 s**，即在任何合法状态下，若 r 成立，则 s 也必须成立。 从关系代数角度看，`r |- s` 等价于 `r ⊆ s`（r 是 s 的子集），即 r 的每一对元组都必须在 s 中出现。 > **解释结构（面向人类读者）：** > “MyRule 要求：每当 r 中存在一对 (a,b)，s 中也必须存在 (a,b)。若违反，则状态非法。” --- ### 2. **约束（Constraint）** 约束是规则的另一种称呼，通常用于强调其限制性。例如： ``` CONSTRAINT NoDuplicates : r ~I ``` 表示 r 必须是反自反的（即 r ∩ I = ∅，其中 I 是恒等关系）。 在关系代数中，这写作：`r ∩ I ⊆ ∅`，或等价地 `r ∩ I = ∅`。 > **解释：** “NoDuplicates 禁止 r 中包含任何形如 (x,x) 的自反对。” --- ### 3. **不变量（Invariant）** 不变量是系统始终必须满足的条件，通常由多个规则共同构成。例如： ``` INVARIANT Integrity : r;s ⊆ t ``` 表示 r 与 s 的合成（composition）必须包含于 t。 在关系代数中，合成记作 `;`，即 `(r;s)[a,c] ⇔ ∃b: r[a,b] ∧ s[b,c]`。 > **解释：** “只要存在 a→b ∈ r 且 b→c ∈ s，就必须有 a→c ∈ t。” --- ### 4. **过程规则（Process Rule）与 ENFORCE 规则** 过程规则描述业务流程中的合法操作路径，而 ENFORCE 规则强制系统在特定条件下执行动作。 例如： ``` ENFORCE ApproveOrder : orderPlaced; approvedByManager |- orderApproved ``` 表示：若订单已下单（orderPlaced）且被经理批准（approvedByManager），则必须标记为已批准（orderApproved）。 > **关系代数解释：** `orderPlaced; approvedByManager ⊆ orderApproved` 此类规则常用于自动化工作流，确保状态转换符合业务逻辑。 --- ### 5. **可删除的原子或元组而不违反不变量** 要判断某原子 a 或元组 (a,b) ∈ r 是否可被安全删除，需检查所有包含 r 的不变量是否在删除后仍成立。 例如，若有不变量 `r ⊆ s`，则删除 (a,b) ∈ r 不会破坏该不变量（因左集变小），但若存在 `s ⊆ r`，则可能违反。 更复杂情形涉及合成：若 `r;s ⊆ t`，删除 r 中的 (a,b) 可能导致某些 (a,c) ∉ t，从而违反不变量。 > **方法：** 对每个相关不变量，验证删除后的关系是否仍满足子集条件。 --- ### 6. **从规则推导结论（What follows from a rule?）** 给定 `r |- s`，可利用关系代数定律推导新事实： - 若已知 `t ⊆ r`，则由传递性得 `t |- s` - 若 `s |- u`，则 `r |- u`（传递性） - 利用德摩根律（De Morgan）：`~(r ∪ s) = ~r ∩ ~s`，可用于分析补集约束 - 分配律：`r;(s ∪ t) = r;s ∪ r;t`，用于展开合成 - 吸收律：`r ∪ (r;s) = r` 当 s ⊆ I（不常见，但可用于简化） - 残差（res

存档时间线

版本索引永久保留；内容副本只保留最新 1 份，更早版本仅留索引与哈希（存档时间线的证据链不会因此断裂）。

下载存档内容副本