余代数框架下的精确实数表示与广义上递归方法

理论计算机科学电子笔记164（2006）121-139www.elsevier.com/locate/entcs正合实数的上归纳域与广义上递归Milad Niqui Milad Niqui1，2奈梅亨大学理学院计算与信息科学研究所Toernooiveld 1，6525 ED，奈梅亨，荷兰摘要在这篇文章中，我们提出了一种方法来定义代数结构（场运算）的实数表示的共归纳流。场运算将以两种算法给出（单应性和quadraticalgorithm）thavetooperateonstre amsofM？obiusmaps. 所有的递归函数都是流的余代数上的余代数映射，因此它们将被形式化为一般的余递归函数。我们使用的Coq证明助理共归纳类型的机器，目前的形式化。关键词：上归纳类型，精确实数运算，广义上递归1引言余代数提供了一个合适的语义来处理只有部分观测可用的无限现象无限对象的各种轮回，如实数，标记转移系统，面向对象的模块和动力系统可以在余代数的框架下研究。由于各种原因，实数的情况特别有趣。首先，实数的普遍性和理论上的重要性使它们成为证明余代数框架可表达性的重要候选者。这将为分类可计算的余代数映射铺平道路，这反过来又有助于提升无限对象编程的余代数语义的状态。此外，它使我们能够使用共代数语义的精确实数运算，精度驱动的方法，实数计算，其应用领域的数值计算正在增加。另一方面，实数的特殊性质1 荷兰科学研究组织（NWO）支持的研究。2 电子邮件：M. cs.ru.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.06.008122M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121(such由于需要有一个冗余的表示）一旦翻译成coalge-language给出了有价值的洞察各种概念的共归纳原则和互模拟等价，可以使用的其他地方。对应于实数的最终余代数具有相对简单的结构。在文献中，它们通常表示为列表函数X <$−→1 +A×X或第一个函数X <$−→A×X的最终余代数[29，28]，并通过代数表示为具有A-元素和B-运算函子X<$−→A×X+B×X2的表达式树的最终余代数[23，24]。 然而，succhasimpl e structur e本身并没有捕捉到数学分析的全部力量：人们需要能够为实数的余代数配备代数结构（场运算）和序结构（柯西完备性）。Pavlovi'icandPratt[29]通过定义Cantor空间和Baire空间中的列表函子和流函子，研究了范畴Set中的上实余代数的性质. 然而，通过只刻画连续统的阶类型，它们的构造并没有解决实数的代数性质。Freyd给出了Dedekind实数的另一个刻画（见[20，§D4.7]），即偏序集范畴中的“楔”函子的对角化这一思想是由Escardo和Simps在[15]中提出的，其中ycharacter e是指在Dedekind reals 中有理数的Cauchy完备性，它获得了一个允许类似于原始递归的普适性质。这些特征恢复了实数的一些代数性质，同时依赖拓扑逻辑来实现这一点。在目前的工作中，我们计划实现一个类似的目标：一个实数的coalgebraic视图，其中计算非常接近于精确算术的实际实现。首先，我们通过基于Haskell编程语言的语法给出实数流上的一些算法但这项任务并不容易，主要是由于生产力的问题[11]。生产函数是那些在无限对象上产生可证明的无限输出的函数。从最终煤族的普遍性中得到的基本迭代格式可以用来直接定义大量的标准流函数，但它有其局限性[31]。为了克服这个限制，已经提出了几个更强大的方案，每个方案都包括一个不断扩大的规范类。其中有上递归[16]、值递归过程的对偶[31]、点函子的T-上迭代[21]、分配律的λ-上迭代[2]和双代数T-上迭代[6]。但这些方案有一个共同点：它们都对它们能够处理的规范类施加了某种语法标准;而实数算法的生产力不能从语法上检测。事实上，标准滤波器函数在自然数流上的生产率也是不可判定的（这里P是布尔值M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121123自然数（Natural Number）filter（x：xs）：=.x：filterxsifP（x），过滤器xs否则。通过适当地选择P，人们可以将上述函数的生产率问题简化为数学中的一个开放问题;参见[23，例4.7.6]，P的选择表明，上述函数的生产率等价于是否存在无穷多个孪生素数。因此，似乎提供语法生产力测试不能覆盖无限对象的递归规范的最一般类别。因此，人们必须坚持语义手段，以便能够使用框架的余代数的编程一般，并为编程的实数特别。例如，对于素数上的滤波器的情况，必须（1）考虑素数的个数的数论构造性证明，（2）从这个证明中摘录返回第n个素数的函数κ，（3）使用κ以通过生产力语法测试的方式重写过滤器，即，使用上述语法方案之一[23，§4.7]。用余代数的语言形式化步骤（1）要求人们要么将自己限制在存在某种逻辑或推理概念的范畴内。有几种明确的方法可以实现这一点：一种是在连续性和近似性的证明是内置的类别中工作[26]。另一种更通用的方法是在topos中工作并使用内部逻辑。这与Freyd等人[20，15]采取的方法相似。另一个密切相关的可能性是在一个类型范畴中工作，并在命题和计算对象共存的情况下使用构造性类型理论。通过这种方式，人们可以使用构造类型论的机器来推理和形式化生产力的在本文中，我们采用最后一种方法，即，我们提出了一个coalgebraicformalisation我们的算法在一个版本的建设性的类型理论扩展的co-ductive类型。共归纳类型被添加到类型论中用于处理无限对象[22]。通常，在模型类型论的范畴中，它们被解释为（弱）3最终余代数。弱终结性用于内涵类型理论，其中唯一性不能用归约规则表示。扩展地工作，或者在setoid范畴中（互模拟作为setoid相等），可以公式化唯一性属性[7，p。74]。我们的工作类似于[8，3]中的形式化，其中实数流被形式化为具有代数结构（场运算）的共归纳类型。然而，我们的工作在许多方面是不同的：我们使用更一般的设置Edalat等人[14]同时定义代数运算，+、×、−和除法在一个算法中（二次算法）。因此，我们的方法依赖于形式化的非语法生产功能，我们使用的方法，我们称之为一般corecursion。 这是一个与之相关（但又不同）的问题。3 具有唯一性的最终余代数被丢弃。124M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121Bertot在[4]中提出了一种形式化Eratosthenes筛的方法。此外，我们对单应和二次算法的形式化是迈向Edalat和Potts [14，30，24]的非常强大的规范化算法的形式化的第一步，该算法给出了实数上的所有初等函数。本文中的材料已经在Coq证明助手中实现。我们首先在第2节中介绍Coq中共归纳类型的实现。在第3节中，我们将单应和二次算法作为Haskell类规范。在第4节中，我们提出了这些算法的形式化作为一个coalgebra映射的coalgebra的流，使用一般corecursion方法。在第5节中，我们通过提出进一步研究的一些方向来结束本文在本文中，我们使用了一种松散地基于Coq语法的语法，适合在文章中呈现。形式化的实际代码，包括所有必要的Coq引理的证明，可以在网上找到[25]。2Coq中的共归纳类型Coqproof assistant[9]是一个实现的演算的归纳构造（CIC）的exte ddw ithinductv e tyes。 这是一个不合理的价格，因为Martin-Lofintenin i n i na l ty ype thery。 Co i m i m n e z [ 1 8 ]将C oi nuctiv e typesdd o Coq。它们的实现遵循与CIC中归纳类型相同的哲学，即有一个通用的方案，如果给出了它们的构造函数，并且这些构造函数满足严格的正性条件，则允许形成共归纳类型。 严格正构造函数的定义对于归纳和共归纳类型是相同的，并且类似于单项内函子的定义（即，涉及乘积和指数的内函子 直觉上，构造函数c对于x是严格正的，如果x不出现在c中的→的左边。一 个正式的定义可以在[27]中找到。 这意味着下面的形式是归纳的（分别为）。coinductive）类型I，前提是关键字Inductive（分别）CoInductive），并且所有的ci尊重我。（Co）InductiveI（x1：X1）.（xi：Xi） ：（y1：Y1）.（ym：Ym），s：=|c1: ∀(z11: Z11)...（z1k1：Z1k1），It11.. t1m.|cn: ∀(zn1: Zn1)...（znkn：Znkn），It11.TN M。在这样的声明中，s是一个排序，即，s∈ {Set，Prop，Type}。 此外，x是s（相应地，yis）是通用的（分别是递归的）参数I.例如，可以将流的最终余代数定义为共感应流（A：设置）：设置：=| Cons :A→流A→流A。M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121125请注意，这是一个多态类型，形成了其通用参数的元素流。在定义了一个共归纳类型之后，我们可以将它的居民和函数引入其中（即，最终余代数的元素）。这样的定义是由一个上定点算子给出的。这是一个类似于结构递归的不动点运算符的运算符。当给出一个满足保护性条件的良型定义时，这个算子将引入弱最终余代数的一个元素。该运算符的类型规则由以下判断给出（这里，让我是一个参数为P0，.，Pi）。柯菲克斯法则Γ，f：B<$N：BBx0：X0，.，Xj：Xj，（IP0. .Pi） G（f，B，N）F：B：=N：B根据这个规则，如果f，B和N满足边条件G，则cofixf是类型B的居民，这是一个共归纳定义的类型。 在这种情况下，N是可能包含f的定义的主体。边条件G（f，B，N）被称为Coq保护条件，是另一个句法标准，旨在确保无限对象的生产力。这个条件检查f的声明是否被I的构造函数保护。这意味着f在f体中的每一次出现都应该是f I的一个常数的直接参数。这一结论是由于Gimm mne z [18]和Coquand [ 10 ]的一项较好的工作。G的精确定义可以在[18]中找到。与其他coiteration的语法扩展一样，Coq的guardedness条件限制性太强，以至于不能形式化所有的生产函数。最后，我们提到对应于cofix运算符。 设F=g：B：=N。 然后，共定点展开是遵循规则。match（FP0. Pj）：X，|r0R0|......这是什么？| rk⇒ Rkend ~匹配（N[g←F]P... Pj）：X，|......这是什么？|... | rk⇒ Rkend .因此，只有在对上定点进行案例分析时，才允许对上定点进行扩展。从余代数的观点来看，这种通过构造子和上定点算子来处理余归纳类型的方法然而，以Coq方式表示共归纳类型更接近于惰性函数式编程语言（如Haskell4）的语法，因此对许多应用程序非常有用此外，正如我们在第4节中所展示的，人们可以使用Coq来定义生产函数的一般形式，从而可以构建更复杂的共代数结构。在任何情况下，理论上这不会改变共代数语义，并且共归纳类型仍然可以被解释[4]请注意，在Haskell中，归纳和共归纳类型之间没有区别，所有数据类型都可以被认为是潜在无限的，因此对应于Coq共归纳类型。126M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121C d作为弱最终余代数在CIC的任何范畴模型中（见[1]，其中证明了一个此外，通常的上迭代和上递归方案可以根据cofix算子导出[17]。因此，在本文中，我们使用Coq语言提出了我们的方法，并理解它可以很容易地在CIC5的任何分类模型中转换为标准分类符号。3单应和二次算法：规范在这一节中，我们介绍了在流表示上进行场运算的算法，用于正实数的量化，即，[0，+∞]中的（扩展）实数。该算法类似于Goaly的算法[ 19 ]，用于连续分数的加法和乘法。它们也构成了Edalat和Potts方法的基础，以懒惰的精确实算术[14，30]。在这里，我们使用一种比连分数简单得多的表示法，并且它具有足够的冗余性以确保生产率。事实上，我们可以抽象出我们使用的[−∞，+∞]的数字集和紧致子区间，但这样算法就会变得太高阶。一般情况的处理可以在[23 ， § 5] 中 找 到 。 因 此 ， 出 于 表 示 的 目 的 ， 我 们 考 虑 一 个 固 定 的repreentaing[0，+∞]coni gig i g its，其中h ichih i h ihaMobiusap。莫比乌斯地图是以下形式的地图：ax+Bx<$−→，cx+d其中ea，b，c，d∈Zand−bc/=0。一个Mobiusmap是重新定义ifit将封闭的int erval[0，+∞]映射到i telf。通常情况下，大多数内存都不是由这些系数组成的。对于我们的表示，我们考虑集合DIG ={L，R，M}，并通过DIG ω来表示关于DIG的 序 列 的 集 合。 我们通过一个重新定义的Mobübius映射来创建一个dig it，如下所示。L=[10]，R =[11]，M =[21]。1 1 0 1 1 2DIGω是[0，+∞]具有足够冗余的表示（基于Stern-Brocot树）的事实这意味着存 在 表 示 （ 即 ， 一 个 从 DIGω 到 [0 ， +∞] 的 全 满 映 射 ） ρ 使 得 对 所 有f0f1··· ∈DIGω，我们有{p（f0f1. ）}=∞i=0时Σ去... fi（[0，+ ∞]）.Σ在Whatf ollows中，我们使用μ=abto be arefiningigMüobiusmap。 THE单应算法是给定μ和一个流α∈DIGω的算法输出流δ，使得μ（ρ（α））=ρ（δ）。为了呈现出家庭的形象，算法，我们需要定义一个数字d=2019 -01-2201-01- 2201 - 01-22∈DIG[5]事实上，在本文中，我们不需要CIC中的宇宙，因此，Martin-Léofty理论的简单范畴化模型-suchaMartin-Léofty范畴M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121127化的Abottetal[1]-willsucceed。128M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）1210101e f Gh和μ作为以下谓词包括（μ，d）：= ad21≤ cd11<$dd12≤ bd22<$cd12≤ ad22<$bd21≤dd11。直觉是，我们正在检查包含区间μ（[0，+∞]）d（[0，+∞]），这是两个具有有理端点的区间（考虑+∞ = 1/ 0作为伪分数）。这个谓词使我们能够陈述单应性算法：单应μ（x：xs）：=⎧单应性（L−1μ） （x：xs）如果包括（μ，L），⎪⎨R:homographic(R−1◦μ)(x:xs)elseifIncl(μ,R),M：单应性（M−1 （x：xs）else if Incl（μ，M），我的数学老师很聪明。这里d-1和d-1表示通常的矩阵求逆和矩阵乘积。由这一算法得出的直觉是，有两种方法可以通过对Mobius映射的定义来实现，其中除了第一个映射之外，所有映射都是数字。我们开始通过absorbin g digi ts（新定义的M o？biusmap）将μ推向无限性，并在每个元素都包含hdi n的情况下进行mitting di g its，即，当M？obius映射应用于区间[0，+∞]时，其范围在一个数字的范围内。μdd···~d（d−1μ）dd· · ·ifIncl（μ，d）.对于算法的更正式的语义，请参见[23，§5.6]中给出的正确性的语义证明。为了计算场运算，我们考虑二次映射，（x，y）：=+bx+cy+d、exy+fx+gy+h其中a，b，c，d，e，f，g∈Z，可用其2× 2× 2系数张量表示.一个二次映射是非奇异的，如果所有构成系数张量的六个矩阵都是非奇异的。一个精化二次映射是一个非奇异的二次映射<$使得<$（[0，+∞]，[0，+∞]）<$[0，+∞].在本节的其余部分，我们假设=ab cd是一个精化二次型地图二次算法是一种算法，它给出了n和两个流α，β∈DIGω，输出一个流δ，使得n（ρ（α），ρ（β））=ρ（δ）。该算法使用下面给出的二次映射的发射条件Incl（d，d）：=ed12≤ad22f d12≤bd22gd12≤cd22hd12≤dd22ad21≤ ed11≤ bd21≤ f d11≤ cd21≤ gd11≤ dd21≤ hd11.我们使用不确定性来确定一个Müobiusmapd和一个二次映射p d的共同位置（注意，结果仍然是一个二次映射）。 此外，我们还用φ·1d和φ·2d来M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121129表示构成二次型130M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121120 0 0 1m apandaMo？biusmapy nsideng e Mo？biusmapassst（resp. second）论证。用这个符号，我们可以提出二次算法：二次多项式（x：xs） （y：ys）：=⎧L：二次（L−1 （x：xs）（y：ys）if Incl（x，L），⎪⎨R:quadratic(R−1◦ξ)(x:xs)(y:ys)elseifIncl(ξ,R),M：二次（M−1 （x：xs） （y：ys）else if Incl（m，M），二次（x·x·y）xsy不是她的智慧。该算法背后的直觉与单应性算法相似。单应性和二次算法都是Edalat和Potts[30，23]的归一化算法的基本情况。单应性算法可用于计算实数的线性分数变换，而二次映射可用于二进制场运算（例如取[1 000]，它给出乘法）。也要注意，这里我们关注的是（扩展的）正实数。添加（冗余）符号位非常简单，并且可以在整个实数行上进行计算[30]。4单应和二次算法：通用余递归版本前一节的算法指定流的最终余代数上的态射。将这一具体化转化为范畴语言意味着我们应该确保上域确实是最终余代数，即，算法的结果是无限流。这两种算法都类似于滤波器算法的一般形式（见第1节）。因此，通常的句法模式并不成立。我们需要的是纳入一个范畴对象，它捕捉了结果的有限性的语义这样的证明依赖于这样一个事实，即在算法的每一步，在吸收有限个数字之后，发射条件肯定成立，因此我们输出一个数字[23，引理5.6.10]。我们计划在一个递归函数中捕获它，该函数在每一步都输出下一个数字，生产率的模数。然后，原始算法将在每一步调用此函数以获取下一个数字，同时跟踪应传递给未来步骤的新参数。Bertot [4]利用这个思想给出了在Coq中定义滤波器的一般方法。在本节中，我们将对Bertot方法进行修改，4.1单应算法我们在CIC的分类模型中工作设M（resp.T）是表示Müobiusmaps（resp）的集合的 对 象 。 在 这 个 分 类 中 ， 第 6 页 。 我们 定义 了一 个 余 代 数 映 射 h ：M×DIGω−→DIGω，它对应于[6]它们可以分别被认为是Z4和Z8，忽略了细化和非奇异性质。通过考虑记录（非奇异型），增加非奇异性和精化准则是微不足道的M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121131α，算 法 但 是 h 是 一 个 部 分 函 数 ， 可 能 不 是 在 每 一 点 都 是 有 效 的 。Soinsteadofdefininginghwehalldefine eamap<$：（μ：M）（α：DIGω）.Ph（μ，α）−→其中Ph（μ，α）是谓词（即，Prop类型的术语），其预期含义是单应性算法的规范在应用于μ和α时是有效的。换句话说，它指定了部分函数h的定义域。Ph 的 定 义 是 基 于 生 产 率 的 模 数 。 该 模 是 递 归 函 数 mh ：M×DIGω−→DIG× M×DIGω，其预期含义是mh（μ，α）=d，μJ，αj当且仅当单应μ α~d：单应μJ J其中我们希望这是一个对α进行递归调用的函数，但这是不可能的。原因是α是最终余代数的元素，而在递归方案中，我们需要初始代数的元素换句话说，我们需要用一个归纳定义的参数来适应函数mh的域，该参数将用于递归调用。这种情况类似于部分递归函数或具有非结构递归参数的递归函数的情况。为了在构造类型论中形式化这样的函数，有一种添加归纳域谓词的方法，该方法在[12]中引入并由Bove和Capretta [5]广泛发展。根据这种方法，我们需要定义一个归纳定义的谓词Eh（μ，α），其预期含义是μ和α在mh的域中，这反过来意味着单应算法在应用于μ和α时至少应该发出一个数字。我们定义Eh为下列严格正的Prop值函子F（X）：= Σ（μ：M）（α：DIGω），Incl（μ，L）+（μ：M）（α：DIGω），Incl（μ，R）+（μ：M）（α：DIGω），Incl（μ，R）+（μ：M）（α：DIGω），<$Incl（μ，L）× <$Incl（μ，R）× <$Incl（μ，M）×X（μπ（hdα））（t1α）。在Coq语法中，这将被给出为电感Eh：M→DIGω→Prop：=|EhL: ∀(μ: M)(α: DI Gω),In cl(μ,L)→Ehμα|EhR: ∀(μ: M)(α: DI Gω),In cl(μ,R)→Ehμα|EhM: ∀(μ: M)(α: DI Gω),In cl(μ,M)→Ehμα|Eh ab: ∀(μ: M)(α: DI Gω),¬In cl(μ,L)→¬In cl(μ,R)→¬In cl(μ,M)→Eh（μπ（hdα））（tlα）→Ehμα。这里hd和t1是流余代数的析构子，EhL，EhR，EhM和Ehab是Eh的构造子.这使我们能够定义生产率的模数，即，递归函数mh：<$（μ：M）（α：DIGω）.Eh（μ，α）−→DIG×M×DIGω132M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121如下不动点mh（μ：M）（α：DIGω）（t：Ehμα）{structt}：DIG*（M*DIGω）：= matchIncldec（μ，L）with| left_⇒ ⟨L, ⟨L−1◦ μ, α⟩⟩| 右tlmatchIncldec（μ，R）with| left_R，R−1μ，α| 右TRmatchIncldec（μ，M）with| left_⇒⟨M,⟨M−1◦μ,α⟩⟩| right tm⇒ mh(μ ◦(hd α)) (tl α) (Ehabinv μ α tltrtmt) end结束结束。这里是固定点（struct）是Coq关键字，用于表示递归定义（分别为结构递归调用的递归参数）。此外，在定义的主体中使用了两个术语Incldec和Ehab这两项都可以作为Coq中的引理来证明。第一个引理如下。引理In cldec：（μ：M）（d：DIG），In cl（μ，d）<$In cl（μ，d）.该术语提取谓词Incl的信息性计算内容，该谓词Incl是Prop类型的术语。这是必要的，因为在CIC中，不能通过命题的模式匹配来获得Set类型的元素。因此，我们必须使用：Prop×Prop−→Set--加上它的左和右共投影--将命题转换为一个布尔和，我们可以在这个布尔和上进行模式匹配。因此，上述引理是不可避免的，虽然它的证明是相当平凡的7。第二个引理陈述了Ehab的最后一个构造函数的逆。引理Ehabinv：n（μ：M）（α：DIGω），<$Incl（μ，L）→ <$Incl（μ，R）→ <$Incl（μ，M）→Ehμ α→Eh（μ m（hd α））（t1α）。这个引理可以很容易地证明，因为Ehab是一个归纳类型，因此它的所有规范对象都应该由它的一个构造函数生成注意，在mh中，输出与证明t无关。项t只是作为一种催化剂，允许在所有其他参数都不是归纳的情况下使用递归。因此，我们应该能够证明一个证明无关的结果，为mh。引理mhPI：m（μ：M）（α：DIGω）（t1t2：Ehμα），mhμα t1=mhμα t2。[7]这一证明以及以下所有引理都在Coq中实现，可以在[25]中找到M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121133上述引理的证明基于Eh的相关归纳方案，该方案比从初始性获得的通常归 纳 方 案 更 专 业 ：普 通 归 纳 法 可 以 用 来 证 明 一 个 性 质R ：M→DIGω→Prop，而相关归纳法可用于证明一个性质R：ε（μ：M）（α：DIGω）.Eh（μ，α）→Prop.引理mhPI使我们能够证明mh函数的不动点方程不动点方程实际上是mh定义体的展开;它们将在后面用于证明单应性算法的类似结果。因此，我们在这里提到它们：引理mhL：λ（μ：M）（α：DIGω）（t：Ehμα），在cl（μ，L）→mhμα中t=。引理mhR：m（μ：M）（α：DIGω）（t：Ehμα），。引理mhM：m（μ：M）（α：DIGω）（t：Ehμα），<$Incl（μ，L）→ <$Incl（μ，R）→Incl（μ，M）→mhμα t=<$M，<$M−1<$μ，α<$M。引理mhab：λ（μ：M）（α：DIGω）（t：Ehμα），<$Incl（μ，L）→ <$Incl（μ，R）→ <$Incl（μ，M）→（tJ：Ehμ（hdα）（tlα）），mhμα t=mhμ（hdα）（tlα）tJ.注意，最后一个引理陈述了一个比mh递归定义的第四分支更一般的事实，因为证明义务tJ被抽象了。然而，它的证明与其他三个相似在定义了mh之后，我们在定义Ph之前还需要一个辅助谓词。这个辅助谓词是一个归纳谓词，它确保Eh对mh的任何有限次迭代都成立（这里πij表示j元组的第i次投影电感电流：N→ M→DIGω→Prop：=|Ψh0: ∀(μ: M)(α: DI Gω),Ehμα →Ψh0 μα|ΨhS: ∀(n: N)(μ: M)(α: DIGω)(t: Ehμα),πhn（π23（mhμα t））（π33（mhμα t））→πh（Sn）μα.我们使用上述谓词来定义Ph，这是一个捕获单应性算法的生产性的谓词。此谓词将是具有一个构造函数的归纳类型。电感Ph：M→DIGω→Prop：=|Ph ab: ∀(μ: M)(α: DI Gω),(∀(n: N),Ψh(Sn)μα)→Phμα.这种类型的唯一构造器确保在每次发射之后（在使用Eh之前发生），新的Mo？biusapp adat e homo grahi c al t e u s a p a d a t e homo l teus a t et e h新的发射。这一事实隐含在以下两个性质中，这两个性质是定义单应算法所需要的。第一个引理陈述了Ph和Eh之间的关系：134M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121引理PhEh：φ（μ：M）（α：DIGω），Phμα →Ehμα.第二个引理与mh和Ph有关，并表明Ph确实传递给未来的参数。引理mhPh：π（μ：M）（α：DIGω）（t：Ehμα），设μJ：=π23（mhμ α t），设αJ：=π33（mhμα t）在Phμα →PhμJαJ中.上述两个引理的证明都是基于逆的构造函数，即下面的两个引理。引理h0inv：（n：N）（μ：M）（α：DI Gω），hnμα →Ehnμα.引理hSinv：（n：N）（μ：M）（α：DIGω）（t：Ehμα），π h（Sn）μ α → π hn（π23（mhμ α t））（π33（mhμ α t））.引理h0inv和h Sinv又是我们在上面作为mhPI陈述的mh的最 后 ， 我 们 准 备 好 将 单 应 算 法 定 义 为 函 数 h<$ ：M （ μ ： M ） （ α ：DIGω）.Ph（μ，α）−→DIGωthaccomm odatefi ts自身的生产力作为其参数之一。这里CoFixpoint表示我们正在使用cofix规则（参见第2节）。CoFixpointh<$（μ：M）（α：DIGω）（p：Phμα）：DIGω：=π13（mhμ α（PhEhμ α p））（h<$ π23（mhμ α（PhEhμ α p））π33（mhμ α（PhEhμ α p））（mhPhμα（PhEhμα p）p））。这个定义通过了Coq的警戒条件。因此，我们通过改变职能领域和增加举证义务来解决生产力问题。接下来的两个步骤将确定该homom ograhi c algorithm的性能。在这一点上，我们需要在流的最终余代数上使用一个扩展等式，这也是一个互模拟等式。在这里，我们对DIGω而且我也不想让你知道。CoInductiveω=：DIGω→DIGω→Prop：=|∼=c: ∀(α1α2: DIGω),hdα1=hdα2→tlα1∼=tlα2→α1∼=α2.不是只有这样，才能解决问题=有一个简单的关系。这是一个等价关系的证明可以在C o q的标准库中找到[9]。更进一步，Giméménéz表明了它是一个简单的等式，并导出了通常的共归纳原理[18，§4.2]。M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121135Weuse=toprov e anextens iona l pro oofirrelevannc e forh？ 该定理的证明使用了模函数的不相关性mhPI。引理h<$EPI：（μμJ：M）（ααJ：DIGω）（p：Phμα）（pJ：PhμJαJ），μ=μJ→α=αJ→h<$μα p<$=h<$μJαJpJ。随后，我们使用上面的引理和mh的不动点方程来证明h We我们称之为单应算法的不动点方程，因为它们可以被认为是递归函数的不动点方程的对偶引理h<$L：P（μ：M）（α：DIGω）（p：Phμα），Incl（μ，L）→h<$μαp=ConsL（h<$（L−1 <$μ）α）。引理h<$R：n（μ：M）（α：DIGω）（p：Phμα），<$Incl（μ，L）→Incl（μ，R）→h<$μαp=ConsR（h<$（R−1<$μ）α）。引理h<$M：（μ：M）（α：DIGω）（p：Phμα），<$Incl（μ，L）→ <$Incl（μ，R）→Incl（μ，M）→<$hμαp<$=ConsM（h<$（M−1<$μ）α）。引理h<$ab：（μ：M）（α：DIGω）（p：Phμα），<$Incl（μ，L）→ <$Incl（μ，R）→ <$Incl（μ，M）→（pJ：Phμμαp=h<$μπ（hdα）（tlα）pJ.该算法是对第3节的具体化，实际上是单应性算法的形式化。当然，我们只是把单应算法的形式化处理为一个生产性的余代数映射，而不是它的正确性。事实上，上述算法（不对μ施加任何条件）对于非精化或奇异的Müobiusmaps是无效的。 这意味着必须对这两个方面进行改进，以减少生产率和正确性方面的问题。这与一般递归的Bove-Capretta方法[ 5 ]中的终止性为了证明正确性，我们需要定义一个合适的语义（例如使用另一个实数模型），并证明上述算法的结果等于M？obiusmap在reanumbers的定义域中的有效性。 这是作者正在进行的项目，并将在未来的工作中提出。4.2二次算法在二次算法的情况下，我们遵循相同的方法，我们用于单应算法。我们首先定义模函数定义域的初始代数。电感Eq：T→DIGω→DIGω→Prop：=|EqL: ∀(ξ: T)(α β: DI Gω),In cl(ξ,L)→Eqξα β|EqR: ∀(ξ: T)(α β: DI Gω),In cl(ξ,R)→Eqξα β|EqM: ∀(ξ: T)(α β: DI Gω),In cl(ξ,M)→Eqξα β136M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121|Eqab: ∀(ξ: T)(α β: DI Gω),¬In cl(ξ,L)→¬In cl(ξ,R)→¬In cl(ξ,M)→Eq（n·1（hdα））·2（hdβ）（tlα）（tlβ）→Eq<$α β。利用这一点，我们通过对上述类型的项进行结构递归来定义模函数。 注意，在这种情况下，模函数mq返回四元组由发射的数字组成的二次映射，新的二次映射传递给二次算法的延拓和两个数字流的余数（未被吸收的部分）。不动点mq（t：T）（αβ：DIGω）（t：Eq<$αβ）{structt}：DIG*（T*（DIGω*DIGω））：=matchIncldec（L，L）with| left_L，L−1，α，β| 右tlmatchIncldec（R，R）with| left_L，R−1，α，β| 右TRmatchIncldec（m，M）with| left_⇒⟨L,⟨M−1◦ξ,⟨α,β⟩⟩⟩| right tm⇒ mq(ξ ·1 (hd α)) ·2 (hd β) (tl α) (tl β)（Eqabinvα β tltrtmt）端结束结束。这里Eqabinv是归纳类型Eq的最后一个构造函数的逆（参见。Ehabinv forhomographic algorithm）。此外，我们必须证明证明无关性和mq的不动点方程。为了简洁起见，我们在这里不提他们，但他们的陈述和证明可以在[25]中找到接下来，我们定义归纳谓词q，它确保了Eq对mq的有限次迭代的有效性：电感式电容器q：N→ T→DIGω→DIGω→Prop：=|Ψq0: ∀(ξ: T)(α β: DI Gω),Eqξα β→Ψq0 ξα β|ΨqS: ∀(n: N)(ξ: T)(α β: DI Gω)(t: Eqξα β),<$qn（π24（mq<$α β t））（π34（mq<$α β t））（π44（mq<$α βt））→<$q（Sn）<$α β.这允许我们将Pq定义为归纳谓词：电感Pq：T→DIGω→DIGω→Prop：=|Pqab: ∀(ξ: T)(α β: DI Gω),(∀(n: N),Ψqnξα β)→Pqξα β.我们再一次需要证明两个引理，它们与Pq和Eq及mq有关.M. Niqui/Electronic Notes in Theoretical Computer Science 164（2006）121137引理PqEq：<$（T：T）（α β：DI Gω），Pq<$αβ→Eq<$αβ. 引理mqPq：n（n：T）（αβ：DIGω）（t：Eq<$αβ），令αJ：=π24（mq<$α β t）in令αJ：=π34（mq<$α β t）in令βJ：=π44（mq<$α βt）inPq<$α β→Pq<$ JαJβJ.最后，我们可以