可重构位置/转换系统中的变换

### 可重构位置/转换系统中的变换 #### 1. 基本概念 - **直接变换与变换序列**：给定规则 `prod = (L l←K r→R)` 和对象 `G` 以及态射 `m : L →G`（称为匹配），从 `G` 到对象 `H` 的直接变换 `G prod,m =⇒H` 由特定的推出来定义。一系列直接变换 `G0 =⇒G1 =⇒... =⇒Gn` 称为变换，记为 `G0 ∗ =⇒Gn`。 - **粘合 HLR 系统**：粘合 HLR 系统 `AHS = (C, M, RULES)` 由（弱）粘合 HLR 范畴 `(C, M)` 和一组规则 `RULES` 组成。 #### 2. 可重构 P/T 系统 - **P/T 系统定义** - **P/T 网**：`PN = (P, T, pre, post)`，其中 `P` 是位置集合，`T` 是转换集合，`pre` 和 `post` 是从 `T` 到 `P ⊕` 的函数。 - **P/T 系统**：`PS = (PN, M)`，其中 `M ∈P ⊕` 是标记。`P ⊕` 是 `P` 上的自由交换幺半群，例如 `M = 2p1 ⊕3p2` 表示位置 `p1` 有两个令牌，位置 `p2` 有三个令牌。 - **转换启用与跟随标记**：对于标记 `M ∈P ⊕`，如果 `pre(t) ≤M`，则转换 `t ∈T` 是 `M` - 启用的。此时，跟随标记 `M ′ = M ⊖pre(t) ⊕post(t)`，并且 `(PN, M) t −→(PN, M ′)` 称为一个激发步骤。 - **P/T 态射** - 给定 `P/T` 系统 `PSi = (PNi, Mi)`（`i = 1, 2`），`P/T` 态射 `f : (PN1, M1) →(PN2, M2)` 由 `f = (fP, fT)` 给出，其中 `fP : P1 →P2` 和 `fT : T1 →T2` 满足： - `f ⊕ P ◦pre1 = pre2 ◦fT` 且 `f ⊕ P ◦post1 = post2 ◦fT`。 - `M1(p) ≤M2(fP (p))` 对于所有 `p ∈P1`。 - 如果 `fP` 和 `fT` 是单射，并且 `M1(p) = M2(fP (p))` 对于所有 `p ∈P1`，则称 `f` 为严格 `P/T` 态射。 - **可重构 P/T 系统定义**：给定 `P/T` 系统 `(PN, M)` 和一组规则 `RULES`，可重构 `P/T` 系统定义为 `((PN, M), RULES)`。 #### 3. 示例说明 以考古灾难/恢复任务场景为例，团队由团队领导（图片存储设备）、相机设备和桥梁设备组成。团队的协作过程可以用 `P/T` 系统 `(PN1, M1)` 建模，工作通过激发步骤进行。 - **规则应用**：可以应用规则来修改网络。例如，规则 `prodphoto` 可以将拍照活动细化为单个步骤，规则 `prodfollow` 可以引入桥梁设备的移动活动。 #### 4. 冲突问题 在 `P/T` 系统中，传统的并发情况是两个具有重叠前置域的转换都被启用，并且它们一起需要的令牌数超过当前标记中的可用令牌数。在可重构 `P/T` 系统中，冲突和并发的概念更加复杂。 - **不同情况的条件** - **正方形 (1)**：转换 `t1` 和 `t2` 需要无冲突，以便它们可以以任意顺序或并行激发，产生相同的标记。 - **正方形 (2) 和 (3)**：需要并行独立性，即转换步骤和激发步骤可以以任意顺序执行，导致相同的 `P/T` 系统。 - **正方形 (4)**：目前需要使用粘合 HLR 系统的结果来给出并行或顺序应用两个规则的条件。 #### 5. 相关定理 - **局部 Church - Rosser 定理**：允许以任意顺序应用两个图变换 `G =⇒H1` 和 `G =⇒H2`，前提是它们是并行独立的，并且在这种情况下，两个规则也可以并行应用。 - **并行性定理**：需要二进制余积以及与 `M` 的兼容性（即 `f, g ∈M ⇒ f + g ∈M`）。 - **并发定理**：用于处理因果相关变换的同时执行，可以构造并发规则 `prod1 ∗prod2` 来进行直接变换。 #### 6. P/T 系统作为弱粘合 HLR 范畴 - **推存在性与态射保持**：在 `PTSys` 中沿着 `Mstrict` 态射的推出存在，并且保持 `Mstrict` 态射。 - *