单调递归定义序列的收敛速度与不动点理论的应用

≤理论计算机科学电子笔记120（2005）125-133www.elsevier.com/locate/entcs递归定义序列Branimir Lambov1金砖奥胡斯大学计算机科学系IT-parken，Aabogade 34DK-8200 Aarhus N，Denmark2摘要本文给出了Matiyasevich的一个结果的推广，该结果给出了单调递归定义序列的显式收敛速度。推广的动机是不动点理论的最新发展和搜索证明挖掘领域的应用 它放宽了对单调性的要求，使其形式为xn+1（1 + an）xn + bn，其中参数序列必须在和上有界，并且还提供了处理计算错误的方法。本文还给出了一个实例结果，证明挖掘的不动点理论的应用，这可以实现的方法在本文中讨论。保留字：单调序列，证明挖掘，可计算极限，不动点理论1介绍在经典数学中，许多有趣的结果都是基于这样一个事实：(1)每一个有界单调实数序列收敛到一个有限极限。不幸的是，这一事实没有得到建设性的反映，即。没有定理让我们计算序列的收敛速度，这将需要计算极限。此外，如Specker在[8]中所示，可以构造1电子邮件地址：barnie@brics.dk2计算机科学基础研究（www.brics.dk），由丹麦国家研究基金会资助。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.06.039126B. Lambov/Electronic Notes in Theoretical Computer Science 120（2005）125≤ ≤≤.Σ即可计算单调序列，其极限是不可计算的，因此在某些情况下甚至不可能找到如果我们有兴趣从使用这个事实的证明中提取有效的数据，这就带来了一个重大的问题。由于我们没有一个建设性的类比，我们通常无法继续应用它，隐藏在证明中的定量信息可能因此看起来难以接近。有时可以使用收敛性陈述的（建设性的）弱化版本来绕过这个问题，比如它的Herbrand标准形式（HNF）：（二）<$k ∈ N <$g：N → N <$n（g（n）≥ n → |x n− x g（n）|≤ 2 −k）。这种修改不足以允许Specker示例，我们甚至有一个解决方案的一般定理的形式，一个功能（为u xixi+1 v所有i）（三）H（u，v，k，g，x）<$µi≤（v−u）2kgi（0） x0：通过f的连续性，在x0和v之间存在一个不动点，然后序列单调增加，并且从上到下以该不动点4为界，因此通过（1）它收敛;• f（x0） α（k）（am2−k），i=0时∞0≤bn，bi≤B∈R，nk∈m >β（k）（bm2<−k）.i=0时0≤cn，km> γ（k）（cm<2−k）对于某些A、α、B、β和γ。设d =（x0+ B）eA和F在[0，d]上以模ω一致连续，即k. ，xr−1∈[0，d]<$y0，y1， . . yr−1∈[0，d]（九）r−1i=0时|2− ω（k）→|F<（x 0，x 1，.|F(x0,x1, . . . xr−1）−F（y0，y1， . . yr−1）|<2−kΩ并且具有F（x，x，... ，x）= 0，具有一致的唯一性模η，即（十）然后（十一）哪里k∈[0，d]. （|F（x，x， . . . x）的|<2−η（k）|F（y，y， . . . 年）的|<2−η（k））→|x-y|<2−kΩ。k|2 − k Ω，|<2 −kΣ,φ（k）=p（r−1）+max（α（q），β（q），γ（η（k+1）+1））q = θ（k）+ 3 +[log 2（d +1）r|p=[d·2θ（k）<$+ 1θ（k）= max（k，ω（η（k+1）+1））证据引理3.1确保序列（xn）的所有成员都在[0，d]内，因此我们可以安全地使用模ω和η，并自由地将d替换为任何xn的上界。B. Lambov/Electronic Notes in Theoretical Computer Science 120（2005）125131I+J（r−1）我我我我0使用α和β，我们可以确保，从某个点开始，序列（xn）在一组r个连续元素中的任何增长都是严格受限的。对于任何i≥max（α（q），β（q））（使用引理3.1，r2q，且ex≤1+ 2x，x≤1），我们有：x−x≤（x+j2−q）ej2−q−x≤（x+j2−q）（1+j2−q+1）−x（十二）对于任何jr。<≤j2−q（2xi+ 1+j2−q+1）（d+1）r2−q+2≤2−θ（k）−1现在我们将证明序列中足够远的元素之间的显著距离必须在另一对元素之间的距离中重复设n和m是自然数，m，n≥max（α（q），β（q），γ（η（k+1）+1）），且xm+（r−1）≥xn+ 2−k。根据它的定义，我们知道θ（k）≥k，因此（12）产生xm−xn=xm+（r−1）−xn−（xm+（r−1）−xm）≥2 −k − 2 −θ（k）−1≥ 2 −k−1。通过F（x，x，.）的根的唯一性（10）， ，x）= 0，我们可以推断|F（xi，xi，... 、x i）|≥2−η（k+1），其中r是rn或m。通过将F的概念（9）应用于F（xi，xi， . . ，xi）和F（xi，xi+1， . . . ，xi+r−1），其中|F(xi,xi, . . . ，xi）−F（xi，xi+1， . . ，xi+r−1）| ≥2−η（k+1）−ci≥2−η（k+1）− 2−（η（k+1）+1）≥2−（η（k+1）+1）我们知道存在j∈{1，2， . . . ，r−1}suchthat|xi−xi+j|≥2−ω（η（k+1）+1）≥2−θ（k）。因为（12）的序列不可能是由nxi和xi+j组成的，因此，(13)xi−xi+j≥2−θ（k）。现在对xm，xn+（r−1）之间的距离必须至少为2−k（为了简单起见，我们只写i=n的情况，i=m的情况产生相同的结果）：xm−xn+（r−1）≥（xm−xm+（r−1））+（xm+（r−1）−xn）+（xn−xn+r−1）>−2−θ（k）−1+ 2−k+（xi−xi+j+xi+j−xi+r−1）>−2−θ（k）−1+ 2 −k+ 2 −θ（k）−2 −θ（k）−1(14)=2 −k。保持相同的距离如果m−（r−1）继续大于或等于max（α（q），β（q），γ（η（k+ 1）+ 1）），这个论点可以再次应用。为了继续证明的主要部分，固定一个任意的k，让n0=φ（k），m0∈N。 Suppose|xm0+n0−xn|≥2−。在下面的例子中，KC ase1. xm0+n0≥xn0+2−。K设n i+1= n i+（r− 1）且m i+1= m i− 2（r− 1）。 通过归纳，使用（14）与n=ni，m=ni+mi−（r−1）作为归纳步骤，我们知道至少对于i≤ [m0<$我132B. Lambov/Electronic Notes in Theoretical Computer Science 120（2005）125我我我 我我我我我我我我 我000Q（因为ni+mi保持大于或等于max（α（q），β（q），γ（η（k+1）+1）xmi+ni ≥xni + 2 −k。特别地，对于s =[m0 因此，我们有0≤ms r和xn+m-xn≥2−k，即矛盾（12）。2（r−1）s s sC ASE2. xm0+n0≤xn0−2−。K设ni+1：=ni−（r− 1）和mi+1：=mi+2（r−1）。由于n0= max（α（q），β（q），γ（η（k+ 1）+ 1））+p（r−1），我们可以应用（14）p次，取n=mi+ni和m=ni−（r−1）。因此，对于任何i≤p，我们有xn≥xm+n+ 2−k，而且（使用（13）），对于每次迭代，存在不同的索引li∈{ni-（r-1），ni+mi}，其中序列的值显著下降，即哪里xli -xl+j≥2−θ（k）对于一些JR。 (note两个点不可能重合，因为两个点至少（r−1）-apart）我们将证明这些液滴是累积的，而我们对p的选择使得这是不可能的。我们将定义两个额外的序列来测量（xn）可以增长多大，以及它与实数（xn）之间的差异。令ty0=x0，yn+1=（1+an）yn+bn，zn=yn−xn。对于所有n，我们可以简单地得出xn≤yn≤yn+1和zn+1≥（1+an）yn+bn−（1+an）xn−bn≥zn。Lemma3.1c可以用于（yn）作为满足（6）的序列的实例，具有相同的常数，因此（yn）(and（）（。对于每个ip，存在jr，使得 d，这是个矛盾在任何情况下，假设|x n−x m+n|≥ 2 −k导致与我们的n0的选择，因此（因为k和m0是任意的）k|2 − k Ω。|<2 −kΣ.我我我我B. Lambov/Electronic Notes in Theoretical Computer Science 120（2005）1251334结论和今后的工作本文利用Matiyasevich的一种方法，探讨了从非有效数学证明中恢复有效信息的问题我们已经给出了它的一个应用和一个由不动点理论的最新发展所激发的推广作为未来的工作范围内的主题，我们有兴趣在非平凡的应用程序的广义结果。另一方面，根据Kohlenbach在[3]中的一个结果，在非常一般的条件下，甚至从根的唯一性的高度非线性证明中，也可以提取出本文所提出的处理的主要前提条件，即唯一性模我们感兴趣的是找到Matiyasevich的原始定理或这里给出的推广结果的应用，其中找到模是不平凡的，但可以使用[3]中的定理来实现引用[1] Hillam，B.，Krasnoselski定理在实直线上的推广1974年至1975年，《杂志》第47-48167-168.[2] 科伦巴赫大学，在分析中分析证据。在：W.Hodges，M.海兰角Steinhorn，J. Truss，编辑，逻辑：从基础到应用。European Logic Colloquium（Keele 1993），pp. 225-260，牛津大学出版社（1996）[3] K ohlenbach，U. ，Escherichectivemoldulifrminectiveuniquenessprofs。关于Chebyche逼近的新证明.Annals of Pure and Applied Logic 64（1993）pp. 27比94[4] 科伦巴赫大学，Borwein-Reich-Shafrir定理的一个定量版本。数字。功能Anal. 和Optimiz。22（2001），pp.641-656[5] 科伦巴赫大学，Lambov，B.， 渐近拟非扩张映象迭代的界。 发表于：《不动点理论与应用国际会议论文集》，巴伦西亚，2003年，横滨出版社。[6] Matiyasevich ， Y.五 、 单 调 序 列 收 敛 的 一 个 充 分 条 件 。 Zapiski Nauchnykh Seminarov LeningradskovoOtteleniya Matematicheskogo Instituta imeni V.A. 斯 泰 克 洛 娃 Akademii Nauk SSSR ， Vol. 20（1971），pp. 97-103.英文翻译J. Sov. Math.1，No.1（1973），pp. 59-63[7] Schu，J.，渐近非扩张映象不动点的迭代。J. 数学Anal. Appl.158（1991），pp. 407-413[8] Specker， E. ， NichtkonstruktivbeweisbareSaützederAnalysis. TheJourn alofSy mbolicL ogic， 14（ 3）（1949），pp. 145-158[9] Qihou，L.， 渐近拟非扩张映象的迭代序列。 J. 数学Anal. Appl. 259（2001），pp. 1-7号。[10] Qihou，L.，一致凸Banach空间中渐近拟非扩张映象具误差项的迭代序列。J. Math. Anal. Appl. 266（2002），pp. 468-471.[11] 徐，Y.，非线性强增生算子方程的带误差的Ishikawa和Mann迭代程序。J. 数学Anal. Appl. 224（1998），pp.91比101