没有合适的资源?快使用搜索试试~ 我知道了~
连续域环境中证明实数计算的非序列性
理论计算机科学电子笔记173(2007)41-46www.elsevier.com/locate/entcs论实数计算域模型的非序列性托马斯的一个nberr'e1英国伯明翰大学计算机科学学院摘要因此,HofmannanandStreichen ehemenvirent中的rea l-numbercm up论证的一部分涉及到证明加法运算不是Vuillemin顺序的。我们将其推广到所有连续域环境中的实线。 导致这种现象的实数线的关键属性是 它的连通性。我们证明了任何连通拓扑空间的任何连续域环境都表现出类似的平行效应。保留字: Domain理论,实数计算,序列性,连通性1引言Escardo',Hofman nnanddStreicher[4]通过其众所周知的区间域环境(例如, [2]和[3]。[4]的主要结论是,通过区间域对实数进行的等式运算是极其严格的,以至于甚至连加法之类的基本运算都不是顺序的。[4]中的论证有两个主要步骤:(1)实数上的加法运算到区间域上的扩展不是Vuillemin序列的(见下面的定义2.1),(2)在顺序编程语言的自然假设下,弱parallel-or运算符可以定义为任何不能成为Vuillemin序列的函数。在一类感兴趣的域中,如果该域是实数线的任意域环境,则可能是区间域的限制,或者这可能是区间域的限制。 本文的一个主要结果是,第一步推广到任何连续域环境的真实1 电子邮件:T. cs.bham.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2007.02.02642T. Anberrée/Electronic Notes in Theoretical Computer Science 173(2007)41(定理3.4及其推论)。因此,我们可以说这不是区间域的限制,而是实数线的固有性质。本文件的第二个贡献是确定这一属性。我们证明了任何连通拓扑空间的任何连续域环境都具有平行效应。更准确地说,我们证明了只有非常有限的二元操作在这样的空间可以扩展到Vuillemin连续域环境中的顺序操作(定理3.3)。2预赛我们假设对拓扑学和Domain理论有一定的了解[1],包括dcpo(有向完备偏序集),连续Domain,Scott拓扑和(Scott)连续函数的概念。偏序集的元素x的上集记为↑x。给定函数f:D×E→F和元素d0∈D,e0∈E,我们用f(−,e0)表示将任意d映射到f(d,e0)的函数D→F,用f(d0,−)表示将任意e映射到f(d0,e)的函数E→F所谓实数线,我们指的是由开区间生成的具有通常拓扑的实数集。下面的定义取自[4]。直觉是,如果一个二元函数是顺序的,那么它必须首先查看它的一个参数,如果这个参数没有进展,那么函数本身的值也不能取得任何进展。定义2.1定义域的连续函数f:D×E→F称为Vuillemin序列,如果对D中的任意d和E中的任意e,(i) f(d,eJ)=f(d,e)对于所有eJ±e,或(ii) f(DJ,e)=f(d,e)对所有DJ±d.等价地,函数f(−,e)在↑d处是常数,或者函数f(d,−)在↑e处是常数。定义2.2拓扑空间X的域环境是包含X作为相对Scott拓扑中的子空间的连续域E注意,我们定义2.3如果E是拓扑空间X的域环境,我们说一个运算X×X→X是Vuillemin序列的,如果它至少有一个Vuillemin序列扩张E×E→E。3连通空间我们证明了对于连通拓扑空间的任何连续Domain环境,只有非常有限的二元运算可以是Vuillemin序列的。我们把论点分成两步。引理3.1T. Anberrée/Electronic Notes in Theoretical Computer Science 173(2007)4143但其结论的第(i)项与连通性密切相关,因为它在引理3.2中变得明显。引理3.1如果f:D×E→F是连续域上的Vuillemin序列函数,R是E的子空间,则对D中的每个d,(i) f(d,−)在R的某个开覆盖的每个开集上是常数,或者(ii) f(−,r)在↑ d处是常数,对于R中的某个r。证据假设(2)不成立。为了证明(i),设r在R中,Y是远低于r的元素的集合。因为f(−,r)在↑d处不是常数,所以在↑d中有d0和d1,使得f(d0,r)/= f(d1,r).(一)由于f是Scott连续的,r是有向集Y的上确界,我们有两.f(d0,r)=.f(d0,y)和f(d1,r)=f(d1,y).(二)y∈ Y y∈ Y从断言(1)和(2),我们可以得出结论,对于Y中的某个y0,f(d0,y0)/=f(d1,y0)..否则,由于f的连续性,就有y∈Yf(d0,y)=y∈Yf(d1,y),因此f(d0,r)=f(d1,r),与(1)相矛盾。换句话说,函数f(−,y0)在↑d处不是常数。因此,由于f是Vuillemin序列,函数f(d,−)是在 ↑y0 处 不 变 。 因 为 ↑y0 是 r 的 邻 域 , 所 以 有 一 个 开 子 集 Urof↑y0suchatUrhasaamember。集合{Ur}r∈R是R的一个非零覆盖,使得f(d,−)在每个Ur处都是常数.Q回想一下,拓扑空间R称为连通的,如果当两个开集V和W使得V<$W=R且V<$W=R时,其中一个集V和W是空的。等价地,R是连通的,如果R和R是唯一的闭序圈(闭的和开的)。 连通空间的典型例子是实区间,包括R自己我们将使用下面引理3.2(iii)给出的特征,这是众所周知的特征(ii)的重新表述。引理3.2对于任何非空空间R,下列等式等价:(i) R连接。(ii) 任何从R到离散空间的连续函数都是常数。(iii) 任何定义在R上的集合论函数,如果在R的某个开覆盖的每个开集上都是常数,那么它就是常数。虽然这个结果是标准的,但为了完整起见,我们还是包括了一个证明证据㈠=㈡。假设X是一个离散空间,f:R→X是连续的。L etr∈R。集合f−1({f(r)})不是简单的(becauseitcontainsr),并且是闭合的(因为{f(r)}是闭合的,并且f是连续的),因此它是整个空间R(因为R是连通的),这意味着f是常数。44T. Anberrée/Electronic Notes in Theoretical Computer Science 173(2007)41(ii)=(iii)。设f:R→X是定义在R上的集合论函数,在R的某个开覆盖{Ui}的每个开集上为常数。赋予X离散拓扑。 那么f是连续的,因为单元素构成X的基,并且对于任意一个基的元素{x},集合f−1({x})是一个单元素集合的集合,即那些直接像是{x}的U i。所以,由(ii),f是常数。(iii)=(i)。如果U是R中的闭叉,则U和它的补数形成R的开覆盖,并且通过(iii),U的特征函数必须是常数,所以U必须是R或R。Q下面是引理3.1和3.2的直接结果。引理3.3如果f:D×E→F是连续域上的Vuillemin序列函数,R是E的连通子空间,则对任意d∈D,(i) 函数f(d,−)在R处是常数,或者(ii) 函数f(−,r)对于某个r∈ R在↑ d处是常数。我们说一个函数在一点是局部常数,如果它在该点的给定性质p和一个点y,我们说p(yJ)对某个尽可能接近y的yJ成立,如果对y的每个邻域V都有yJ使得p(yJ)成立。回想一下,一个空间是局部连通的,如果每个点都有一个连通集的邻域基。定理3.4若X是局部连通空间,且函数g:X×X→X是关于某个连续区域环境的Vuillemin序列,则对X中的任意x和y,(i) 函数g(x,-)在y处是局部常数,或者(ii) 函数g(-,yJ)在x处是局部常数,对于任意接近y的y j。证据设E是X的整环环境,f:E×E→E是g的Vuillemin序列扩张. 设x和y在X中,并假设(ii)不成立。 这这意味着对于y的某个邻域V和所有yJ∈V,函数g(−,yJ)在x处不是局部常数,因此,对于x以下的每一个d,它的扩张f(−,yJ)在↑d处不是常数。通过局部连通性,我们可以假设V是连通的,并且,通过引理3.3,当R=V时,我们得出结论:对于x的每一个d路,函数f(d,−)在V处是常数。因此,通过f的连续性,函数f(x,−)以及g(x,−)在V处是常数,即(i)持有。Q正如在引言中所讨论的,在[4]中表明,当E是区间域,X是通过单点映射嵌入Ex→ {x},不存在扩充加法运算的Vuillemin序列映射E×E→E.我们的主要结果是,这适用于所有域环境和大量的操作。推论3.5加法,乘法,最大值和最小值不能是Vuillemin顺序的,对于任何连续域环境为实数行。T. Anberrée/Electronic Notes in Theoretical Computer Science 173(2007)4145注意定理3.4中的条件(ii)例如,设X为实数直线,定义g为g(x,y)= max(|X|,y)。对于除0以外的所有y,函数g(−,y)在0处是局部常数。 因此,对于x= 0和y= 0,函数g满足条件(ii)。但是函数g(−,0)在0处不是局部常数。然而,这个例子不是Vuillemin顺序的(考虑到x=y= 1)。4可能的概括在引理3.1的证明中,只要跳过Y的定义,就可以得到下面这个稍微更一般的引理的证明。引理4.1设f:D×E→F是dcpos上的Vuillemin序列函数,R是E的子集.假设对R中的每个r,存在E的有向子集Y,使得r是Y的上确界,并且对Y中的每个y,上集↑y是r的邻域。然后,对于D中的每个d,(i) f(d,−)在R的某个开覆盖的每个开集上是常数,或者(ii) f(−,r)在↑ d处是常数,对于R中的某个r。一个例子,其中这种推广是感兴趣的是一个特定的商的域3∞,其中3∞是一组有限和无限序列的数字-1,0或 1,在prefix命令中。3∞中的最大元素,即无限序列,Σ在[-1,1]区间内通过映射s→西岛i≥02i+1对于3∞中的任何s,s以上的实数集是一个区间。我们定义了一个等价关系,在3∞上,通过规定s≠sJ当且仅当s和sJ定义相同的区间。商3∞/∞是一个不连续的dcpo。其实很容易为了验证,虽然每个最大元素都是元素的有向连接,在它之下,一个非最大元素然而,引理4.1允许我们立即将定理3.3和定理3.4用相同的证明扩展到R嵌入到3 ∞/min。这不是太难检查这个dcpo是拟连续的[5,p。#22626;,很自然地要问我们的结果是否推广到这样的DCPO。另一类一个可能要考虑的域是拓扑域的范畴[6]。这是留给未来的工作。致谢。马汀·埃斯卡·德·波塞德把这些问题告诉了我,然后我们就走了,Achim Jung和Steve Vickers对本文的前几个版本给出了详细的反馈。引用[1] S. Abramsky和A.俊作。域理论In S. Abramsky,D. M. Gabbay和T.S.E. Maibaum,编辑,计算机科学中的逻辑手册,第3卷,第1-168页。 Clarendon Press,1994.46T. Anberrée/Electronic Notes in Theoretical Computer Science 173(2007)41[2] A. Edal atanddM. H. 是的。 IntegrationinR eal PCF(扩展为b s tract)。 在1996年第11届IEEE计算机科学逻辑年会的第382-393页上发表。[3] M. 是的。 PCFextendddwithelnumbers:一种用于高精度数字计算的并行应用程序。伦敦大学帝国学院计算机系博士论文,1996年。[4] M.是的,先生。 霍夫曼 和T 。 我 是 一 个 很 好 的 人 。由于实 数计 算的 整数 维 模型 的非 等同 性,Mathematical Structures in Computer Science,14(6):803[5] G. Gierz,K.H. Hofmann,K. Keimel,J.D.劳森,M。Mislove和D.S. Scott. 连续格和域,数学百科全书及其应用第93卷。剑桥大学出版社,2003年。[6] A.K.辛普森关于拓扑域的一个方便的范畴。《第十三届ALGI研讨会论文集》,京都大学,2003年。
下载后可阅读完整内容,剩余1页未读,立即下载
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.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)