程序设计语言中的继续：理论与实践
文献类型：学位论文
| 作者 | 喻钢 |
| 学位类别 | 博士 |
| 答辩日期 | 2008-05-29 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 中国科学院软件研究所 |
| 导师 | 柳欣欣 |
| 关键词 | 继续 程序设计语言 传名调用 CPS 求值上下文 FANF 异常处理 |
| 其他题名 | Continuations in Programming Language: Theory and Practice |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 继续表示程序在某个执行状态下的剩余计算抽象。继续在计算机科学的各个分支中都有重要的应用。本文讨论继续在程序设计语言中的理论与应用。 继续传递风格(CPS)变换是表达$\lambda$演算和函数式程序设计语言语义的重要手段。作为活性语言基础的传值调用策略CPS变换已经被广泛研究。而惰性语言采用的传名调用策略CPS变换研究则稍显不足。本文在理论基础方面着重讨论常数传名调用语言的CPS变换理论。 在区分常数语言中，本文给出传名调用求值上下文及在此基础上的项和求值上下文的CPS变换，证明了Plotkin的模拟定理。在证明过程中，本文提出了两种证明思路，本文对两种证明思路进行了对比，也和相关工作进行了比较。在一般常数语言的CPS变换讨论中，本文针对一般常数的动态归约特征提出了二值传递变换思想，并在此基础上给出了CPS变换闭语言。相比Plotkin的工作：本文提出的二值传递CPS变换表达更简洁、CPS语言是归约闭语言、归约过程中产生的额外归约更少、且是完全风格的CPS变换。本文也纵向比较了区分常数语言和一般常数语言在求值归约以及CPS模拟方面的区别。 继续在函数式程序设计语言中已经得到广泛的实现和应用。函数式程序设计语言的继续操作符都是由特定的系统基本操作符提供。在主流面向对象语言中并不提供这些控制操作符，仅仅提供基本的异常处理操作符try/catch/throw等。如何在主流面向对象语言上运用异常处理技术实现系统抽象控制栈的保存和重载，即，如何实现继续对象，成为重要的应用研究问题。本文在实践方面着重讨论面向对象语言的控制栈获取和编程技术。 函数式程序设计语言的A范式被证明是CPS变换在编译优化过程中的重要产物，是函数式应用程序的线性控制范式。本文分析并给出了命令式语言对应的线性控制范式：程序的切片A范式(FANF)。首先，讨论了由程序的优化CPS表示到FANF的变换过程。定义基本的优化CPS表示语言，给出求值语义，给出由优化CPS语言到FANF的变换步骤，最后形式给出切片A范式文法。由于作为变换源语言的优化CPS语言无法建模主流语言的变量赋值副作用，本文又讨论了直接从命令式语言出发获取FANF的办法。建模一个模拟Java的小命令式语言，给出变换步骤，并最终给出目标FANF。本文也分析讨论了两种方法在获取FANF时的异同。 在FANF程序之上，本文给出了添加异常处理模块和继续帧定义获取程序继续对象的方法。本文归纳能应用此方法得到程序继续的语言公共特征，给出抽象的、一般的系统类设计。本文也讨论了具体语言实现继续中的特殊技术以及异常处理技术获取程序继续在程序尾递归优化中的作用。 本文最后讨论了面向对象语言的高阶控制编程技术。在获得FANF程序后，可以在程序系统栈上添加基础设施来实现程序的高阶控制编程。本文实现了高阶控制操作符run和fcontrol的标志控制系统。将同边树判定问题作为无标记标志控制系统的具体应用实例。本文也将标志控制系统扩展到带标记版本，并实现了一个多级的线程轮询调度器。实践证明，在获得FANF程序后，主流面向对象语言也可以和函数式程序设计语言一样应用高阶控制编程。 |
| 英文摘要 | Continuation, which has a broad application in many areas of computer sciences, is an abstraction of the remaining computation on current execution state. The dissertation discusses the theory and application of continuation. Continuation always exists implicitly behind the current evaluation program. However, Continuation Passing Style(CPS) transforms the normal program into the one which the continuation appears as a normal object. This explicitly expressed continuation is made used for formally specifying the reduction strategies in $\lambda$ calculus. Call-by-value, which is the basis for eager language, has an extensive CPS research focus. On the other hand, call-by-name, the theory for lazy reduction, has little results. This dissertation shows special interest on the CPS theory for call-by-name language with constants. On the CPS transformation of divided constant language, we firstly define the call-by-name evaluation context and present the CPS transformation for contexts and terms. Then, we define the simulation relation between the source language and CPS language and give the simulation proof on the relation. On the incomplete simulation for the specified term, we give two solutions. Compared with other works, we get a simpler proof on both direction of the simulation and we also precisely characterize the CPS reduction rules. On general constant language transformation, we bring up a two-values passing solution for constant encoding on dynamic reduction status. Based on the encoding we get the reduction-closed CPS language and inverse mapping from the CPS language to the source language. Compared with Plotkin's classic work, our work distinguishes at: a simpler and full CPS-style transformation, the reduction-closed CPS language and less administrative steps. We also compare the general language with the divided one on expressive power and CPS simulation. In functional programming languages, continuations are provided as first-class objects through primitive operators. Nevertheless, mainstream Object-Oriented languages, such as \emph{C++/C\#/Java}, only support exception handling operators \emph{try,throw,catch} etc. The problem of how to obtain and reconstitute the control stack from exception operators comes to the fore. Program transformation is an essential part for exceptional continuation. Previous works have provided plenty of similar transformations for different control purposes. In this dissertation, we bring up a general transformation framework for variants of control tasks. Administrative Normal Form(ANF) is a significant result on the control serialization for functional languages, we present the same control lineralization form FANF(Fragmented ANF) for imperative language. We have developed two transformation approaches for FANF: the optimized CPS language and the imperative language directly. As for the optimized CPS approach, we define the language, the reduction semantic, the transformation steps and the targeted FANF. Since optimized CPS approach ignores the side-effect which is commonly used in imperative language, we develop another transformation which operates directly on a Java-like imperative language. We present the language, the transformation steps and the normal form intended. Based on FANF, we give the general and automatic mechanism for obtaining the control stack from exception handling system. We summarize on the general properties that are essential for the implementation, present the general and reusable UML class hierarchies. We also discuss the obstacles in the implementation in different languages. Another important application of our FANF framework is the higher-order control programming. We implement Sitaram's delimited control operator \emph{run/fcontrol}. We show trees' same-frindge problem as an example of the untagged prompt control transfer. We also extend the system to a tagged version and show a round-robin thread scheduler as an instance. The practice shows that once programs transformed to FANF, they can also support higher-order programming paradigms as functional languages do. |
| 公开日期 | 2011-03-17 |
| 源URL | [http://124.16.136.157/handle/311060/5934]  |
| 专题 | 软件研究所_软件所图书馆_早期 |
| 推荐引用方式 GB/T 7714 | 喻钢. 程序设计语言中的继续：理论与实践[D]. 中国科学院软件研究所. 中国科学院研究生院. 2008. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。