内涵的隐式微积分：程序分解与组件构造

可在www.sciencedirect.com在线获取理论计算机科学电子笔记336（2018）207-222www.elsevier.com/locate/entcs类型化内涵λ演算中的自引用巴里·杰伊艺术智能中心软件悉尼科技大学悉尼澳大利亚摘要Intensional Algorithm在Algorithm中加入了Intensional Combinator以方便分析。特别是，它们用于将数据结构和程序分解为可使用的组件将抽象转换为组合子。 本文介绍了如何构造一个内涵的隐式微积分使用不超过F系统的类型。甚至用于访问程序语法的引号函数也可以可以定义和类型化，它的逆也可以：演算支持类型化的自引用。因此，可以在程序分析和程序执行之间自由地交替。所有结果的证明均已在Coq中验证保留字：微积分，组合子，自解释，类型论1引言编程语言的默认实现是用另一种较低级别的语言编写反过来，这可能被证明是一种中间语言，通过一系列翻译，最终实现在机器代码中。为了避免这种链，提供一个自解释器是常规的（参见[21，25，2，22，23]和[4，28，18]和[5，6，7]），在其中语言本身被实现，因此可以分析自己的程序。因此，程序语法在微积分中有两种解释。标准项产生一个可约项，所有可能的评估策略都在发挥作用。新颖的一种是引用，它将程序表示为一种数据结构，可供分析。最简单的分析形式仅仅是取消对程序的引用，以恢复标准的解释。更一般地说，分析可以用来优化，或施加一个评估策略，然后转换为可执行文件。让我们考虑报价应满足的一些理想1电子邮件：Barry. uts.edu.auhttps://doi.org/10.1016/j.entcs.2018.03.0241571-0661/© 2018由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。208B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207首先，对可以进行的分析的性质不应有任何限制。它不足以支持一个单一的自我解释器，或一个小的分析套件。例如，它应该可以决定程序的语法平等，或执行死代码分析。第二，当语言由一个并发演算（例如λ演算[1]）表示时，优化的机会最大化，因此可以自由地操纵评估策略。第三，微积分应该是类型化的。这提供了对整个方法的健全性检查。特别是，通常通过在类型层次结构中上升一个级别来对解释的每个阶段进行建模。这在本质上是困难的，并且经常限制可能的分析的性质。换句话说，如果分析是在源语言中完成的，那么类型化编程语言的所有常见参数也适用于此。第四，分析应该是动态的，而不仅仅是静态的。例如，在分阶段计算[27，9]中，一个阶段的计算结果可以在下一个阶段进行分析。更一般地说，这是动态程序分析所必需的。尽管这一挑战意义重大，但在自我解释的背景下，它通常被认为太难了从λ演算的观点来看，甚至不清楚这种自引是否有意义。毕竟，引用不能作用于可归约项，因为归约改变了引用产生的句法的性质。解决方案是识别具有封闭范式的程序，只有当它们应用于参数时，才开始减少。然而，即使在这个受限的领域，这个任务也超出了纯λ-演算，因为它本质上是外延的：没有纯λ-项可以以统一的方式揭示闭正规λ解决方案是以能够查询术语内部结构的组合子的形式向λ演算添加内涵。 最简单的系统是SF-演算[16]，它的因子分解算子F能够暴露复合项的分量。最近的工作[14]引入了λSF-演算，其中抽象可以分解，就像组合子一样。本文延续了这一观点发展，引入一个内涵λ演算，• 是连续的• 是强类型的• 定义程序平等，• 定义了自我引用和自我解释。尽管有这种表现力，实际的机器是比较轻的重量。这些类型由System F[10]的类型给出，并使用了表示类型抽象和实例化的子对象。这些项是通过将以下运算符添加到λ演算中来给出的：O：：= S|K|一|Y|G| DS| DK| DA| DY| DE| DG|DG.运算符S和K是标准的。算子A是新的，具有约简B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207209规则AMNP−→MNP。也就是说，A是一个三元恒等运算符：给定三个参数，它表现为恒等运算符。它可以用S和K来定义，但在控制评估方面起着重要作用，特别是定点。定点运算符Y不是标准的。它的归约规则YM−→M（AY M）插入A的一个副本以防止不必要的归约。我们可以添加一个算子I，但让我们将其定义为SKK，因为对于任何P和Q，我们有SKPQ−→KQ（P Q）−→Q，这表明SKP是任何项P的恒等函数。S、K、A和Y是外延运算符，之所以这样称呼是因为它们不查询其参数的内部结构。它们的类型很容易从它们的归约规则中猜测出来。其余的操作符都是内涵式的;键入它们有点难度。运算符E测试运算符的相等性其主要类型是Ty [E]= λX。很好。Z.X→Y→Z→Z它相当于X。X→Y→Bool，其中Bool被定义为Z →Z→Z。请注意，被比较的运算符可能有不同的类型，例如ESK与其约简KI具有相同的类型。算子G是SF-演算中因子分解算子的一个变体。其唯一的归约规则是GMP−→ MP |[P（P是可因式分解的）]其中P|而[P]是P的左分量和右分量。如果P是，比如说，SP1P2，那么它的分量就是SP1和P2.由于需要分解抽象，可分解形式的完整说明变得更加复杂。规则中的项M必须是足够多态的，以处理P的分量，不管它们的类型证明是什么。因此，G的主要类型是Ty [G]= πX。很好。（瑞士）（Z → X）→ Z → Y）→ X → Y。因此，如果上述规则中的P：X具有分量P1：Z和P2：Z→X，则MP1P2：Y，条件是M：Z. （Z→X）→Z→Y）→X→Y。其余的运算符是对应于我们已经遇到的基本运算符的情况运算符。每一个都有一对归约规则。比如我们有DS MNS−→MDS MNP−→ NP（PS可因式分解）。它表示一个模式匹配函数，将S映射到M，并将N应用于其他任何内容。其类型为Ty [DS] = ΔX。Ty[S]→（Y.Y →Y）→X→X注意在DS的主类型中使用了S的主类型。 用一个算子D来代替case算子族是很有吸引力的，它的应用会产生DS，等等。然而，D的类型需要引用排除其他类型的算子的主类型的方法。虽然这是可能的，但它需要对类型系统进行添加因子分解支持一种分而治之的程序分析方法，210B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207很直接例如，自引用可以被非正式地描述为一个模式匹配函数，它将运算符映射到它们自己，以及MN到A（引用M）（引用N）形式的复合词。作为微积分的一项，它由下式给出：引号= AY（λq.λp.Eppp（G（λx.λy.A（qx）（qy））p）.这是一个封闭的范式，因为A的应用阻止了定点运算符Y的归约，直到提供了一个参数。E用于检查p是否是运算符。如果不是，则G用于因式分解p并递归。此外，它具有类型报价：X.X→X.本文中的所有证明都使用Coq证明助手[3]进行了验证本文的结构如下。第一部分是引言。第二节介绍化合物。第三节介绍了微积分的归约规则第四节介绍了微积分的类型。第5节展示了如何定义和类型的平等的程序。第6节定义了引用和取消引用。第7节讨论了Coq中的验证。第8节考虑相关工作。第9节得出结论。2可因式分解形式这一节将发展必要的机制来描述下一节给出的归约规则争论的焦点是内涵算子的归约规则有副条件，要求自变量是可因子分解的形式，即算子或复合算子。后者包括一些抽象，其右组件由星抽象给出。因此，业务的顺序将是：星形抽象;组件;然后是复合。2.1星抽象术语的语法在第1节中给出。M关于x的星抽象λ<$x.M定义为：λx.x=Iλx.y = Ky（y/=x）λ<$x.O = KO（O为算子）λ<$x.λy.M = A（λx.λ<$y.M）λ<$x.MN = S（λx.M）（λx.N）.这个定义修改了组合子M的λx.M的传统定义（参见，[11]以两种方式。首先，当主体是应用MN时，结果使用λx.N而不是λx.N。为了理解为什么这是必要的，考虑λx.S（KN1N2）。现在S（KN1N2）不是一个Redex，所以将S与KN1N2分开是安全的，但是λ≠x.KN1N2破坏了RedexKN1N2.因此递归调用λx在这里是不 安 全 的 。 第 二 ， 当 身 体 是 抽 象 的 λy 时 ， 需 要 有 一 个 λx 的 规 则 。 结 果 是 A（λx.λ<$y.M）而不是λ<$x.λ<$y.M，因为跟踪信息要求每次只删除一个抽象，即最里面的抽象。B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207211下面是一些简单的星形抽象的例子。在SKI-演算中，λ-抽象λx.λy.y可以表示为：λx.λ y.y=λx.I=KI其中λ用于以传统方式将抽象转换为组合子在λSF-演算中，λx.λy.y已经是一个闭规范型。然而，它的因式分解将引入λ<$x.λy.y，其计算如下：λ<$x.λy.y = A（λx.λ <$y.y）= A（λx.I）。这消除了最内在的抽象，就像SKI演算中计算λx.λ y.y的第一步一样第二个因子分解揭示了λx.SKK = S（λx.SK）（λx.K）。进一步的因式分解消除了剩余的抽象以产生组合器S（S（KS）（KK））（KK）当应用于项M和N时，其简化为N，就像原始的抽象一样。当然，这并没有利用标准优化，其中λ<$x.I利用x在I中不是自由的这一事实来产生KI。在λSF-演算[14]中已经解决了这个优化问题。2.2组件为方便起见，对任意项给出了分量的定义，不管它们是否证明是复合的左分量M|项M的右分量[M]定义如下（λx.M）|=左腹肌（明尼苏达州）|= MM|= KM（否则）[（MN）=N[（λx.M）=λ<$x.M[M=M（否则。）其中abs left=I用作抽象的左分量。关于abs left的关键点是，如果它是应用程序IN的左组件，那么该应用程序是一个redex，因此不会被证明是一个复合。一般来说，sans-serif中的单词，例如abs left可以用来命名微积分的特定术语，以及元变量M和N等。 因此，GMO将简化为M（KO）O。如果像通常那样，这是不可取的，那么必须首先使用E来识别它们，就像前面介绍的引用的例子一样2.3化合物在组合演算中，复合算子就是部分应用算子。例如，在SF-演算中，复合词都是SM或SMN或FM或FMN形式的项。这些形式在λSF-演算中也是复合的，就像所有其他部分应用的算子一样，例如KM和EM形式的算子，DSM N. 所有其他复合将是抽象λx.M，其分解为：212B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207感应状态_值：=| Reducible：status_val| Lam：nat-> status_val（* 活动变量 *）| Active：nat -> status_val（* 活动变量 *）| Ternary_op（* S，A*）| Binary_op0（* K，0个渴望参数*）| Binary_op2（* E，2个渴望参数*）| Binary_op1（* G，1 eager argument*）| Ternary_op1（*DO*）| Unary_op（*Y *）| Lazy2（* 需要两个参数*）| Lazy1（* need one arg*）| Eager2 (* DOM *)| Eager（*EO *）.Fig. 1. Coq中的状态值安全，因为M已经是可因式分解的，或者M的最外层约简等待x的实例化。反过来，这需要跟踪哪些变量需要值，以便进行头部减少，即哪些变量在项中是活动的 更一般地说，每个术语都有一个状态，它跟踪确定术语是否可分解所需的所有信息。自由变量和内涵运算符之间的相互作用使这变得复杂，因为后者渴望它们查询的参数为了避免转录错误和其他问题，最安全的方法似乎是按照Coq实现中的定义给出定义状 态 值如图1所示。Reducible表示存在头部减少。Lam n表示其活动变量具有de Bruijn指数n的λ-抽象。Active n表示其活动变量为n但不是抽象的项相反，它要么是第n个其他状态值用于以一种自解释的方式对可因子分解的形式进行术语状态的定义见图2。为了节省空间，程序被分成三列，以便连续读取。例如，第二列以App M1 M2的情况开始，在第一列开始的对M的模式匹配中运算符的状态是三进制运算符、二进制运算符0、二进制运算符2、二进制运算符1或三进制运算符1中的一个。现在，如果一个术语的状态是Lazy2、Lazy1、Eager 2或Eager中的一个，则该术语是复合词。 如果它是一个复合或运算符，则它是可因子分解的。虽然这一切都很难理解，但值得注意的是，纯λ-演算的所有闭头范式都是复合的。这里有一些化合物的例子x.xy的主体有x是有效的。λx.λy.x的主体有x是有效的。λx.λy.y的体是一个复合体。λx.G的体是可因式分解的。λx.Gx的主体是可因式分解的。λx.GMx的主体有x活动的，因为G是一个内涵算子，需要知道x的值才能约简。λx.λy.GM（GNx）的体有x是活性的。 Exy有x活动。 EOy有y活动。 E（SK）y的状态是可还原的。如果M是可因子分解的且M−→ N，则M |− → N|且[M−→ [N.也就是说，没有赎回是打破了采取组件的可分解形式。把B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207213定点状态（M：lamSF）：=将M与| Refi=> Active i| Op Sop => Ternary op| Op Aop => Ternary op| Op Kop => Binary op0| Op Eop => Binary op2| Op Gop => Binary op1| Op Uop => Binary op1| Op Yop => Unary op| Op=> Ternary op1| 绝对值M1=>匹配状态M1，| Reducible =>Reducible| Lam 0 =>Lazy1| Lam（S n）=> Lam n| Active 0 =>Lazy1| Active（S n）=> Lam n|=>Lazy1end| App M1 M2 =>匹配状态M1，| Reducible =>Reducible| Lam=> Reducible| 活性n =>活性n| Ternary op => Lazy2| Binary op0 => Lazy1| Binary op2 =>匹配状态M2，| Reducible =>Reducible| Lamn=>Active n| 活性n =>活性n|Ternary op| Binary op0| Binary op2| Binary op1| Ternary op1| Unary op => Eager|=> Reducibleend| 二进制op1 =>渴望| Ternary op1 => Eager2| Unary op => Reducible|Lazy2=> Lazy1| Lazy1 =>Reducible| 挑战者2 =>渴望| 渴望=>匹配状态M2，| Lamn=>Active n| 活性n =>活性n|=> Reducibleend结束结束图二.Coq中的术语状态（λx.M）N−→{N/x}MSMNP−→MP（NP）EOO−→KEOP−→KI（PO是可因子分解的）KMN−→M AMNP−→MNPYM−→M（AYM）K2O→K2O（K2O）（P是一种化合物）GMP−→MP| [P（P是可因式分解的）]DOM NO−→MDOM NP−→NP（P/=O是可因式分解的）图三. 减小规则另一种方法是，有一个导出的归约规则，（n）M−→N（λx.M是可因式分解的）λx.M−→λx.N从形式化的观点来看，更重要的是约简规则上的边条件是可判定的。这里，副条件将取决于具有可因式分解形式的算子的等式，以及是否为可因式分解形式。后者由Coq中的函数给出，因此保证终止。3减少图3给出了内涵λ -演算的归约规则。对应的- ing同余也记为−→，其自反传递闭包为−→。214B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）2073.1基本结果定理3.1 λ SF-演算中的约化是连续的。范式被定义为变量、运算符、范式的抽象和应用MN，其中M和N都是正规的，并且MN的状态是不可约的。定理3.2（不可约正规型）一项是不可约的当且仅当它是正规型。程序是一个封闭的范式。如果目标是分析一个开放范式，那么首先需要绑定它的所有自由变量。定理3.3（程序是可分解的）所有程序都是可分解的 形式。因此，GMP形式的任何闭项都必须减少。这是一种进步的3.2Unstar作为使用中的机器的一个例子，让我们展示如何反转星抽象，如何将λx.M转换为λx.M。模式匹配帐户由下式给出让rec unstarx=匹配x与| O O| Ax ⇒ abs A unstar x| Kx ⇒ abs K x| Sxy ⇒ abs S x y其中，abs S=λg.λf.λx.gx（fx），abs K=λx.λy.x，abs A=λu.λx.λy.u（xy）。例如，|KxabsKx用具有相同类型的项abs K更新运算符K。类似地，S由abs S更新，A由abs A更新。微积分的相应项是unstar=AY（λu.G（DA（abs Au）（DKabs K（G（DSabs SI））定理3.4（unstar star）unstar（λ<$x.M）项简化为λ x. M。3.3外延性在数学上，两个函数f和g是外延等价的，如果它们具有相同的图形。对于一元函数，这意味着fx=g x对所有x。在λ-演算中，通过添加η-归约规则来捕获λx.f x−→f如果x在f中不是自由的。当把它加到基本的λ-演算上时，仅用β-规则，我们就得到了λβη-演算，它是连续的。定义β η =βη是由β-归约和η-归约导出的λ然而，请注意，将η-规则添加到λSF-演算中是不合理的，因为它改变了项的状态B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207215一个更有用的关系是通过排除内涵运算符的规则（图3的第二列中）来获得等价关系E。定义项M和N在外延上等价，如果M∈N。例如，我们有以下定理。定理3.5（星等价绝对值）λ<$x.M<$eλx.M对所有项M。4打字输入内涵λ-演算有三个关键挑战：(i) 输入因式分解运算符，在本例中为G。(ii) 因式分解类型抽象和应用。(iii) 键入相等运算符E和大小写运算符。在解决这些挑战时，我们的目标是保持类型系统尽可能简单首先考虑T型GMP，其中P：U是可因式分解的。 必须有一个Z使得[P：Z，所以P|：Z → U。因此，M必须有类型（Z→U）→Z→T。此外，无法预先确定类型Z。因此，M必须是多态的，是量化类型的。（Z→U）→Z→T，G：（我是Z。（Z→U）→Z→T）→U→T。更一般地，我们有G：是的。很好。（瑞士）（Z → X）→ Z → Y）→ X → Y。对多态性的内在需求，以及函数类型中类型变量的量化，意味着无论是简单类型还是Hindley-Milner系统的类型都不够表达：类型系统必须至少像SystemF一样表达。事实上，这已经足够了。第二，存在表示类型泛化和实例化的挑战。在最初的系统F[10]中，这些类型的变化在术语中是明确的。 例如，如果t：T，则ΛX.t：<$X.T，然后（ΛX.t）U：{U/X}T。然而，如果这样的操作是显式的，那么不清楚如何分解atU形式的类型应用。特别地，如果它被认为具有分量t和U，则类型U也必须是独立的项。这是一个有趣的可能性，但它将使我们远远超出系统F的简单性。相反，让我们使类型级别的操作隐式化，这样类型函数就可以修改术语的类型而不改变术语本身。这样做的基本机制已经众所周知，但需要为我们的目的做一些小的修改例如，考虑一个复合PQ：T，其中Q的类型为U，P的类型为U→T。进一步地，假设类型被推广为PQ：X.T。现在，我们有Q：<$X.U，因此因式分解要求P：（<$X.U）→（<$X.T）。解决方案是执行以下操作：时间：U→T（contravariance）P：（P.P.：P.X. （X.U）→ T（推）。► P：（X.U）→（X.T）216B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207X.TX/∈UX.U→TU1型T2-U2T1→T2→U1→U2TUX.TT2双排U2T1→T2T1 →U2乌布X.U（x：U∈Γ）见图4。 类型实例化（Type instantiation，简写为Pushing）T：U→Tu：UΓ，x：Ut：TΓx：UO：Ty[O]tu：TΓλx.t：U→TT t：TTt：TT：T（X/∈Γ）中文（简体）中文（简体）中文（简体）图五. 类型推导Ty [S] = πX。很好。我是Z （X→Y→Z）→（X→Y）→（X→Z）Ty [K]=X。Y.X→Y→XTy [A] = λX。很好。（X→Y）→X→YTy [Y]=X。（X→X）→XTy [E] = λX。很好。Z.X→Y→Z→ZTy [G]= πX。很好。（瑞士）（Z→X）→Z→Y）→X→YTy [DO] X. Ty[O] →（CHY.Y→Y）→X→X。见图6。 运算符类型第一个使用函数类型的逆变和类型变量实例化。第二个是类型变量X的一般化。第三步不是很标准，因为它涉及到在函数类型上推送一个量化器，使用规则，第十章（U→T）U→ X.T（X/∈U）其中X在U中不是自由的。图4中给出了用于将类型T实例化为类型TJ以及用于将类型T推送为类型TJ的规则的细节。类型判断的形式为Γt：T，其中Γ是上下文，t是项，T是类型。反过来，上下文Γ是不同术语变量的集合，类型xi：Ui.图5中给出了类型派生规则。其中的所有上下文都被假定为格式良好。每个项形式都有一个派生规则，加上三个隐式操作类型的规则，通过实例化，推送，或从类型T推广到它的量化T。剩下的就是输入操作符了。 每个操作符O都有一个指定的类型Ty [O]，如图6所示。类型派生的表达能力由以下定理说明定理4.1（unstar型）unstar：<$X.X→ X.定理4.2（归约保持导子）若Γt：T且t−→tJ，则T.证据考虑（λx.t）u−→ {u/x}t。这保留了类型，因为替换保留了类型。应用于抽象的F规则 其他的案子都是例行公事。QB. Jay/Electronic Notes in Theoretical Computer Science 336（2018）2072175平等通过几个关键的例子来说明整个方法的表达能力本节介绍一个查询示例，即相等。下一节考虑一些更新，即引用和取消引用。从定理3.3可以得出，等式可以通过比较运算符和化合物来确定。算法如下。原子平等性由E决定。运算符和复合运算符永远不相等。如果化合物的组分相同，则化合物是相等的。非正式地，相等性由以下嵌套的模式匹配函数给出：假设rec等于x y=匹配x与| 奥苏埃瓦| x1x2匹配y，| 奥基| y1y2⇒ (equal x1y1) (equal x2y2) (KI).微积分的相应项是相等=AY（λe.λx.λy.Exx（Exy）（G（λx1.λx2.Eyy）（G（λy1.λy2. （ex1y1）（ex2y2）（KI））y））x））。定理5.1（equal type）equal有类型Ty[E]。定理5.2（相等的程序）对所有程序M都等于M M−→K。定理5.3（不等式）对所有不同的程序M和N，M N −→ M KI相等。证据证明是通过归纳M的秩，如Coq实现中所定义的。当M是一个抽象而N是一个应用程序时，唯一感兴趣的情况就会出现。现在N的左分量不可能是abs left，因为abs left的任何应用都减少了，因此M和N的左分量不可能相等。Q6引用和取消引用第1节中对引用的描述是一个轻微的简化，因为它不是从引用的元函数开始的，这里称为mquote。作为模式匹配函数，mquote由下式给出：let rec mquote=| O O| λx.M ⇒ A(mquote abs left)(mquote (λ∗x.M))| MN ⇒ A (mquote M)(mquote N).当然，abs left和λx.M是λx.M的分量，因此，从因式分解的角度来看，上面的第二种和第三种情况可以通过一行代码来处理。因此，我们有以下定理。定理6.1（引用是可定义的）程序的引用可以用引用来定义。定理6.2（引用类型）引用有类型<$X.X→ X。218B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207定理汇合_lamSF_red定理不可约_当否_正规定理程序_are_factorable定理unstar_star定理star_equiv_abs定理unstar_type定理归约_保持_导出定理等价型定理equal_programs定理equal_programs定理quote_is_definable定理quote_typeTheorem unquote_typeTheorem unquote_quote见图7。 Coq中的定理后一个定理意味着没有类型信息已经丢失在quotation。类型也很简单。但是，使用引号代替源程序不会产生类型错误。 如果这是一个问题，解决方案将 可以使系统稍微复杂一些，例如，通过给运算符A类型[X→Y] →[X] →[Y]，其中[T]是一个新的类型形式，T的表达式类型。这个定理也说明了类型X.X→X支持许多有用的程序，包括所有的数据库更新，因此比单位类型更丰富。因此，数据类型必须单独引入函数类型，就像在实践中所做的那样。例如，给定一种自然数，定义一个函数来计算程序的大小，或者它的哥德尔数，这是一个例行程序。unquote的非正式解释同样简单，由模式匹配函数let rec unquote=| O O| A(quote abs left) N ⇒ unstar (unquote N)| AMN ⇒ (unquote M)(unquote N).在取消引用AMN形式的项时，有两点值得注意。首先，泛型等式（以及最终的E）被用来决定非引号M是否为绝对左。第二，DA被用来用I的应用代替A的应用。定理6.3（非引号型）非引号型有<$X.X→ X。定理6.4（非引号）对于所有的程序M，非引号（引号M）归结为M。7在Coq本文中的所有证明都已使用Coq证明助手[3]进行了验证，如补充材料[15]中所提供的。为了便于参考，在这两个地方使用了B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）2072198相关工作8.1自我解读首先，请注意，到目前为止，任何类型的自解释器都不支持自引用。最接近的先前的工作涉及的自我解释的类型，conciliuent结石。Jay和Palsberg[18]基于SF-演算为类型化组合演算创建了自解释器。缺乏第一类λ-抽象是它的主要局限性，在这里克服了。而且，它的类型相等的方法比这里更通用，但代价是给类型系统引入了一些模糊性。通过引入案例操作员来处理更新，系统得到了简化，而不会丢失任何激励性的关于类型化自我解释的最新研究是Brown和Palsberg的[5，6，7]。他们构造了系统Fω的类型化自解释器。这是使用类型层次结构的一个很好的例子，其中一级程序的引用在下一级被键入。 相比之下，这里的系统一个可扩展的类型层次结构。8.2部分求值具有封闭范式的程序的识别提出了λ-演算部分求值的新方法，包括静态和动态[20]。在类型化语言的部分评估中，一个运行的主题是消除与类型标记相关的开销[24]，以寻求Jones最优性[29，8]。在我们的设置中，标记的类似物是在引用的定义中使用A和abs。 有一个最小的意义上，这些携带类型信息，同样的意义上，aλ确实如此，但总的来说，这些类型在表示中几乎没有出现。也许解释开销可以通过应用unquote完全消除，这样，在这个意义上，琼斯最优性将遵循这个更一般的原则。8.3分级评估分阶段的评估[27，9]允许程序执行的每个阶段分析后续阶段的syn-tax由于程序现在可以用数据结构来识别，阶段之间的划分不再是基本的，因为人们可以在闲暇时引用和取消引用。8.4高阶抽象语法内涵性和引用在高阶抽象句法中发挥作用（参见[26]），但与内涵λ演算的关系尚未被探索。8.5程序分析上面的例子说明了如何在封闭的范式上执行从查询和更新构建的分析，而不需要任何元级别的操作，如引用，并且这是在一种类型系统完全标准的语言那么，问题是，将这些程序与220B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207封闭的正规形式要彻底解决这个问题，需要开发一种实际的编程语言，而不是微积分。然而，手头的证据是有启发性的。首先考虑对封闭术语的限制。这个限制不会引起很大的争议，但是如果对开放项感兴趣，则可以通过分析相对于自由变量抽象得到的封闭项来处理。这就简化了上面讨论的问题现在考虑对正规形式或强正规化项的限制。 与通过添加定点算子而获得的系统F的扩展进行比较是有益的。在标准账户中，任何包含定点算子应用的项都将有无限个归约序列。然而，在用我们的A和Y扩展的系统F中，我们可以定义递归函数，这些递归函数在应用于参数之前没有无限约简序列。事实上，通过添加合适的内涵运算符，应该可以在强规范化演算中支持大量的查询和更新，类似于查询演算[13]。以这种方式，自执行器可以是程序，并且因此可以是自应用的。8.6计算基础这项工作继续发展比λ-演算更具表达力的并发演算，包括模式演算[12，17，13]，组合演算SF-演算[16，18]和无类型λSF-演算[14]。各种模式演算支持统一应用于任意数据结构的查询，但不支持到λ-抽象SF-演算支持统一应用于任意闭合范式的查询。λSF-演算将这种方法扩展到λ-演算。它最清楚地暴露了纯λ-演算的局限性，它不能支持内涵计算和外延计算。由于这与计算性质的传统解释相冲突，我们特别小心，通过验证Coq[3]中的结果，并在λ-可定义性的冲突解释中查明传统错误的来源[19]。9结论λ-演算最大的优点和缺点是它是可拓的。隐藏λ-抽象的主体支持关注点的分离，支持模块化程序开发，并允许将数据结构表示为更高阶的多态函数，比如在系统F中然而，意图性是程序分析的核心：我们必须能够在λ之下进行分析。λ演算中自我解释的所有困难，特别是在类型化演算中表现出来的困难，都源于这个根源。因此，解决方案是从一开始就添加内涵，从一个因子分解算子开始，比如G，这样程序就可以通过一种普遍的分而治之的方法。类型化引入了一个微妙的挑战：如何利用在分析过程中获得的类型信息。按照数据库方法，我们将注意力限制在两种分析上，即查询和更新。B. Jay/Electronic Notes in Theoretical Computer Science 336（2018）207221使用操作符E可以很容易地键入更新，而使用与每个基本操作符O相关联的情况操作符DO可以键入更新。这种方法已经通过考虑程序相等性（查询）以及引用和取消引用程序的更新来说明。所有的定理都在Coq[15]中得到了验证。以这种方式，所有基于查询和更新的程序分析都可以被类型化，并且这只使用系统F的类型。将引用定义为一个术语的能力，支持自引用，意味着程序分析可以动态地执行，而无需进一步的麻烦。确认感谢匿名推荐人提供的有益建议。引用[1] H. 巴伦德雷 Lambda演算：它的语法和语义。 北荷兰，1984年。 修订版。[2] H.巴伦德雷lambda演算中的自我解释。J. Functional Programming，1（2）：229-233，1991.[3] B. Barras，S. 布廷角Cornes，J. 当然，J. - C. Fillispanatatre，E. 给我，H。 Her belin，G. 休特角穆尼奥斯，C. Murt hy，C. P是nt，C。 Paulin-Mohring，A. S abi和B. 沃纳 《辅助程序参考手册》：第6.1版。研究报告RT-0203，INRIA，1997年5月。网址https://hal.inria.fr/inria-00069968。项目成本确认[4] A. Berarducci和C. B？ohm. 一个有正规形式的微积分的自我解释者，85-99页。施普林格柏林海德堡，柏林，海德堡，1993年。ISBN 978-3-540-47890-4。[5] M. 布 朗 和 J. Palsberg 。 吉 拉 德 系 统 中 的 自 我 表 征 。 第 42 届 ACM SIGPLAN-SIGACT Symposium onPrinciples of Programming Languages，POPL'15，第471-484页，纽约，美国，2015年ACM。ISBN978-1-4503-3300-9。[6] M.布 朗 和 J. Palsberg 。突 破 规 范 化 障 碍 ： f-omega 的 自 解 释 器 。第 43 届 ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languages，POPL'16，第5-17页，纽约，美国，2016年ACM。ISBN 978-1-4503-3549-2。[7] M.布朗和J. Palsberg。 通过内涵类型功能进行类型化自我评价。 第44届ACM SIGPLAN Symposium onPrinciples of Programming Languages，第415ACM，2017年。[8] O. Da nvy和P. E. 我的天啊。 标记，编码，和琼斯最优性，第335-347页。 施普林格柏林海德堡，柏林，海德堡，2003年。[9] R. Davies和F.芬宁 分阶段计算的模态分析。J. ACM，48（3）：555-604，May2001. ISSN 0004-5411。[10] J. - Y.吉拉德 ， Y 。Lafont 和 P. Taylor 。 证明和 类型。 理论计算 机科学中的Tracts in TheoreticalComputer Science剑桥大学出版社，1989年。[11] R.亨德利和J·塞尔丁。介绍组合器和lambda演算。剑桥大学出版社，1986年。[12] B. 杰 模 式 演 算 。 ACM Transactions on Programming Languages and Systems （ TOPLAS ） ， 26（6）：911[13] B. 杰模式演算：用函数和结构计算。Springer，2009年。[14] B. 杰作为λSF演算中的数据结构的程序电子笔记理论计算机科学，325：221ISSN 1571-0661。第三十二届编程语义学数学基础会议（MFPSXXXII）。[15] B. 杰2017年1月，Coq中的Typed Lambda Factor Calculus证明库htt