演绎数据库理论(数据库)

时间：2022-12-03 14:30:01 | 来源：信息时代

时间：2022-12-03 14:30:01 来源：信息时代

    演绎数据库理论 : 采用谓词逻辑实现演绎数据库的一套理论与原理。通常,演绎数据库采用的数学工具以逻辑(主要包括一阶谓词逻辑演算)为主,逻辑程序是一组基于Horn子句的规则,它们采用逻辑证明论、逻辑模型论和函数模型论来描述和解释。实现演绎数据库的理论和原理是建立数学模型系统,其核心是逻辑程序的模型语义(包括Herbrand基、逻辑满足、最小模型的唯一性、模型相交定理和最小模型的极小不动点等),并在证明论与模型论等理论的基础上建立相应的算法来实现。
1.基于一阶逻辑的证明论理论
逻辑证明论(logic proving theory)是数据逻辑中的一个传统分支,作为演绎数据库的一种模型理论,它采用公理系统来求解问题。由给定公理,通过证明过程而得定理,这就是证明论求解问题的方法。按逻辑证明论观点,每个关系数据库本身被视为常量原子公式,即每个关系元组本身即为一闭合原子。这样,关系数据库与逻辑程序只是同一事物的两种不同的表示形式,从而有可能将其与规则一起共同构成一个前提公式集,并推演出新目标或演绎数据,而使检索处理转化成推理过程。
证明系统(proving system)又称为推理系统(inference system)或一阶谓词演算的公理系统。在证明系统中,包括公理(集)、定理和证明。公理是广义于所有数据的,在一阶谓词演算公理系统中,公理均为一阶谓词演算公式。通常,它由唯一命名公理(UNA)、域闭包公理(DCA)、闭包世界公理(CWA)等组成公理集。证明系统中的定理,也是一阶谓词演算公式,它是由公理通过证明而得到的,而证明则是指由公理通过推理而得到定理的过程。从证明论的角度看,演绎数据库即可视为一个一阶谓词演算的公理系统。表1给出逻辑证明论中的(公理)证明系统与演绎数据库的关系对照。
逻辑证明论实现演绎数据库的原理实际上是将演绎数据库视为一个定理证明系统,通过构造一个关系系统(理论)T,使演绎数据库成为唯一模型。在该理论下,查询求值和完整性约束被视为待证明的定理。设L为一阶谓词逻辑语言,则对L中任何合式公式W, T⊦W当且仅当W可从理论T及公式集中导出。逻辑证明论使一阶逻辑和关系数据库形成自然联系,用一阶逻辑公理定义数据库成为可能。在逻辑证明论中,为确保理论上的严格性,有必要引入若干公理,包括唯一命名公理(UNA)、域闭包公理(DCA)、闭合世界公理(CWA),及它们组成的公理集。

表1 证明系统与演绎数据库的关系对照

证明系统	演绎数据库
公理	数据、窗口、逻辑规则
定理	查询、快照、数据模式、完整性约束
证明	查询、快照的实现、数据模式的检验、完整性约 束的检验

