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.

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.

basic research in computer science and software engineering at sklcs

The State Key Laboratory of Computer Science (SKLCS) is committed to basic research in computer science and software engineering. The research topics of the laboratory include: concurrency theory, theory and algorithms for real-time systems, formal specifications based on context-free grammars, semantics of programming languages, model checking, automated reasoning, logic programming, software testing, software process improvement, middleware technology, parallel algorithms and parallel software, computer graphics and human-computer interaction. This paper describes these topics in some detail and summarizes some results obtained in recent years.

function definition language fdl and its implementation

A Function Definition Language (FDL) is presented. Though designed for describing specifications, FDL is also a general-purpose functional programming language. It uses context-free language as data type, supports pattern matching definition of functions, offers several function definition forms, and is executable. It is shown that FDL has strong expressiveness, is easy to use and describes algorithms concisely and naturally. An interpreter of FDL is introduced. Experiments and discussion are included.

一种新型递归函数的求值算法

上下文无关语言上递归函数(recursive functions on context-free languages,简称CFRF)是为描述计算机上用的非数值算法而提出的一种新型递归函数.该函数的一个重要研究方面是函数的求值算法研究.对此问题的一些研究结果进行了总结.在讨论计算和语法分析的结合方式之后,对主要算法按照算法适用范围从小到大的顺序(同时也是算法研究和提出的顺序)做了较为全面的介绍,着重介绍一种通用的新的高效求值算法,即面向树的求值算法.同时对把CFRF扩充为多种类递归函数后的求值方法进行了说明.CFRF的几个求值算法均已在机器上实现,得到了实践的检验.

上下文无关语言分析树的一种表示形式

介绍了上下文无关语言 (CFL)的句子的一种分析树表示 ,它适合用于一类与以往不同的 CFL 的应用 ,即对分析树空间效率要求较高且不需标记分析树的应用 ,典型的就是把 CFL的句子用作算法加工对象 .这种表示比传统分析树不仅空间较小 ,而且进行结构匹配的速度快 .还介绍了这种分析树表示的实现技术 .

Polarization Self-Modulation Phenomenon in a Free Oscillated Nd: YAG Laser

Polarization self-modulation effect in a free oscillated Nd:YAG laser is investigated after a quarter wave plate is introduced independently in the two positions of the cavity. As described in the previous experiments, the intensity components in the orthogonal directions are modulated with a period of the round-trip time or twice. Different pulse shapes reveal that the seed field from the spontaneous emission is not uniform and seems to be stochastic for each pulse.

A Breakdown Criterion of Free Molecular Flows and an Optimum Analysis of EBPVD

Two important issues in electron beam physical vapor deposition (EBPVD) are addressed. The first issue is a validity condition of the classical cosine law widely used in the engineering context. This requires a breakdown criterion of the free molecular assumption on which the cosine law is established. Using the analytical solution of free molecular effusion flow, the number of collisions (N-c) for a particle moving from an evaporative source to a substrate is estimated that is proven inversely proportional to the local Knudsen number at the evaporation surface. N-c = 1 is adopted as a breakdown criterion of the free molecular assumption, and it is verified by experimental data and DSMC results. The second issue is how to realize the uniform distributions of thickness and component over a large-area thin film. Our analysis shows that at relatively low evaporation rates the goal is easy achieved through arranging the evaporative source positions properly and rotating the substrate.

Growth and production of free-living heterotrophic nanoflagellates in a eutrophic lake - Lake Donghu, Wuhan, China

In situ growth of heterotrophic nanoflagellates (HNF) in Lake Donghu, a eutrophic shallow lake in mainland China, was studied from January 1999 to March 2000 using a modified Weisse protocol. The study results indicated that the growth rates of HNF showed pronounced seasonal variation (-0.37-1.25 d(-1)), reaching the maximum during spring to early summer. When the water temperature was higher than 25.5 degreesC, HNF growth was inversely proportional to water temperature. There was an effect by bacterial abundance and autotrophic picoplankton on HNF growth that depended on location. HNF biomass was the highest in late spring, and the HNF production ranged from -2.25 to 35.45 mg l(-1) d(-1) with mean of 3.17 mg l(-1) d(-1). When considered in the context of biomass and production data for zooplankton in Lake Donghu, it was evident that HNF contributed significantly to the total zooplankton production in Lake Donghu. These in situ studies indicate that temperature and food supply are the major determinants of HNF abundance and productivity.

Ultrafast sum-frequency polarization beats in twin Markovian stochastic correlation

An analytic closed form for the second- order or fourth- order Markovian stochastic correlation of attosecond sum- frequency polarization beat ( ASPB) can be obtained in the extremely Doppler- broadened limit. The homodyne detected ASPB signal is shown to be particularly sensitive to the statistical properties of the Markovian stochastic light. fields with arbitrary bandwidth. The physical explanation for this is that the Gaussian- amplitude. field undergoes stronger intensity. fluctuations than a chaotic. field. On the other hand, the intensity ( amplitude). fluctuations of the Gaussian- amplitude. field or the chaotic. field are always much larger than the pure phase. fluctuations of the phase-diffusion field. The field correlation has weakly influence on the ASPB signal when the laser has narrow bandwidth. In contrast, when the laser has broadband linewidth, the ASPB signal shows resonant- nonresonant cross correlation, and the sensitivities of ASPB signal to three Markovian stochastic models increase as time delay is increased. A Doppler- free precision in the measurement of the energy- level sum can be achieved with an arbitrary bandwidth. The advantage of ASPB is that the ultrafast modulation period 900as can still be improved, because the energy- level interval between ground state and excited state can be widely separated.

Modelling raindrop impact and splash erosion processes within a spatial cell: a stochastic approach

A new approach is proposed to simulate splash erosion on local soil surfaces. Without the effect of wind and other raindrops, the impact of free-falling raindrops was considered as an independent event from the stochastic viewpoint. The erosivity of a single raindrop depending on its kinetic energy was computed by an empirical relationship in which the kinetic energy was expressed as a power function of the equivalent diameter of the raindrop. An empirical linear function combining the kinetic energy and soil shear strength was used to estimate the impacted amount of soil particles by a single raindrop. Considering an ideal local soil surface with size of I m x I m, the expected number of received free-failing raindrops with different diameters per unit time was described by the combination of the raindrop size distribution function and the terminal velocity of raindrops. The total splash amount was seen as the sum of the impact amount by all raindrops in the rainfall event. The total splash amount per unit time was subdivided into three different components, including net splash amount, single impact amount and re-detachment amount. The re-detachment amount was obtained by a spatial geometric probability derived using the Poisson function in which overlapped impacted areas were considered. The net splash amount was defined as the mass of soil particles collected outside the splash dish. It was estimated by another spatial geometric probability in which the average splashed distance related to the median grain size of soil and effects of other impacted soil particles and other free-falling raindrops were considered. Splash experiments in artificial rainfall were carried out to validate the availability and accuracy of the model. Our simulated results suggested that the net splash amount and re-detachment amount were small parts of the total splash amount. Their proportions were 0.15% and 2.6%, respectively. The comparison of simulated data with measured data showed that this model could be applied to simulate the soil-splash process successfully and needed information of the rainfall intensity and original soil properties including initial bulk intensity, water content, median grain size and some empirical constants related to the soil surface shear strength, the raindrop size distribution function and the average splashed distance. Copyright (c) 2007 John Wiley & Sons, Ltd.