数据模式转换中的约束保留和新约束引入的代数方法与无点程序转换和Haskell的应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记290（2012）3-18www.elsevier.com/locate/entcs约束感知模式转换蒂亚戈湖阿尔维斯1Universidade do Minho，Portugal软件改进小组，荷兰保罗·F 席尔瓦2Universidade do Minho，葡萄牙Joost Visser3Software Improvement Group，荷兰摘要数据模式转换发生在软件演化、重构和跨范式数据映射的上下文中。当初始模式上存在约束时，需要将这些约束转换为目标模式上的约束。此外，当高级数据类型被细化为较低级别的结构时，必须引入额外的目标模式约束来平衡结构的丢失并保持语义。我们引入了一个代数的方法来模式转换，是约束感知的意义上，约束保留从源到目标模式，并在需要的地方引入新的约束。我们的方法基于精化理论和无点程序转换。数据细化被建模为携带无点谓词作为约束的类型上的重写规则。在每个重写步骤中，reduce上的谓词是从redex上的谓词计算出来的。一个额外的无点函数重写系统用于规范化沿着重写链构建的谓词我们在函数式编程语言Haskell中以类型安全的方式实现了我们的重写系统。我们展示了它们的应用约束感知层次关系映射。关键词：模式转换，约束，不变量，数据精化，策略重写，无点程序转换，Haskell。1介绍数据模式是软件系统的核心例如关系数据库模式、XML文档模式、语法和形式规范中的代数数据库。数据模式不仅规定了数据实例1电子邮件：t. sig.nl2电子邮件：paufil@di.uminho.pt3电子邮件：j. sig.nl1571-0661 © 2012由ElsevierB. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2012.11.0084朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3→→IB到A、T从φ′φzzAJψA，AJ数据类型和转换数据类型A型到Aj型的T由Aj型迁移函数A（满射）φ，φJ约束和变换约束，导出AJ型迁移函数AJz，t新引入的约束φJ=φ，从φ图1.一、 约束t-aw是具有约束φin的数据类型A到具有约束φ ′的数据类型A′的变换。 对目标类型的约束是以下的逻辑合取：（i）对源类型的约束，该源类型与从的迁移函数一起构成，以及（ii）由类型改变引入的任何新约束。当φ′被归一化时，它直接作用于A′而不是通过A。必须符合，但它们也规定了数据查询和最新函数的格式良好性。一般来说，模式定义由一个结构描述组成，这个结构描述用捕获额外语义限制的约束来增强，例如SQL和XSD模式可以声明引用完整性约束，语法包括运算符优先级，VDM规范包含数据类型不变量。数据模式转换发生在各种上下文中。例如，软件维护通常涉及用于存储或导出应用程序数据的数据格式的增强。同样，编程语言的发展带来了不同版本之间语法的修改。编程范例之间的数据映射涉及到更复杂的模式转换[14]，例如XML和SQL之间的当数据模式被转换时，相应的数据实例、查询和约束也必须被调整。例如，在将XML模式映射当XML模式增加了新的文档元素时，为该模式开发的查询可能需要进行调整以考虑这些元素。当形式规范中的数据类型被修改时，它的不变函数和更新函数也必须被修改。在以前的工作中，我们和其他人已经解决了转换的问题-将模式与数据实例和与它们耦合的查询结合在一起。我们已经证明，数据精化理论可以用于形式化模式转换[1]以及相应数据实例的转换[9]。结合无点程序转换，这种形式化扩展到数据处理器的迁移[11]，包括结构性查询和更新函数[12]。我们已经在各种类型安全重写系统中利用了这种理论处理，并将其应用于VDM-SL规范[1]，XML模式和查询[11，5]以及SQL数据库[1，5]。我们还讨论了约束的传播和引入问题[5]。然而，这种方法没有理论上的支持，没有实现类型安全，并且仅限于引用完整性约束。在本文中，我们提出了一种改进的方法来约束感知模式转换。图1简明地展示了新方法。而不是拉-朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）35图二.电影和电视剧的XML数据库的模式，灵感来自IMDb（http://www.imdb.com/）。阴影元素表示各个集合元素中的唯一键此外，播放元素的年份和标题是进入节目集合的外键。与[5]中的交叉引用信息转换的类型不同，我们用强类型函数表示所表示的一般约束来增强它们。 约束传播是通过将源数据类型上的约束φ与目标和源类型之间的反向转换函数组合来实现的。约束引入是通过将一个新的约束映射到所传播的约束的逻辑合取来实现的。最后，无点程序变换被应用于将合成约束的各种成分融合成简化形式。本文的结构如下。我们在第2节中用一个激励性的例子介绍了约束感知模式转换的问题。我们在第3节中提供了有关精化理论和无点程序计算的背景知识。第4节提供了有关约束表示和重写的理论支持。 在第5节中，我们解释了如何使这一理论以强类型重写系统的形式在函数式编程语言Haskell中实现。我们回到第6节中的激励示例来演示我们的重写系统在模式感知的层次关系映射中的应用。我们将在第7节讨论相关工作，并在第8节总结。2激励的例子为了说明我们方法的目标，我们将从[5]中选取激励性的例子图2中的图表表示电影和电视剧数据库的XML模式。该模式指示数据库包含两个主要集合：一个用于节目（电影或电视连续剧），另一个用于在这些节目中演出的演员。除了数据库的结构之外，还存在以下唯一性约束：(i) 一个节目是由它的年份和标题识别。(ii) 一个演员是通过他/她的名字来识别的。(iii) 一个季节是由它的年份来确定的。(iv) 一个被扮演的元素通过它的年份、标题和角色来识别。6朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3还存在以下参照完整性约束：(v) 播放元素的年份和标题是指演出的年份和标题。在XML Schema中，这种唯一性和引用完整性约束由所谓的标识约束定义，使用key、keyref和unique元素。可以存在更多的约束，例如值总是非零的，或者剧集的名称与相应系列的标题不同。这样的约束可以通过一般查询来表达，例如：使用的是当一个XML到SQL的数据映射被应用到我们的XML模式时，一个SQL数据库模式应该产生在各种约束被适当地传播的此外，SQL模式上需要存在新的约束，以平衡由于对关系形式的过度关注而导致的结构损失。我们需要的模式如下：show（year，title）reviews（id，year，title，review）foreign key（year，title）references show（year，title）movies（year，title，director）foreign key（year，title）references显示（year，title）票房（id，year，title，country，value）外键（year，title）引用电影（year，title）系列（year，title）外键（year，title）引用显示（year，title）季节（year，title，yr）外键（年份，标题）引用系列（年份，标题）剧集（id，年份，标题，年份，姓名，导演？）foreign key（year，title，yr）引用seasons（year，title，yr）actors（name）playeds（name，year，title，role）foreign key（year，title）references显示（year，title）foreign key（name）references演员（name）奖项（姓名、年份、职务、角色、ID、奖项）foreign key（name，year，title，role）引用playeds（name，year，title，role）在这个伪SQL表示法中，主键用下划线表示。第一个外键约束是一个新引入的约束的例子这是因为评论嵌套在XML模式中的节目中，但出现在SQL模式中的单独顶级表。playeds表上的第一个外键是原始XML模式中存在的约束的一个示例，并通过数据映射传播在本文的剩余部分中，我们将演示如何从强类型代数组合子构造模式初始约束的传播和新约束的引入都是免费的。3背景在本节中，我们将解释如何通过数据精化理论和无点程序转换来形式化模式转换我们从3.1节开始，提供数据精化理论及其在两级转换中的应用的背景。在第3.2节中，我们概括了无点程序转换，并展示了如何将其与数据精化相结合，以模拟由模式转换驱动的查询迁移。朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）37顺序和结构组成to to'to'·to如果A，≤zB且B，≤zC，则A，≤zC从'从·从'到F到如果A，≤zB，则FA，≤zFB从F层次关系数据映射As≤IN ~A列表消去2A=A~1集消元一个？=1~A可选消除A+ B≤A？×B？和消元法A×（B+C）=（A×B） +（A×C）在和上分配乘积A ~（B+C）≤（A ~B）×（A ~C）和（值域）上的分布映射（B+C）~A=（B~A）×（C~A）和（整环）上的A ~（B×（C ~D））≤（A ~B）×（A×C ~D）平坦套映射图三.数据精化理论的总结。对于一个完整的帐户，读者是指奥利维拉[20]。请注意，·~·表示一个简单关系，其中有限映射是一个特例。3.1作为数据细化数据精化理论提供了一个用数据进行计算的代数框架[20，16，18]。下面的不等式抓住了将数据类型A细化为数据类型B的本质：到A，≤从个zlb哪里⎧⎨⎩to：A→B单射和全射从：B→A满射从·到=idA这里，idA是数据类型A上的恒等函数。因此，不等式A≤B表示B是A的一个精化，这可以通过转换函数to和from来证明。 (In事实上，to可以是任何单射和整体关系，不一定a function.）在细化以两种方式工作的特殊情况下，我们有同构A→B。由于这些数据库用于数据的简化，建立了数据库计算的代数理论。图3总结了这一理论。数据精化理论可以用来形式化模式及其实例的耦合转换[9]。这种两级转换可以通过数据细化规则的顺序和结构组合来捕获。特别是，层次关系数据映射可以通过重复应用消除，分布和注意规则来建模，直到达到固定点[1]。3.2无点程序变换在他1977年的图灵奖演讲中，巴克斯倡导了一种无变量的函数编程风格，其基础是易于在此类程序上用代数定律进行公式化和推理[3]。在Backus之后，其他人采用、补充和扩展了他的工作;这种无点编程风格的概述见[10]。图4显示了本文中使用的一些函数组合子和相关定律。8朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3本原组合子id：A→Aπ1：A×B→Aπ2：A×B→Bδ：（A~B）→集合Aρ：（A~B）→集合B（B）：（B→C）→（A→B）→（A→C）（o）：（A→B）→（A→C）→（A→B×C）（×）：（A→B）→（C→D）→（A×C→B×D）列表：（A→B）→（[A]→[B]）集合：（A→B）→（集合A→集合B）0n：（（A~B）×（（A×C）~D））→（A~B×（C~D））0−n1：（A~（B×（C~D）→（（A~B）×（（A×C）~D））法律fid=fidf=f F id=idf（gh）=（fg）h FfF g=F（ fg）π1（fog）=fπ1oπ2=idπ1<$（f×g）=f<$π1id×id=id列表id=idset id=idπ2π（fog）=g（f×g）（hoi）=（fh）o（gi）π2<$（f×g）=g<$π 2（f×g）（h×i）=（fh）×（gi）listflist g=list（fg）setfset g=set（fg）图四、无点程序转换概述完整的说明，请参阅Cunha et al.[10 ]第10段。在模式转换之后可以使用无点程序转换来简化计算转换函数和从源代码迁移查询[11 ]第11话，或者说，在5.4节中，我们将使用无点程序转换来迁移和简化模式转换期间的约束4带约束在本节中，我们提供了理论支持约束表示和重写。约束的形式化在4.1节中给出。第4.2节讨论了如何将约束添加到数据精化定律中，以形式化模式转换期间约束的传播和引入。4.1带约束的数据类型上的约束可以建模为一元谓词，即区分合法值和违反约束的值的布尔函数。为了将一个约束关联到一个类型，我们将它写成下标：Aφ其中φ：A→IB全函数。这个符号以及下面的一些结果起源于[19]。我们将尽可能多地将约束写成无点表达式，以便使用它们进行后续计算例如，以下数据类型表示两个具有外键约束的表（（A~B）×（C~A×D））（setπ1）<$ρ <$π2<$δ <$π1这里我们使用投影函数π1和π2来选择左表或右表，我们使用δ和ρ来选择映射的域和朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）39范围，并设置f来将函数f映射到集合的元素上此外，我们使用集合包含运算的一个变体10朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3∼提升到无点函数：：（A→Set B）→（A→Set B）→（A→IB）。因此，定义的约束规定，在左表中定义的所有A的值必须包含在右表的键集中当第二个约束被添加到受约束的数据类型时，两个约束都可以用逻辑合取来组合：（Aφ）Aφ。当一个约束存在于一个函子下的一个数据类型上时，这个约束可以通过函子拉出来（关于分类证明，参见[19]）：F（Aφ）<$（FA）（Fφ）函子拉力例如，列表元素的约束可以被拉到列表的约束：（Aφ）（A）listφ。4.2引入、传播和消除约束必须增强数据精化演算的定律，以处理受约束的数据集。首先，如果一个受约束的数据类型是用一个“经典”定律来定义的如果A，到≤从个zlb则Aφ到从z轴Bφ·from因此，源数据类型的约束被传播到目标数据类型，在目标数据类型中，它被向后转换函数从后组合。这样的组合可以产生无点程序转换的机会，我们将在后面看到。通过给目标类型添加一个约束，几个精化定律可以从不等式变成同构。例如，图3中的求和消去法、map在其范围内的分布以及嵌套map的收敛性可以增强如下：A+B ×B？（π1）（π2）A ~（B+C）=（A ~1）×（A ~ B）×（A ~ C）（δ <$π2<$δ <$π1）<$（δ <$π3<$δ<$π1）A ~（B×（C~D））=（A~B）×（A×C ~D）（集合π1）<$δ <$π2<$δ<$π1在这里，我们使用了无点的异或变体（exclusive disjunction，缩写为EJ）和一个空的可选（optional，缩写为EJ）的测试。当应用一个将约束引入到已经有约束的数据类型的法则时，新的和现有的约束必须组合在如果到从vB则Aφ到从_zB）φ·fromφBφ（φ·from）这是[19]的不变牵引定理。一种更一般的情况是，不仅目标而且来源都受到所适用法律的约束≤，≤，≤（朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）311如果Ax，到≤从z_B超然后Aφ，到z_直径（φ·from）从这 里 我 们 使 用 逻 辑 蕴 涵 （ logical implications ） 的 一 个 无 点 变 体 （ point-freevariant）来说明A上的实际约束φ必须隐含所需的约束χ。除了引入和传播之外，约束也可以被削弱甚至消除，凭借以下条件：如果φ，则Aφ≤A。在一个特殊的情况下，即“”是常真谓词，这种弱化归结为消除一个约束。5约束感知重写在本节中，我们将展示如何在重写系统中捕获上一节中增强的数据精化理论，并将其实现为函数语言Haskell中的策略 在5.1节中，我们回顾了如何使用广义代数数据库（GADT）来构造类型和函数的类型安全表示。在第5.2节中，我们将类型表示扩展到受约束的类型。在5.3节和5.4节中，我们解释了如何构造重写系统来转换这种约束类型。5.1类型和函数为了以类型安全的方式表示类型和函数，我们依赖于广义代数数据类型（GADT）[21]。为了表示类型，我们使用GADT：数据类型t，其中One：：Type（）列表：类型a→类型[a]Set：：Type a→Type（Set a）·~·：Typea→Typeb→Type（a~b）--我们使用lhs 2 TeX来·+·：a→b型→（a+b）型--各种类型的设置·×·：Type a→Type b→Type（a，b）--Haskell中的符号。String：：Type String...在这个GADT的各种构造函数的结果类型中，参数t已经被实例化为构造函数所表示的类型。这种实例化是GADT与传统参数化代数数据类型的区别。为了表示函数，我们也使用GADT：数据F f，其中id：：F（a→a）··：F（b→c）→F（a→b）→F（a→c）··：：F（a→IB）→F（a→IB）→F（a→IB）·A·：：F（a→（集合b））→F（a→（集合b））→F（a→IB）≤B12朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3π1：：F（（a，b）→a）π2：：F（（a，b）→b）·×·：F（a→b）→F（c→d）→F（（a，c）→（b，d））·o·：：F（a→b）→F（a→c）→F（a→（b，c））...注意，结果类型中的参数被实例化为所表示的函数的类型。为了简洁起见，只显示了几个构造函数。函数表示可以计算为表示的函数eval：：Type（a→b）→F（a→b）→a→b.请注意，GADT帮助我们强制所生成的函数的类型与函数表示的类型相5.2约束类型为了表示受约束的数据库，需要增强上面的第一个GADT数据类型t，其中...（·）·：Typea→F（a→IB）→Typea因此，（·）·构造函数的第一个参数是被约束的类型，第二个参数是表示约束的函数。在这里使用GADT是值得的，因为它强制函数是正确的类型。这种在类型表示中使用函数表示的重要后果是，函数的重写系统将嵌入到类型的重写系统中，我们将在后面看到为了验证约束是否对特定值有效，我们定义了check：check：：Type t→t→Boolcheck One=Truecheck（t1×t2）（x，y）=check t1x checkt2 y...check（tφ）x=eval（Func t Bool）φxcheck t x此函数通过类型表示和相应的值进行下降。每次找到一个约束时，eval函数都会被应用来检查它的值。5.3重写类型和函数无点程序转换的规则可以在以下类型的重写规则中捕获：类型RuleF = a b. F（a→ b）→可能（F（a → b））我们利用Maybemonad来处理问题。例如，规定id是composition的恒等式的定律定义如下：朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）313idR：：RuleFidR（f_id）=return fidR=mzero这种单步规则可以使用如下组合器组合成完全重写系统：nop：：RuleF--identity（d）：：RuleF→RuleF→RuleF --顺序合成（n）：：RuleF→RuleF→RuleF--左偏选择多：：RuleF→RuleF--重复once：：RuleF→RuleF--任意深度规则应用对于这些和其他组合子的实现，我们参考其他地方[12，11]，以及如何将它们组合到重写系统中，例如：Simplify：：RuleF--穷尽地应用规则，直到达到标准形式为了实现类型转换，我们需要一个两级重写系统。两级重写规则可以表示如下[9]：typeRule = Rulea。 类型a →可能（视图（类型a））dataView a，其中View：：（a→b）→（b→a）→Type b→View（Type a）View构造函数表示，如果类型a和类型b之间存在一对转换函数，则可以将类型a细化为类型b。请注意，只有源类型a从View的类型构造函数中逃逸。Rule类型表示，当重写类型表示时，我们不替换它，而是用表示函数来增加它，以便在源和目标类型之间进行转换为了用单个规则组成两级重写系统，定义了策略重写组合器，类似于重写无点函数的组合器。例如，在[9]中定义了层次关系映射的策略atten5.4构造约束感知重写规则约束感知重写规则的构造在三个重要细节上不同于常规规则首先，规则需要在目标类型上引入约束。其次，它们需要考虑可能存在对源类型的第三，某些规则要求存在对源类型的约束，这必须在规则应用之前进行检查。为了说明前两个问题，我们考虑一下嵌套映射的规则中文（简体）atMap（a~（b×（c~d）=return（View0−n10n（tφ））其中t=（a~b）×（（a×c）~d）14朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3φ=（（set π1）<$（δ<$π2））<$（δ<$π1）PRACTATMAP t=propagatePRACTATMAP t第一个等式负责不变量的引入，其中约束φ与结果类型t相连。约束传播的问题由辅助函数propagate处理，定义如下：propagate rule（aφ）=do（View to from b）←rule alet=φfromreturn$View to from（b）传播=mzeropropagate函数将其参数重写规则应用于受约束的数据类型a，以获得新的数据类型b以及转换函数to和from。它将约束φ与from后组合以获得新的约束φ。最后，将该约束附加到结果类型b。第三个问题是检查所需约束的存在性，它在构造互逆规则时起作用，该规则将一个映射嵌套到另一个映射中：nestMap：：RulenestMap（a~b）×（（×c）~d））（setπ1）<$（δ <$π2））<$（δ <$π1）=return$视图0n0−n1nestMap=mzero（a~（b×（c~d）这里，模式匹配是对类型和约束进行的。 只 如果此约束等于所需约束，则规则成功。这并没有考虑实际约束暗示所需约束的可能性，但不等于它。在这种情况下，需要一些满足性证明，这超出了本文的范围（但参见[17]）。在应用重写步骤期间创建的函数组合和嵌套约束可以使用以下规则来简化compose constraint：：Rulecompose constraint（（aφ））=return（View id id id（a（φ）compose constraint=mzerofuse constraint：：Rule熔断器约束（aφ）=do←简化φreturn（View id id（a））熔断器约束=mzero在后一个重写规则中，无点函数的重写系统简化被调用，这意味着我们的第一个函数重写系统将嵌入到我们的类型重写系统中。朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）315× × ××× × ××× × × ××× ××6层次关系映射的应用现在我们将重新讨论第2节的例子。图2的模式可以通过以下类型表示来捕获：imdb=（actors×show）imdbinv其中imdb inv=（setπ1）fuse（setδ）ρπ1<$δ<$π2show=（“年份”ד标题”）~（（列表“评论”）×（电影+系列））电影=（列表（“国家”ד价值”））ד导演”series =“Yr”~（列表集）episode=“Name”×（可能是“Director”）actors=“Name”~playedplayed=（（“Year”דTitle”）דRole”）~（List“Award”）原始模式的主键约束通过使用有限映射在结构上被捕获。外键约束由imdb inv捕获，它指定played域中的值包含在show域中，即played的年份和标题（在域中定义）是对show（域）中定义的年份和标题的引用。这个约束应该通过模式转换过程传播使用[9]的约束简化策略，从层次结构到其关系等价物的转换结果如下：（playeds奖演员表演评论季节情节系列电影boxo电影）inv哪里playeds=（“Name”“Year”“Title”“Role”）~Oneawards=（（“Name”“Year”“Title”“Role”） Int）~“Award”actors=“Name”~一个显示=（“年份”ד标题”）~一个reviews=（（“Year”דTitle”）×Int）~“Review”季节=（（“年份”ד标题”）ד年份”）~一集=（“年份”ד标题”）ד年份”）×Int）~（“姓名”×（可能是“导演”））系列=（“年份”ד标题”）~一部电影=（“年份”ד标题”）~“导演”boxo格式=（（“年份”ד标题”）×整数）~（“国家”ד数值”）inv= fk1 fk2 fk3 fk4 fk5 fk6 fk7 fk8 fk9 fk1=（ setπ1）δπboxo电影fk 2=（集合π1）<$δ<$π剧集<$δ <$π季节 fk3=（集合π1）<$δ<$π季节<$δ<$π系列 fk 4=（集合π2）<$δ<$π评论<$δ<$π节目 fk5=δ<$π电影<$δ<$π节目fk6=δπ π级数 δfk7=（ setπ1）δπawardsδπplayedsfk 8=（ setπ1<$π1<$π1）<$πplayed<$δ<$πactorsfk9=（ set（π2× id）<$π1）<$δ<$πplayeds<$δ<$π表示在这里，我们引入了表名，以提高可读性，并与第2节中伪SQL中显示的预期结果进行比较。结果由10个表组成：3个来自actor子模式，7个来自show。此外，还得到了9个约束条件，其中8个是在转换过程中引入的。约束fk9由原始约束imdb inv的传播产生。注意，在没有调用简化重写系统的情况下，合成的约束将不会被16朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3←←←←如此简洁。例如，如果没有重写，fk2约束的初始片段将是：fk2=（setπ1）<$δ<$π2）<$δ <$π1）<$（（assocl~id）×id）◦ （id×（assocl~id））（id×（assocl~id））（（assocr~id）×id）（id×（ass ocr~id））请注意，一般来说，简化不能推迟到重写之后，因为在约束上匹配的规则期望它们是简化的形式。为了验证结果，我们可以将信息插入数据库并观察约束检查结果。例如，我们可以添加有关电影中演员角色的> dbJaddActorsPlayed db（（“Jet Li”，（2001，“The One”）），“Lawless”）> check imdbResultdbJFalse约束正确地失败，因为演员的名字和演出都不存在。我们应该首先添加这些信息：> dbJaddShow db（2001年，“The One”）> dbJJaddActor dbJ李连杰> dbJJJaddActorsPlayed dbJJ（（“李连杰”，（2001，“TheOne”）），“Lawless”）> check imdbResultdbJJJTrue现在，约束检查成功。7相关工作已经提出了大量的方法来将XML映射到关系数据库[7，6，2，4]，但通常没有考虑约束。 Lee et[15]第一次提出了约束保持的问题。他们的CPI算法处理引用完整性和一些基数约束，这些约束存储在带注释的DTD图中。当图被序列化为SQL模式时，各种SQL约束与表一起生成。与我们的方法相反，这种基于图的算法不处理任意约束，它专门用于层次关系映射，并且缺乏类型安全和形式化的公正性。Chen等人 [8]基于路径表达式引入了XML函数依赖（XFD）的概念。提供了映射算法，将XFD传播到目标关系模式，并利用XFD来达到具有较少冗余的模式。Davidson等人 [13]提出了另一种约束保持方法，也使用路径表达式。相反，我们的约束并不局限于关系完整性约束。我们已经将约束表示为无点函数，它可以自动转换为包括路径表达式在内的结构害羞程序[12]。朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）317Barbosa等人 [4]讨论了关系模式上的约束的生成，这些约束使XML-关系映射保持信息，即同构。初始XML模式上的非结构性约束不被考虑在内.约束和转换函数用Datasheet（的变体）表示，Datasheet可以以机械方式（手动）重写为标准形式Berdaguer等人[5]使用类型注释机制来捕获约束。因此，涵盖了较小类别的可能约束然而，注释机制允许对约束感知模式转换进行组合处理而不是路径表达式或标签，我们的方法采用强类型的布尔函数来捕获约束。 这样做的好处是更有表现力，并允许完全的合成处理。还要注意，我们的方法并不局限于层次关系映射，因为它可以用于一般的模式转换8总结发言贡献我们对数据精化和无点程序转换应用于数据模式、数据实例和查询的耦合转换问题的一系列研究做出了对约束感知模式转换的处理[20，1，9，11，12，5]。特别是• 我们已经展示了如何增强数据精化理论[20]以包括受布尔谓词约束的类型，这相当于扩展了[19]的工作;• 我们增强了层次关系映射的精化规则[1，5]，以便在目标类型上引入适当的约束，将某些精化转换为同构;• 我们已经扩展了两级变换[9]和耦合变换[11]的重写系统，以包括约束的传播，引入和简化。此外，我们已经表明，值级重写需要在类型级重写期间完成，因为类型级重写规则可能只在具有规范化约束的类型上• 我们已经演示了使用扩展重写系统来将XML模式映射到SQL模式，其中自动为目标模式生成引用完整性约束。本文所采用的方法是[5]方法的替代方案，[ 5 ]方法仅限于用特定的标记技巧表示的约束，而我们通常处理约束展望了今后工作的几个方向约束作为共相关关系我们将约束建模为布尔函数。另一种方法是将约束建模为相互依存关系。另一种方法的一个优点是，它允许我们在重写过程中使用关系证明系统[17]来检查redex的实际约束是否暗示了具有约束源数据类型的规则所需的约束18朗格Alves et al. /Electronic Notes in Theoretical Computer Science 290（2012）3集成我们希望将这里提出的约束处理与在基于标签的处理[5]的上下文中开发的前端和名称保留进行集成。同样，我们希望为[12]的结构性查询集成重写系统，以便我们可以处理结构性约束。确认感谢Jo s'eNunoOli veira和AlcinoCunha的启发性讨论。首两名作者分别由联邦调查委员会资助，编号为SFRH/BD/30215/2006及SFRH/BD/19195/2004引用[1] 阿 尔 维 斯 ， T.， P. Silva ， J. Visser和 J. Oliveira， Strategic term rewriting and its application to aVDM-SL to SQL conversion. ，in：J. Fitzgerald，I. Hayes和A. Tarlecki，editors，Formal Methods，LNCS3582（2005），pp. 399-414[2] Amer-Yahia，S.，F. Du和J.Freire，XML到关系映射问题的全面解决方案，WIDM31比38[3] Backus，J.，编程能从冯·诺依曼风格中解放出来吗？函数式风格及其程序代数。，Commun. ACM21（1978），pp. 613-641[4] Barbosa，D.例如，Designing information-preserving mapping schemes for XML，in：VLDB109-120.[5] Berdaguer，P.，A. Cunha，H.Pacheco和J.XML和SQL的耦合模式转换和数据，在：M。Hanus，editor，Proc. of Practical Aspects of Declarative Programming（PADL290-304[6] Bohannon，P.例如， From XML schema to relations：A cost-based approach to XML storage，in：ICDE'02：Proc. 第18届国际Conf. 数据工程（2002），pp。64岁[7] Bohannon，P.等人，LegoDB：为XML文档定制关系存储。，in：Proc. 28th Int. Conf. 非常大的 数据库（2002），pp。1091-1094.[8] Chen，Y.例如，约束保持从XML到关系的模式映射。第五届国际网络与数据库研讨会（WebDB），2002年，第100页。7-12.[9] Cunha，A.，J. Oliveira和J.Visser，Type-safe two-level data transformation，in：J.Misra等人，编辑，Proc. 正式方法，第14届国际。Symp. 欧洲正式方法，LNCS 4085（2006），pp. 284-299。[10] Cunha，A.和J. S. Pinto，无点程序转换。Fundam.告知。66（2005），pp. 315[11] Cunha，A.和j.Visser，耦合软件转换的强类型重写，ENTCS174（2007），pp. 17-[12] Cunha ， A. Visser ， Transformation of Structure-Shy Programs ： applied to Structure-Queries andStrategic Functions，in：G. Ramalingam和E. Visser，editors，PEPM（2007），pp. 11-20.[13] Davidson，S.例如，将XML约束转换为关系，见：Proc. 19th Int. Conf. on Data Engineering（2003），pp. 543-.[14] 拉梅尔河 和E. Meijer，Mappingsmakesdataproprocessinggo'ound ，in：R. L'ammel，J. 撒莱va和J. Visser，编辑，软件工程中的生成和转换技术，LNCS4143（2006年）。[15] Lee，D.和W. W. Chu，CPI：将XML DTD映射到关系模式的约束保持内联算法，DataKnowl.Eng.39（2001），pp. 三比二十五[16] 摩根角P. Gardiner，Data refenement by calculation，Acta Inform