简单类型λ-演算的前向自动微分推广

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）257-272www.elsevier.com/locate/entcs一种简单类型的前向自动微分λOleksandr Manzyuk亚历山大·曼久克1，2爱尔兰梅努斯梅努斯摘要本文给出了一个带有前推算子的简单类型λ-演算的推广。这种扩展的动机是希望纳入前向自动定向，这是一种重要的技术在数值计算中，转化为函数式编程。我们的演算类似于Ehrhard和Regnier我们证明了，像diffezziλ-演算，我们的演算可以在diffezziλ-范畴中得到合理的解释。关键词：切丛，对偶λ-演算，对偶范畴，范畴语义。1引言自动微分（AD）是一种强大的技术，用于计算程序语言中程序给出的函数的导数[6]。AD优于分裂微分，因为AD生成的导数值没有近似误差，并且优于符号微分，因为它可以处理非常高复杂度的代码，并且因为它给出了强的计算复杂度保证。存在许多AD系统3（以库和代码预处理器的形式）。这些AD系统中的大多数都建立在命令式编程语言（Fortran，C/C++）之上，而AD的思想最自然地体现在函数式编程语言中。事实上，微分算子几乎是高阶函数的范例。然而，尽管有大量的1这项工作得到了爱尔兰科学基金会首席研究员赠款09/IN.1/I2637的部分支持。2电子邮件：manzyuk@gmail.com3http://www.autodiff.org/?模块=工具1571-0661 © 2012 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2012.08.017258O. Manzyuk/电子笔记理论计算机科学286（2012）257研究4和AD实现的扩散，在第一类函数存在的情况下，缺乏AD的清晰语义，这抑制了将AD并入函数式编程。Siskind和Pearlmutter [12]讨论了试图用AD运算符扩展函数式编程语言所面临的问题。特别是，他们强调了高阶函数AD的微妙之处他们描述了[13]一种新的AD系统，STALIN，并声称它正确地处理了高阶函数虽然STALIN的答案是正确的，在已知其他系统失效的示例中，没有证明正确性结果，这很难令人满意。为了解决这些问题并为支持AD的函数式编程语言奠定理论基础，我们建议使用AD算子扩展λ演算。在本文中，我们为实现这一目标迈出了第一步。AD有几种变体：正向、反向及其混合。我们提出了一个简单的类型λ演算的前向AD，留下更复杂的反向AD的未来工作。用微分算子扩展λ-演算的想法并不新颖。Ehrhard和Regnier从线性逻辑中汲取灵感，引入了微分λ演算[4]。尽管它起源于线性逻辑的指称语义，但微分λ-演算也是一个有吸引力的基础，在此基础上可以构建一个内置支持微分的函数式编程语言。例如，与符号微分不同，微分λ-演算不仅可以处理数学表达式，还可以处理任意λ-项。最值得注意的是，它可以通过和高阶函数的导数。然而，像符号微分一样，简单地实现微分λ-演算，会产生一种非常低效的计算导数的方法，因为失去了共享。我们提出了一个变化的微分λ-演算，微扰λ-演算，其中，我们推测，不需要这种损失的效率。与前向AD一样，微扰λ-演算基于前推的微分几何思想而不是导数。与微分λ-演算类似，微扰λ-演算可以在Bucciarelli等人的任意微分λ-范畴中解释。我们证明这种解释是合理的。我们认为，文[4]中关于微分λ-演算的连续性和强正规化的证明可以适用于微扰λ-演算。然而，这些问题的正式处理留给未来的研究。2前向AD为了激发微扰λ-演算的定义，我们简要概述了前向AD背后的他们是最自然的解释，在不同的几何术语。设TX表示光滑流形X的切丛。例如，欧氏空间Rn的切丛TRn可以用卡氏积Rn×Rn来标识。切丛TRn的一个元素（XJ，x）被看作4在撰写本报告时，http://www.autodiff.org网站的出版物数据库包含1277个条目O. Manzyuk/电子笔记理论计算机科学286（2012）257259作为原始x∈Rn与切线（或扰动）xJ∈Rn配对。光滑流形f：X→Y之间的光滑映射产生光滑映射Tf：TX→TY，称为f的前推。 例如，前推Tf：光滑映射f：Rm→Rn的TRm=Rm×Rm →Rn×Rn=TRn由Tf（XJ，x）=（Jf（x）·XJ，f（x））给出，其中Jf（x）是f在点x处的雅可比矩阵.对应X<$→TX，f<$→Tf构成光滑流形范畴到自身的函子。组合的保持是链式法则的一个结果。此外，T保存产品。非正式地，这意味着为了计算复合函数的前推，它需要知道它的成分的前推。前向AD的实现利用了这一点，通常采用以下方式之一• 通过重载原语，使它们可以接受数字和切束对作为输入。每个重载原语表示两个函数：最初由该原语计算的函数及其前推。然后，任何由重载原语构建的用户定义过程也表示（并且可以通过提供适当类型的参数来计算）两个函数：函数f：Rm→Rn和它的前推Tf：TRm→TRn。• 通过生成（由编译器内部或由预处理器外部）计算前推Tf的过程的源代码：TRm→TRn从计算函数f的程序的源代码中得到函数f：Rm→Rn。这种转换方法可以被看作是一种增强的符号化，通过同时操纵原始值和正切值来恢复共享无论哪种方式，在程序中定义一个计算函数f的过程自动地提供了对计算f的前推的过程的访问。让我们用一个包含普通算术的例子来说明这个方法。由于切丛函子T保积，所以运算+，·：R×R→R的向T（+），T（·）：TR ×TRT（R×R）→TR的推进使TR具有环的结构. 切丛TR同构为一个环通过（xJ，x）→x+xJε到对偶数环R[ε]/（ε2），下面我们用R[ε]/（ε2）来标识TR。TR中的操作+和·正好对应于R中操作+和·的前推。因此，我们可以重载+和·来表示两者。计算一个由+和·构建的函数的前推相当于在对偶数上解释函数的主体例如，λx的导数。通过计算λx的前推得到点3处的x2 + 1。 x2+ 1在点3+1 ε =3+ ε处，并取结果的扰动部分。前者相当于在点3 +ε处对表达式x2+1求值，将+和·分别解释为对偶数的加法和乘法：T（λx. x2+ 1）（3 + ε）=（λx. x2+ 1）（3 + ε）=（3 + ε）·（3 + ε）+1= 10 + 6 ε。换句话说，函数f在点x处的导数可以计算为：Df x=E（f（x+ε）），其中E由E（x+xJε）=xJ给出。260O. Manzyuk/电子笔记理论计算机科学286（2012）257在存在第一类函数的情况下，情况变得更加复杂，因为过程输入和输出的空间不再需要是欧几里得空间，而可以是函数空间。此外，正如Siskind和Pearlmutter [12]指出的那样，实现必须小心，不要混淆多次向前推动同一函数时出现的扰动我们用一个涉及导数算子D的嵌套调用的例子来说明这个扰动混淆的问题，例如D（λx）。 x·D（λy. x）2）1.因为内导数等于0，所以整个表达式的值也应该为0。然而，简单地应用D的公式，我们得到：D（λx. x·D（λy. x）2）1 = E（（λx. x·D（λy. x）2）（1 + ε））=E（（1 + ε）·D（λy. （1 + ε））2）=E（（1 + ε）·E（（λy. （1 + ε））（2 + ε）=E（（1+ε）·E（1+ε））=E（（1 + ε）·1）= E（1 + ε）= 1/= 0。正如在[12]中所解释的，这个错误的根源是我们没有区分由D的内部和外部调用引入的扰动。有一些方法可以解决这个问题，例如，每次调用D时用新的ε标记扰动，并引起跟踪哪个ε与D的哪个调用相关联的簿记开销。尽管如此，我们希望这个例子能够说明AD λ演算的清晰语义的价值和重要性。当我们说象征性的差异化支持了分享的损失？那么，AD是如何解决这个问题的呢？让我们用一个例子来说明。考虑计算n的乘积的导数的问题函数：f（x）= f1（x）·f2（x）·. ·f n（x）。应用产品规则，我们得到导数的表达式，其大小为n的平方：fJ（x）=f1J（x） ·f2（x） ·. . . · fn（x） +f1（x） ·f2j（x） ·. . . ·fn（x）+·· ·+ f1（x）·f2（x）·· . . ·fnJ（x）。简单地计算它会导致对每个fi（x）进行n-1次计算。如果我们的成本模型是计算fi（x）或fiJ（x）每个成本为1，并且算术运算是自由的，那么f（x）的成本为n，而fJ（x）的成本为n2。与前向AD相比：前推Tf（x+xJε）是乘积（在对偶数）的前推Tf1（x+xJε），Tf2（x+xJε），.，Tfn（x+XJε）.计算每个Tfi（x+xJε）相当于计算fi（x）和fiJ（x），因此成本为2。因此，Tf（x+ε）的成本为2n。一般来说，前向AD保证计算fJ所花费的操作不超过计算f的操作的常数因子倍。3Di-λ-范畴微扰λ-演算的解释的定义及其可靠性的证明依赖于不同微扰λ-范畴中的切丛理论O. Manzyuk/电子笔记理论计算机科学286（2012）2572611开发[9]。为了使本文自成一体，我们在这里总结了该理论的结果。读者可参考[9]了解更多详情。设C是一个范畴，X，Y，Z是C的对象. 我们用X×Y表示X和Y的乘积，π1：X×Y→X，π2：X×Y→Y是投影。终端对象表示为，对于任何对象X，我们表示为！X是从X到1的唯一态射。 对于一对态射f：Z → X和g：Z→ Y，记f，g∈：Z→X×Y为f和g的配对，即，唯一态射使得π1f，g=f和π2f，g= g.一个范畴C称为闭范畴，如果对于任意一对对象X和Y，存在一个对象X<$Y，称为指数对象，和一个态射ev X，Y：（X<$Y）×X→Y，称为赋值态射，满足以下普适性质：由Λ -（g）= ev X，Y <$（g × id X）给出的映射Λ-：C（Z，X<$Y）→C（Z×X，Y）是双射的。令Λ：C（Z×X，Y）→C（Z，X<$Y）表示Λ-的逆。换句话说，对于态射f：Z×X→Y，Λ（f）：Z→X<$Y是唯一的态射，满足e vX，Y<$（Λ（f）×idX）=f。态射Λ（f）称为f的currying。我们将利用这些方程Λ（f）g= Λ（f（g×id）），（1）evΛ（f），g=fid，g，（2）这是从《易经》的定义中引申出来的。范畴的概念是由Blute等人[2]引入的，作为可区分映射的公理化，以及一个统一的框架，在其中研究不同的概念，让人想起可区分演算。定义3.1（[2，定义1.1.1]）范畴C是左可加的，如果每个hom-集都具有交换幺半群（C（X，Y），+，0）的结构，使得（g+h）<$f=（g<$f）+（h<$f）且0<$f =0。C中的态射f是可加的，如果它满足f（g+h）=（fg）+（fh）且f0= 0。定义3.2（[2，定义1.2.1]）一个范畴是左可加范畴，如果它是一个左可加范畴，其乘积使得所有投影都是可加的，并且所有可加态射的配对都是可加的。注3.3设C是一个Carnival左可加范畴。然后配对图−，−此外，对于每对对象X和Y，存在态射11d=efidX，0：X→X×Y和12d=ef0，idY：Y→X×Y ， 它 们 满 足 方 程 π11=idX ， π212=idY ， πk1=0ifk/=1 ， 和nd1π1+π2π2=idX×Y。然而，请注意，与加法范畴相反，在左加法范畴中，这些方程并不意味着态射ι1和ι2使X×Y具有X和Y的余积的结构。这在加法态射的子范畴上是如此，但在全范畴上不一定。定义3.4（[2，Section 1.4，定义2.1.1]，[3，定义4.2]）一个Carnival闭范畴是Carnival闭左可加的，如果它是Carnival左可加范畴，使得每个Currying映射Λ：C（Z×X，Y）→C（Z，X<$Y）262O. Manzyuk/电子笔记理论计算机科学286（2012）257是可加的：Λ（f+g）= Λ（f）+ Λ（g）且Λ（0）= 0。一个卡氏（闭）双加范畴是一个卡氏（闭）左加范畴，它配备了一个算子D：C（X，Y）→C（X×X，Y），满足以下公理：D1. D（f+g）=D（f）+D（g）且D（0）= 0。D2. D（f）h+k，v=D（f）h，v+D（f）k，v和D（f）0，v= 0。D3. D（id）=π1，D（π1）=π1<$π1，D（π2）=π2<$π1。D4。 D（f，g）= D（f，g）D5。 D（f D（g），g.D6。 D（D（f））g，0，h，k= D（f）g，k.D7。 D（D（f））0，h，g，k= D（D（f））0，g，h，k.卡氏范畴的典型例子是光滑映射范畴，它的对象是自然数，态射m→n是光滑映射Rm→Rn。 算子D取f：Rm→Rn，并产生aD（f）：Rm×Rm→Rn由D（f）（XJ，x）=Jf（x）·XJ给出，其中Jf（x）是f在点x处的雅可比矩阵。对公理的一些直觉：D1说D是可加的; D2说D（f）在其第一个坐标上是可加的;D3和D4断言D与乘积结构相容，D5是链式法则。我们请读者参考[2，引理2.2.2]来证明D6本质上要求D（f）在其第一个变量中是线性的（在下面定义的意义上D7本质上是部分分化顺序的独立性根据[2]，我们说态射f是线性的，如果D（f）=f<$π1。 通过[2，引理2.2.2]，线性态射类在和，合成，配对和乘积下是封闭的，并且包含所有的恒等式，投影和零态射。此外，公理D2意味着任何线性态射都是可加的。范畴的概念部分地是由对Erhard和Regnier [4]的微分λ-演算进行范畴化建模的愿望所激发的。Blute等人[2]证明了carbohydrandi-calibration范畴是合理的和完备的，可以对合适的项演算进行建模。然而，由于微分算子不一定与卡氏闭结构相容，因此卡氏微分范畴的性质太弱，无法建模完整的微分λ-演算。为此，Bucciarelli等人[3]引入了双线性λ-范畴的概念。定义3.5（[3，定义4.4]）一个离散λ-范畴是一个Carnival闭离散范畴，使得D（Λ（f））= Λ（D（f）∈π1× 0 X，π2× id X∈）成立，对每个f：Z×X→Y。这个不同的λ-范畴公理本质上要求求值态射ev在它的第一个参数中是线性的。例3.6Blute等人[1]证明了方便向量空间和光滑映射的范畴是一个Carnival闭的Dixival范畴。我们在[9]中已经证明它实际上是一个双线性λ-范畴。我们请读者参考[3]中的另外两个例子。O. Manzyuk/电子笔记理论计算机科学286（2012）257263微分算子D允许我们从微分几何中复制光滑流形的切丛的构造。设C是一个carbohydrategy. 切丛函子T：C→C定义为TX = X×X和T（f）=。引理3.7（[9，引理3.1.3]）如果f是线性的，则T（f）= f×f。切丛函子T是单子的一部分。对于C的每个对象X，单子的单位ηX是态射<$0 ， idX<$ ： X→X×X=TX ， 单 子 的 乘 法 μX 是 态 射 <$π2<$π1+π1<$π2 ，π2<$π2<$：TTX=（X×X）×（X×X）→X×X=TX。单子（T，η，μ）是强的[10，定义3.2]。张量强度t X，Y：X×TY→T（X×Y），也称为右张量强度，由tX，Y= 0，π1，=给出。利用C的对称性c A，B=<$π2，π1<$$>：A×B→B×A，我们也可以定义左张量强度为tJX，Y = T（c Y，X）<$t Y，X<$c TX，Y：TX × Y → T（X ×Y）。更 明确地说，tJX， Y =<$$>π1<$π1，0 <$，<$π2<$π1，π2<$$>=<$π1×0，π2× id Y<$。因为函子T是强单子的一部分，通过[7，定理2.1]，T成为monoidal函子（T，T，T，T0）：C→C，如果我们使T X，Y等于复合函数T X，Y= μX×Y TT（t X，Y）<$tJX，T Y ：TX×TY→T（X×Y），并将η1：1→T1。X，Y的定义是不对称的，实际上也存在态射X，Y=μX×Y<$T（tJX，Y）<$tT X，Y：TX×T Y→T（X×Y）thatalsomakesT是么半群函数。 态射和态射可以显式计算。在[9，引理3.4.1，3.4.2]中，证明了σ_I与σ_i相等，且与分配同构σ一致.特别地，（T，η，μ）是一个交换单子[7，定义3.1]。引理3.8（[9，引理3.4.5]）设f：Z→X，g：Z→Y是C中的态射.则T f，g= T（f），T（g）。从现在起我们假设C是一个双线性λ-范畴。命题3.9（[9，命题3.6.2]）设g：A×B→C是中的态射，C. 设h = T（g）<$tJ：TA × B → TC. 则T（Λ（g））= Λ（π1<$h），Λ（π2<$h）<$：TA→T（B →C）。Carnival闭范畴C是一个对称monoidal闭范畴，具有由乘积给出的monoidal结构，因此也是Eilenberg和Kelly的闭范畴[5]。由[5，命题4.3]，幺半群函子（T ，λ ， λ0 ）：C→C给出了一个闭函子（ T ，λλ， λ0 ） ：C→C，其中λλ =λλX ， Y ：T（XλY）→（TXλTY）由λλ =Λ（T（ev）λλ）给出. 我们在[9，3.7节]中证明，T（ev）=ev（π1×π2）+D（ev）t（π2×id），ev（π2×π2）：T（XY）×TX→TY.（三）Carbohydrate闭范畴C产生一个富含C的范畴C：C的对象是C的对象，对于每对对象，C（X，Y）=X<$YC的X和Y。 由[8，定理1.3]，函子T：C→C装备有264O. Manzyuk/电子笔记理论计算机科学286（2012）257张量强度t产生C函子T：C→C，使得TX=TX，T=TX，Y：（X<$Y）→（TX<$TY）由T= Λ（T（ev）<$t）给出。定理3.10（[9，定理3.8.2]）T是线性态射。命题3.11（[9，命题3.8.3]）设f：Z×X→Y是C中的态射。则T<$Λ（f）= Λ（T（f）<$t）。我们还需要下面的定义和简单的引理。定义3.12（[3，定义4.6]）设sw = swX ，Y，Z表示态射sw =π1，π2：（X×Y）×Z→（X×Z）×Y。显然，sw是一个线性态射。此 外 ，sw f，g，h=f，h，g。引理3.13T（sw）<$tJ<$（t× id）= t<$sw：（X×TZ）×Y→T（（X×Y）×Z）。4微扰λ-演算在本节中，我们描述微扰λ-演算。它的语法与Ehrhard和Regnier [4]的微分λ-演算的语法非常相似，但有两个显著的区别：• 我们没有引入表示s在方向t上的导数的句法形式Ds·t，而是用表示s向前推进的句法形式Ts来扩展λ演算。• 为了在语法上强调pairs是线性的，我们引入了两种语法形式：ik s（将s注入到乘积的第k个因子中）和πk s（将s投影到第k个坐标上），k= 1， 2。使用注入的语法，pairs可以作为语法糖引入，线性是自动的。更正式地说，微扰λ-项的集合Λp和单λ-项的集合Λs由互感定义如下：Λ p： M，N：：= 0 |S|s + N，Λ s：s，t：：= x |λx。 S |SN |T s |s |π k s，k = 1，2，因此，每一个微扰λ-项都是一个有限（可能是空的）单λ-项包的形式和。运算+被推广到任意微扰的λ-项，其明显的方式是袋的并。表示空袋子的项0是和的中性元素。我们考虑扰动λ-项到α-变换，结合性和交换性.我们写MN，如果M和N在语法上相等，直到前面提到的等价。项Ts是s的前推。M的自由变量集合FV（M）的定义与通常一样。我们O. Manzyuk/电子笔记理论计算机科学286（2012）257265i=1我i=1我Ki=1我Ki=1我i=1我i=1我K我K 我我我12122Γ（x）=σΓx：σr;x：σs：τΓ λx. s：σ→ τΓs：σ→τΓN：σrsN：τΓ0：σΓs：σΓN：σΓs+N：σ联系我们最大值：σ1×σ2Γεs：σ1×σ2Γπk s：σkτs：σ→τTσ→TτFig. 1. 微扰λ-演算引入以下语法糖：λx。.卢恩sd=efnλx。 s，1。卢恩sd=efn是的，T.卢恩sd=efnTs，π。卢恩sd=efnπ s，.卢恩sNd=efnsN，M， M，d=efiM+1 M，其中，如果n= 0，则总和减少到项0。请注意，上述等式左侧的项在语言中不是有效项。它们是方程右侧相应项的焦距变化。还要注意的是，通过这种方式，我们在操作员位置上从语法上捕获了抽象、前推、注入、投影、对和应用程序让我们定义表征简单类型的微扰λ-演算的类型系统。 我们假设给定一些原子类型α，β，. ..， 若σ和τ是型，则σ×τ和σ→τ也是型。我们定义一个类型函数T，Tσ=σ×σ。类型规则如图1所示。他们是标准的打字员简单类型λ-演算与产品的规则，由类型规则扩展为T和sum。设M，P为微扰λ-项，x为变量.用P替换M中的x，记为M[P/x]，由图2所示的M上的归纳定义。通常的警告适用于（λy）的定义。s）[P/x]，即α-转换我们可以假设xy和yi∈FV（P）。我们采用图3中列出的归约规则：通常的β-归约（λx. s）N →βs [N/x]和投影注入规则π k（ι ks）→×s和π k（ι ls）→×0，其中k，l∈ {1，2}，kl = l. T也有一个约化规则，它在形式上类似于微分λ -演算中D的约化规则，但它是由微分λ -范畴中切丛的一般范畴性质提出的[9]。 更具体地说，T的归约规则是T（λx）。s）→Tλx。 Txs，其中TxM是根据图4所示的方程通过M上的归纳法定义的。 Tx（λy. s）受标准附带条件的约束，即：[5] T的定义的动机是我们希望在不同的λ-范畴中解释微扰λ-演算方便向量空间E的切丛同构于E×E，我们在微积分中通过定义Tσ为σ×σ来表示。推广T以允许类型σ是一般光滑空间，Tσ是切丛，这将是有趣的，它一般不能定义为σ×σ。我们把这个留给以后的工作。i=1i=1i=1i=11266O. Manzyuk/电子笔记理论计算机科学286（2012）257..Xy[P/x]=P如果x=y，否则，0[P/x] = 0，（λy. s）[P/x] = λy。（s [P/x]），（s + N）[P/x] = s [P/x]+ N [P/x]，（sN）[P/x] =（s[P/x]）（N[P/x]），（Ts）[P/x]= T（s [P/x]），（π k s）[P/x] = π k（s [P/x]）.图二. 替代的定义（λx. s）N →βs [N/x] π k（ι k s）→×sπ k（ι l s）→×0 T（λx. s）→Tλx。 Txs图3.第三章。微扰λ-演算的约化规则Ty=xifx =y否则，Tx0 = 0Tx（λy. s）=λy。π1（Txs），λy. π2（Txs）πTx（s + N）= Txs + TxNTx（sN）=（Txs）（TxN）Tx（kk s）=k（π1（Txs）），k（π2（Txs））Tx（Ts）=<$T（π1（Txs）），T（π2（Txs））<$Tx（πk s）=<$πk（π1（Txs）），πk（π2（Txs））<$M<$Nd=ef<$（π1M）（π2N）+π1（（T（π2M））N），（π2M）（π2N）<$见图4。 x的定义α-转换我们可以假定x不同于y。为了简化表示法，我们引入了一些语法糖：操作，它也在图4中定义。语法形式的类型规则可以从其他语法形式的类型规则中推导出来，如下所示Γ<$M：T（σ→τ）Γ<$N：TσΓ<$M<$N：Tτ让我们对这些方程作一些直观的说明。我们定义Txx=x，因为恒等函数的前推是恒等函数;类似地，如果x/=y，我们设置Txy=ι2y，因为常数函数的前推是返回提升值的常数函数。命题3.9和方程（3）分别给出了抽象和应用上的Tx的Tx在T，πk和k上的定义具有给定的形状，因为T，πk和k是线性态射（定理3.10中T是线性的）。最后，和上的Tx的定义由切丛函子的可加性得出用→表示→β→×→T的上下文闭包。引理4.1单类型摄动λ-演算的类型系统满足O. Manzyuk/电子笔记理论计算机科学286（2012）257267ΓT（λx. s）= λx。Txs：Tσ→Tτrs1N1=s2N2：τTs=Tt：Tσ→Tτr=s1+N1=s2+N2：σΓπk（ιk s）=s：σ图五. 微扰λ-理论规则rπk（ls）= 0：σ以下属性。(a) 若r; x：σ<$M：τ且r <$N：σ，则r <$M [N/x]：τ。(b) 若Γ; x：σ <$M：τ，则Γ; x：T σ <$TxM：T τ。(c) 若Γ π k（k N）：σ，则ΓN：σ。(d) 若Γ <$N：σ且N→NJ，则Γ <$NJ：σ。证据（a）及（b），然后直接归纳相应的打字判决的证明的长度。(c)明显(d)由（a），（b），和(c)因为类型派生是上下文相关的。Q为了便于证明应用归约规则保持了意义，这就是可靠性的真正含义，我们引入了微扰λ理论的概念。 设T是具有如下形状的判断的集合：即，Γ<$M：σ和Γ<$N：σ。 如果T是闭的，则称之为微扰λ-理论在图5所示的规则下（其中k，l∈ {1， 2}且k l），关于反射性、传递性和对称性的明显规则。等式（β）、（T）、（π）由归约规则施加。其余的规则说，平等关系是上下文。5范畴语义学在这一节中，我们证明了，像Ehrhard和Regnier [4]的Differentialλ-calculus的简单类型变体一样，简单类型的扰动λ-演算可以由Bucciarelli等人[3]的Differentialλ-范畴建模。我们在[9]中已经证明了任意的离散λ-范畴都具有一个规范的前推结构。微扰λ-演算将前推结构捕捉为一种句法操作。设C是一个二次λ-范畴。让我们在范畴C中定义前一节中的简单类型微扰λ-演算的解释。该定义类似于简单类型的微分λ-演算Γ λ（λx. s）N：τΓ λ（λx. s）N = s[N/x]：τ（β）Γ T（λx. s）：Tσ→T τ（T）r;x：σs=t：τΓλx. s = λx。 t：σ → τ（）Γs1=s2：σ→τΓN1=N2：σ（Ap）Γεs =t：σ x：τ/∈Γr;x：τs=t：σ（W）Γεs=t：σ→τ（TAp）Γεs =t：σ1×σ2Γπk s =πk t：σk（π）rs1=s2：σrN1=N2：σ（总数）Γs=t：σkΓiks =ik t：σ1×σ2（i）Γs：σΓs：σ（m）268O. Manzyuk/电子笔记理论计算机科学286（2012）257在[3]中定义的不同的λ-范畴中。类型解释如下：|α|= A，对于某个对象A，|σ×τ|为|σ| × |τ |得双曲正弦值. |σ→τ|为|σ| ⇒ |τ |.上下文的解释与往常一样：|∅|= 1和|Γ; x：σ|为|Γ | × |σ|.判断的解释是：从|Γ|到|σ|表示为|M σ|其定义如下：• |r; x：σ = π 2：|Γ |× |σ| → |σ|;|;• |r; x：σ =|y τ |Γ π π 1：|Γ| × |σ| → |τ |对于x / = y ;|for x /= y;• |r =ev|sσ →τ|Γ，|Nσ|你好：|Γ| → |τ|;|;• |(λx. s）σ→τ|1999年10月20日，|s τ|r; x：σ）：|Γ |→ |σ|⇒ |τ|;• |r =T|σ|、|τ |◦|sσ → τ|Γ：|Γ|→ T |σ|电子邮件|τ|;|;• |r = 0：|Γ| → |σ|;|;• |r =|s σ |Γ +|N σ |Γ：|Γ| → |σ|;|;• |r = Ik|s σk |Γ：|Γ| → |σ 1|×| σ 2|，k = 1，2;|, k = 1, 2;• |r = πk|s σ 1 ×σ2 |Γ：|Γ| → |σ k|，k = 1，2.|, k = 1, 2.唯一有趣的情况是Ts，这是我们真正想要的;其他情况是标准的。根据定义，|南卡罗来纳州|Γ = π|M|Γ，|N|你好。我们将省略|M σ|当没有混淆的风险时。给定一个不同的λ-范畴C，我们定义C的理论为：Th（C）={rM = T：σ|Γ M：σ，ΓN：σ，|M σ|Γ 为|N σ|}。我们要证明| · |对于简单类型的微扰λ-演算是合理的，即，Th（C）是微扰λ-理论。我们首先证明一些引理。引理5.1和5.2是标准引理。引理5.1|M|r; x：σ; y：τ= |M|r; y：τ; x：σsw.引理5.2若Γ ∈M：τ且x/∈ FV（M），则|M τ|r; x：σ= |M τ|1.引理5.3设Γ <$M：T（σ→τ）和Γ <$N：Tσ。然后|Γ = T（ev）|MT（σ→τ）|Γ，|NT σ|你好。|Γ⟩.证据扩展MN并应用解释的定义，我们发现，|门|r等于吉尔耶夫斯基π1 |M |Γ，π2π |N |Γ + π1 ev Tπ2 |M |Γ，|N|你好，evπ2 |M |Γ，π2π |N |Γ⟩⟩=ev（π1×π2） +π1ev（Tπ2×id），ev（π2×π2）|M|Γ，|N|你好。加数π1<$ev<$（T<$π2× id）等于π1<$T（ev）<$t<$（π2×id）=D（ev）<$t（π2×id）由T和T的定义。 我们的结论是|门|r等于ev |M|Γ，|N|其中h与T（ev）重合|M |Γ，|N|由等式（3）得到。QO. Manzyuk/电子笔记理论计算机科学286（2012）257269引理5.4（替换）设Γ;x： σM： τ和Γ CUP： σ。然后|r =|Mτ|Γ; x：σ_n|Γ|、|P σ|你好。|Γ⟩.证据证明是通过归纳M。唯一的新病例是MTs、Mks和Mπk s。 然而，他们是直截了当的。 比如说，|（Ts）[P/x] |r =|T= T |s[P/x]|由替换的定义和|·|，它等于T|S |Γ; x：σ_n|Γ|、|P|r=|Ts|Γ;x：σ_n|Γ|、|P|通过归纳和定义，|·|.|.Q引理5.5设Γ; x：σ <$M：τ。 然后|（TxM）Tτ|01 -02|M τ|r; x：σ）证据 证明是通过归纳M。• 我的天那么，一方面，|Txx|Γ; x：Tσ= |X|Γ; x ：Tσ= π2，由Tx的定义和|· |.另一方面，扩大定义|·|1.2π 2 = π2×π2，因为π2是线性的，所以我们得到T（|X|Γ; x：σ）0 × π1，id ×π2，它通过左可加范畴的性质约 化 为 π 2 .• My/=x。然后，一方面，由Tx的定义和|·|，我们有|Γ; x：T σ=|ι 2y |r; x：T σ = 10，|y |r; x：T σ = 0，|y |Γ π 1 π。|Γ◦ π1⟩.另一方面，扩大定义|·|T（π1）= π1×π1，因为π1是线性的，所以我们得到T（|y|2）x=0（|y|1）A（|y|（1）T=T（|y|1）π1×π1，π 2 × π 2，π 1×π2，π2×π2，π2|y|Γ） 0，π1的性质。这是从解释的定义开始的。|·|的|y|r是投影的合成，因此是线性的。2.1.7. T（|y|（r）= |y|Γ×|y|I.此外，每个线性态射都是可加的，因此，特别地，|y|r=0。断言如下。• M. 通过T x的定义和引理5.3，我们有|Tx（sN）|Γ; x：Tσ=|Γ;x：Tσ=T（ev）|Txs|r;x：Tσ，|Tx N|r; x：T σ τ。|Γ; x: Tσ⟩. 根据诱导假说，|Txs|01 -02|S|r; x：σ）τ t和|TxN |01 -02|N |r; x：σ）因此，我们认为，|Tx（sN）|（1）A（1）A（2）A（3）A（|S|（1）x = 0，y =0。|N|（1）A（x）=A（x）= A（x）=A（|S|（1）x=0， y=0。|N|r;x：σ）t，其中h等于T（ev）T（|S|r;x：σ，|N|r;x：σ）t=T（ev |S|r;x：σ，|N |2）x = 0（|SN|由引理3.8，T的函性，以及|·|.• M（λy. s）τ1→τ2，其中通过α变换，我们可以假定x不同于y。 根据Tx的 定义 ，|·|，我们有|Tx（λy. 个）|Γ; x：Tσ=|⟨λy. π1（Txs），λy. π2（Txs）π|Γ; x：Tσ= π|λy。 π1（Txs）|r; x：Tσ，|λy。 π2（Txs）|Γ; x：Tσ=π Λ（π1π|Txs|r; x：Tσ; y：τ1），Λ（π2π|Txs|r; x：Tσ; y：τ1）根据引理5.1，这可以变换为<$Λ（π1<$|Txs|r; y：τ1; x：Tσsw），Λ（π2τ|Txs|1、A：B：C：D：|S|1）A（x = 0，y = |S|r;y：τ1; x：σ）t sw）by归纳假说 命题3.13，方程（1），以及270O. Manzyuk/电子笔记理论计算机科学286（2012）257T允许我们把这个表达式写成如下：2019- 01-2200：01：01 |S|r; y：τ1; x：σ）<$T（sw）<$tJ<$（t × id）），2019 - 02-2201：01：02 |S|r; y：τ1; x：σ）<$T（sw）<$tJ<$（t × id））<$10 -12 - 13 -2000- 02 |S|1）A（1）A（2）B（3）C（|S|Γ; y：τ1; x：σ <$sw）<$tJ）<$t <$10 -12 - 13 -2000- 02 |S|1）A（1）A（2）B（|S|r; y：τ1; x：σ sw）tJ）t。第3.9节：最后一个表达式等于T（|S|（1）（2）（3）（4）（5）（6）（7）（8）（9）（10）（11）（10）（11）（11）（10）（11）（11 |S|（1）A =（1）A =（|λy。 S|r;x：σ）由引理5.1证明。• 我的天。 根据Tx的定义，|·|根据归纳假设，|Γ; x：T σ=|T（π 1（T x s）），T（π 2（T x s））|Γ; x：T σ=|Txs|Γ;x：Tσ，T<$π2<$|Γ;x:Tσ,T◦π2◦|Γ;x：Tσ=（T×T）|Txs|（1）A=（1）A=（1）A=（|S |r; x：σ）|Γ; x: σ) ◦ t. 根据定理3.10，态射T是线性的。因此T×T=T（T）由引理3.7。 我们的结论是|Tx（T s）|（1）T= T（1）T（|S|r; x：σ）t = T（T|S|2）x= 0（|T s|Γ; x：σ）的函数性。• 其余的情况（M0，Ms+N，Mks和Mπk s）是直接的。引理已被证明。Q定理5.6设C是一个 奇异λ-范畴. 那么Th（C）是微扰的λ理论证据 我们必须检查Th（C）是否在图5的规则下闭合。（B）根据定义|· |，我们有|（λx. s）N|2016- 05 - 25 00：00：00（|S|r; x ：σ），|N|你好。另一方面，根据引理5.4，|s [N/x] |r= |S|Γ; x：σ_n |Γ|、|N |1999年，张晓刚（|S|r; x：σ），|N|（2）。（三）以德为本。| · |，我们有|（T（λx. s））Tσ→Tτ|01 - 02|s τ|r; x：σ）。根据引理5.5，|（λx. Txs）Tσ→Tτ|1999年10月20日，|（Txs）Tτ|T（x）=T（|s τ|（1）A：A|s τ|r; x：σ），命题3.11。（三）以其为中心，|·|，我们有|π k（π l s）|r= π k l |S|r，它等于|如果k = 1，则为r，否则为0。|Γ if k = l and to 0 otherwise.弱化规则（W）由引理5.2得出。对称性、自反性和传递性从Th（C）的定义中显而易见。其余的规则来自解释的定义。Q6结论和今后的工作我们提出了一种新的微积分--微扰λ-微积分，它与Ehrhard和Regnier的微分λ-微积分[4]有一些相似之处，但它是基于前推的微分几何思想而不是导数的思想.我们相信这个特性使得微扰λ-演算非常适合于前向AD的推理。