单价宇宙下的可逆编程语言关系

可在www.sciencedirect.com在线获取理论计算机科学电子笔记336（2018）5-25www.elsevier.com/locate/entcs从可逆程序到单叶宇宙雅克·卡雷特麦克马斯特大学陈朝宏印第安纳大学摘要我们建立了一个可逆的编程语言之间的紧密联系，基于类型同构和一个正式提出的单价宇宙。对应关系的组合子见证类型同构的编程语言中的路径在单价宇宙;和组合子优化的编程语言中的2-路径在单价宇宙。结果表明，一个简单的计算解释的路径和univalence在熟悉的编程结构，只要宇宙的问题是可计算的。保留字：可逆编程、unilance、Agda1引言在2012年的程序设计语言原理研讨会上[1]，有两篇明显不相关的论文：James和Sabry的信息论和Licata和Harper的2维类型理论的规范性。第一篇论文，由计算的物理性质[23，26，29，5，13]的动机，提出了，在其他结果中，一个可逆的语言，其中每个程序都是一个类型同构。第二篇论文，由同伦理论和类型理论之间的联系[31，28]的动机，提出了一个判断公式的内涵依赖类型理论与两次迭代的单位类型。在会上的介绍和随后的讨论中，从直觉和非正式的角度来看，这两份文件显然有很大的相似之处。 将精确的联系形式化是 然而，远非显而易见在这里，我们报告一个正式的关系，适当制定可逆的语言一方面和其他univalent宇宙。在下一节中，我们给出了可逆编程语言的合理重构，重点是https://doi.org/10.1016/j.entcs.2018.03.0131571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。6J. Carette等人/理论计算机科学电子笔记336（2018）5BØ‘B在一个小的“羽毛重量”碎片上节中3.我们回顾了导致单价纤维化的基本同伦类型理论（HoTT）背景，这使我们能够给出“小”单价宇宙的正式介绍节中4我们定义并建立了在第2节中提出的sucaunivalentntsubuniverseU的基本属性[2]。5作为健全和完整的相对于可逆的语言2。秒6讨论了我们的工作的影响，并将其置于现有文献的更广泛的背景下。2可逆编程语言从“信息守恒”的物理原理出发从技术上讲，计算是类型同构，至少在有限类型的情况下，在信息论意义上显然保持了熵[18]。我们用一些例子来说明语言家族的一般性的语法，然后确定一个“轻量级”的语法版本，称为语法2，在我们的正式开发中使用。2.1示例下面的示例假设布尔类型2的表示为不相交并集11，其中左注入表示假，右注入表示真。给定一个任意的a1a型可逆函数f，我们可以构造一个受控于f的可逆函数，它取一对2型a和检查传入布尔值;如果它为假（即，我们在左注入中），函数的行为就像恒等式;否则函数将f应用于第二个参数。然后重新构造传入的布尔值以保持可逆性：控制 ：@a. pa1aqp2ba12baq受控f“2ba1x展开boolbidyp1”1qba1x分布yp1baqp12ba左列显示了在计算过程中访问的类型序列;右列显示了证明相应类型同构的组合子1的名称受控f的代码提供了建设性证据（即，程序、逻辑门或硬件电路）上的自同构：它可以自上而下或自下而上地来回读取下面的not函数是swap`的一个简单提升，它交换了sum类型的左注入和右注入。使用受控构建块，我们可以构建一个受控非（cnot）门和一个受控-受控非门，也被称为to-cannoli门。后一个门是组合布尔电路的通用函数，因此显示1.我们使用的名字希望非常容易记忆;对于组合子的精确定义，请参见参考-论文[18，6，19，20，8]或www.example.com上的随附代码https://git.io/v7wtW。J. Carette等人/理论计算机科学电子笔记336（2018）57ØØ**FF不不Fig. 1. 非3的图形表示语言的表现力不是：212不是cnot：2b212b2cnot到阿利波利：2bp2b2q12bp2b2q到“虽然我们用等式推理的风格编写了控制，但没有用无点组合器的风格编写。这些等价于在序列组合子d 1的项中定义的 x1x′y。正如在任何编程语言的语义观点中的习惯，我们感兴趣的问题是两个程序何时是考虑以下6个类型2的程序：id %1id %2id %3不% 1不%2不% 3：2Ø12id1id% 2id3not2not3这些程序都是同一类型的，但这显然不是“等价”的充分条件延伸思考，即，通过查看所有可能的输入-输出对，很容易验证六个程序分为两类：一类由全部等价于恒等函数的前三个程序组成，另一类由全部等价于布尔否定的其余三个程序组成。在这种情况下，我们可以提供证据（即，类型2的可逆程序，其操纵类型1的较低级可逆程序），所述类型1的较低级可逆程序可以构造性地标识每个等价类中的程序。我们展示了这样一个2级程序，证明了不3等于不3。为了说明，图3中描绘了用于非31.一、 我们鼓励读者将下面的步骤映射到操作8J. Carette等人/理论计算机科学电子笔记336（2018）5阿斯克西在这个图表上，它将逐步简化它：notOpt：not3不2不notOpt“uniti<$d1pswap<$d1ppnotbidqd1pswap<$d1unite<$qqq2xiddassocLefty单位<$d1pswap<$d1pnotbidqqd1pswap<$d1unite<$q2xiddpswap左didqy单位<$d1ppidbnotqd1swap<$qd1pswap<$d1unite<$q2xiddpiddassoc左qyuniti<$d1ppidbnotqd1ppswap<$d1swap<$q d1unite<$ qq2xiddpiddpleftInvdidqqyuniti<$d1ppidbnotqd1pidd1unite<$qq2xiddpiddid Leftqyuniti<$d1ppidbnotqd1unite<$q2xassocLeftypuniti2xuniti左didypnotd1unitixassocRightynotd1puniti<$d1unite<$q<$2xiddleftInvynotd1id=2xidRighty值得一提的是，上面的推导也可以被画成一个（大！） 在适当的类别中的交换图，每个2作为2-箭头（并表示自然同构）。[ 27 ]见《明史》卷2.2一个小型的可逆布尔语言：B2B2在说明了通用的语言家族的语言，我们提出了一个完整的细节，基于Agda的形式化的一个小的基于语言，我们将使用建立连接到一个显式的univalent宇宙。语言是限制的情况下，只有一个类型2：数据2：U，其中0212：2A2的语法由以下四个Agda定义给出第一个定义是“2” ， 它引入了语言的类型集合：这个集合只包含“2”，它接下来的三个定义介绍了按层次分层的语言中的程序（组合子）。类型1的1级程序在类型之间映射;类型2的2级程序在1级程序之间映射;类型3的3级程序在2级程序之间映射：数据“2：U”，其中“2：U 2--------data_1_：（AB：2）U其中‘id‘not！1_ ：@{A B}（A1B）（B1A）_d1_：@{ABC}（A1B）（B1C）（A1C）--------不J. Carette等人/理论计算机科学电子笔记336（2018）59Ødata_2_：@{A B}（p q：A1B）Uwhere！2_ ：@{A B}{pq：A1B}2q）2p）_d2_：@{A B}{pq r：A1B}（p2q）（q2r）（p2r）‘idl‘idr‘assoc（pd1q）d1r_l2_：@{A B C} {pq：A1B} {rs：B1C}（p'！：@{A B}{p q：A 1B}（p2q）（！1便士2便士！1q）'！l：@{AB}（p：A1B）（pd1！1p2'！r：@{A B}（p：B1A）（！1pd1pd2'id）'！id：@{A}！1'！不是：！1'！：@{A B C}{p：A快！1（pd1q）2（！1q）d1（！1p）'！！：@{A B}{p：A 1B}！1（！1p）100万2p--------data_3_{AB} {p q：A1B}（u v：p2q）：U其中在之前的文章[6，18，8]中，3级程序，只包含一个简单的程序 更大的一级和二级程序的完整的Java语言[8]已经专门为我们的小语言。对于第一级构造函数，表示可逆程序，类型同构，有限集合之间的置换，或取决于一个人最喜欢的解释的等价物，我们有两个规范程序“id”和“在逆下不封闭！1和顺序组合物D1。对于2级构造器，表示可逆程序变换，类型同构的一致性条件，排列之间的等价性，或程序优化，取决于一个人最喜欢的解释，我们有以下几组：（i）第一组包含恒等式，逆和顺序组合;（ii）第二组建立了第一级顺序组合的相干律（例如，它是结合的）;（iii）最后，第三组包括第一级构造子的反转的一般规则。每一个p 2 q型的2级组合子都可以很容易地在1级程序p和q之间建立等价关系（如以前的工作[8]和第2节所示）。5）。例如，否定的合成等价于恒等式：10J. Carette等人/理论计算机科学电子笔记336（2018）5ÑÐÑnotd1notkey2id：'not d 1 'not key2 'id not d 1 notkey2id =（（！2'！not）l 2'id 2）d 2（'！r 'not）然而，特别有趣的是，上面的2级组合子的集合是完整的，因为1级程序p和q之间的任何等价性都可以使用2级组合子来证明。形式上，我们有两个规范的1级程序p2为了证明这一点，我们引入了一种类型，它编码的知识，其中1级程序是规范的。类型命名的子集的规范形式：dataWhich：UwhereIDNOT：Whichrefinne：（w：Which）fineNOT=这使我们能够计算任何2-组合子c（的名称）的标准形，以及证明c等价于它的标准形：canonical：（c：canonical'not = NOT，'id 2canonical（！1c）与规范c... |ID，c=ID，（'！ c2id d2'！页号... |NOT，c2not = NOT，（'！ c2不是d2'！不）canonical（_d1_{_} {'2 } c 1 c 2）与canonical c1|正则C2... |ID，c2 2 id = ID，（（c 1 2 id l 2 c 2 2 id）d 2 'idl 'id）|ID , c2ÐÑ2id = ID , ((c1ÐÑ2id l 2c2ÐÑ2id) d2‘idl ‘id)... |NOT，c 2 2 not = NOT，（（c 1 2 id l 2 c 2 2 not）d 2 'idl 'not）|NOT , c2ÐÑ2not = NOT , ((c1ÐÑ2id l 2c2ÐÑ2not)d2‘idl‘not)... |ID，c 2 2 id = NOT，（（c 1 2 not l 2 c 2 2 id）d 2 'idr 'not）|ID , c2ÐÑ2id = NOT , ((c1ÐÑ2not l 2c2ÐÑ2id) d2‘idr‘not)... |NOT，c1不适用2不适用|NOT，c22not = ID，（（c12not l 2c22not）d2notd12id）值得注意的是，canonical的证明并没有使用所有的二级组合子。然而，更大的2-组合子集合对于建立与下一节中给出的模型的更直接的联系3HOTT背景我们工作在内涵型理论与一个单叶宇宙U封闭下命题截断。本节的其余部分致力于解释这意味着什么。我们遵循HotTT书中使用的术语[28]。为了简洁起 见 ， 我 们 通 常 只 给 出 类 型 签 名 并 省 略 术 语 。 详 细 信 息 可 以 在www.example.com上的随附代码中找到https://git.io/v7wtW。J. Carette等人/理论计算机科学电子笔记336（2018）511Ñ Ñ»UU»3.1等价给定类型A和B，函数f：A<$B是拟逆函数，如果存在另一个函数g：B A，它同时充当f的左逆和右逆：is-qinv：{AB：U}（f：A<$B）Uis-qinv{A} {B}f=<$[g：（B<$A）]（g<$fnid<$f <$gnid）一般来说，对于一个给定的f，可能有几个不相等的is-qinvf型居民。正如HoTT书的第4章[28]详细说明的那样，这在HoTT的证明相关设置中是有问题的。为了确保函数f至多可以在一种方式下是等价的，在拟逆上增加了一个额外的相干条件来定义半伴随等价：is-hae：{AB：U}（f：A<$B）Uis-hae{A}{B}f=[g：（BA）][η：gfid][ε：fgid]（apfηεf）qinv-is-hae：{AB：U} {f：A<$B}is-qinvfis-haef使用后一个概念，我们可以定义两个类型之间的等价性的良好概念：is-equiv=is-hae_»_：（A B：U）UA»B=[f：（A<$B）]（is-equivf）将路径提升到等价物是很简单的，如下所示：ide：（A：U）A»AideA=id，id，re，re，（rere）运输当量：{A：}（P：A）{a b：A}a==b P a P b运输当量P（rea）=ide（Pa）id到equiv：{AB：U}A==B A Bid-to-equiv=运输-equiv id对偶地，单价允许我们从等价物构建路径。在我们的Agda库中，我们假设一价性是一个公理：假设单价：（A B：U）等价（id-to-equiv{A}{B}）我们还给出了一个由等价求路的简化形式ua，并证明了它的一些计算规则：12J. Carette等人/理论计算机科学电子笔记336（2018）5»ÑU◦„◦„◦„U 简体中文U 简体中文U 简体中文模块_{AB：}其中ua：A B A==Bua=pr1（单价A B）ua-β：ID至当量ua IDua-β=pr1（pr2（pr2（单价A B）ua-β1：转运体id uapr1ua-β1eqv=转运_（ua-βeqv）（appr1）ua-η：ua ID到当量IDua-η=pr1（pr2（单价A B））3.2命题截断一个类型A是可收缩的（h-水平0或（-2）-截断），如果它有一个收缩中心，并且A的所有其他项都通过一条路径连接到它is-contr：（A：）is-contrA=<$[a：A]<$[b：A]（a==b）如前一节所述，等价是可收缩的（[28]中的is-equiv-is-contr：{AB：U}{f：A<$B}is-equivfis-contr（is-equivf）一个类型A是一个命题（h-水平1或（-1）-截断），如果A的所有项对都由一条路连接。这种类型最多只能有一个居民;它是“如果有人居住，就会最后，一个类型A是一个集合，如果对于A的任意两个项a和b，它的路的类型a==b是一个命题：is-prop：（A：）is-propA=<$[a：A]<$[b：A]（a==b）is-set：（A：）is-setA=<$[a：A]<$[b：A] is-prop（a==b）任何类型都可以通过自由添加路径来截断为命题。这是命题截断（或（-1）-截断），可以表示为一个更高的归纳类型（HIT）。类型构造函数将类型A作为参数;|_|c将A的项转换为截断中的项;路径构造函数ident识别截断中的任何两个点，使其成为一个命题。我们必须这样做，因为Agda还不支持HIT：假设联系我们 ：（A：U）U|：{ A：U }（a：A）A|:{A:U}Ñ(a:A)ÑǁAǁJ. Carette等人/理论计算机科学电子笔记336（2018）513ÑUU光纤Ppxq光纤Ppyq纤维Ppxq»纤维Ppyqx y x基本空间A基本空间A图二. （左）型族P：A<$U作为纤维化，全空间为<$px：AqPpxq;（右）基空间中的路径xident：{A：U}{a b：A}a==b-这使得A是任何类型A上的递归原则（下面）确保我们只能消除命题截断到一个命题类型：模_{A：U}（P：U）（f：A P）（f：is-propP）其中假设rec--：APrec-α- β-β：α [a：A]（rec-α-β|一|==f a）3.3类型族是纤维化如示于图 2，型A上的型族P是具有基空间A的纤维化，其中A中的每个x诱导纤维Px，并且具有全空间<$[x：A]（Px）。2将基空间中的路径映射到总空间中的路径的路径提升属性可以定义如下：电梯：{A：} {P：A } {xy：A}（u：P x）（p：x==y）（x，u）==（y，transferPp u）liftu（re x）=re（x，u）如下图所示，点迁移P p u在空间P y中。从该点到P y中另一点v的路径可以被看作是u和v之间“位于”p之上的虚拟在Licata和Brunerie [24]之后，我们经常使用语法u==v[Pp]作为路径运输P p u==v来加强这一观点。换句话说，下面的u和v之间的弯曲[2]在本图和下图中，我们用蓝色表示路径，用红色表示函数。14J. Carette等人/理论计算机科学电子笔记336（2018）5ÓÑÓÑ˝一uXpy运输P p uvPpxqPPY Q给定一个纤维化P和上面的点x、y、u和v，我们有全空间中相关路径的模块_{A：U} {P：AU} {xy：A} {u：Px} {v：Py}，其中dpair=：[p：x==y]（u==v[P p]）（x，u）==（y，v）dpair=（re x，reu）=re（x，u）dpair=-β：（w：n [p：x==y]（u==v[P p]））（appr1dpair=）w==pr1wdpair=-β（rex，reu）=re（rex）dpair=-e：（x，u）==（y，v）x==ydpair=-e=appr1第一个函数在给定位于基空间中的路径p上的u和v之间的路径的情况下在总空间中构建路径;第二个函数是该路径的计算规则;并且第三个函数将总空间中的路径消除为 基地空间。3.4单价纤维化单价纤维化是由Kreplkin和Lumsdaine [21]在单纯集（sSet）模型中定义的。在我们的上下文中，一个类型族（纤维化）P：AU是单价的。如果地图运输等效P定义在第节。3.1是等价的，也就是说，如果基空间中的路径空间等价于相应纤维之间的等价空间。图2（右）说明了这种情况：我们知道，对于任何纤维化P，基空间中的路径p通过输运等价P p导致纤维之间的等价。要使纤维化是单叶的，反过来也必须成立：纤维之间的每一个等价都必须在基空间中导出一条路径形式上，我们有以下定义：J. Carette等人/理论计算机科学电子笔记336（2018）515简体中文˜is-univ-fib：{A：U}（P：AU）Uis-univ-fib{A}P=@（a b：A）is-equiv（transport-equivP{a}{b}）我们注意到，（对于U的）单价公理是is-univ-fi b到恒等纤维化id的特化。更一般地说，我们可以用塔斯基的方法定义宇宙，方法是用代码U表示宇宙，用解释函数El表示U。如果El是一个单价纤维化，那么这样一个呈现的宇宙就是单价的：U=[U：U]（UU）是单价体：Uis-univalent（U，El）=is-univ-fibEl正如克里斯滕森[9]所解释的，U型很少是单价纤维化的基础。然而，在同一篇论文中，克里斯滕森刻画了一类类型，这类类型总是单价纤维化的基础。我们将在下一节中解释这一点，并利用它来构建一个自定义的单叶子宇宙。4第一千一百零八章亚宇宙中国[2]我们现在拥有了定义我们感兴趣的那类单价子宇宙所需的所有要素给定任何类型T，我们可以建立一个命题谓词，它从论域中的所有类型中准确地挑选出那些被T标识的类型。这让我们建立一个U[_]：（T：U）UU[T]=U，El哪里U=[X：U]X==TEl=pr1我们将在这一节和下一节证明，选择T为2会产生一个关于语言T2是健全和完备的论域。本文的主要内容是建立U_n [2]是一个univaletuniverse。 我们在第一小节中重点讨论这个论点。在接下来的两个小节中，我们使用这个结果来描述这个宇宙的代码类型中的点和路径。节中图5将显示点和路径的这种表征，以匹配图2的类型和组合子。4.1纤维化E12是单价的单位U[2]由元素的编码的基空间U[2]和解释函数E12组成，定义如下：U[2]：UU[2]= pr1U[2]-=[ X：U ]X ==216J. Carette等人/理论计算机科学电子笔记336（2018）5»ÑUU»Ñ◦„（2）|第2条|）==（X，|p|）E12：[X：U]X==2UEl2=pr1类型族El2定义了一个基空间为U[2]的纤维化，如下所示：光纤2光纤X基本空间U[2]=[X：U]X==2我们的目标是证明El2是一个单价纤维化。我们通过链接两个等价物来建立这一点第一个等价性是简单地诉诸于一价性，以建立（X==2）»（X»2），即，我们的基本空间相当于[X：U]我们将这个空间命名为BAut2。一般来说，BAutT是（仅仅）等价于T的所有类型的第二个等价是证明了对于所有形状为的空间，对于任何类型的T，在BAutT上的第一个投影实际上是一个单叶纤维化。这是下面的引理is-univ-fib-ElB，其最初的公式是由Christensen [9]提出的：BAut：（T：U）UBAutT=[X：U]X»TElB：{T：U}BAutTUElB=pr1transport-equiv-ElB：{T：}{v w：BAutT}（p：v==w）pr1（transport-equiv ElBp）==transport-id（dpair=-ep）transport-equiv-ElB（re-equiv）=re-equidis-univ-fib-ElB：{T：}is-univ-fib ElBis-univ-fib-ElB（T，q）（Tgeqv=dpair=（uaeqv，ident）η：g运输当量ElB idη（相对湿度_）=ap dpair=（dpair=（ua-η（re_），prop-is-set（λ_ε：运输当量ElBgidJ. Carette等人/理论计算机科学电子笔记336（2018）517UUεeqv=eqv=（运输当量-ElB（dpair=（uaeqv，ident））·ap（传输id）（dpair=-β（uaeqv，ident））Ua-β1方程式）这确定了El2是一个单叶纤维化，给了我们U[2]中路径的一个特征，我们接下来将利用布尔等价。4.2基础空间U[2]基空间U[2]中的点都具有形式（X，|p|其中p是类型X==2。我们显然有一个典型的点20：20：U[2]20=（2，|第2条|）它直接对应于RISK2中的布尔类型。我们提醒读者，通过构造，U[2]是路径连通的。剩下的就是刻画U[2]中的1-路、2-路和可能更高的路，并将它们与U[2]中的1-组合子、2-组合子等联系起来。为了方便地引用U[2]中的路径，我们定义了一个（点）类型上的循环空间，并证明了BAut2上的循环空间等价于2»2：Ω：Ω [T：]TΩ（T，t0）=t0==t0Aut：（T：U）UAutT=T»Tb0：{T：U}BAutTb0{T} = T，|IDET|ΩBAut»Aut[_]：（T：U）<$Ω（BAutT，b0）»AutTΩBAut»Aut[T]=输运等效ElB，is-univ-fib-ElB b0b0上述结果说明，一般地，T型的分类空间的循环空间等价于T的自同构型。特别地，它遵循Ω（BAut2，20）»Aut2，这将U[2]上的路的特征化问题简化为布尔类型上的自同构的特征化问题我们现在把注意力转向解决这个问题。4.32上的自同构类型2有两个点构造函数，没有路径构造函数，这意味着它的点上没有非平凡的路径，除了路径。事实上，我们可以在内涵类型理论中使用大消去法证明这两个构造函数是不相交的。这是18J. Carette等人/理论计算机科学电子笔记336（2018）5在Agda中使用依赖模式匹配时，反映在荒谬模式中。更一般地，2>>1Z1和两个集合的不相交并是一个集合：02‰12：02==12K02‰12p=transportcodeptt其中代码：2U代码02=J代码12=K利用02‰12和可拓函数（可从单位元导出），我们可以证明2和2之间正好有两个不同的等价关系.此外，对于任何等价f，利用is-equiv f是一个命题这一事实，我们可以证明2 » 2恰好有两个居民：id»not»：2»2id»=id，qinv-is-hae（id，rev，rev）not»=not，qinv-is-hae（not，（λ{02<$re <$02;12 <$re<$12}），（λ{02<$re <$02;12 <$re <$12}）其中：22不是02=12不是12=02这里发生了一些非常特殊的事情：虽然一般来说，通过取n个1的不交并而形成的类型具有大小为n的自同构空间！在我们的例子中，我们有2和2»2是相同的大小。这个组合的偶然性实际上可以被提升，以表明2 » 2和2之间存在等价性。 通过构成等式链sΩ（U_n，20）»Ω（BAut（2） ，b0）»（2»2）»2，我们得到：2»Ω20：2»（20==20）只有两个不同的1-循环U[2]。 把它们称为id2而不是2，我们得到 分解：all-1-loops：（p：20==20）（p==id2）+（p==not2）U[2]中的每个循环都可以用恒等式或布尔否定来标识。对于U[2]中的2-环，下面的分析表明它们可以用平凡路来标识。首先，通过应用不相交并的归纳原理和路归纳，我们可以证明2是一个集合：2-is-set：is-set22-is-set0202（req.02）（re. 02）=re（re 02）2-is-set0212（）2-is-set1202（）2-is-set1212（req.12）（repe.12）=re（re 12）J. Carette等人/理论计算机科学电子笔记336（2018）519ÑÑ_（2）¢由此，我们得到20==20也是一个集合，通过使用ua和运输。这又显示了2-环的可收缩性：Ω20-is-set：is-set（20==20）Ω20-is-set=运输is-set（ua2»Ω20）2-is-set所有2-循环：{p：20==20}（γ：p==p）γ==rep全2-环{p}γ=Ω20-is-setp pγ（rep）在下一节中，我们将使用全1-循环和全2-循环作为显示U[2]和U2之间对应关系的关键成分。请注意，本节中的大多数结果都是通用的。然而，当我们超过2时，路径空间的组合爆炸是这样的，显式枚举很快变得不切实际，其他技术将变得必要。5U[2]和U2之间的对应关系从精确的意义上说，形式化编程语言中的可逆函数与单价宇宙中的路径之间的联系，尽管看起来很直观，但却相当微妙。HoTT中的路径配备了“单例可收缩性”、“传输”和“路径归纳”等原则，但这些原则似乎都没有在可逆编程中有任何直接的对应物。然而，我们将演示如何将整个（但不可否认很小）可逆编程语言（如P2P2）的语义捕获为紧凑的规范如[X：U]<$X==2<$。我们的精确对应将包括在Un[2]和Un[2]之间建立映射，对于点、1-路、2-路和3-路，使得每个映射在适当的等式概念下是可逆的。这给出了每个级别的可靠性和完整性的概念。5.1映射点（0级）的映射是直接的，因为U [2]和U[2]都是单例：[2]第二次世界大战（1）02‘2=2个）0 0x_y0：U[2]2x_ y0=Level-1是第一个非平凡的层次。对于每个句法组合子c：A1B，我们关联一条从A0到B0的路径，反之亦然。从单价论域映射回可逆语言的语法是唯一可能的，因为我们对论域中的路径有一个完整的表征（在上一节的全1循环20J. Carette等人/理论计算机科学电子笔记336（2018）5（）（）（）（Ⅲ）<$_）1：{AB：<$2}A1B<$A）0==<$B）0K‰‘idl2=单位p1<$u1d2u2）2=<$u1）2<$u2）2<$¢）1¢）1！p¢）1_¢）2个¢u¢¢）2个u‘id‘not（1）1--ppd1q1=p1<$q1x_y1：20==20x20y01x20y0xpy1withall-1-loopsp... | inl pid=‘id... | inr pnot =‘not在第二层，我们通过前一节中的全2-环的构造知道，单价宇宙中的所有自路径都是平凡的。然而，来回的映射需要相当多的（乏味的）工作。我们在下面展示了从2-组合子到2-路的映射的几个例子，在第一个方向上，这是一个利用单价宇宙中路径的必要性质的问题（例如，每条路径都有一个逆）。通过路径归纳法证明了这些性质。相反的方向再次关键地依赖于1-循环的特征，以及恒等等价和交换两个布尔值的等价是不同的这一事实2（2）！：{A B：2} {pq：A1pB}（u：p2q）第二类p）1==q1‘id {p=p}=re（2）2--u'！ u啊！（2）– remaining cases arex_y2：{pq：20==20}p==qxpy12xqy1x_y2{p}{q}u，全为-1-loopp|所有1-l操作q... | inl q=id = 'id2|inl q=id=‘id2... |inrq=not = K -elim（id 2‰ not 2（（！|inr q=not = K-elim (id2‰not2 ((!p=id）<$u<$q=not））... |inl q=id = -elim（id 2 not 2（（！|inl q=id =-elim (id2 not2 ((! q=id）<$！ u<$p=not））... | inr q=not = 'id2|inr q=not =‘id2对于最后的第三层，从单叶宇宙映射到N2是微不足道的，因为后者在第三层只有一个构造函数另一个方向需要在单价宇宙中进行一些复杂的推理，以构建所需的3-路径：）1）2个J. Carette等人/理论计算机科学电子笔记336（2018）521引理：{p q r：20==20}（p=r：p==r）（q=r：q==r）（u：p==q）u ==p=r<$（！p=r）<$u<$q=r）<$（！q=r）22J. Carette等人/理论计算机科学电子笔记336（2018）5（3））1（Ⅲ）（K ‰）¢yXp（Ⅲ）（Ⅲ）（Ⅲ）<$x py1））1withall-1-loopsp|正则x py1（Ⅲ）（Ⅲ）<$_）3：{AB：2}{pq：A1B}{uv：p2q}（α：u3v）<$u）2==<$v）2（all-2-loops（！p=id，u2<$q=id）<$！（all-2-loops（！p=id，（all-2-loops（！p=不，u2<$q=不）<$！ （all-2-loops（！p=不，p1 y 1与典范p|全1- 1操作系统Quuy（2）v_{... | inlp=id|inlq=id=引理p=id q=id^ap（λx ^p=id ^x ^！q=id）|全1-环（1）！ （引理p=id q=id<$v）2）<$）... |inr q=not = K -elim（id 2‰ not 2（（！|inr q=not = K-elim (id2‰not2 ((! p=id）<$u2<$ q=not））... |inl q=id=|inl q=id =-elim（id2not2（（！q=id）<$！u2-p=不））... | INRp=无|inrq=不=引理p=not q=not（2）ap（λx）=非x！q=无）v2<$q=不）！（引理p=not q=no<$t<$v））2）<$）x_y3：{pq：20==20}{uv：p==q}u==vxuy23xvy2x_y3=5.2一致性现在需要证明的是，所有这些映射在每个往返产生一个与原始项可识别的项的意义上是相互一致的，从而有效地表明了关于λ2的单价宇宙的可靠性和完备性。在0级，这是微不足道的。在第1级，可靠性意味着映射是逆映射：● 任何映射到一个1-路径并返回的1-组合子p都是2-等价于它自身，并且● 在发送到1-组合器的1-路径p和返回之间总是存在2-路径。这在代码中更简洁）1 1X：（p：‘2（1）1p1. .. |I）D，p<$id |inl p=id=p<$id<$）... |inr p=not = K -elim（id 2‰ not 2（！|inr p=not = K-elim (id2‰not2 (! （（！p=not）p<$id（2））... |inl p=id = K -elim（id 2‰ not 2（（！|inl p=id= K-elim (id2‰not2((! p=id）<$p <$not （2））... |inr p=not = p <$not|inr p=not = pônotx_y11：（p：20==20）p==xpy11... |ID，p <$id = p=id|ID, pôid= p=id... |NOT，p <$not = K -elim（id 2 <$not 2 p <$not |NOT , pônot = K-elim(id2‰not2pônot （ 二）... |ID，p <$id = K -elim（id 2‰ not 2（！|ID, pôid= K-elim (id2‰not2 (! 波伊德（ 2））... |NOT，p <$not = p=not|NOT , pônot = p=not2<$q=id）p¢x_J. Carette等人/理论计算机科学电子笔记336（2018）523它们在以下意义上也是完整的24J. Carette等人/理论计算机科学电子笔记336（2018）5（2）（2）））（2）y（）（）（）（Ⅲ）K‰ÐÑÐÑÑ¢)¢) Ñ ÐÑ（！xvy22）¢ap（λxpy1）1 x！<$xqy1）1<$）<$α））3¢）¢● 对于映射到由2-路相关的1-路的任何两个1-组合子，1-组合子由2-组合子相关，并且● 对于映射到由2-组合子相关的1-组合子的任何两个1-路，它们由2-路相关。通常，完备性是一个相当难证明的结果。但在我们的例子中，上一节的基础设施使证明变得直接：首先，关键是使用的二级编译器的可重复性！2;对于它的第二个pro完备性1：{p q：完全数s1{p}{q}u=xp1y1d2（xuy2d2！2xq1y1）完全烯s1-1：{pq：20==20}xpy12xqy1p==qcompletenes s1-1{p}{q}u=xpy11<$u2<$（！xqy11）对于第2级，这些陈述在非正式方面非常相似（所有级别都增加了一个）。对于2-组合子，结果是平凡的。对于从2-路径开始的另一个方向，在单价宇宙中，合理性是很难甚至状态的，主要是因为ty p在x中是未知的。u2y2和xuy22是不平凡的。但1-循环的枚举）2 2Xy u：{pq：=‘2（3）22（u：p2q）u3（x<$p）1y1d2（x<$u）2y 2d2（！2x<$q）1y1）x_y22：{pq：20==20}（u：p==q）<$u==xpy11<$xuy22“（！xqy11）x_y22{p}{q}u，全1-l oopp|所有1-l操作q... | inl p=id| inl q=id=（lemmap=id q=id u）·（ap（λxp=id <$x <$！q=id）（all-2-loops（！p=id <$u <$q=id）... | inl p=id| inr q=not = K-elim (id2‰not2 ((! p=id）<$u<$q=not））... |inl q=id|inl q=id =-elim（id2不是2（！ （（！ p=not）<$u<$q=id）..