ORM推导规则：形式化与计算特性解析

### ORM推导规则：形式化与计算特性解析 #### 1. 一阶语义与概念模式 一阶语义以精确且无歧义的方式规定了概念模式的准确含义。例如，某些概念模式可以轻松地表示为UML类图和EER图。 #### 2. 推导规则示例 推导规则在ORM中有重要应用，可分为子类型推导规则和事实类型推导规则。 - **子类型推导规则**：将实体类型定义为其他实体类型的特化。 - **事实类型推导规则**：通过更具体的参数类型定义事实类型。 推导规则是沿着ORM图中一条或多条路径定义的约束集合。例如，之前的图未准确捕捉Visitor实体的预期含义，缺少“所有VISA持有者都是访客”的约束。为了准确表示所有访客，我们可以添加新的VisitorWithVisa实体作为PersonWithID的子类型，并附上推导规则： ```plaintext Each VisitorWithVisa is by definition some Person with ID that is identified by some Document that is some Visa. ∀x.VisitorWithVisa(x) ↔ PersonWithID(x) ∧ ∃y.isIdentifiedBy(x, y) ∧ Visa(y) ``` 这个推导规则通过“当且仅当”语句精确地定义了持VISA的访客。 基于带有此推导规则的ORM概念模式，SomeVisitor实体应是VisitorWithVisa的子类型，这一推理可由逻辑证明器使用ORM概念模式的语义翻译自动计算。 此外，还有另一种表达相同推导规则的方式。由于文档可以是VISA或IDCard，但不能两者都是，我们可以添加VisitorWithoutIDCard实体，其推导规则如下： ```plaintext Each VisitorWithoutIDCard is by definition some Person with ID that is identified by some Document where that Document is no IDCard. ∀x.VisitorWithoutIDCard(x) ↔ PersonWithID(x) ∧ ∃y.isIdentifiedBy(x, y) ∧ ¬IDCard(y) ``` 可以得出，这个新实体的行为与之前的VisitorWithVisa相同，它们是等价的。 假设所有持有IDCard的人都是公民，无国籍人士是那些没有任何文档的人，我们可以定义以下推导规则： ```plaintext Each Citizen is by definition some Person with ID that is identified by some Document that is some IDCard. ∀x.Citizen(x) ↔ PersonWithID(x) ∧ ∃y.isIdentifiedBy(x, y) ∧ IDCard(y) Each Stateless with ID is by definition some Person with ID that is identified by some Document where that document is no IDCard and that Document is no VISA. ∀x.StatelessWithID(x) ↔ PersonWithID(x) ∧ ∃y.(isIdentifiedBy(x, y) ∧ ¬IDCard(y)) ∧ ∃z.(isIdentifiedBy(x, z) ∧ ¬Visa(z)) ``` 推理过程的结果表明，有ID的人被划分为公民和持VISA的访客，且不可能有有ID的无国籍人士，因为有ID的人必须有一份文档，而无国籍人士被定义为既不持有VISA也不持有IDCard，这使得StatelessWithID实体不一致。 我们还对之前的图进行了一些更改，引入了更通用的Person实体作为PersonWithID的超类型，并关联了“Person is identified by document”事实类型。Stateless成为Person的子类型，SomeVisitor carries Visa事实类型的子集约束通过事实类型推导规则隐式表示： ```plaintext SomeVisitor carries Visa if and only if that SomeVisitor is some Person that is identified by some Document that is that Visa. ∀x, y.carries(x, y) ↔ SomeVisitor(x) ∧ Person(x) ∧ isIdentifiedBy(x, y) ∧ Document(y) ∧ Visa(y) ``` 推理结果显示，SomeVisitor carries Visa事实类型是Person is identified by document的子集，SomeVisitor实体是VisitorWithVisa的子类型，新定义的Stateless实体类型是一致的，且与PersonWithID不相交，原因是Person实体没有强制约束要求必须有文档。 #### 3. 形式语法和语义 我们为完整的ORM推导规则语言的一阶片段提供形式化，