PELCR及其扩展：交互几何中的虚拟归约与并行实现

理论计算机科学电子笔记135（2006）107-117www.elsevier.com/locate/entcs支持PELCR安东尼奥·科森蒂诺1Dipartimento di Informatica，Sistemi e Produzione，非独立数据段是RomaMarco Pedicini2Istituto per le Appliazioni del Calcolo“M. Picone弗朗西斯科·夸利亚3Dipartimento di Informatica e Sistemistica，Univrsit`adegliStudiRoma“L a S a p i e n z a“，V i a S a l a r i a 113，R om e，I t a l y.摘要在[10，11]中，PELCR已经被引入作为从相互作用几何导出的实现，以便在并行/分布式计算系统上执行虚拟归约本文提出了一种基于有向虚归约[2]的PELCR的扩展，即虚归约的限制[3]，它是计算相互作用几何[5]的一种特殊方法，类似于Lamping 此外，所提出的解决方案保留了[11]中研究的本地和异步减少所产生的并行性的可扩展性。关键词：函数规划，最优约简，线性逻辑，交互几何，虚拟约简，并行实现。1电子邮件：我不知道你在说什么。它2e-mail：marco@iac。CNR. 它3e-mail：qua g lia@ d is. 一个人1. 它4个P通常由CNR/CNRS合作伙伴提供。162511571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.025108A. Cosentino等人理论计算机科学电子笔记135（2006）1071引言PELCR（Parallel Environment for optimal Lambda Calculus Reduction）是一个在并行/分布式计算系统上支持最优Lambda演算约简的软件包。它被设计为纯lambda演算（完全）归约的解释器，其开发依赖于相互作用几何[5]以及函数编程和线性逻辑领域的连续结果[3]，这些结果表明lambda项的归约可以映射到称为定向虚拟归约（DVR）的图形重写技术上，参见[2]。具体而言，PELCR为DVR实现了一种特殊的策略，称为半燃烧（HC），参见[10，11]，该策略允许通过允许在图形的同一节点上重合的两个边之间的合成来充分利用并行性，只要这些边可用于托管该节点的处理器一组优化也实现PELCR内允许减少通信开销，和一个公平的政策，用于分配动态起源的负载（即减少过程中产生的新节点和边缘）处理器之间。虽然纯lambda演算有各种各样的应用，但许多函数式编程语言倾向于偏离它，以便对程序员更具吸引力和效率，并注册使用非函数式构造。关于这一点，让我们引用最常用的函数式语言的例子，即ocaml和haskell，两者都具有ad-basetype类型和与底层操作系统显式交互的设施在本文中，我们将展示如何在PELCR中支持类似的扩展，而不阻止利用并行性（从而实现运行时的效率）所产生的几何相互作用的可能性我们的出发点是麦基新的生成器形成了一个等式理论，定义了一个特定的抽象数据类型。通过推广Mackie此外，相比Mackie本文其余部分的结构如下。在第2节中，我们提供了A. Cosentino等人理论计算机科学电子笔记135（2006）107109→∈为前面提到的扩展提供理论框架在第3节中，我们提出了在动态图中的扩展lambda演算的解释，其中x-函数在有向虚归约之上执行如何在PELCR中支持扩展在第4节中描述。在第5节中，我们给出了一个使用x函数的代码示例，并报告了与运行时行为相关的实验数据，同时改变了所使用的处理器数量。2相互作用的几何和扩展的L*我们提供的扩展是按照Mackie在[7]中介绍的方法获得的，然后由Pinto在[13]中扩展。这种技术可以总结为在L语言中添加生成器，其中计算结果包括要操作的数据和交互发生时要评估的可执行文件。这项工作探索了这个方向，事实上，我们将这些生成器映射到用C语言实现的外部库中定义的数据结构和函数上。让我们回顾平托然后给出了一对特殊的相互作用方程Sn=（n+1）S，（ 1）S=1，（ 2）并将其添加到代数L中。注意，虽然等式（1）的评估被呈现为重写，但是它已经附加了计算结果S（n）的计算任务。事实上，这些规则在以下术语中更好地理解：我们为L添加一个函数的生成器S和一个代表基础类型对象的生成器N，在这种情况下是一个自然数添加到代数的任何生成器都有相应的分配内存空间：• 在对象类型为N的情况下存储其状态n，由N：n表示，• 在函数的情况下存储程序地址p，由S：p表示。因此，现在等式（1）和（2）可以重新表述为：（S：p）（N：n）=（N：p（n））（S：p），（3）（S：p）（S：p）= 1。（四）注意，p（n）是通过调用地址为p的函数，参数存储在N中，并将结果存储在为N分配的空间中来获得的。这种方法有两种问题。首先，我们需要考虑如何将这种方法扩展到具有多个参数的函数：f：A1×A2×.. Ak→B。第二，我们必须考虑部分求值函数的生成元，因为在曲率中，生成元F∈L110A. Cosentino等人理论计算机科学电子笔记135（2006）107Fig. 1. Pinto约化一个涉及后继项（（λx.x）λa. S（a）0）与f相关联的，与它的参数一个接一个地交互为了给出方程（1）和（2）的一般形式，我们引入一个新的生成元族，比如x-生成元，其标识符为i，升程1为常数，记为xi;从代数的角度来看，xi的行为类似于升程1的指数生成元，然后我们指定与任何生成元相关联的计算任务，即其计算结果。对于任何xi，我们有一个类型τ（i）和一个状态（i），状态存储关于计算任务的类型及其评估状态的信息;本质上我们有两类评估状态：• 在数据的情况下，由xi：a表示，xitype是基础类型，并且其评估状态是存储值a;• 在由xi：（p，v）表示的函数的情况下，xi类型是函数类型，并且其求值状态由函数指针p和长度严格小于函数的arity的值v的有序列表给出。注意，向量可能是空向量。为了简单起见，我们假设一个唯一的基类型σ和箭头类型构造函数，所以类型集S是S：= σ|σ→S。 我们表示 σ→（σ→. （σ→σ）. ）由σn→σ。定义2.1对于任意xi，我们有状态（i）=ττ，p，v，其中它的类型τ=σn→σ∈S，p是对函数码的引用，v=（a1，a2，...，am），其中0 ≤m

下载后可阅读完整内容，剩余1页未读，立即下载