目前,用逻辑证明论实现演绎数据库,即建立一阶谓词逻辑演算的公理系统,主要是通过采用基于一阶谓词逻辑语言Prolog和Datalog来实现的。由于演绎数据库采用一阶逻辑作为知识表示工具,一般都是采用基于一阶逻辑的证明论理论。其公理系统的实现步骤如下:
(1)建立一组公理(公式的集合)。公理可认为在该系统内普遍有效,即公理中的公式永为真。演绎数据库一般有特殊性公理、事实性公理和演绎性公理等。其中,事实性公理数量较多,因为每一数据事实都有一条公理。演绎性公理给出了演绎数据库中的规则,一般在Datalog中以规则形式出现。
(2)建立一组推理规则,即演绎的方法,一般的推理规则可以是: A,A→B,|-B。
(3) 由公理与推理规则给出一组证明过程。一般,一个证明过程可定义为一个公式的序列,其中序列内的公式(k),可由(1)-(k-1)及公理通过推理规则而得到。
(4)最后,可得到公理系统的定理,一般对某组公理如有证明过程P₁,P₂,…,P_n,而P_n即为该公理系统通过证明过程而得的定理。在演绎数据库中,定理相当于对规则的查询(结果),它有时也可作为演绎数据库的完整性、一致性及相容性的校验工具。
在证明论理论中所用的推理规则及证明过程是一种演绎性的推理方法,一开始无法在计算机上自动实现。1956年,美国数理逻辑学家R·Robinson证明了这个问题在理论上的可行性,并给出了自动证明的算法——归结原理(resolution principle)。
如上所述,在证明论解释下,将演绎数据库中存放的EDB关系元组看作事实,规则看作公理。规则定义的IDB关系就是利用数据库中的事实,使用规则可以证明的事实(即定理)集合。查询处理过程就是定理证明过程。在此观点下,演绎数据库可视为一个具有演绎功能的公理系统。基于证明论的归结原理为逻辑规则的自顶向下处理奠定了基础。
2.基于一阶逻辑的模型论理论
模型论(model theory)是数据逻辑中的传统分支,在演绎数据库中,一般是采用一阶逻辑模型论方式求解问题。模型论一般可用如下的一个三元组组成:(L,∑,M),其中L是书写的语言,∑是用L书写的句子集,M是L的一个解释,称为结构或L-结构。
基于一阶逻辑的模型论理论是以Datalog为书写语言L,以演绎数据库中的事实与规则为句子集∑,并构作模型M(满足M|=∑,且为最小),其最小模型即为演绎数据库的演绎结果,而最小模型可通过对∑的关系代数方程组的最小不动点来求得。为获取此项结果,目前一般采用代数方法,即将求得最小模型变换成为某代数方程组的求解,其求解的算法有以“Bottom Up”方法所形成的算法体系,以及将证明论中的“Top Down”算法体系与“Bottom Up”相结合所形成的魔集(magic set)算法。
逻辑模型论(logic model theory)作为演绎数据库中一种常用的数据模型,它将关系数据库视为一阶逻辑闭合公式集。在一阶逻辑中,使得一组(个)闭合公式为真的解释,分别称为这组(个)公式的模型。以此为基础,可重构关系数据库理论,并因此引出数据库的逻辑模型论。逻辑模型论的原理是: ①数据库之内涵由一组闭合公式描述。这组公式相当数据库的完整性约束,作用于数据库对象的全体,亦即这组公式相当于约束条件的全称闭包; ②数据库的外延为用于描述数据库的一阶公式的模型。若令一阶公式为G,数据库为D,则D为G的一个模型,亦即D为G的一个解释,使得G中所有公式为{X|W(X)},其中,X为一变量(如元组),W(X)为一阶公式,X为W(X)中的唯一自由变量。检索表达式针对数据库取其真值,即在数据库规则公式的解释中发现所有X的实例对象,使得W(X)为真。可见,数据库的逻辑模型论简明地建立起数据库关系理论与一阶谓词逻辑理论之间的联系。该模型将查询求值的完整性约束视为在真值语义定义下的解释环境中的求值,这是从语义角度看待和实现演绎数据库。逻辑模型论使演绎数据库的研制相对简化,但它在描述视图重构、空值、否定和析取等方面仍存在局限性。
在规则的模型论理论解释下,一组规则被看作定义了一个可能的模型。谓词的解释是使得谓词为真的所有可能实例。模型的解释是使得规则集中所有规则都为真的解释,而演绎数据库中的数据就是最小(极小)模型。规则的模型论解释为用最小(极小)不动点定义规则的计算含义提供了基础。在此理论下,随后相继出现了规则的自顶向下算法,如朴质算法、半朴质算法、魔集算法等。
3.基于函数论的模型理论
函数论模型(functional theory model)是一种构造性求值模型。该模型建立在集合、函数、算子和变换这四个层次上。其中,集合是函数论的基础,由集合构造函数,而算子则在建立函数之上构造新的函数,包括反函数、迭代、复合、递归、插入及删除等。变换给出了函数构造集合的方法,包括λ-变换和μ-变换,它们分别将显函数和隐函数构造成集合。因此,在函数论模型下,查询求值可利用基本函数通过算子构造出许多新函数,再通过变换构造集合来实现。如上所述,演绎数据库的构造性求值模型就是通过构造上述算子及变换来实现的。
4.逻辑程序计算的有效性
演绎数据库的实现,十分关注基于规则的逻辑程序的计算有效性问题。通常,逻辑规则处理的算法大体分为自顶向下与自底向上两大类。自顶向下是由目标进行推理,其理论基础是归结原理。大部分自顶向下的方法都可以看作Prolog所用方法的基于关系的版本和改进。与Prolog不同,演绎数据库采用一次一个关系,而不是一次一个元组的处理方式。自顶向下的方法具有很好的聚焦性(从而具有较高的求值效率),但其实现较为复杂,并且收敛性难以保证和判断。与此相反,基本的自底向上算法是朴质算法和半朴质算法,其理论基础是不动点原理。它们具有实现简单、收敛性易于判定等优点。但是由于缺乏聚焦性,自底向上这种算法很难单独使用。
魔集算法的发现是递归查询处理研究的重要里程碑。针对具体查询,魔集算法首先改写规则,然后自底向上地计算新规则的不动点,得到查询的回答。魔集算法保持了自顶向下和自底向上方法的全部优点,避免了两者的缺点。魔集算法的发现使得规则的自底向上处理方法开始走向实用,成为递归查询处理的主要方法,并推动了基于变换的查询优化技术的研究。魔集算法有许多拓广,包括处理带函数词的规则、带聚集函数的规则和包含否定词的规则。魔集变换的思想还被用于处理一些特殊的,在实践中经常出现的递归查询,如右线性递归、左线性递归、混合线性递归和计数线性递归。