超有限离散化推广到超有限泛函的非标准类型结构及其应用

理论计算机科学电子札记73（2004）141-147www.elsevier.com/locate/entcs实域上连续泛函型结构的非标准刻画达格·诺曼挪威奥斯陆大学数学系摘要我们将实数线的超有限离散化推广到超有限泛函的类型化结构，并证明了遗传近标准泛函对应于从区域理论获得的实数上的关键词：连续泛函，非标准，超有限，全1介绍如果我们把Domain理论看作是通过完备化和拓扑学对有限信息的有序集进行的数学分析，那么另一种工具就是使用非标准分析。看待非标准分析的一种方式是，我们超越了完备化，完备化的每个元素都由几个超有限对象表示，这些超有限对象共享有限对象的代数在非标准分析中，人们处理两个类型结构之间的相互作用，完整的类型结构{Tp（n，R）}n∈N和扩张{Tp（n，R）<$}n∈N. 这种非标准的扩展是初等的，1电子邮件地址：dnormann@math.uio.no1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.08.007142D. Normann / Electronic Notes in Theoretical Computer Science 73（2004）141-×------联系我们一阶逻辑这个事实被称为转移原理。扩展类型结构中的对象称为内部对象。构 造 非 标 准 扩 张 的 一 种 方 法 是 通 过 超 积 ： LetSnbet et e tetofinfiniteesequencesα<$={αn}n∈NofelementsinTp（n，R）。设F是N上的非主超滤子。Ifα<$andβ<$areeelemtsoffSn，weletα<$β<$if{n|αn=βn} ∈F.这是一个等价关系，Tp（n，R）是Sn中的等价类的集合（直到同构）。如果α<$∈Sn+1且β<$∈Sn，则我们将α<$（β<$）denoteλn。αn（βn）。这导致了Tp（n+ 1，R）的应用算子Tp（n，R）≠ R。映射是Tp（n，R）到Tp（n，R）的嵌入，其中x∈是等价的，λn.x的值类，即常数序列。这是对Tp（n，R）n∈N的多类语言的初等嵌入及其应用.我们将用它的特征函数来识别一个集合。因此，我们有例如N和Q分别的非标准版本N和Q 如果x由有限对象组成，则x的元素称为超有限。在域理论中，如果一个元素的信息可以以有限的方式给出，我们通常称之为无限。非标准版本将被称为超有限性。设c0是λn.n的等价类。 则c0∈N<$设c是λn.n的等价类！然后我们也有c∈N<$。 这是我们在构建中使用的数字。让Xn=K2{n！| −(n!)成为标准。然后{d ∈ N}|X∈Fa，b∈H（x德拉克斯ϵb|f（a）−f（b）|<）}的情况是内部的，因为它只能从内部对象定义。因为这个集合包含一个非标准自然数的初始段，所以它必须包含一个标准数n。但这意味着对于某些有理数p和q，{（xn，[p，q]）}<$σfpq。结果是wst（f）是全的。使用权利要求1和归纳假设，很容易证明a）的另一部分。b)设x ∈ Dσ为全。 根据权利要求2，存在一个y ∈ F c，使得x ±σy。根据权利要求1，存在一个f ∈ Hσ使得y <$σf。 让我们来看看。那么wst（a）和wst（b）是一致的，总对象，所以x（wst（a））=x（wst（b））。 因此f（a）和f（b）是等价的，所以f ∈ H ns。权利要求3建立了Hns中的等价类与遗传全对象的等价类之间的1-1-对应。显然，这与应用是相对应的，并且定理得到了证明。Q3讨论考虑这个例子的动机是，基于域外理论的方法，看看实数上类型结构的自然构造，并看看结果是否与标准构造之一相对应现在的问题是，这种非标准分析的使用是否以域理论中可表达的方式提供了对效率的洞察。非标准分析的优势主要在于它为以下结构的使用打开了大门，DDDD. Normann / Electronic Notes in Theoretical Computer Science 73（2004）141-147× → −是分析中结构的替代物，而不是它们的代表。示例是分布和随机过程的非标准方法，参见Albeverio，Fenstad，Høegh-Krohn和Lindstrøm [1]。这些结构的分析往往导致内部算法的一个简单的种类，但有效性是失去了当我们去的标准部分。一个例子是解微分方程。设F：R R[1，1]是连续的.然后我们可以用初值解微分方程yJ= F（x，y），y（0）= 0时，则为零用一个代表G代替F并求解差分方程，k+1k1k k然后0= 0，0 =c）= Y G（c）+c G（c，Y G（c））。K Ky（st（c））=st（YG（c））解得很好，解得很好。然而，映射Φ（G）=YG不是标准的，并且没有办法以连续的方式选择方程的解。实际上，Birkeland和Normann [3]实质上证明了，通过选择F的适当的代表G，方程的所有解都可以作为某个YG的标准部分得到。目前还不清楚这与域理论有何关系，但例如现在可以提出这样的问题：解的集合是否可以表示为某个幂域在R→R上，这可以从非标准方法中提取出来引用[1] Albeverio，S.，J. E.芬斯塔德河Høegh-Krohn和T. Lindstrøm，[2] Bauer ，A. ，M.H.Escard'oandA. Simpson ， Comparingfunctionalparadigmsfororrexactreal-number computation，Lecture Notes in Computer Science 2380（ICALP），pp.488[3] 伯克兰湾和D.Normann，方程yJ= f（y，t）的非标准处理，数学预印本系列，奥斯陆1980 - 17。[4] Escard'o，M. H. 张文，张文，张文，[5] Normann，D.，The continuous functionals of finite types over the reals，Electronic Notesin Theoretical Computer Science35（2000），URL：http://www.elsevier.nl/locate/entcs/volume35.html.[6] Normann，D.，实数上有限型的连续泛函，在K。凯梅尔，G.Q. Zhang， Y. Liu和Y. Chen（eds.）“Domains and Processes”, 103 - 124, Kluwer Academic Publishers,