R-演算：基于组件的形式模型及重构特征

理论计算机科学电子笔记135（2006）49-59www.elsevier.com/locate/entcs重构演算（延伸摘要）Sonia Fagorzi2和 埃琳娜祖卡3DISI热那亚大学Genova，意大利摘要我们提出了一个简单的演算，称为R-演算（为形式上，这是通过引入微积分配置的基本术语来实现的，粗略地说，这些配置是由命名组件的（开放的，相互递归的）集合组成的对，表示在这些组件的上下文中运行的程序的术语。 R演算最初被开发为大型编程的形式模型，其中计算对应于在软件组件的某些上下文中运行的应用程序，并且元级别的操作对应于动态加载、更新或一般操纵这些软件组件而不停止应用程序的可能性。然而，微积分也可以编码小问题中的编程，因为配置结合了lambda抽象（第一类函数），记录，具有相互递归定义的环境和模块的特征。我们陈述了演算的连续性，并定义了一个按需调用策略，该策略导致了按需调用演算的泛化，包括重构特征。保留字：模块演算，重新配置，按需呼叫策略。介绍在过去的几年里，大量的精力投入到开发内核模块/片段演算[13，12，5，11]上，为操作1 由APPSEM II -专题网络IST-2001-38957和MIUR EOS提供- 可扩展对象系统。2Email：fagorzi@diisi. 联合王国It3Email：zucca@disi. 联合王国It1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.02050S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）49和软件组件的组合。然而，这些演算是基于软件组成的静态视图，在这个意义上，开放的代码片段可以灵活地组合在一起，但在实际开始执行计算之前，我们必须获得一个完全简化和封闭的代码片段。在模演算中，这在形式上是由这样一个事实来反映的：选择，用e.X表示，其中e是一个模表达式，X是一个模的名称。组件，只能在e是基本模块（无模块）时执行运营商仍有待减少），而且没有任何部件仍需进口。然而，现代编程环境越来越多地包括动态重新配置特征，在这个意义上，允许在重新配置步骤和标准执行步骤之间进行交错重构特性的例子有动态加载，如Java和C#，其中单个代码片段动态链接到已经执行的程序，动态重新绑定[9]，即在执行时改变应用程序使用的名称的含义的能力，将值或计算从一个运行的应用程序编组/解编组到另一个。在这里，我们提出了一个简单的演算，称为R-演算（形式上，这是通过定义为微积分配置的基本术语来实现的，粗略地说，这些术语是由命名组件（形式上，基本模块）的（开放的，相互递归的）集合和表示在这些组件的上下文中运行的程序的术语组成的对配置可以通过经典的模块/片段操作符组合（特别是，我们将CMS的一个变体作为底层模块演算[5]），因此，归约步骤可以是程序的执行步骤或执行模块操作符的步骤（重构步骤）。如上所述，R演算的最初动机是寻找大规模编程的形式模型。 在这方面，计算是支持重构功能的系统基础工作流[1，3，2，4]的一部分，其中系统结构可以在执行期间动态变化。然而，微积分也可以编码小问题中的编程，因为配置结合了可编程抽象（第一类函数），记录，具有相互递归定义的环境和模块的特征。在这项工作中，我们专注于后者。在第一节中，我们将R-演算作为纯演算（没有归约策略），并陈述其推论。S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）4951我我我我我我e∈Exp：：=表达式|xvariable|[ι;o;ρ](dom(ι)∩dom(ρ)= ∅)basicmodule|e]（dom（i）n dom（ρ）= n）b a sic c o n fig u r a t i on|e](dom(ι)∩dom(ρ)= ∅)basicconfi gu rati o n|e1+ e2sum|e|σ r e duct|σore duct|freezeσefreeze|e↓X运行|e↑结果i：=xi→∈IXi输入分配mento：=Xi→∈Ie输出分配mentρ：=xi→∈Ielocalassignmentσ：=Xi→∈IY， Yj∈Jrenamingi i jFig.1. 语法恩塞。然后，我们概述了一个按需调用策略，它导致了一个泛化，包括重新配置功能，如[8，6]中所述的按需调用算法第二部分将在本文的完整版中完成，其中还将包括对R的可能类型系统的研究。第一章R演算在本节中，我们通过示例介绍R-演算，其组织方式如下：首先，我们说明演算的模块片段，它是[5，13]（mixin）模块演算的变体;然后我们介绍配置并说明程序执行和重构的交错;最后，我们讨论演算的高阶特征，显示重构如何在许多级别上发生图中给出了形式1，Fig. 2和图3，分别。模块运算符演算的术语表示模块（输入或输出或本地组件的集合）或配置（由模块和在模块所操作的组件的上下文中运行的程序模块表达式是在基本模块之上通过三个运算符构建的：sum，reduce和freeze。 这些操作符的语义是CMS操作符的一个轻微变体[5]，其中我们放宽了reduce和freeze操作符的适用性。此外，我们还包含了一些规则，以m演算[13]的风格通过替换来简化基本模块，并以let-in演算[8，6]的风格重新关联模块绑定（参见下面的解释基本模块的形式为[i;o;p]，其中：i是从延迟变量到输入名称的映射，o是从输出名称到表达式的映射，p是从局部变量到表达式的映射。名字X，Y，Z，... 用于引用来自模块外部的组件（因此它们由模块使用52S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）49σ我我⇐⇒1 2 2 1 1 2单洞上下文和上下文闭合E：：= Q |[i; O; ρ]|[i; o; L]|[i; O; ρ|e]|[i; o; L|e]|[i; o; p|E]|e+E|σ ι |E|σ o|冻结σ E|E↓ X |E↓X| E↑R：：= Q |R+ e|O：：=X→ E，oL：：=x→ E，ρσι|R|σo|冻结σRv∈Val：：= [i; o; ρ]|[i; o; p|v]的e ）e′（E）E[e]）E[e′]模块简化（m-和）[11;o1;p1]+ [12;o2;p2]）[11，12;o1，o2;p1，p2]dom（i1，p1）<$ FV（[i2;o2;p2]）=<$dom（i2，p2）<$ FV（[i1;o1;p1]）=<$（m-reduce）ι|[i1，i2;o;p]|O ）[σιηι1，ι2;oησo;ρ]cod（ι2）dom（σι）=dom（m-freeze）（m-subst）Σ冻结σxiΣi→∈IX，i;o;ρ ）的方式Σi;o;p，xicod（i）i→∈Io（σ（X））x2/∈HB（E），x2∈dom（ρ）∗[i; o; x1→ E[x2]，ρ] ）[i; o; x1→E {ρ（x2）}，ρ]x2/）x1ι，o，ρ（m-subst-out）[i; X<$→ E [x]，o; x<$→e，ρ] ）[i;X→ E{e}，o;x<$→e，ρ]x/∈HB（E）（m-砷）[i1; o1; p1，x→（R [i2; o2; p2|e]）↑] ）的方式[ι1;o1;ρ1，x<$→a，ρ2]（FV（e）<$FV（ρ2））dom（ι2）=dom（ρ2）<$（FV（o1）<$FV（ρ1））=<$模变量∗给定ι，o和ρ，x）y是由下式导出的最小传递和自反关系ι，o，ρX）x <$x∈FV（ρ（x））<$（x∈dom（i）<$x∈ FV（o））ι，o，ρ图二. R-演算的模表达式运算符），而变量x，y，z，. 用于从内部指代组件。例如，表示为e[x1，. 、.、xn]一个可能包含∆σS. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）4953∆x1，.，xn作为自由变量，e0= [x <$→X，z<$→Z; Y<$→e1 [x，z，y]; y<$→e2 [x，z，y]]是一个具有两个输入、一个输出和一个本地组件的基本模块。当地组件可以相互递归。求和运算符允许通过执行输入组件的联合以及输出和本地组件的不相交联合两个模块中具有相同名称的输入组件在结果模块中共享，而延迟或局部变量之间的冲突通过α重命名解决。例如，我们可以对上面的e 0进行求和，其中e5=[y <$→ Y，w <$→ Z; X <$→ e3 [y，w，x]; x <$→ e4 [y，w，x]]，得到基本模e6=54S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）49XσσXXσι||σ|o σ|oσ重组和置换R[i;o;p] ）R′[i′;o′;ρ′]（conf/subst/assumption）（subst-prg）αR[i; o; ρ|e] ）R ′[i′; o′; ρ′|α（e）]x/∈HB（E）升降[i;o;p|E[x]]）[i;o;ρ| E{ρ（x）}]x∈dom（ρ）（升力和）[ι1; o1; ρ1|e] ↑ +[ι2; o2; ρ2]）[i1; o1; p1|e +[ι2; o2; ρ2]] ↑（减升力）[ι; o; ρ|e] ↑）i; o; ρ |e↑（freeze-lift）冻结（[i; o; ρ|e] ↑） ）[i; o; ρ|冻结（e）] ↑（运行-提升） （R [i; o; p|e] ↑）↓）R [i; o; ρ|e↓] ↑运行和结果（运行） [i; o; p] ↓）[i; o; p|o（X）]（res）（R [i; o; p|e]）↑）eFV（e）dom（i，ρ）=图三. R-演算的构形归约规则[x<$→X，z<$→Z，yJ<$$> →Y，w<$$> →Z;Y<$→e1[x，z，y]，X<$→e3[yJ，w，xJ];y<$→e2[x，z，y]，xJ<$<$→e4[yJ，w，xJ]]，其中输入名称Z由两个变量z和w共享，而e 5中的变量y和x分别被α重命名为yJ和xJ，因为它们与e0中的变量一致。reduce操作符允许重命名组件名称，其中输入和输出名称被独立重命名.输入重命名是一个映射，其域和共域分别是旧的和新的输入名称，而输出重命名则相反。为例 如 ，X1<$→X，X2<$→X，<$→W|[x1<$→X1，x2<$→X2，x3<$→X3;Y<$→e1，Z<$→e2;x<$→e3]|Y1›→Y，Y2›→Y简化为[x1<$→ X，x2<$→ X，x3<$→ X3，w <$→ W; Y1<$→e1，Y2<$→ e1; x <$→ e3].非内射输入重命名允许合并两个输入名称（如示例中的X1和X2到X中），而非满射输入重命名用于添加伪输入名称（如W），这些名称绑定到新变量（示例中的w）。非内射输出重命名允许定义的重复（在示例中，Y的定义用于Y1和Y2），其中非满射用于删除输出组件（在示例Z中）。freeze操作符允许在模块内部链接输入和输出名称。也就是说，该操作符解析输入名称，以便将输入组件转换为本地组件。例如，冻结X<$→X，Z<$→Y（e6）简化为S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）4955∗[y′→Y;Y<$→e1[x，z，y]，X<$→e3[y′，w，x′];y<$→ e2 [x，z，y]，x′<$→ e4 [y′，w，x′]，x <$→ e3 [y′，w，x′]，z <$→ e1 [x，z，y]，w <$→ e1 [x，z，y]]。规则（m-subst）和（m-subst-out）允许用局部变量在模块组件中的定义替换局部变量 在规则（m-subst）中，边条件x2/）x1意味着 （局部）坐标x2does不依赖于ι，o，ρ（局部）分量x1（见图1）（2）依赖关系的形式化定义）。如果没有这个条件，R-演算就不是连续的（见[7，13]）.在解释规则（m-asynchronous）之前，我们说明配置的归约规则。一个基本的配置是一对[i; o; ρ|e]，由一个基本模块和一个表达式组成，称为程序。一个基本的配置可以通过程序的归约步骤来演化;此外，局部变量可以用它们的定义表达式来替换（参见规则（subst-prg）），如下面的归约序列所示：[; X<$→x; y<$→1，x<$→2+ y|x] ）[; X<$→x; y<$→1，x<$→2+ y| 2+y]）[; X<$→x;y<$→1，x<$→2+y| 2+ 1] ）[; X<$→x;y<$→1，x<$→2+y|3]。此外，在前一节中描述的模块操作符也可以应用于配置，并作为重构操作符，在某种意义上，它们允许在程序执行期间修改程序的上下文这是由规则（reconf/subst/asynchronous）执行的，其中R表示仅由模运算符组成该规则还允许可变子项-配置组件内的关联步骤注意，在规则的前提中，模块级的归约步骤用α标记。这只是为了跟踪并传播到程序中，在模块评估步骤中可能发生的α由于模块操作符，可以使用所需的输入组件，如下所示：冻结Z<$→Z[z <$→Z; ; y<$→ 1，x<$→ 2+ z|x]+ [; Z<$→ 3; ]）冻结Z<$→Z[z <$→Z; ; y<$→ 1，x<$→ 2+ z| 2 + z]+ [; Z<$→ 3; ]）冻结Z<$→Z[Z <$→z; Z<$→ 3; y<$→ 1，x<$→ 2+ z| 2 + z]）[; Z<$→3; y<$→1，x<$→2+ z，z<$→3| 2+ z]）[;Z <$→ 3; y <$→ 1，x <$→ 2+ z，z <$→ 3 |2+ 3]）[; Z <$→ 3; y <$→ 1，x<$→ 2+ z，z<$→ 3 |5]。高阶特征和配置层次由于程序可以是一个配置，局部变量解析步骤和重构步骤都可以在外部配置层次（所需变量的最内层）进行 这通过以下归约序列来说明：冻结Z<$→Z（[z <$→Z; ; y<$→ 2 |[; X<$→x; x<$→y + z|x]] + [; Z<$→3; ]））冻结Z<$→Z（[z<$→Z; ; y<$→ 2 |[; X<$→x; x<$→y + z|y + z]] + [; Z<$→ 3; ]））冻结Z<$→Z（[z<$→Z; ; y<$→ 2 |[; X<$→x; x<$→y + z|y + z]] + [; Z<$→ 3; ]））冻结Z<$→Z[z <$→Z; Z<$→ 3; y<$→ 2 |[; X<$→x; x<$→ 2+ z| 2 + z]] ）的方式56S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）49[; Z<$→ 3; y<$→ 2，z<$→ 3 |[; X<$→x; x<$→2+z| 2+z]]）... ）的方式[;Z <$→ 3; y <$→ 2，z <$→ 3 |[; X <$→ x; x <$→ 2+ z |5]]。在解释提升规则之前，我们先说明run和result运算符。Run和resultrun操作符允许从一个（基本）模块中获得基本配置，通过开始执行其输出组件之一例如，表达式[;X<$→x;y<$→ 2，x<$→ 2+y]↓X在一步中简化为前面所示的基本构型结果运算符允许从配置中提取程序。形式上，配置级别由形式R[i; o; p]的表达式建模|e]。只有当程序不引用所考虑的配置级别的基本配置中的任何变量绑定时，才可以安全地应用结果运算符。此条件可防止变量的作用域挤压，这将导致动态错误。例如，在表达式（freezeZ<$→Z（[z <$→Z; ;|[; X<$→x; x<$→ 2+z|x] ↑]+ [; Z<$→ 3; ]）↑，最里面的结果运算符不能执行，因为程序仍然引用在封闭的基本配置中绑定的变量x。因此，我们首先需要解决x，得到（冻结Z<$→Z（[z <$→Z; ;|[; X<$→x; x<$→ 2+ z| 2 + z] ↑]+ [;Z<$→3; ]）↑。 在在这一点上，我们可以应用重构步骤，或者最内层的结果运算符。通过选择后一种约化方案，我们得到了构造（冻结Z→Z; |2 + z]+ [; Z<$→3; ]）↑，最终减少到5。绑定重新关联和提升规则（m-asynchronous）的灵感来自于associa，在[8，6]中的作用规则它用于允许使用程序，即使它依赖于绑定在当前级别的变量。事实上，这种依赖关系并不总是可以通过替代来解决，也就是说，当变量相互依赖时。例如，在表达式[;; m <$→ [;; y <$→ x，x <$→ y]中，|[; Z<$→ x，W <$→ 1;]] ↑|m\Z]我们想使用（内部的基本模块）m，即使它指的是y，是在一个循环里。注意m永远不会使用y的定义。（sum-lift）、（reduct-lift）和（freeze-lift）规则也受到了[8，6]中提升规则的启发。它们允许在应用结果运算符的基本配置中移动模块运算符。当程序不能被提取时，这是有用的，但是在执行了在外部配置级别中应用的一些模块操作符之后，可以安全地提取例如，在表达式[; ; x <$→ y，y <$→ x]中，|[; Z <$→ x，W <$→ 1;]] ↑\Z，在hav-ing删除输出组件Z，基本模块可以安全地提取因为它不再引用绑定在当前级别的变量R的值的集合Val，范围为v，在图的顶部定义二、它们包含基本模块和配置。R演算具有Church-Rosser性质。定理1.1（Church-Rosser）约化关系）是连续的。S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）49572按需呼叫策略R-演算可以配备不同的策略，可以用来编码/推广其他原始演算，如lambda演算和模块演算。在这个扩展的摘要中，我们概述了一个按需调用策略，它导致了一个泛化，包括重新配置功能，如[8，6]中的按需调用算法规则（E）现在处理（单孔）求值上下文而不是（任意）上下文。上下文D[x，xn]用于表示一组声明s.t.x的求值传递依赖于xn的求值，如[8，6]所示。值与微积分不同的是：如果一个配置的运行程序是一个值，那么它就是一个值，即使仍然有一些模块操作符被应用。规则（m-sum）、（m-reduce）和（m-freeze）如图2所示2（因此未报告）。我们不允许模块组件简化，因此上下文[i;O;ρ]和[i;o;L]被删除，并且规则（m-subst），（m-subst-out）和（m-assumption）也被删除。事实上，直觉是模块组件的简化只在被执行程序触发时发生（参见下面的规则（subst），（asstrom）和（m-asstrom-D）在rule（reconf）中，重新配置现在仅在执行需要一个延迟变量。事实上，在这种情况下，重构步骤可能会使变量成为局部变量。注意，由于不再有规则（m-subst）、（m-subst-out）和（m-assumption），因此该规则只能在作为模运算符的应用步骤的前提下应用，因此，只处理重构步骤。在规则（subst-prg）中，用程序内部的定义表达式替换局部变量x的实例现在只发生在程序执行需要这个变量时，并且定义表达式已经被减少为一个值。如果不是这种情况，则触发对x的定义的求值，这可以递归地触发对其他定义的求值，直到找到其求值不依赖于任何其他定义的局部变量xn（求值上下文[i;o;D[x，x]，x ›→evE， ρ|E ev[x]]）。当一个局部变量x的定义是无无无无无无无减少到一个值，这个值可以用来替换一个需要的引用xn另一种定义（规则（subst））。规则（assoc-input）、（assignment）和（m-assignment-D）执行按需绑定重新关联。当程序需要一个变量x，它的定义既不是一个值，也不是一个可以进一步简化的表达式时，就使用它们而是一个答案（粗略地说，一个包含自由变量的值插入到一个可以为这些变量提供定义的上下文中）。在这种情况下，按需呼叫策略应避免在不必要的情 况 下 评 估 这 些 定 义 。 如 果 没 有 对 延 迟 变 量 的 引 用 （ rule（asynchronous）），则可以消除重新配置级别并重新安排本地绑定。58S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）49n需要需要需要需要需要）需要评价背景、价值观和答案Eev：：=Q |[i; o; p |Eev]|[i; o; ρ，D [x，xn]，xn <$→ Eev|Eev [x]] |Eev+ e |[i; o; p]+ Eev|E ev [ x ]] + E ev| Eev|冻结σ Eev|Eev ↓X| Eev ↓X | Eev↑12σ ι ||σ oD[x，xn]：：=x→Eev[x1]，x1→<$E ev[x2]， . . ，xn−1›→Eev[xn]1v∈Val：：= [i; o; p] |R [i; o; ρ|v]的a∈Ans：：= v|（R [i; o; p|a]）↑重组和置换n−1α′ ′ ′ ′R[i;o;p]ne）edR[i;o;p]x/∈HB（Eev）（确认）R[i; o; ρ| Eev [x]] ）R ′ [i′; o′; ρ′|α（Eev[x]）]x∈dom（i）（subst-prg）（subst）[i; o; ρ，x <$→ v |Eev[x]]）[i;o;ρ，x<$→v|Eev{v}]x/∈HB（Eev）x/∈HB（Eev）结果[i;o;D[x，xn]，xn<$→v，ρ|Eev[x]]）[i; o; D[x，xn {v}]，xn<$→ v，ρ |Eev[x]]（res） （R [i; o; p|a]）↑ ）一个 FV（a）dom（i，ρ）=dom结合再结合R[ι2;o2;ρ2]α）RJJjev（assoc-input）需要ι2;o2;ρ2x/∈HB（E）[i1;o1;p1，x→（R[i2;o2;p2|a]）↑|Eev[x]]）（FV（a）<$FV（ρ2））dom（ι2）/=domˆι1;o1;ρ1，x<$→`RJiJ;oJ;ρJ|α（a）α ′需要↑|E ev[x]222x/∈HB（Eev）（asymmetry）[i;o;ρ，x →（R[i;o;ρ|Eev [ x ]]）| Eev[x]])（FV（a）<$FV（ρ2））dom（ι2）=1 112 2 2需要dom（ρ2）<$（FV（o1）<$FV（ρ1））=<$（天冬氨酸-D）升降[ι1; o1; ρ1，x→a，ρ2|Eev [x]][i1; o1; p1，D[x，xn]，xn→（R[i2; o2; p2|a]）↑|E[i1; o1; ρ1，D [x，xn]，xn→a，ρ2|Eev [x]]ev[x]]）x/∈HB（Eev）（FV（a）<$FV（ρ2））dom（ι2）=dom（ρ2）<$（FV（o1）<$FV（ρ1））=<$e=a或（sum-lift）e=Eev[x]EV[i1; o1; p1|e] ↑+[ι2; o2; ρ2] ）[i1; o1; p1|e+[ι2; o2; ρ2]] ↑（x/∈HB（E），（reduced-lift）e=a或EVx∈dom（ι1））EV（冻提）σι |[i; o; p |e] ↑|σo需要i; o; ρ|σι|e|σo ↑e=E[x]（x/∈HB（Ee=a或EV），x∈dom（i））EV冻结σ（[i; o; ρ|e] ↑） ）[i; o; ρ|冻结σ（e）S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）4959] ↑e=E[x]（x/∈HB（E），x∈dom（i））（运行-提升）（R[i;o;p|a]↑）↓Xne）edR [i; o; ρ|a↓X] ↑见图4。 按需呼叫缩减规则60S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）49需要需要ings。在另一种情况下（rule（assoc-input）），有必要首先执行重新配置步骤，直到不再有对延迟变量的引用。规则（sum-lift）、（reduct-lift）和（freeze-lift）仅在运行程序不能进一步减少时执行模块运算符的提升，也就是说，它是一个答案或需要一个延迟变量x，该变量x不能在当前配置级别提供，这是一个基本配置（因此，不能执行更多的重新配置步骤），但可能是可配置的。通过外部配置级别提取程序后显示最后，rule（run）类似于微积分（因此，没有报告），而rule（res）现在只作用于配置，作为运行程序，在当前级别没有变量约束的答案（回想一下，应用于一般的res运算符，也就是说，即使在当前级别没有关闭，答案也由rules（assoc-input）和（assign）处理）。定理2.1（的可靠性和完备性）• 如果e）eJ，则e ）eJ。）的方式需要• 如果e ）v，则存在a使得e）a。3结论我们已经介绍了R-演算，一种演算，其中标准执行（即，执行由代码片段描述的单个计算）可以与元级别的操作交织，该操作可以以各种方式操纵我们已经陈述了演算的连续性，然后概述了一个按需调用策略，该策略导致了按需调用演算的推广，包括重构特征，如[8，6]所示这一部分将在本文的完整版中完成，其中还将包括对R的可能类型系统的研究。 进一步的工作包括应用演算来建模动态绑定，重新绑定和编组机制，例如[9]。引用[1] D.安科纳湾Fagorzi和E.祖卡动态链接的演算。ICTCS2003，LNCS 2841，第284-301页[2] D.安科纳湾Fagorzi和E.祖卡低优先级链接的动态重构演算。电子笔记理论计算机科学，2004年。WOOD地出现。[3] D.安科纳湾Fagorzi和E.祖卡一种带有惰性模运算符的微积分。 在TCS 2004（IFIP Int. Conf.理论计算机科学），第423-436页。Kluwer Academic Publishers，2004.[4] D.安科纳湾Fagorzi和E. 祖卡 用于动态重新绑定的混合模块。 2005年TGC可信全球计算研讨会（Symposium on Trustworthy Global Computing，LNCS）Springer，2005年4月。地出现。）S. Fagorzi，E.Zucca/理论计算机科学电子笔记135（2006）4961[5] D. Ancona和E.祖卡模系统的演算。你好of Functional Programming，12（2）：91 -1 3 2 ，200 2 .[6] Ariola，Z. M.和Blom，S.（1997年）。循环lambda结石。在计算机软件的理论方面，第77[7] Z. M. Ariola和J. W.克洛普Lambda演算与显式递归。信息与计算，139（2）：154-233，12月。一九九七年。[8] Z. M.作者声明：by M.按需调用lambda演算。你好，7（3）：265 -301，1997。[9] G. Bierman，M.作者：Hicks，P. Stoyle和K.旺斯布罗用于编组和更新的动态重新绑定，具有销毁时间λ。见ICFP 2003，第99-110页。ACM Press，2004.[10] S. Fagorzi. 动态重构的模块演算。PhD thesis，Dipartimento di Informatic aeScienzedell' I nformazio n e，U ni v ersi t ` a d i G e n ov a，2005.[11] T. Hirschowitz ， X.Leroy 和 J.B. 井 按 值 调 用 混 入 模 块 ： 归 约 语 义 、 边 对 象 、 类 型 。ESOP2003，LNCS 2986，第64-78页。Springer，2004.[12] E. Machkasova和F.A.特巴克链接时编译的演算。见ESOP 2000，LNCS 1782，第260-274页。斯普林格，2000年。[13] J. B. Wells和R.韦斯特加德用于与第一类本原模链接的连续等式推理。见ESOP 2000，LNCS1782，第412-428页。斯普林格，2000年。