定义一致语义的有效方法

### 定义一致语义的有效方法 在处理任务类型和任务等价性的问题时，我们需要一套有效的方法来确保语义的一致性。下面将详细介绍相关的概念、算法以及如何应用它们来判断任务的等价性。 #### 任务类型的表示 为了避免引入新的数据类型，我们将任务产生的类型表示为 `Val` 的实例。具体来说，`Int` 类型用 `Int 0` 表示，`String` 类型用 `String ""` 表示。我们定义了一个类 `type` 来确定任务的类型： ```haskell :: Type :== Val class type a :: a → Type ``` 对于 `Val` 和 `ITask`，这个类的实例与之前定义的 `val` 实例相同。只有 `BVal` 的实例稍有不同： ```haskell instance type BVal where type (Int i) = BVal (Int 0) type (String s) = BVal (String "") type VOID = BVal VOID ``` 这种复用 `Val` 类型来表示实例类型的方法，在生成测试 `iTasks` 属性所需的值时非常方便。 #### 任务的等价性 根据 `iTasks` 的语义，我们可以定义任务的等价性。非正式地说，如果两个任务具有相同的语义，我们就认为它们是等价的。然而，由于包含编辑器的任务可以应用无限多个更新事件，我们不能通过应用所有可能的输入序列来确定等价性。此外，包含绑定操作符的任务还包含函数，而函数的等价性通常是不可判定的。因此，开发一个有用的任务等价性概念并非易事。 我们定义了一个相当严格的任务等价性概念：如果任务 `t` 和 `u` 在所有可能的事件序列之后具有相等的值，并且在每个中间状态都启用了相同的事件，那么它们就是等价的。由于事件的标识对于使用 `iTask` 系统的工作人员是不可见的，我们允许应用于 `t` 和 `u` 的事件列表在事件标识上有所不同。 为了更好地理解任务的等价性，我们先引入模拟的概念。如果一个任务 `u` 可以模拟任务 `t`，即工作人员使用 `u` 可以完成使用 `t` 能完成的所有事情，我们用 `t ≼ u` 表示。具体要求如下： 1. 对于 `t` 的每个可接受事件序列，都存在 `u` 的一个相应可接受事件序列。 2. 应用这些事件后，任务的值相等。 3. 应用事件后，`t` 的所有启用事件在 `u` 中都有匹配事件。 两个事件 `e1` 和 `e2` 等价（`e1 ∼= e2`），如果它们最多在标识上不同。形式化定义如下： ```haskell t ≼ u ≡ ∀i ∈ accept(t). ∃j ∈ accept(u). i ∼= j ∧ val(t @. i) = val(u @. j) ∧ collect(t @. i) ⊆ collect(u @. j) ``` 需要注意的是，`t ≼ u` 不是对称的，`u` 很可能比 `t` 能做更多的事情。例如，对于所有非正规形式的任务 `t` 和 `u`，有 `t ≼ t .||. u` 和 `t ≼ u .||. t`。任何任务都可以模拟自身，即 `t ≼ t`。一个基本值 `v` 的编辑任务可以模拟返回该值的按钮任务：`ButtonTask id1 "b" (Return (BVal v)) ≼ EditTask id2 "ok" v`。 两个任务 `t` 和 `u` 被认为是等价的，当且仅当 `t` 可以模拟 `u` 且 `u` 可以模拟 `t`，即： ```haskell t ∼= u ≡ t ≼ u ∧ u ≼ t ``` 这种等价性概念比通常的双模拟定义更弱，因为我们不要求事件相等，只要求等价。 下面是一些任务示例及其等价关系： ```haskell u1 = ButtonTask id1 "b1" (Return (BVal (Int 1))) u2 = EditTask id2 "b2" (Int 1) u3 = EditTask id2 "b3" (Int 2) u4 = EditTask id2 "b4" (String "Hi") u5 = u1 .||. u2 u6 = u2 .||. u1 u7 = u2 .&&. u4 u8 = u4 .&&. u2 u9 = u2 ⇛ λv. Return (BVal (Int 1)) u10 = u2 ⇛ λx. u4 ⇛ λy. Return (Pair x y) ``` 这些任务之间的非平凡关系如下： - `u1 ≼ u2` - `u1 ≼ u5` - `u1 ≼ u6` - `u1 ≼ u9` - `u2 ≼ u5` - `u2 ≼ u6` - `u5 ≼ u6` - `u6 ≼ u5` - `u10 ≼ u7` - `u10 ≼ u8` - `u2 ∼= u9` - `u5 ∼= u6` 需要注意的是，`u7 ≇ u8`，因为它们产生不同类型的值。但如果交换 `u7` 或 `u8` 结果对中的元素，这些任务就等价了，例如 `u7 ⇛ λ(Pair a b) → Return (Pair b a) ∼= u8`。 由于任务表达式中存在函数，通常无法判定一个任务是否能模拟另一个任务或它们是否等价。这意味着测试方法需要以某种（最好是安全的）方式近似这种等价关系。不过，在很多情况下，我们可以通过检查决定任务行为的任务树来判断任务之间的关系。 #### 任务树等价性的判定 任务的等价性要求在所有可能的可接受事件序列之后结果相等。即使对于一个简单的整数编辑任务，也有无限多个事件序列。因此，通过应用所有可能的事件序列来检查任务的等价性通常是不可能的。 为了近似任务的等价性，我们引入了两种算法： 1. **通过应用事件确定等价性**： 1. 首先确保 `ITasks` 被规范化，并提供一个整数参数 `N` 表示最大的归约步骤数。 2. 函数 `equivalent` 首先检查任务当前是否返回相同的值。 3. 如果两个任务都需要输入，检查以下条件： - 任务是否具有相同的类型。 - 任务当前是否为工作人员提供相同数量的按钮。 - 任务是否具有相同数量的必需按钮。 - 任务是否提供等价的编辑器。 4. 如果这些条件都满足，递归地应用事件后检查等价性。 5. 如果有必需事件，一次性应用它们；否则，尝试所有按钮事件的组合，检查是否有组合使任务等价。 6. 如果任务中有启用的编辑任务，结果最多为 `Pass`