没有合适的资源?快使用搜索试试~ 我知道了~
数据精化的范畴理论模型
理论计算机科学电子笔记225(2009)21-38www.elsevier.com/locate/entcs数据精化的范畴理论模型迈克尔·约翰逊1,4麦考瑞大学澳大利亚悉尼2109David Naumann大卫·瑙曼2,5史蒂文斯理工学院Hoboken NJ07030,USAJohn Power约翰·鲍尔3,6巴斯大学计算机科学系地址:Claverton Down,Bath BA2 7AY,UK摘要我们给出了一个帐户的使用范畴理论在建模数据精炼在过去的二十年。我们从Tony Hoare在范畴论术语中对数据精化的表述开始第一个由伴随模拟给出,第二个由松散逻辑关系的概念给出它们提供了可用于组合语言的技术,例如带有过程传递的命令式语言。关键词:数据精化,松弛自然变换,伴随模拟,松弛逻辑关系。1作者感谢ARC赠款[2]本文作者感谢NSF基金INT-9813854的支持。3作者感谢EPSRC赠款GR/586372/01的支持4电子邮件:mike@ics.mq.edu.au5电子邮件:naumann@cs.stevens-tech.edu6电子邮件:ajp@inf.ed.ac.uk1571-0661/© 2008 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2008.12.06422M. Johnson等人/理论计算机科学电子笔记225(2009)211引言1987年,Tony Hoare写了一篇论文草稿[9],在其中他使用范畴论为他在过去20年中的数据精化发展提供了一个抽象的形式主义[8]。 正如霍尔在[9]中所说,显然有一个统一的身体, 范畴理论的基础,他的建设,但他不知道的细节。对于Hoare这个问题的答案在[17]中得到了进一步的发展。但是,这项工作只是对命令式语言的数据细化给出了合理的解释,而没有任何过程传递。 和如何扩展这项工作以考虑过程传递或甚至考虑一个小应用性语言并不明显。从这一点开始,就出现了不同的做法。瑙曼已经将霍尔的方法以其最初的基本形式应用Power与其他同事合作[14,31,16,18,34],发展了松散逻辑关系的概念。这两种方法本质上都是范畴论的,但它们是完全不同的。在本文中,我们概述了我们的各种尝试,使用范畴理论模型数据细化,我们的出发点是霍尔在第2节中,我们描述了一种简单的命令式语言,我们将在其中构建Hoare对命令式语言的数据精化的解释。 Hoare用由L自由生成的具有结构C(L)的范畴识别了一种语言L,他还识别了一种具有域C(L)的结构保持函子的L模型。我们通过一个实质性的例子来解释为什么这是一个合理的基础,可以在此基础上添加一个数据细化的帐户。 霍尔把所有的事情都归结为一种任意的语言,但为了具体起见,我们研究一种简单的语言。在第3节中,我们介绍了Hoare的向下模拟的概念,等价于我们的命令式语言的结构保持宽松的自然变换,概述了两个主要结果,并指出该定义如何扩展到更一般的命令式语言类,而无需过程传递。霍尔也定义了向上模拟,但它们是向下模拟的一种变体,基本上同样的技术也适用于它们;因此为了简单起见,我们在这里将其省略。向下的模拟似乎是不够的高阶结构。因此,我们必须修改这个概念,以便将过程传递或应用语言纳入我们的分析。在第4节中,我们展示了松散的自然转换如何对数据细化进行建模 用于包括现代数据库系统的特定类别的非高阶系统。我们的分类模型在数据细化中的应用已经达到了工业应用的阶段,它表明了松散的自然转换框架如何简单地应用于一个通常被认为与编程语言语义完全不同的领域。在第5节中,我们给出了两种可能的方法中的第一种,以给出适用于高阶函数和命令式语言的数据精化的范畴论解释。此帐户使用一个语义类别,其中附加条件M. Johnson等人/理论计算机科学电子笔记225(2009)2123⊥--可以在不失去表现力的情况下施加于向下的模拟。我们解释了如何霍尔最后,在第6节中,我们解释了松散逻辑关系的概念,并展示了如何它允许人们为简单的应用语言建模数据精化,特别是由简单类型的λ-演算给出的具有一些基本类型和基本运算符的语言。这是基于[31]的工作我们展示了霍尔的两个主要定理如何松散逻辑关系的概念可以扩展[16,34]以解释涉及函数式和命令式特征的更复杂的语言。2作为具有结构的范畴的命令式语言;作为结构保持函子在本节中,为了具体起见,我们描述了一种简单的命令式语言,我们将在后面的章节中考虑它,以给出数据精化的范畴论解释。我们描述的公理结构并不局限于这种语言。特别是,我们可以解释非决定论,尽管这是一种确定性语言。事实上,我们可以解释霍尔的所有语言Lsimple本质上是Tennent书中的简单命令式语言我们假设有基本数据类型unit和bool,诸如NAT之类的其它基本数据类型和诸如堆栈之类的抽象数据类型,以及表示程序状态的特殊类型STAT判定mand.” 我们假设在数据类型上有一些操作符 而且我们假设可数集合I=10,11,.,恩,... 变量标识符的集合和从I到原始数据类型集合的类型赋值函数π 0。我们不允许π0(i)=stat。使用这种表示法,Lsimple的派生语法和命令式语法如表1所示。我们在描述Lsimple时没有包括类型之间、操作符之间或命令之间的等式。引入方程是正常的,无论是直接的还是通过操作语义,例如,这意味着Lsimple的运算符的组合是结合的,单位由id给出。显然,一个完整的语言将包括这样的方程。 我们默认任何合理的语义都需要满足这样的方程我们给出了一个语义L简单的集,类别的点集和保函数,如下。[[unit]]d=ef1<$=<${1,<$1},<$1<$,[[bool]]d=efB={true,false,B},B,[[stat]]d=efSd=efi∈I[[π0(ιi)]],Set中的乘积,其他数据类型可以自由地由SetObject的任何对象建模。 外延24M. Johnson等人/理论计算机科学电子笔记225(2009)21⎣0⎥⎦⎣0⎥⎦!: op[stat,unit]id:op[τ,τ]FJ:op[τJ,τJJ]F:op[τ,τJ]FJF:op[τ,τJJ]π0(i)=τi:op[stat,τ]B:op[τ,bool]F0:op[τ,τJ]F1:op[τ,τJ]ifBthenF0elseF1:op[τ,τJ]skip:跳diverge:跳E:op[stat,τ]π0(i)=τ i:=E:τB:op[stat,bool]C0:C1:ifBthenC0elseC1:C0:C1:C0;C1:B:op[stat,bool]C:whileBdoC:表1简单命令式语言的派生语法和命令式一个arity(τ,τJ)的算子的是集合n中从[τ]]到[[τJ]]的态射,其导出算子的语义如下生成[[!]]d=ef[s<$−→1],[[id]]d=efid[[τ]],[[FJF]]d=ef[[FJ]]f[[F]]ifF:op[τ,τJ]和FJ:op[τJ, τJJ]。[[in]]d=ef[s-→sn]其中sn是s的n次component,如果[B]](t)=,[[ifBthenF0elseF1]]d=eft−→[[F]](t)如果[B]](t)=真,⎪⎩[[F1]](t)if[B]](t)=false其中t是[τ]的元素,一个命令的表示被定义为集合S中S上的自同态,如下所示。在定义in:=E时,我们认为元组是严格的。[[skip]]d=efidS,[[div]]d=ef[s−→S],[[n: =E]] d=ef[s0s1. . sn. . . −→s0s1. . . sn−1[[E]](s)sn+1. . . ]、[[C0;C1]]d=ef[[C1]][[C0]],如果[B]](s)=,[[ifBthenC0elseC1]]d=efs−→[[C]](s)if[B]](s)= true,[[C1]](s)if[B]](s)=falseM. Johnson等人/理论计算机科学电子笔记225(2009)2125..→{→|∈||}[[whileBdoC]]d=ef[[Cn]],0≤n其中,while语句的定义中的Cn归纳定义如下:C0d=efdiv,Cn+1d=efifBthen(C;Cn)elseskip,和是指集合n中态射链的最小上界。这给出了Lsimple的传统语义。观察到范畴Set的局部有序结构对于建模while是必不可少的。 语义也可以被描述为具有域C(Lsimple)的结构保持函子,其为定义如下。定义2.1句法范畴C(Lsimple)是由节点为Lsimple的数据类型,从τ到τJ的边为arity(τ,τJ)算子的图生成的结构自由的局部有序范畴; 须作出跳过恒等式,发散最小元素,赋值由可数建模产品,序列(;)的组合,如果语句的有限余积,而语句的最小上限,以及类似的运营商,受方程确定的完整的我们的语义函数确定了一个从C(Lsimple)到局部序范畴Set_n的保结构局部序函子。相反,从C(Lsimple)到SetC的任何保持局部有序函子的结构决定了语义功能协调发展的因此,霍尔用局部有序范畴来识别语言L简单goryC(Lsimple),他用从C(Lsimple)到SetC的相应结构保持局部有序函子来识别Lsimple的语义。我们只在局部有序范畴SetA上使用了特定的结构,所以这种对应从SetA中的语义推广到任何具有必要结构的局部有序范畴A中的语义:参见[17],以获得广泛普遍性的精确陈述。这一现象和一系列的例子。3命令式语言我们将简单命令语言的术语Lsimple表示为L,并设M,N:C(L)A为L的两个模型,即局部序范畴A的结构保持局部序函子.对于M是N的精化,Hoare要求一族映射ρa:M(a)N(a)一C(L). 这个想法ρa表示N(a)的哪个值由M(a)中的给定值表示有人可能会问这是一个自然的变换,但霍尔想放松自然性条件,以便使M比N更有定义。为了说明这一点,考虑一种语言,它有一个类型栈,并且有空操作符:op[unit,stack]和pop:op[stack,stack]。将顺序视为我们希望N保持unfined。另一方面,我们不关心表示M取什么值。更精细的M也可能使pop空无一物,26M. Johnson等人/理论计算机科学电子笔记225(2009)21→→⇒→⊥◦≤◦⇒⇒∗∗或者它可以将其带到任意元件。因此,我们只需要(1)N(pop)ρstack≤ρstackM(pop),而不是自然转化所需要的平等。这个论点从定义性推广到其他可以建模的正确性概念 一个命令,更具体地说,让A=SetA,如第2节中所述,通过观察M (unit)=N(unit)=1A来定义M,N:C(L)→SetA,因为这是由L的语义确定的,并且N(stack)=N,N(empty)(1)=0,N(pop)(n+1)=n,N(pop)(0)=N,M(stack)= n {有限二叉树},空树n,M(empty)(1)= n,单点树,M(pop)(t0,t1)=t1,M(pop)(pop)= pop,并定义ρstack:M(stack)N(stack),方法是将树发送到其最右边分支的边数。这个定义自然地扩展到C(L),条件(1)成立。因此,在pop时,M比N更有定义;M(pop)取to,而N(pop)取0到N,因此N(pop)ρstackρstackM(pop)。 既然我们不在乎 值解释分配给非法术语,如pop empty,我们说M给出了N的表示,ρ给出了一个细化。然而ρ不是自然的;事实上,从M到N没有自然的变换。然而,ρ是一个松弛变换。扩展我们的例子,当A是具有结构的集合的局部有序范畴时如果存在松弛变换α:MN:C(L)A从M到N,M(a)被认为是N(a)的表示,αa:M(a)N(a)将M(a)中的每个值映射到它所表示的,对于C(L)的每个对象a。霍尔用向下模拟这个术语来表示松弛变换。术语前向模拟已经普遍用于这个概念,以及对偶的向后或向上模拟[5]。历史和预言这两个术语也是常用的[19]。有些来源在相反的意义上使用向上和向下。一个更自然的范畴论定义,也是一个允许更强结果的定义(见[18])是将向下模拟定义为一个结构,它遵循从结构保持函子M到结构保持函子N的松弛自然变换。所以我们把它作为我们的定义。霍尔寻求的主要结果定理3.1· 如果α:M N和β:N P是向下模拟,则合成βα是从M到P• 每个定义在基类型和基运算符上的向下模拟都扩展到 向下模拟定义在所有类型和所有操作符上。M. Johnson等人/理论计算机科学电子笔记225(2009)2127其中第一个是平凡的;第二个需要证明,并取决于L的结构。它具有实用的重要性,因为L通常只有少量的基类型和基运算符,因此检查某个东西是否当限制到基类型和运算符时,遵守宽松变换的结构是可行的,而C(L)是无限的,因为可以任意多次应用类型构造函数。因此,如果没有将无限体与有限体联系起来的结果,就无法验证具有基于C(L)的关于松弛变换的结构,并且任何合理的数据精化说明都必须说明哪些类型构造器和运算符允许这样的结果。如果L只有有限的乘积类型和常量命令,则唯一的扩展从基类型和操作到所有C(L)的松散转换的结构总是存在的。 然而,如果,例如,L有一个逆变结构或混合方差的结构,如高阶类型给出的,那么扩张一般不存在。因此,霍尔问,是否可以给出一个精确的,一般的说明,哪些结构允许这种独特的扩展。本文[17]致力于回答Hoare重点是• 在定义语言L时可以考虑的结构及其语义是由范畴LocOrdl上的丰富代数结构E_S,E• 基类型和基运算符概念的范畴理论公式对于特定的代数结构,E_S,E_D是E_S,E,D_D的代数结构这些定义支持霍尔所寻求的两个定理;论文[17]给出了细节和例子:例子包括霍尔的所有例子其中的结构是协变的,因此它包含了简单命令语言Lsimple的所有结构,以及一个幂域的结构,以模拟不确定性。但它具体地不包括函数类型,并且有两种方法来包括它们,我们将在第5节和第6节中进行研究。4数据库数据细化和宽松的自然转换在我们继续处理函数类型之前,本节将介绍我们的数据细化分类模型的一个示例应用。 该示例说明了在上述框架中定义的简单协变数据库语言的使用-数据库的结构被呈现为具有结构、模型(也称为“快照”)是结构保持函子(通常在有限集合或有限集合和部分函数的范畴中取值),并且通过(结构保持)松弛自然变换给出数据细化。在下面的段落中,我们将更详细地描述每一种方法,并在本节结束时指出这种方法如何在行业中受益。在[12]中可以找到对这种方法的基础的更严格的介绍28M. Johnson等人/理论计算机科学电子笔记225(2009)21→⇒→数据库经常通过给定实体、实体之间的关系和实体的属性来指定该信息可以概括在有向图中,该有向图具有作为节点的实体、关系和属性值集合,以及从每个实体到其每个属性值集合的边,以及从每个关系到其所涉及的每个实体的边。广泛使用的实体关系建模技术是试图发现这样的图,该图最好地表示要存储在数据库中的数据的结构。但是,当然,在真实世界的系统中,数据将被要求满足ER图中没有记录的许多约束,包括属性只能取一定数量的已知值、某些属性依赖于几个实体(不仅仅是一个)以及某些关系的组合必须相等的要求将图的L和额外的约束条件一起写下来。L是特定数据库可用的语言具有结构C(L)的范畴应该具有什么样的结构?我们需要一个终端对象1,这样我们就可以讨论元素,有限余积,这样我们就可以构造属性值集作为1的固定余积,有限积支持依赖于多个实体的属性,拉回支持关系组合。所以我们要求C(L)是由L自由生成的具有有限余积和有限极限的范畴。顺便说一下,在信息系统的分类规范的发展早期, 类别C(L)具有对应于可以应用于具有结构L的数据库的每个结构查询的对象[4]。因此,C(L)是另一种意义上的语言-它体现了结构为L的数据库的查询语言。 像往常一样, C(L)的模型是保结构的 函子C(L)A对于局部序范畴A,通常是指向集的范畴,或者等价地 集合和部分函数的范畴。因为函子保持有限余积,所以属性值集保持不变,直到规范同构在给定数据库的所有模型中,虽然实体或关系可以通过不同模型中的各种基数的集合来建模,作为该实体或关系的实例,从数据库中插入或删除关系如果存在松弛变换α:MN:C(L)A两个模型之间M和N,我们说M是N的数据细化。既然在这里自然变换的使用是很好理解的,我们就集中注意一下这种变换的松弛的松弛,不平等的概括(1) 上面说,如果我们把A的态射的次序看作是有定义的,那么M可能比N更有定义。这在数据库应用程序中尤其重要,其中在一个模型中具有未知值的属性经常被更新为在另一个模型中采用已知(更多定义)值这种方法在工业上是如何发挥作用的?如上所述,实体-关系建模虽然很有用,但忽略了一系列重要的约束.以正式和一致的方式将这些约束包括在模型中,不仅完成了模型,而且经常揭示出开发中模型的不足之处。这种开发方法已被用于与行业的大规模合同,包括一家主要的电信运营商,一家石油公司和一家政府。M. Johnson等人/理论计算机科学电子笔记225(2009)2129◦≤ ◦一一一卫生部,以及其他组织。它一直在分析和具体化阶段增加价值。当然,这个示例应用程序只涉及一阶操作。我们现在继续将数据精化扩展到更高阶的构造。5高阶命令式程序的向下模拟Hoare指出,一般来说,如果结构包括contravari,那么对基类型和运算符的向下模拟可能无法扩展到完整的语言。蚂蚁结构,如指数。霍尔利用域理论中熟悉的嵌入-投影对的概念,将“全模拟”定义Naumann指出,要求每个αa是内部右伴随是足够的,即,存在αo:N(a)→M(a),其中id≤αa<$αo且αo<$αa≤id.Kinoshita和Power在[15,17]中也观察到了这一点,他们表明,如果模拟仅限于伴随模拟,则定理3.1也适用于逆变结构。在他的论文[22]中,Naumann还将Hoare的发展推广到2-范畴,如下所示。 语义范畴被认为是2-范畴,因此不等式被2-胞元代替。结构需要满足标准相干条件,向下和伴随模拟也是如此。主要的应用是2-cell表示精化证明的想法,但该应用 并没有正式开发。在霍尔的手稿的基本风格,它表明,一致性条件被霍尔考虑的所有结构,以及各种额外的2-范畴中出现的。到目前为止,只为局部有序范畴发展了一个精确的一般公式,没有迫切需要更多的Hoare希望对哪些证明技术可以与哪些构造一起使用进行分类。逆变和伴随模拟之间的联系可能是这种分类的一部分,并且高阶结构比一阶结构要求更高也就不足为奇了。另一方面,伴随模拟是不可接受的限制,在一些领先的模型。这导致鲍尔采取了一种似乎非常不同的方法,即松散的逻辑关系(见第6节)。Naumann专注于伴随模拟有用的语义类别。为了以一种强调与逻辑关系的联系的方式介绍这些范畴,我们首先重新考虑第3节的结果。回想一下第3节,Hoare α α M(S)其中程序表示,例如N(S),由连接语言的两个解释的态射α组成。如果没有足够的态射来建立所需的连接,这是不够的。(In在这篇文章中,我们非正式地讨论了充分性,但我们的评论是由完整的-30M. Johnson等人/理论计算机科学电子笔记225(2009)21⊆⊥在文献中的结果)。如果我们把A设为集合A,并把我们自己限制在伴随模拟上,我们只剩下同构,同构是确定的。显然不足以说明在观察上不可区分的不同数据表示。让我们考虑逻辑关系的替代方案,众所周知的功能程序。为了简单起见,让我们忽略发散,并考虑一种语言,如简单类型的lambda演算,具有非发散的基运算符,因此我们可以使用将M,N解释为集合而不是集合n。 一个逻辑关系包括,每个类型a,二元关系Ra<$M(a)×N(a),使得对于每个程序,S:A→B我们有(2)xR ay =<$M(S)x R bN(S)y对于所有x,y。有些作者倾向于强调R和M(S)起着不同的作用;这导致了第6节中的公式。但是逻辑关系条件(2)也可以表示为向下模拟。设Rel是集合之间二元关系的范畴由于Set包含在Rel中,我们可以认为语义函子M,N也包含在Rel中。因此,我们可以用关系组合它们的图像,如下所示M(a)M(S))M(b)(3)R RV V也就是说,N(S)R R M(S)N(a))N(b)N(S)这个不等式等价于(2)。通过在一个更大的范畴(Rel)中嵌入程序语义的范畴(在本例中为Set),我们已经将所需的连接表示为向下模拟正方形。在Rel中,伴随态射是全函数,而全函数甚至不适合确定性一阶程序[5,19]。但是嵌入的想法可以更进一步。我们可以把Rel嵌入到一个更大的范畴中,在这个范畴中,关系不仅是态射,而且是伴随的。诺曼研究的特殊例子是谓词变换器的范畴。在给出它们的一般构造之前,我们遵循历史路径,用基本术语描述谓词变换器。与命令S相关联的最弱前置条件函数wp(S)将后置条件映射到前置条件。作为一个语义模型,谓词转换器具有吸引力,因为它们充分地建模了发散性和不确定性,而不需要提升或幂集[30,10]。 对于第2节的语言,让我们把“谓词”看作是[ stat ]]的子集p,不包含。 则wp(S)(p)是M(S)在p上的逆像。因为谓词转换器是从后置条件到前置条件的函数,所以很自然地用相反的类别来描述它们。 设PSpec具有集合作为对象,并设PSpec(X,Y)为集合从幂集P(Y)到P(X)的单调函数。每一个母集都是局部序的,且≤关于集合的包含的逐点序名称M. Johnson等人/理论计算机科学电子笔记225(2009)2131≤→◦≤◦ ◦≤PSpec暗示了这样一个事实,即这个类别不仅包含程序的表示-它还以这样一种方式对总正确性规范进行建模[1,5], 订单 代表对规范的满足和程序的算法完善。PSpec中的右伴随态射是完全析取函数。PSpec(X,Y)中的完全析取函数与Rel(Y,X)是有序同构;同构发送一个关系到它的正像函数,其左伴随是它的逆像函数。这是关键的诺曼• 将语义类别嵌入到其中所需的向下模拟是伴随模拟的一个中,并检查• 较大的范畴具有伴随模拟扩展所需的结构和性质。手头的例子是一般结构的一个例子。 回想一下,Rel可以被构造为Set上的span,而Set作为右伴随态射嵌入Rel(右或左,取决于人们如何选择制定定义)。跨度构造可以推广为“斜跨度”的概念除了更多的伴随模拟的可用性之外,在同一对象上嵌入更多态射的类别的好处是,更丰富的语言可以 被解释为,例如,PSpec模型天使和恶魔的不确定性。代价是某些结构的性能较弱。 集合的笛卡尔积是这是这种弱化的一个重要例子。 在PSpec中,产品形成了一种非常松散的类型的adjunction。 例如,人们期望不等式π(f,g)f(因为g可以发散)和不等式((π h),(πJh))h(因为h可以是非确定性的);这些都是霍尔但在PSpec中,不平等是有条件的。因为PSpec包含任意单调函数,它包含表现出“奇迹”和“天使般的不确定性”的态射这是建模规范[1]所需要的,但它意味着,例如,第一个投影l awπ(f,g)≤f仅当f,g是严格严格的时才成立。f的不确定性,有时被称为“排除奇迹定律”,可以表示为f发散=发散。使用Hoare手稿中的初等证明,Naumann证明了向下模拟甚至可以扩展到这些非常宽松的产品[ 23 ]。 人们认为,一般理论适用于他们[13],但细节还没有明确地说出来对于PSpec中较高类型的处理,可以使用斜跨结构将结构从Set提升到PSpec[6]。这种提升不会创建新的对象,所以提升后的指数只是函数空间。这足以使用伴随模拟来处理简单类型的lambda演算,通过在PSpec中嵌入Set来组成语义M:C(L)Set。 但对于表示PSpec态射的命令式程序,箭头类型应该由PSpec的内部hom来解释。这是松弛积的一个非常弱的伴随,即使使用条件不等式也很难找到有用的公理化[24]。在32M. Johnson等人/理论计算机科学电子笔记225(2009)21U◦◦⇒U → U×特别地,它不是函子的,所以我们不能应用我们寻求伴随模拟的扩展结果。弱性质的一个原因可以在PSpec的定义中找到:它的对象是幂集,但是取有序homset的幂集完全忽略了它的序结构。这让我们想到了一个稍微更精细的范畴Spec:Ob-1是偏序集,Spec(X,Y)是单调函数Y X的集合,其中X是X上的上交易格,由。Naumann最初用这些基本术语来处理Spec,但后来发现它是偏斜的一个实例。[25 ]第25话,我的意思是,Spec中的lax乘积与PSpec中的lax乘积行为相似,但指数具有稍微好一点的性质;特别是,对态射的作用是函子的。最后,我们得到了Naumann定理5.1基类型上的每一个伴随模拟都扩展到语言的一个伴随模拟,包括指数(Currying,application和arrow functor)。关于定理3.1的第一项,情况很清楚:伴随模拟确实是合成的。虽然定理5.1是用指数来表达的,但对谓词变换的最初兴趣来自命令式语言。第一位作者使用模型Spec为Modula-3这样的传统命令式语言提供语义,其中过程可以存储在状态变量中并作为参数传递[27],他表明这种语言存在伴随模拟的扩展[29]。但是,因为程序被允许有全局变量和参数,与指数的联系有点间接,在引用的工作中,范畴方面被抑制了。直到后来才明确提出了与lambda演算的联系[28]。作为进入下一节的桥梁,让我们回顾一下前面的讨论。起点是一对从C(L)到语义范畴A的结构保持函子M,N,以及一个只定义在L的基本类型和操作上的向下模拟α。像(3)这样的不等式平方是我们感兴趣的主要对象,所以让我们以标准的方式将它们归入Sims范畴:对象是A的态射,态射是构成不等式平方的态射对。以δ0,δ1为Sims到A的明显投影,向下模拟α:MN等于L到Sims的函子α<$,使得M=δ0α<$,N=δ1α<$. 图片看起来是这样的。SimsC(L)((δ0,δ1)v)A AM、N)(虽然这种向下模拟的描述主要用于M. Johnson等人/理论计算机科学电子笔记225(2009)2133∅在A是笛卡尔闭的情况下[7],Spec的例子表明它更通用。主要目标是将仅由基类型和基运算定义的α_n推广到所有C(L)。 只要A具有使M(S),N(S)对于某个程序S是可定义的必要结构,那么这个结构也可以用来定义α的相关分量。结果平方是否是一个不等式,从而定义απ(S),取决于A-上结构的性质,这是扩张定理的内容如定理3.1的陈述所示,目标是使扩展存在,并使模拟合成。这并不意味着模拟必须尊重用于获得扩展的所有结构,在第6节中被使用。为了结束本节,让我们考虑一种高阶数据细化,一个构造的细化,特别是指数。熟悉pred- icate Transformer语义的读者会注意到程序的表示是 在Spec中不是任意的态射;它们享有额外的健康条件--通过非空的交叉点和上升链的并集来保持和分布[30,10]。使用所有单调函数的主要动机是在程序精化的演算中对规范进行建模。由于Spec的强性质,Spec的内函数是有用的;除了定理5.1,我们提到,它产生了归纳数据类型的Lawvere另一方面,为了充分抽象程序语义,我们应该注意程序表示作为Spec的一些完全对象子范畴Prog的嵌入。这里Prog可以是,例如,偏序集,用于简单类型的函数程序,或由上述健康条件给出的Spec的子类别,用于非确定性命令式程序。如果我们将箭头类型的语义视为Prog的内部hom,那么我们需要考虑与Spec的内部hom的联系;这本质上将Prog嵌入Spec中。在[26,第7节]中,在类似于Hoare草案的一般性水平上,用初等术语一个更一般的帐户将是非常受欢迎的。特别是,为了处理递归类型,人们希望有一个适用于CPO上的倾斜跨度类别的帐户。6使用松散逻辑关系在本节中,我们希望尽可能地保持霍尔的基本方法,但特别考虑高阶类型。因此,为了说明的简单性(但更复杂的处理请参见[16]和[34]),我们将注意力限制在简单类型的λ-演算上,它具有一些基类型和一些基运算符的乘积,我们称这样的语言为Lλ。正如在第2节中,霍尔对我们有34M. Johnson等人/理论计算机科学电子笔记225(2009)21−→−→−→×我们已经在第2节中解释了如何处理递归,所以我们不想在这一节中重复它。所以,为了便于说明,我们将忽略局部序结构,并将我们的模型放在Set中。为了符号简单,我们用L表示Lλ。正如Hoare在[9]中所指出的,高阶结构不考虑向下模拟。但是,逻辑关系的更一般的概念是专门设计的,以便高阶结构尊重它[21],因此,逻辑关系的概念产生了霍尔定理3.1的第二部分然而,逻辑关系不构成,所以它们不承认定理3.1的第一部分,因此不像霍尔和我们所理解的那样对数据精化进行建模。因此,经过几次尝试,特别是[14],第三作者和一些同事在这里定义了松散逻辑关系的概念[31],这是逻辑关系概念的温和概括,但满足霍尔的两个标准。所以我们在这里用范畴论的术语来Claudio Hermida在他的论文[7]中指出,逻辑关系可以用范畴论的术语来表达。他的分析的核心包括以下定义和命题,当在我们的范畴闭范畴C(L)的背景下考虑时。定义6.1范畴Rel2定义如下:对象由一对(X,Y)集合和从X到Y的二元关系R组成;从(X,R,Y)到(XJ,RJ,YJ)的映射是一对函数(f:XXJ,g:YYJ),使得xRy蕴含f(x)RJg(y);复合由函数的普通复合给出我们表示从Rel2到Set×Set发送(X,R,Y)到(X,Y)的遗忘函子,(δ0,δ1):Rel2−→Set×Set。证明范畴Rel2是Cardle闭的,并且Cardle闭结构被(δ0,δ1)保持,命题6.2给出一个从M到N的逻辑关系等价于给出一个函子R:C(L)Rel2严格保持Carnival闭结构,使得(δ0,δ1)R =(M,N)。第2版C(L)((δ0,δ1)v)设置设置M、N)我们把Hermida定义6.3从M到N的松散逻辑关系是函子R:C(L)−→Rel2M. Johnson等人/理论计算机科学电子笔记225(2009)2135×⇒⇒严格保持有限积,使得(δ0,δ1)R=(M,N)。第2版C(L) (一)(δ0,δ1)v)设置设置M、N)Henkin模型的概念与这一定义密切相关。一个简单类型λ-演算的Henkin模型是一个从C(L)到Set的有限积保持函子,使得诱导的lax映射是单射的。这是一种松散的模型,但并不完全等同于给出一元松散的逻辑关系;然而,这是一种自然的逻辑关系。和有用的推广的概念模型,我们已经使用,和一个我们的结果经常延伸。霍尔定理6.4· 如果R:M N和S:N P是松散逻辑关系,则关系的逐点组合产生从M到P的松散逻辑关系R;S• 每一个定义在基类型和基运算符上的松散逻辑关系都可以扩展到定义在所有类型和所有运算符上的松散逻辑关系我们也有进一步的定理来表明松散逻辑关系概念的定义性。定理6.5·(Lax逻辑关系的基本引理)关系族R(a)<$M(a)×N(a)对于C(L)的每个对象a,确定从M到N的宽松逻辑关系当且仅当对于C(L)中的每个箭头f:a-→ b,如果x R(a)y,则M(f)x R(b)N(f)y。• 一家人的关系R(a)<$M(a)×N(a)对于C(L)的每个对象a,确定从M到N的宽松逻辑关系当且仅当它确定从M到N的前逻辑关系• 每一个松散的逻辑关系至多是三个逻辑关系的合成。最后一个结果是文[11]中关于前逻辑关系的中心数学结果。7进一步工作我们在本文中尽了最大努力,以统一的方式介绍了我们的各种数据精炼方法,重点是什么使我们的工作团结起来,而不是什么使我们的工作分裂。但对于进一步的工作,考虑布里干酪可能更有指导意义36M. Johnson等人/理论计算机科学电子笔记225(2009)21我们之间的分歧产生了松散的结局,开放的问题和可能的进一步方向。瑙曼和电源的发展霍尔的想法有最共同之处,因为都研究了高阶规划。但他们使用了不同的语义:Naumann采用了谓词Transformer语义,而Power采用了逻辑关系。因此,一个明智的任务是使他们提出的两个扩展之间的关系更加精确。这种关系将为互补的观点提供理论支持,允许根据手头的具体问题使用任何一种观点相比之下,约翰逊专注于数据库的改进。这具有比瑙曼或鲍尔的工作更接近实践的属性,但它也相应地具有较少的理论发展。因此,人们想知道Naumann和Power的高阶分析是否会影响Johnson的数据库工作,特别是实体关系建模。更准确地说,Naumann和Power能解释数据库吗?约翰逊能看到高阶技术的作用本文的三位作者都对我们的共同点感到惊讶和印象深刻。 但这三个发展都引发了各自的问题 也例如,数据精化是一个普遍存在的概念,因此对于高阶编程的许多扩展中的任何一个,人们都可以要求数据精化的扩展理论。同样,行业使用复杂的数据库语言组合,每种语言都需要对数据进行细化分析。在这里讨论的工作中没有建模的一个工业关键语言特性是可变堆对象。 对于数据精炼,人们寻求一种关系的概念,在分离逻辑的意义上是局部支持的[20,2为了将数据精化的分类方法扩展到堆,利用Birkedal和Yang [3]以及Power [33]的最新工作可能是富有成效的从本质上讲,数据精化是我们理解编程的基础,本文的中心主张是霍尔引用[1] 后退,R,A calculus of refinements for program derivations,Acta Informatica25(1988),593[2] Banerjee,A.,和D.A. Naumman,Ownership Confinement Ensures Representation Independencefor Object-Oriented Programs,J. ACM52(2005)894[3] 伯克达尔湖,和H.杨,关系参数化与分离逻辑,[4] Dampney,C.,M. Johnson和G. Monro,ERA的数学基础,[5] de Roever,W. P.,和K. Engelhardt,[6] 加德纳,P.H.,C. E. Martin和O. de Moor,An algebraic construction of predicate transformers,Scienceof Computer Programming,22(1994),21[7] 赫米达角一、“Fibrations, logical predicates, and indeterminates,” PhD thesis, The University ofEdinburgh, 1993, published as CST–103–93, also asM. Johnson等人/理论计算机科学电子笔记225(2009)2137[8] Hoare,C.,数据表示的正确性证明,Acta Informatica1(1972)271[9] Hoare,C.,“Data[10] 霍尔角A. R.,谓词变换的一些性质,J.ACM25(1978)461[11] 洪塞尔F.的方法,和D. Sannella,Pre-logical relations,[12] 约翰逊,M.,和R. Rosebrugh,基于正式规范的模型查看可更新性。计算机科学讲义2021(2001),534[13] Kelly,G.M.,和A.J. Power,Adjunctions whose counits are coequalizers,and presentations offinitary enriched monads,Journal of Pure and Applied Algebra89(1993),163[14] Kinoshita,Y.,P. 动力MTakeyama和R.Tennent,一个公理化的方法,以二进制逻辑关系与应用程序的数据细化,计算机科学的理论方面[15] Kinoshita,Y.,和A.权力,宽松自然通过丰富,纯粹与应用代数杂志112(
下载后可阅读完整内容,剩余1页未读,立即下载
![.pdf](https://img-home.csdnimg.cn/images/20210720083646.png)
![application/pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)