函数式语言LFC的Supercompilation技术研究

监督式编译技术是提高程序运行效率的自动优化技术。虽被提出 40 多年，却不被多数人熟知。为了研究监督式编译，并扩展它的应用，对监督式编译技术做了详细的分析，并将监督式编译应用于函数式语言LFC. 目前最为成熟的监督式编译是基于 Refal 的监督式编译系统。为了将 Refal监督式编译应用于 LFC 语言，详细分析了 Refal 语言和 LFC 语言的语法，数据结构，模式匹配的求值规则等。并提出了将现有的监督式编译应用于 LFC 语言的方法。 监督式编译应用于 LFC的第一种方法是将 LFC程序转换为能够被监督式编译系统优化的程序，即 Refal 程序。为提高程序转换的效率，提出了介于LFC和Refal 之间的中间语言表达形式。根据优化技术中优化器自应用的研究，提出了监督式编译应用于LFC的第二种方法，即利用监督式编译器优化LFC中间语言的解释器和源程序。 由于实验中所使用的监督式编译系统是基于无类型语言 Refal 的 SCP, 而LFC 的类型由上下文无关文法定义。因此，程序转换过程中需对 LFC 程序进行类型检查。对函数定义中的模式使用静态类型检查，判断模式的类型是否为类型声明的子类型；对于程序运行中输入参数的类型检查，提出了新的方法，即将 LFC中的文法转换为 Refal 函数 Filter。程序运行时的输入首先被该函数使用。 实验表明， Filter 函数使得输入参数类型和文法所定义类型一致。同时，结果表明，利用解释器优化 LFC 程序的方法是可行的。针对两种方法的实验结果，分析了影响优化结果的因素。最后，总结并提出了下一步的工作。

Near dipole-dipole effects on the propagation of few-cycle pulse in a dense two-level medium

The propagation behaviors, which include the carrier-envelope phase, the area evolution and the solitary pulse number of few-cycle pulses in a dense two-level medium, are investigated based on full-wave Maxwell-Bloch equations by taking Lorentz local field correction (LFC) into account. Several novel features are found: the difference of the carrier-envelope phase between the cases with and without LFC can go up to pi at some location; although the area of ultrashort solitary pulses is lager than 2 pi, the area of the effective Rabi frequency, which equals to that the Rabi frequency pluses the product of the strength of the near dipole-dipole (NDD) interaction and the polarization, is consistent with the standard area theorem and keeps 2 pi; the large area pulse penetrating into the medium produces several solitary pulses as usual, but the number of solitary pulses changes at certain condition. (C) 2005 Optical Society of America.

Effects of Lorentz local field correction on propagation properties of few-cycle pulse in dense Λ-type atomic medium

By solving numerically the full Maxwell-Bloch equations without the slowly varying envelope approximation and the rotating-wave approximation, we investigate the effects of Lorentz local field correction (LFC) on the propagation properties of few-cycle laser pulse in a dense A-type three-level atomic medium. We find that: when the area of the input pulse is larger, split of pulse occurs and the number of the sub-pulses with LFC is larger than that without LFC; at the same distance, the time interval between the first sub-pulse and the second sub-pulse in the case without LFC is longer than that with LFC, the time of pulse appearing in the case without LFC is later than that in the case with LFC, and the two phenomena are more obvious with propagation distance increasing; time evolution rules of the populations of levels vertical bar 1 >, vertical bar 2 > and vertical bar 3 > in the two cases with and without LFC are much different. When the area of the input pulse is smaller, effects of LFC on time evolutions of the pulse and populations are remarkably smaller than those in the case of larger area pulse. (c) 2008 Elsevier B.V. All rights reserved.

practical type checking of functions defined on context-free languages

A type checking method for the functional language LFC is presented. A distinct feature of LFC is that it uses Context-Free (CF) languages as data types to represent compound data structures. This makes LFC a dynamically typed language. To improve efficiency, a practical type checking method is presented, which consists of both static and dynamic type checking. Although the inclusion relation of CF.languages is not decidable,a special subset of the relation is decidable, i.e., the sentential form relation, which can be statically checked.Moreover, most of the expressions in actual LFC programs appear to satisfy this relation according to the statistic data of experiments. So, despite that the static type checking is not complete, it undertakes most of the type checking task. Consequently the run-time efficiency is effectively improved. Another feature of the type checking is that it converts the expressions with implicit structures to structured representation. Structure reconstruction technique is presented.

pattern matching compilation of functions defined in context-free languages

LFC is a functional language based on recursive functions defined in context-free languages. In this paper, a new pattern matching algorithm for LFC is presented, which can represent a sequence of patterns as an integer by an encoding method. It is a rather simple method and produces efficient case-expressions for pattern matching definitions of LFC. The algorithm can also be used for other functional languages, but for nested patterns it may become complicated and further studies are needed.

yet another meta-language for programming language processing

The formal specification language LFC was designed to support formal specification acquisition. However, it is yet suited to be used as a meta-language for specifying programming language processing. This paper introduces LFC as a meta-language, and compares it with ASF+SDF, an algebraic specification formalism that can also be used to programming languages.

facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.

一个支持规约获取的形式规约语言

该文介绍了形式规约语言LFC设计的一些主要方面，并通过例子说明了LFC的一些特色形式。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数，即定义在上下文无关语言上的递归函数为基础，以上下文无关语言为数据类型，在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明，LFC是一个能力强、易使用的语言，适合软件形式规约获取之用，并且适合其它一些用途。

简单模式的一种匹配方法

模式匹配是包括LFC在内的大多数函数式语言都具有的特点。文章在LFC语言现有的模式匹配实现方法的基础上，结合常用的模式匹配树的构造思想，设计了一种模式匹配方法。这种模式匹配方法通过计算给定模式集合的扩展集合来构造模式匹配树。虽然在最坏情况下，该方法与LFC现有实现的空间复杂度一样，但当函数定义是部分构造式，而定义中的非项模式覆盖了较多项时，这种模式匹配方法可以避免LFC语言现有实现中较大的编码空间。这个方法略作修改即可用于复杂的嵌套模式，是一种通用的模式匹配方法。