哥德尔系统T中的函数连续性及其计算性证明

→→→→→→可在www.sciencedirect.com在线获取理论计算机科学电子笔记298（2013）119-141www.elsevier.com/locate/entcsGödel系统T可定义泛函的E-强迫连续性Martín Escardó1英国伯明翰大学计算机科学学院摘要众所周知，哥德尔系统T可定义函数（N N）N是连续的，并且它们的限制来自Baire型（NN）到Cantor型（N（2）连续一致。 We o bought一个新的、相对简短的、独立的证明。主要的技术思想是一个具体的概念，不依赖于强制、Kripke语义或sheaves的元素，这似乎与编程中的泛型效应有关。 证明使用了编程语言语义学中的标准技术，例如作为对话、单子和逻辑关系。我们从头开始用内涵马丁-勒夫类型理论（MLTT），用Agda符号来写这个证明。因为MLTT有计算解释，而Agda可以作为一种编程语言，我们可以运行我们的证明来计算T-可定义函数的（一致）连续性的模。关键词：哥德尔1引言这是一个相对较短的，独立的，证明众所周知的事实，即任何函数f：（N→N）→N，是在哥德尔的系统T中定义的是连续的，并且它的限制从Baire型（N N）到Cantor型（N （2）是 一致连续的[15，2]。我们相信这个证明是新的，尽管它与下面讨论的以前的工作有关。主要的技术思想是泛型元素的具体概念，它来自逻辑、计算、构造性数学和编程语言语义学的几个著名思想自然地出现在这里，以一种相对简单、独立、希望有吸引力的方式发展。1 电子邮件：m. cs.bham.ac.uk1571-0661 © 2013由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。http://dx.doi.org/10.1016/j.entcs.2013.09.010120M. Escardó/理论计算机科学电子笔记298（2013）119→⇒→→→⇒→→ → →→其思想是用一个有良好基础的对话树来表示函数f：（N N）N，并从该树中提取关于f的连续性信息。 为了从系统T项t计算这样一棵树：（）表示f，我们使用一个辅助在系统T的解释中，给出了一个函数f_∞：（N_∞→N_∞）→N_∞，其中N_∞是系统T的对话树。将f应用于某个类属序列N然后，获得期望的对话树。我们现在更详细地解释这个想法。在系统T的集合论模型中，基类型σ被解释为自然数的集合N，并且如果类型σ和τ被解释为集合X和Y，则类型στ被解释为所有函数X的集合Y.我们考虑一个辅助模型，它取代了由SETN_（？）作为所有集合的形成功能协调发展的 在该模型中，零常数用N的一个合适的元素n_0表示，后继常数用一个函数N_n→N_n表示，每个迭代组合子用一个函数（X→X）→X→N_n→X表示. 集合N的一个元素是一个well-founded对话树，它描述了一个自然的相对于未指定oracle α的数：NN.内部节点被标记为通过表示对Oracle的查询的自然数，并且具有与可能的答案相对应的可计数的许多分支。每个叶子都用一个自然数标记，代表计算的一个可能结果。这些对话代表Kleene意义上的计算[10]。如果给定一个特定的预言α：N→N，我们可以从任何一个自然数得到一个自然数d∈N通过一个分解函数decode：（N →N）→N→N.原来有一个函数泛型：N→N这可以被认为是一个通用的序列，在这个意义上，对于任何特定的序列α：N →N，Ngeneric）N解码αvN解码αv）N.α也就是说，类属序列编码任何具体序列α，只要序列α本身被用作解码的具体预言这个想法是，将函数泛型应用于对话树在其叶子上添加了一个新的选择层接下来，我们证明，对于任何给定的项t：（）表示函数f：标准解释中的（N N）N和f：直径中的（N<$N<$）N<$。逻辑解释，我们有fα= decodeα（f generic）.通过建立集合论模型与离散模型之间的逻辑关系，证明了这一点。因此，我们可以通过将f应用于M. Escardó/理论计算机科学电子笔记298（2013）119121→→→→→→→→→→类属序列对于一个合适的对话框B，集合N被构造为BN。则常数零的解释是η0，其中η是单子的单位，后继常数的解释是由函数性B succ给出的，原始递归常数的解释是由其标准解释的Kleisli扩展给出单子的对象部分BX由构造函数η：X→BX，B：（N→BX）→N→BX，其中η构造叶子，B构造树B Fn，给定可数个树F和标签n。当X=N时，我们有Bη：NBN，并且类属序列是Bη的Kleisli扩张。因此，类属序列似乎是一种[13]意义上的类属效应请注意，我们的解释是莫吉语义学的按名称调用利用这一点，可以得出，如果函数f：（N→N）→N是某个系统T项t：（N →N）的集合论解释，则它是连续的，并且它对N的限制2是一致连续的，其中2是元素为0的集合，1.一、原因是对话框在无限次查询后产生答案，因为它是有根据的，并且函 数（N）的对话树（ 二）N是因为它是无限的分支。回想一下，连续性意味着，对于任何整数序列α：N有m：N，称为f的连续模在点α上，使得任何序列αj在前m个位置与α一致，都给出相同的结果，即fα=fαJ。一致连续意味着存在m：N，称为f在N 2上的一致连续模，使得任何两个在前m个位置上一致的二进制序列α和αJ给出相同的结果。我们的论证是有建设性的，并且我们在内涵马丁-洛夫类型理论（MLTT）中从头开始编写完整的证明，使用Agda符号[4]，而不使用库。我们这个程序/证明[7]的Agda源文件是用Knuth的精简格式编写的制作这篇文章。阿格达既检查证明，并可以运行他们。请注意，MLTT或者Agda不能证明或反证所有函数（N N）N是连续的，因为它们与经典数学和构造性数学都兼容，如Bishop数学[3]。这里的定理是某些函数（N N）N是连续的：那些可以在系统T中定义的相关工作。通过将函数应用于有效参数来计算连续性信息的想法可以追溯到Longley[11]，他将异常传递给函数。在Bauer和Pret-nar [1]给出的示例中描述了类似的方法。当然，使用计算树的想法是非常古老的，可以追溯到Brouwer [2]的直觉数学，以及Kleene [10]的可计算性理论中的对话形式，其中输入被称为oracle。Howard [9]用运算方法推导出系统T的计算树，依次122M. Escardó/理论计算机科学电子笔记298（2013）119⇒∀∀→ →→∀→ → → → → →→减少一个项，使得每次查询由类型为numerical的自由变量给出的oracle时，创建与oracle给出的可能答案相对应的可计数的许多计算分支Hancock和Setzer使用对话树的变体来描述类型论中的交互式计算[12]（参见[8]）。我们的工作直接受到Coquand和Jaber在类型理论中的强迫工作的启发像霍华德一样，他们通过运算方法推导出计算树。他们扩展了依赖类型理论，为泛型元素添加了一个常数，然后用下标来装饰判断，这些下标在计算过程中跟踪关于泛型元素的近似信息（类似于[15]）。通过这种方式，它们提取连续性信息。他们使用Tait的可计算性方法证明了类型论的这种修改的终止性和可靠性，这在这里表现为我们两个模型之间的逻辑关系。他们还提供了一个Haskell实现的系统T的情况下，作为附录，它使用了一个单子，这是组合的列表单子（非确定性）和状态单子。他们的Haskell程序实现了一个规范化过程，其中包含由monad跟踪的簿记信息，并生成计算树。因为它们在Haskell实现中只考虑了一致连续性，所以这样的树是有限的。 他们将他们的工作描述为Beeson [2]中提出的强迫和连续性的计算解释。不同的是，他们的方法是句法的，而我们的方法是语义的，读者可能会感觉到与评估规范化的类比。请注意，这些参数仅表明可定义函数是连续的。为了得到一个所有函数都是连续的构造性模型，他们使用迭代强迫，这与我们的[16]这是另一个故事。Organization. （2）在Agda中的形式证明。 （3）非正式的、严格的证明。2Martin-Löf型理论中的Agda符号证明2.1阿格达省本小节的目的有两个：（1）开发一个小型的Agda库，用于以下部分，以及（2）简要解释MLTT的Agda符号[4]我们假设基本的知识（内涵）马丁-勒夫型理论和BHK解释的quantifier作为产品和总和。我们如果我们试图成为纯粹主义者，我们将使用W类型，而不是使用Agda关键字data的一些归纳定义。请注意，本文电子版中的彩色文本是Agda代码。所有类型的全域都用Set表示，类型称为集合（这是a universe à la Russell）.产品编号在Agda中表示为。考虑标准组合子的定义（解释）K：{XY：集合}XYXKxy=x：{X Y Z：设置}（XYZ） （XY）XZfg x=f x（g x）M. Escardó/理论计算机科学电子笔记298（2013）119123rec：{X：Set}→（X→X）→X→N→X→≡--→∀→ → →→∀→ → ∀→→∀→ ∀→≡→≡∀→ ∀→≡→≡→≡∀→ ∀→ → ∀→≡→≡集合变量周围的花括号表示这些是隐式参数，当使用verK和k时由Agda推断。 如果阿格达不能唯一地推断出缺失的字母，则必须写为例如。 K<${X}{Y}xy而不是缩写形式K<$xy。以下内容应该是不言自明的：__：{X Y Z：Set}→（Y→Z）→（X→Y）→（X→Z）gf=x→g（f x）dataN：Setwherezero：Nrecsucc：N→Nf xzero=xrecf x（succn）=f（recf x n）Agda有一个终止检查器，可以验证递归是有根据的，因此所有函数都是总数。我们还需要二进制数字、有限列表和有限二叉树的类型：dataN2：Setwhere0 1：N2dataList（X：Set）：Setwhere[]：ListX_：：_：X→列表X→列表XdataTree（X：Set）：Setwhereempty：TreeX分支：X→（N2→TreeX）→TreeX和不是内置的，因此需要定义：数据集{X：Set}（Y：X→Set）：Setwhere_，_：（x：X）（y：Y x）→{X}Y定义说，一个元素的<${X} Y是一对（x，y）与x：X和y：Y X。请注意，逗号不是一个保留符号：我们将其定义为一个二元运算符来构造依赖对。因为如果假设η -定律，Y=（x：X）Y x，并且因为第一个参数是隐式的，我们可以将X Y写成Y或\（x：X）Y x，其中反斜杠与lambda相同。我们将使用反斜杠专门为总和。π0：{X：集合} {Y：X集合}（\（x：X）Y x）Xπ0（x，y）=xπ1：{X：集合} {Y：X 集合}（t：\（x：X）Y x）Y（π0t）π1（x，y）=y单位类型IdX xy被写为xy，其中X是隐式的，并且被归纳地定义为“最小相关关系”：data__{X：Set}：X→X→Setwherere：{x：X}→xx对称：{X：集合}{x y：X}xyyxsymre=re反式：{X：集合}{x y z：X}xyyzxztransre re=recong：{X Y：集合}（f：XY）{x0x1：X}x0x1f x0f x1congfre=recong2：{X Y Z：Set}→（f：X→Y→Z）124M. Escardó/理论计算机科学电子笔记298（2013）119f→→→→≡→→∀→ → →→丛2{x0x1：X}{y0y1：Y}x0x1y0y1f x0y0f x1y1re re=re2.2对话和连续性我们考虑泛函（XY）的计算 Z与对话树 我们使用以下归纳定义类型的（良好建立的）对话树，由三种类型X，Y和Z索引。这些是Y分支树，内部节点用X标记，叶子用Z数据D（X Y Z：设置）：设置其中η：Z→DX Y ZB：（Y→DX Y Z）→X→DX Y Z一个叶子被写为η z，它给出最终的答案z（η将是单子的单位一个森林是一个Y-指标的树族F.给定这样一个森林F和x：X，我们可以构建一个新的树B Fx，其根标记为x，对于每个y：Y都有一个子树Fy。我们可以把x：X想象成一个查询，对于这个查询，一个预言机α给出了一个中间答案y=α x：Y。在这个答案y之后，我们移动到子树Fy，对话以这种方式进行，直到到达具有最终答案的叶子对话：{X Y Z：设置}DX Y Z（XY）Z对话（ηz）α=zdialogue（BFx）α=dialogue（F（αx））α我们说一个函数（X→Y）→Z是雄辩的，如果它是通过某种对话计算雄辩的：{X Y Z：Set}→（（X→Y）→Z）→Set雄辩的f=\d→α→对话dα<$fα这里我们感兴趣的是X=Y=Z=N的情况。把函数α：N看作自然数的序列。这种序列的集合称为Baire空间：Baire：设置Baire=N→N功能BaireN由一种特殊的对话树编码，即BN其中B定义如下：B：设置设置B=DN N我们使用了一种改进的连续性，它比第1节介绍的传统概念提供了更多的信息，其中连续性的模是指数的有限列表，而不是指数的上界。由索引列表确定的一致关系归纳定义如下，其中α[s]αJ表示序列α和αJ在列表s中收集的索引处一致：(i)α[ [] ]αJ，(ii)α i<$αJi→α<$[s]αJ→α<$[i：：s]αJ。我们在Agda中将这个归纳定义写成如下，其中我们将第一个子句的证明命名为[]，将第二个子句的证明命名为：：M. Escardó/理论计算机科学电子笔记298（2013）119125∀→≡∀→∀→∀→ ≡→≡∀→≡→≡→∀→≡→≡∀→≡→≡是，使用与归纳定义类型的列表相同的构造函数名称：data_[_]_{X：Set}：（N→X）→ListN→（N→X）→Setwhere[]：{αα_：：_：<${α α连续：（Baire→N）→Set连续f=（α：Baire）→\（s：ListN）→（α这是一个留给读者的简单练习，通过取列表s的最大值来产生一个阿格达证明，证明这个精炼的连续性概念蕴涵着传统的连续性概念。由对话定义的函数是连续的，因为一个对话在无限次查询之后产生一个答案对话连续性：（d：B N）连续的（对话d）对话连续性（ηn）α=（[]，引理）其中引理：α'α[[]]α引理α对话连续性（BFi）α=（（i：：s），引理）其中IH：（i：N） continuous（dialogue（F（α i）IHi=对话连续性（F（αi））s：列表Ns=π0（IHiα）权利要求0：（α'：Baire）α[ s]α索赔0=π1（IHiα）权利要求1：（α'：Baire）α i α ' i对话（F（α i））α '对话（F（α ' i））α'权利要求1α引理：（α'：Baire）α[i：：s]α引理α这个正式的证明非正式地解释如下。 我们证明了（d：BN）→连续（对话d）在D上的感应。 扩大定义，这相当于，使用Agda符号，d →对于基本情况d=η n，函数dialogue的定义给出了dialogued α =n，因此我们必须证明，对于任何α，\s→我们可以取s=[]，然后我们就完成了，因为n n是自反的。这就是形式证明的第一个等式所说的。因此，请注意，阿格达，根据MLTT，通过还原到正常形式，默默地扩展了定义。对于归纳步骤d=BFi，扩展对话函数的定义，我们需要证明的是，对于任意α，\sJ →归纳假设是 （i：N） 连续（对话（F（α i），它给出， 对于任意i和任意α，\s →使用两个投影π0和π1，我们得到s，并证明126M. Escardó/理论计算机科学电子笔记298（2013）119→→≡→→∀→∀→∀→ →→→∀→ →≡∀→≡→≡∀→ → ∀→≡→→≡→ → → →→<$αJ→ α <$[s] αJ→对话（F（α i））α =对话（F（α i））αJ。因此，我们可以取SJ=i：：s，并且期望的结论保持不变，使用传递性和定义αi<$αJi→α<$[s]αJ来替换equals（使用→α[i：：s]αJ。这相当于证明的第二个等式，其中在引理的证明模式中，我们有r：αi<$αJi和rs：α<$[s]αJ。我们需要下面的技术引理，因为在内涵MLTT中不能证明任何两个函数相等，如果它们逐点相等。这个证明是用相当简洁的形式写的，这关键是连续性的概念请注意，函数可拓性公理（任何两个逐点相等的函数相等）不是假的，而是不可证明或不可证伪的，并且是一致的[14]。连续-伸展：（f g：BaireN）（αfαgα）continuous fcontinuousgcontinuous-extensionalf g t cα=（π0（c α），（πα' r transs（sym（t α））（transs（π 1（c α）α ' r）（t α '）elongent-is-continuous：（f：Baire N）雄辩的f连续的ff（d，e）=continuity-extensional（dialogued）f e（dialogue-continuityd）一致连续性的发展与上述类似，关键的区别是CN中的对话树是有限的：Cantor：SetCantor=N N2C：Set SetC=DNN我们使用统一连续性的一个改进版本（参见。第1节），其中模是指数的有限二叉树，而不是指数的上界。我们可以使用一个索引列表，但是使用树的证明更短，更直接。由指数树定义的一致关系归纳定义如下，其中α[[s]]αJ表示α和αJ在树s中收集的位置上一致：数据[[_]]_{X：Set}：（NX）Tree N（NX）Setwhereempty：{α α分支机构：树{α α→αi<$α我们再次使用与树类型相同的构造函数名称。一致连续：（Cantor→N）→Set一致连续f=n\（s：TreeN）→ n\（α α对话-UC：（d：C N）一致连续（对话d）dialogue-UC（ηn）=（empty，哪里IH：（j：N2） 一致连续（对话（F j））IHj=对话-UC（Fj）s：N2TreeNsj=π0（IHj）声明：j α α'α[[ sj]]α索赔j=π1（IHj）引理：<$α αM. Escardó/理论计算机科学电子笔记298（2013）119127→≡≡→→∀→≡∀→ →→→引理α α事实0：对话（F（αi））α对话（F（αfact0=cong（jdialogue（Fj）α）r事实1：对话（F（α事实1=声明（αUC-伸展：<$（f g：Cantor→N）→（<$（α：Cantor）→fα<$gα）UC-扩展a→l一致连续f→一致连续gf g t（u，c）=（u，（nα α雄辩是UC：（f：CantorN）雄辩f一致连续f雄辩是UCf（d，e）=UC扩展（对话d）f e（对话-UCd）我们通过证明一个雄辩的函数的限制来结束这一节f：Baire→N到Cantor型也是有说服力的。我们首先定义一个从BN到CN的剪枝函数，它实现了限制：嵌入-N2-N：N2N嵌入-N2-N0=零嵌入-N2-N1=succ零embed-C-B：Cantor→Baireembed-C-Bα=embed-N2-NαC限制：（Baire→N）→（Cantor→N）C-限制f=fembed-C-Bprune：BNCNprune（ηn）=ηnprune（BFi）=B（j→prune（F（embed-N2-Nj）i修剪行为：（d：BN）（α：Cantor）对话（pruned）αC-限制（对话d）α修剪行为（ηn）α=reprune-behavior（BFn）α=prune-behavior（F（embed-N2-N（αn）α雄辩的限制：（f：Baire→N）→雄辩的f→雄辩的（C-限制f）功能限制f（d，c）=（pruned，cα→transs（prune行为d α）（c（embed-C-Bα）2.3哥德尔为了简单起见，我们以系统T的原始组合形式工作。 这是不失一般性，因为组合形式和微积分形式都定义了集合论模型的相同元素，这里我们感兴趣的是可定义泛函的连续性。系统T型表达式和术语归纳定义如下：数据类型：设置位置类型__：type→type→typedataT：（σ：type）SetwhereZero ：TSucc：T（时间）Rec：σ）K：n{σ τ：type}→T（σ<$τ<$σ）S：<${ρ σ τ：type}→T（（ρ<$σ<$τ）<$（ρ<$σ）<$ρ<$τ）_·_：<${στ：type}→T（σ<$τ）→Tσ→Tτ在fixr1_中_in fixl1_·_128M. Escardó/理论计算机科学电子笔记298（2013）119¢¢）的方¢¢（1）→（2）（Ⅲ）（三））T可定义的x=\t→<$t）x→⇒（1））（（Ⅲ）（Ⅲ））∀→→（）（）（）请注意，这里有五个常量（或组合子）和一个二元构造函数（应用程序）。还请注意，只能构建类型良好的术语。类型表达式和项的集合论解释由下式给出：Set_：type→Set设置 n）=N设置 στ）=设置σ）→ 设置τ_：{σ：type} T σSet σ零=零RecKS=rec=K=t·）u为不u集合论模型的一个元素称为T可定义的，如果有一个T项表示它：T-可定义的：{σ：type}→Set<$σ）→Set如上所述，在最后一节中证明的主要定理是每个T-可定义函数Baire→N是连续的。这类泛函的系统T型是（）。我们还考虑系统T扩展了一个形式化的预言机Ω：dataTΩ：（σ：type）SetwhereΩ：TΩ（Ω）零：TΩSucc：TΩ（Ω）Rec：σ）K：τ{σ τ：type}→TΩ（σ<$τ<$σ）S：<${ρ σ τ：type}→TΩ（（ρ<$σ<$τ）<$（ρ<$σ）<$ρ<$τ）_·_：τ{στ：type}→TΩ（στ）→TΩσ→TΩτ在标准的集合论解释中，神谕可以被认为是在类型表达式的解释Baire的元素上的自由变量联系人：<$_）Ω零SucccRec=KK）S ’t·）ut' α（u ' α）要将TΩ视为T的扩展，我们需要使用嵌入：嵌入：{σ：type}TσTΩσ嵌入零=零嵌入Succ=Succ嵌入Rec=Rec嵌入K=K嵌入S=Sembed（t·u）=（embedt）·（embedu）’成功=成功）M. Escardó/理论计算机科学电子笔记298（2013）119129→∀→ → →→∀→ →→∀→ →≡→≡∀→2.4系统T的对话解释现在我们考虑用预言机扩展的系统T的辅助解释，以证明原始T可定义函数BaireN是连续的。在替代语义中，类型被解释为对话单子的某些代数的底层对象。基类型被解释为标准解释的自由代数，函数类型被解释为函数集。为了简洁起见，我们将只包括单子定义中我们实际需要的部分。kleisli扩展：{X Y：集合}（XBY） BXBYKleisli扩张f（ηx）=f xkleisli-扩张f（BFi）=B（Bj→kleisli-扩张f（Fj））iB-函子：<${XY：Set}→（X→Y）→BX→PYB-函子f=kleisli-扩张（η∈f）以下两个引理是至关重要的。我们首先交换dialogue函数的两个参数，以获得这样的观点，即从Baire类型的元素中，我们得到一个B-代数BX→X，对于任何X：解码：{X：集合}Baire BX Xdecodeαd=对话d α解码映射对于任何oracleα：Baire都是自然的：BXBg）BY解码αv解码α）vX年。Gdecode-α-is-natural：{XY：Set}（g：XY）（d：BX）（α：Baire）g（decode α d）decodeα（B函子g d）decode-α-is-naturalg（ηx）α=redecode-α-is-naturalg（BFi）α=decode-α-is-naturalg（F（αi））α下图对任意f：X→BY都是可交换的：BXkleisli扩张f）BY解码αv）的情况）解码αvXBYF解码αY。decode-kleisli-extension：{X Y：Set}（f：XBY）（d：BX）（α：Baire）decodeα（f（decode α d））decodeα（kleisli-extensionf d）decode-kleisli-扩张f（ηx）α=redecode-kleisli-扩张f（BFi）α=decode-kleisli-扩张f（F（αi））α系统TΩ型表达式被解释为对话单子的某些代数的底层集合基类型被解释为标准解释的自由代数的基础集合，函数类型被解释为130M. Escardó/理论计算机科学电子笔记298（2013）119→→→→ <$）→ →<$）B-集<$σ<$τ）=B-集<$σ）→B-集<$τ）→∀→≡→→<$）→<$）B<$_）：T{σ：type}→TΩσ→B-集<$σ）函数集，利用代数是指数理想的事实（如果Y是代数的底层对象，那么所有函数X的集合也是Y代表任何X，具有逐点结构）。B-Set_：type→SetB-Set（Ⅲ））=B（Set（Ⅲ））根据单子的代数的正式定义，要证明集合X是代数的基本对象，必须提供一个结构映射B X X。或者，对我们来说更方便的是，我们可以提供一个广义的Kleisli扩张算子，定义如下，其中基本情况只是Kleisli扩张，归纳步骤是逐点扩张：Kleisli扩展：{X：Set} {σ：type}（XB-Set σ）B XB-Set σKleisli扩张{X} {X} =Kleisli扩张Kleisli扩张{X}{στ}=σg d s→Kleisli扩张{X}{τ}（σx→g x s）d有了这个，我们现在可以定义系统TΩ的对话解释。在这种解释下，Baire类型的泛型元素将解释Baire oracle Ω：通用：BNBN类属=kleisli-扩张（Bη）正如第1节所讨论的，泛型元素的关键属性是：BNgeneric）BN解码αvN解码αv）N.α通用图：（α：Baire）（d：B N）α（decode α d） decodeα（generic d）类属图α（ηn）=re一般图α（BFn）=一般图α（F（αn））zero和successor的其他解释是显而易见的：zerozerosucc原始递归组合子的解释再次以一种明显的方式使用了Kleisli扩展：rec'：{σ：type}（B-Set σB-Set σ）B-Set σB NB-Set σrec这是对对话的诠释。请注意，K、S和应用的解释是标准的。这是因为我们将函数类型解释为函数集：<$Ω）=通用BM. Escardó/理论计算机科学电子笔记298（2013）119131（Ⅲ）（三））∀→ ∀→ ∀→¢）（三）（）（）（）（Ⅲ）（2）→∀→ ≡∀→ ≡→∀→ ≡（2）∀→ ≡（2）J）B零=零'BRecBKBS=rec=K=Bt·）u=B不（二）u）这个语义给出了所需的对话树：对话树：T（（））→BN对话树t=B （embedt）·Ω开发的其余部分是对话树函数的正确性的公式化和证明。我们用简单的证明来结束这一节，证明T嵌入到TΩ中保持了标准解释，而且与神谕无关：保存：{σ：type}（t：T σ）（α：Baire）t嵌入t’保存零α=恢复保存成功 α =恢复保存Recα=恢复保存Kα=恢复保存Sα=恢复保存preservation（t·u）α=cong2（nf x→f x）（preservationt α）（preservationuα）2.5将两种模式主要引理是，对于任何项t：TΩ，解码α（Bt）。<$t）αβ<$我们用下面的逻辑关系来证明这一点：R：B {σ：type} →（Baire→Setσ）→B-Setσ→设R{n}n（α：Baire）→nαR{στ}f f（x：Baire→Set σ）（x'：B-集 σ）→R{σ}x x我们需要一个（相当普遍的）技术引理，它用于使用Kleisli扩展算子解释的常数。在我们的例子中，这只是递归组合子。证明是通过类型表达式的归纳，关键依赖于引理decode-kleisli-extension，但在其他方面是常规的：R-kleisli-引理：n（σ：type）（g：N→Baire→Setσ）（g'：N → B-集σ）→（n（k：N）→R（g k）（g→ R（n：Baire→N）（nR-kleisli-引理gg哪里事实0： αdecodeα（g事实0=decode-kleisli-扩展g事实1： α g（nα）αdecodeα（gfact1α=rg（n α）α事实2：αdecodeα（gfact2α=cong（decodeα（g事实3：α g（nα）αdecodeα（g事实3α=transs（事实1α）（事实2α）B成功=成功132M. Escardó/理论计算机科学电子笔记298（2013）119（2）→∀→≡→≡∀→≡→≡∀→ → ∀→ ≡lem→ma→∀→ → ∀→ ≡lem→ma→→ <$）→ → <$）→ B（x：Baire→Set<$σ））（x∀⇒⇒ →¢)≡→→∀→（2）（Ⅲ）⇒ ⇒ ⇒ ⇒¢）（（）（）→ →∀→→R-kleisli引理（στ）g g=yy主要引理的证明是通过项的归纳法，主要依赖于引理generic-diagram（对于项Ω），decode-is-natural（对于项Succ）和R-kleisli-引理（对于项Rec）。项K和S是常规的（但在非正式计算中要正确计算是费力和困难的），应用的归纳步骤也是如此：主引理：<${σ：type}（t：TΩσ）→R不’（Bt）的范围内主引理Ω=引理，其中声明：αn n索赔αn n引理：（n：BaireN）（n'：B N）（α n α decode α n'）α α（nα）decodeα（genericnn nmain-lemmaZero=αremain-lemmaSucc=lemma哪里claim：αn n索赔αn n引理：（n：BaireN）（n'：B N）（α n α decode α n'）αsucc（nα） decodeα（B-函子succnn nmain-lemma{（σ. σ）。是 的。σ}Rec=引理，lemma：n（f：Baire→Setσ→设置σ）（f'：B-集σ→B-Setσ）→R{σ<$σ}f f'R{σ}x x'（n：BaireN）（n'：B N）R{}n n'R{σ}（σ αrec（f α）（x α）（n α））（Kleisli扩张（rec f ' x'）n'）引理f fg： NBaire设置σgkα=rec（f α）（x α）kggrg：（k：N）R（g k）（g ' k）rgzero=0rg（succk）=rf（gk）（g主引理K=xx主引理S=<$f f主引理（t·u）=主引理tu' Bu（main-lemmau）这给出了上面定义的对话树函数的正确性：术语的标准解释由其对话树计算dialogue-tree-correct：（t：T（（）（α：Baire）tαdecodeα（dialogue-treet）dialogue-tree-correcttα=transclaim0claim1其中权利要求0：不α≡（embedt）·Ω’声明0=cong（cong→g α）（保存tα）权利要求1：（embedt）·Ω’claim1=main-lemma（（embedt）·Ω）α预期的结果直接来自于此：M. Escardó/理论计算机科学电子笔记298（2013）119133∀→ →→∀→ →→⇒⇒remod-bottom-obst（t⇒Ìα雄辩定理：（f：Baire→N）→T-可定义f→雄辩f雄辩定理f（t，r）=（dialogue-treet，nα→transs（sym（dialogue-tree-correcttα））（cong（ng→gα）r））推论0：（f：BaireN）T-可定义f连续f推论0f d=雄辩是连续的f（雄辩定理f d）推论1：（f：BaireN）T-可定义f一致连续（C-限制f）推论1f d=雄辩是UC（C-限制f）（雄辩限制f（雄辩定理f d））这结束了完整的，自包含的，MLTT证明在Agda符号，从头开始。因为MLTT证明是程序，我们可以运行这两个推论来计算T-可定义函数的（一致）连续模。由于MLTT本身在ZF（C）中有一个解释，其中类型是经典数学意义上的集合，因此本文的结果在经典数学中也成立。因为本文的LATEX源代码[7]是一个简单的Agda文件，读者人们可以设想这样一个未来，在这个未来，写（建设性的和非建设性的）正式证明比写非正式的、严格的证明更容易，让我们的思想集中在洞察力上。这无疑是一个挑衅性的声明。但是，事实上，这里提出的证明是直接以其正式的形式写出来的，没有一个非正式的草稿，而只是从引言中描述的类属序列的概念开始的一个心理图像，在阿格达的一些基本帮助下完成了例行的步骤。基于战术的系统，例如Coq，提供了更多的帮助，在某些情况下，即使它们最终基于算法，也可以被认为是非常规的。但我们在MLTT或基于可实现性的计算机系统（如NuPrl，Coq，Lego，Agda，Minlog等）中编写此正式证明的主要动机是上面提到的，证明也是一个程序，因此可以用于计算（均匀）连续性的模，而不需要编写基于非正式的，严格证明的单独算法，因为它通常是目前完成的，包括我们自己在以前的工作中。话虽如此，有一个自包含的非正式严格证明是有用的，我们将在下一节中介绍。在此之前，我们通过运行我们的形式构造性证明来结束本节，以便于说明。2.6实验为了说明上述形式证明是构造性的具体意义，我们做了一些实验。这些实验并不意味着表明上面证明的定理的有用性。它们只是表明这些定理确实有具体的计算内容。首先，给定一个项t：（） 我们可以计算它的模（uni- 形式）的连续性。mod-：T（（））→Baire→列表Nmod-tα= π（推论t（t，re）α）mod-blog-obs：0：T（α=0分））））：Baire）现代化（dialogue-continuity（dialogue-treet））α→α≡π0134M. Escardó/理论计算机科学电子笔记298（2013）119→→→ →→→··（三）→¢）≡∀→⇒→（Ⅲ）∀→⇒¢）¢）in fixl0_：：_在fixl1_++__++_：{X：Set}列表X列表X列表X[]++u=u（x：：t）++u=x：：t++u添加：{X：Set}树X列表X空的标签=[]atten（分支x t）=x：：mod-unif：T（（））→ListNmod-unift=π atten（π0（推论1不（t，re）下面的Agda声明允许我们写3而不是succ（succ（succ zero））：{-#BUILTINNATURALN#-}{-#BUILTINZEROzero#-}{-#BUILTINSUCsucc#-}我们面临的一个困难是，在系统T的组合版本因此，我们开始开发一些机器。我：{σ：type} T（σσ）I{σ} =SK（K{σ}{σ}）I-行为：{σ：type}{x：Set σ}IXxI-行为=反应number：NT数字零=零number（succn）=Succ·（numbern）这是我们的第一个例子：t0：T（（））t0=K·（第17号）t0-解释：的t0≡ńα→17t0-interpretation=re-example0example0示例0=mod-modt0（modii）示例0这两个例子的计算结果都是[]。为了提供更复杂的例子，我们使用一个贫乏的上下文G，它允许我们只考虑一个自由变量v，它由I组合子表示五：{G：type} T（GG）v=I应用于这样的上下文相当于S组合子：in fixl1_·__·_：<${Gσ τ：type}→T（G <$σ<$τ）→T（G<$σ）→T（G<$τ）f·x=S·f·x编号：{G}→N→T（G）数字n=K·（数字n）下面是一个示例：t1：T（（））t1=v·（数字17）t1-解释：t1≡ńα→α17M. Escardó/理论计算机科学电子笔记298（2013）119135（Ⅲ）·⇒ ⇒