关系代数派生算子语义表达式间等价性证明

计算机科学与探索 ›› 2008, Vol. 2 ›› Issue (1): 97-103.

关系代数派生算子语义表达式间等价性证明

杨波^1,2,3+,薛锦云¹

1. 江西省高性能计算技术重点实验室（江西师范大学），南昌 330022
2. 中国科学院软件研究所，北京 100080
3. 江西财经大学信息管理学院，南昌 330013

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-02-20 发布日期:2008-02-20
通讯作者: 杨波

Proof of equivalence between semantic expressions of derived relational algebra operators

YANG Bo^1,2,3+, XUE Jinyun¹

1. Jiangxi Key Lab of High Performance Computing Technology， Nanchang 330022， China
2. Institute of Software， Chinese Academy of Sciences， Beijing 100080， China
3. School of Information， Jiangxi University of Finance and Economy， Nanchang 330013， China

Received:1900-01-01 Revised:1900-01-01 Online:2008-02-20 Published:2008-02-20
Contact: YANG Bo

摘要/Abstract

摘要： 关系代数的派生算子在关系数据库查询语言中得到了广泛应用。它们的语义有两种常见的表示方式，一种是基于原始算子的表达式，一种是基于一阶逻辑的表达式。但有关的文献资料都没有给出这两种表达式等价性的严格证明。文章尝试通过一系列等价变换，证明派生算子语义的这两种表达式间的等价性。从派生算子（主要是除算子）语义的原始算子表达式出发，根据关系代数表达式的特点，通过一步步的等价变换，得到派生算子语义的一阶逻辑表达式。所使用的变换方法能为关系代数表达式的正确性证明打下基础。

关键词: 关系代数的派生算子, 原始算子, 一阶逻辑, 除算子, 等价变换

Abstract: The derived relational algebra operators are widely used in the relational database query languages.There are two kinds of representations for their semantics. One is the expression described by original relational operators， the other is the expression described by one order logic. However， the strict equivalence proof of the two different semantic expressions is not given in related documents. The present study manages to prove the equivalence of the two different kinds of semantic expressions through a series of formal deductions step by step according to some related characteristics of relational algebra. The beginning of these deductions is the semantic expression described by original relational operators； the end is the semantic expression described by one order logic. The foundation of correctness proof of relational algebra expressions can be laid by the present deduction method.

Key words: derived relational algebra operators, original relational algebra operators, one order logic, relational division operator, formal deductions

杨波1,2,3+ ,薛锦云1 . 关系代数派生算子语义表达式间等价性证明[J]. 计算机科学与探索, 2008, 2(1): 97-103.

YANG Bo^1,2,3+, XUE Jinyun¹. Proof of equivalence between semantic expressions of derived relational algebra operators[J]. Journal of Frontiers of Computer Science and Technology, 2008, 2(1): 97-103.