96网址:http://www.elsevier.nl/locate/entcs/volume67.html20页连续域及其信息系统的逻辑表示Benjam n Ren e Callejas Bedregal1北里奥格兰德联邦大学信息学与应用数学系巴西纳塔尔Ivanosca Andrade da Silva2北里奥格兰德联邦大学信息学与应用数学系巴西纳塔尔摘要在这项工作中,我们将介绍一个用于连续域的尼特信息逻辑,作为连续域逻辑的互补逻辑[BA95,Bed96,BA99,Keg99]。在这里,分析的是连续域的逻辑方面,而不是整个类。为了做到这一点,我们将使用连续域的连续信息系统表示[Hoo 93,Bed96],并通过同构将两种结构联系起来。这种三元组(连续域、同构和连续信息系统)称为连续逻辑系统。从连续逻辑系统中可以定义出满足关系、信息量、模型、理论、逻辑推论、信息量序等概念,并在连续域和连续信息系统的构造子的基础上,分别定义出连续逻辑系统的构造子。最后,我们将从连续逻辑系统中提取出一个连续域逻辑,并基于模型的概念给出这个逻辑的可靠性和完备性结果关键词:域理论,连续信息系统,逻辑系统,模型,因果关系1引言Domain理论研究一类合适的空间,通过求解递归方程得到语义函数,给出1 电子邮件地址:bedregal@dimap.ufrn.br2 电子邮件地址:ivanosca@dimap.ufrn.br2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。97编程语言[Sco82,Gun85]。(代数)域逻辑是Abramsky [Abr 87,Abr 91]为了研究逻辑方面而提出的(一个证明系统)的领域,因为它是用在指称语义的编程语言。然而,代数域不支持一个自然的和一致的拓扑解释的真正的间隔数据类型。然而,连续域对这种数据类型有一个理想的解释。类似的工作斯科特[斯科82]代表具体的代数域,霍夫曼在[胡93]介绍了替代描述连续信息系统连续域。粗略地说,一个连续信息系统是由一组标记、一个连续谓词和一个蕴涵关系组成的三元组。令牌是信息的nite单元,在某种意义上,它们是从观察具有nite工作量的nite时间的程序执行导出的计算的信息。因此,与连续信息系统相关的逻辑语言Scott信息系统与连续信息系统的主要区别在于,从逻辑的观点看,Scott信息系统中的蕴涵关系是一种推论关系[Gab94],即是自反的、单调的和传递的。只要在连续信息系统中,蕴涵关系不满足自反性的性质[Hoo93]。连续信息系统表示法将信息的概念明确化,在这个意义上,域中的每个元素都被视为它所满足的信息的集合。虽然域和信息系统在范畴上是等价的,但信息系统允许我们捕捉域的逻辑方面,在这个意义上,域的属性可以从关于计算属性的命题之间的蕴涵中导出。因此,例如,实区间的连续域被表示为连续信息系统,其基本信息是有理区间。在这项工作中,我们将看到连续域和它们的连续信息系统表示为逻辑系统,这使我们能够探索连续域的元素之间的逻辑关系与从它们的连续信息系统中获得的信息语言。从这个逻辑系统中,我们可以定义几个概念,如:满足关系、信息内容、模型、理论、逻辑结果、信息内容顺序等。这就形成了连续域逻辑[BA95,Bed96,BA99,Keg99]的一个补充逻辑,在连续域逻辑中,分析的是连续域的逻辑方面,而不是整个类。在连续论域和连续信息系统构造子的基础上,我们分别定义了连续逻辑系统的构造子。最后,我们将从连续逻辑系统中提取出一个连续域逻辑,并基于模型的概念给出这个逻辑的可靠性和完备性结果982连续domain自从Scott和Strachey的开创性工作以来,一些数学结构已经被广泛地用作程序语言的指称语义的模型。连续域,基本上是一个连续的格子[Sco72],可能没有顶部元素。连续域允许我们发展区间算术和数值分析的理论[Aci91]。该理论具有构造性和计算性的优点,并将程序设计语言语义学和计算数学理论统一起来。以下是正式的定义。设D= hD; i是偏序集(poset)。非空集如果每个nite子集都有一个上界,或者等价地,9c 2使得c和b c。偏序集D是完备的(for简称cpo),如果每个有向集都有一个上确界或最小上界(用F表示),并且有一个底元素,通常用?表示我们说a比b小得多(用a表示b)如果对于每个有向集使得对于某个x2,b F然后a x。设#x为集合fy2D= y XG. 一个cpo D称为连续的,如果对所有的x2D,集合#x是有向的且x = F#x. A子集BD是如果对于eachx2D,集合#Bx=fy2B=yxg是定向的,且x=F#Bx。一个连续的CpoD,其中每个Ch由一个集合组成(一个集合有一个上界)在D中有一个上确界,称为连续域。连续域D = hD;;的元素x?如果x y意味着x = y,则称i是全的。我们用Tot(D)表示整环D例2.1设I(R)=f[r;s]=r; s2R且rsg[f[1;+1] g是以实数为端点的闭实区间或单纯实区间的集合。在I(R)上定义以下偏序:[r;s]v[t;u]i[r;s]=[1;+1]orr(rRtanduRs):三元组<=hI(R);v;[1;+1]i是连续整环. 与相关联的下面的关系定义为:[r;s][t;u]i[r;s]=[1;+1]orr(rRtanduRs):它的连续域的基是集合I(Q)=f[p;q]=p;q2Q和p