Explaining the lazy Krivine machine using explicit substitution and addresses

In a previous paper, Benaissa, Lescanne, and Rose, have extended the weak lambda-calculus of explicit substitution λ σ _w with addresses, so that it gives an account of the sharing implemented by lazy functional language interpreters. We show in this paper that their calculus, called λ σ _w ^a , fits well to the lazy Krivine machine, which describes the core of a lazy (call-by-need) functional programming language implementation. The lazy Krivine machine implements term evaluation sharing, that is essential for efficiency of such languages. The originality of our proof is that it gives a very detailed account of the implemented strategy.     

On the correctness of the Krivine machine

We provide a short proof of the correctness of the Krivine machine by showing how it simulates weak head reduction.     

Circular programs and self-referential structures

A circular program creates a data structure whose computation depends upon itself or refers to itself. The technique is used to implement the classic data structures circular and doubly-linked lists, threaded trees and queues, in a functional programming language. These structures are normally thought to require updateable variables found in imperative languages. For example, a functional program to perform the breadth-first traversal of a tree is given. Some of the examples result in circular data structures when evaluated. Some examples are particularly space-efficient by avoiding the creation of intermediate temporary structures which would otherwise later become garbage. Lastly, the technique can be applied in an imperative language to give an elegant program.     

Strongly reducing variants of the Krivine abstract machine

We present two variants of the Krivine abstract machine that reduce lambda-terms to full normal form. We give a proof of their correctness by interpreting their behaviour in the λ σ-calculus. This article is an extended version of a paper presented at the ‘Lisp and Functional Programming’ Conference in 1990 and the work was done at Ecole Normale Supérieure between 1989 and 1991.     

The costs and benefits of lazy interactive input in pascal

The programming language Pascal was designed and implemented in a non-interactive programming environment. This paper surveys proposals for incorporating interaction into Pascal, and focuses on a scheme known as ‘lazy evaluation’. It presents and compares performance measurements of two Pascal run-time systems for the same compiler; a buffered, non-interactive version, and a modification of that system to support lazy evaluation.     

Fast video segment retrieval by Sort-Merge feature selection, boundary refinement, and lazy evaluation

We present a fast video retrieval system with three novel characteristics. First, it exploits the methods of machine learning to construct automatically a hierarchy of small subsets of features that are progressively more useful for indexing. These subsets are induced by a new heuristic method called Sort-Merge feature selection, which exploits a novel combination of Fastmap for dimensionality reduction and Mahalanobis distance for likelihood determination. Second, because these induced feature sets form a hierarchy with increasing classification accuracy, video segments can be segmented and categorized simultaneously in a coarse-fine manner that efficiently and progressively detects and refines their temporal boundaries. Third, the feature set hierarchy enables an efficient implementation of query systems by the approach of lazy evaluation, in which new queries are used to refine the retrieval index in real-time. We analyze the performance of these methods, and demonstrate them in the domain of a 75-min instructional video and a 30-min baseball video.     

Using typed lambda calculus to implement formal systems on a machine

Much research has been devoted in building computer systems for checking proofs or for developing interactively correct proofs in specific logical systems. However, implementing a proof environment for a specific logical system is both complex and time-consuming, this-together with the proliferation of logics-suggests that a uniform and reliable alternative is desirable. One such alternative is the Edinburgh Logical Framework (LF), developed in the late eighties at the LFCS (Laboratory for Foundations of Computer Science). The LF is a logic-independent tool which, given a specification for a logical system, synthesizes a proof editor and checker for that system. Its specification language is based on a general theory of logics, which enables one to capture uniformities and idiosyncrasies of a large class of logics without sacrificing generality for tractability. Peculiarities (such as side conditions on rule application, variable occurrence or formula formation) are expressed at the level of the specification. In this paper we are going to provide a broad illustration of its applicability and discuss to what extent it is successful. The analysis (of the formal presentation) of a system carried out through encoding often illuminates the system itself. This paper will also deal with this phenomenon.     

对象式Lambda演算的自作用部分计值

讨论了一个对象式Lambda演算的部分计值器.对象式Lambda演算在Lambda演算的基础上添加了对象机制.部分计值器的构造是采用传统的三步法,首先定义对象式Lambda演算的元解释器;然后提出对象式Lambda演算的约束时间分析方法(binding-timeanalysis),约束时间分析决定哪些计算可以在编译时完成,哪些计算需留在运行时执行;最后定义部分计值器,同时,给出了元解释器和部分计值器的正确性证明.     

A generic lazy evaluation scheme for exact geometric computations

We present a generic C++ design to perform exact geometric computations efficiently using lazy evaluations. Exact geometric computations are critical for the robustness of geometric algorithms. Their efficiency is also important for many applications, hence the need for delaying the costly exact computations at run time until they are actually needed, if at all. Our approach is generic and extensible in the sense that it is possible to make it a library that users can apply to their own geometric objects and primitives. It involves techniques such as generic functor-adaptors, static and dynamic polymorphism, reference counting for the management of directed acyclic graphs, and exception handling for triggering exact computations when needed. It also relies on multi-precision arithmetic as well as interval arithmetic. We apply our approach to the whole geometry kernel of Cgal.     

An efficient abstract machine for Safe Ambients

Safe Ambients (SA) are a variant of the Ambient Calculus (AC) in which types can be used to avoid certain forms of interferences among processes called grave interferences.An abstract machine, called GcPan, for a distributed implementation of typed SA is presented and studied. Our machine improves over previous proposals for executing AC, or variants of it, mainly through a better management of special agents (the forwarders), created upon code migration to transmit messages to the target location of the migration. Well-known methods (such as reference counting and union-find) are applied in order to garbage collect forwarders, thus avoiding long – possibly distributed – chains of forwarders, as well as avoiding useless persistent forwarders.We present the proof of correctness of GcPan w.r.t. typed SA processes. We describe a distributed implementation of the abstract machine in OCaml.More broadly, this study is a contribution towards understanding issues of correctness and optimisations in implementations of distributed languages encompassing mobility.     

Linguistic extension of abstract machine modelling to aid software development

The traditional use of abstract machine models is to provide a conceptual framework for software design and to aid portability and machine independence. Access to the abstract machine model from the higher-level system on which it is based provides a powerful tool for software development. This paper describes a technique in which the higher-level system is interfaced to the underlying abstract machine, thus allowing use of the higher-level system to analyse and debug its own implementation. The application of this technique in the implementation of SL5 is given as an example. Experience with the use of the facility and a discussion of basic design considerations are included.     

A Fully Labelled Lambda Calculus: Towards Closed Reduction in the Geometry of Interaction Machine

We investigate the possibility of performing new reduction strategies with the Geometry of Interaction Machine (GOIm). To this purpose, we appeal to Lévy's labelled lambda calculus whose labels describe: a) the path that the GOIm will follow in the graph of a term and b) the operations that the GOIm requires to compute the multiplicative part from the Multiplicative and Exponential Linear Logic encoding that the machine uses. Our goal is to unveil the missing exponential information in the structure of the labels. This will provide us with a tool to talk about strategies for computing paths with the GOIm.     

State-transition machines for lambda-calculus expressions

The process of compiler generation from lambda-calculus definitions is studied. The compiling schemes developed utilize as their object language the set of state transition machines (STMs): automata-like transition sets using first-order arguments. An intermediate definition form, the STM-interpreter, is treated as central to the formulation of STMs. Three compiling schemes are presented: one derived directly from an STM-interpreter for the lambda-calculus; one formulated from an STM-interpreter variant of Landin’s SECD-machine; and one defined through meaning-preserving transformations upon a denotational definition of the lambda-calculus. The results are compared and some tentative conclusions are made regarding the utility of compiler generation with the STM forms. Permanent address: Computing and Information Science Department, Kansas State University, Manhattan, KS 66506, USA.     

Improving on-line handwritten recognition in interactive machine translation

On-line handwriting text recognition (HTR) could be used as a more natural way of interaction in many interactive applications. However, current HTR technology is far from developing error-free systems and, consequently, its use in many applications is limited. Despite this, there are many scenarios, as in the correction of the errors of fully-automatic systems using HTR in a post-editing step, in which the information from the specific task allows to constrain the search and therefore to improve the HTR accuracy. For example, in machine translation (MT), the on-line HTR system can also be used to correct translation errors. The HTR can take advantage of information from the translation problem such as the source sentence that is translated, the portion of the translated sentence that has been supervised by the human, or the translation error to be amended. Empirical experimentation suggests that this is a valuable information to improve the robustness of the on-line HTR system achieving remarkable results.     

A new implementation technique for applicative languages

It is shown how by using results from combinatory logic an applicative language, such as LISP, can be translated into a form from which all bound variables have been removed. A machine is described which can efficiently execute the resulting code. This implementation is compared with a conventional interpreter and found to have a number of advantages. Of these the most important is that programs which exploit higher order functions to achieve great compactness of expression are executed much more efficiently.     

Web-based algorithm for cylindricity evaluation using support vector machine learning

This paper introduces a cylindricity evaluation algorithm based on support vector machine learning with a specific kernel function, referred to as SVR, as a viable alternative to traditional least square method (LSQ) and non-linear programming algorithm (NLP). Using the theory of support vector machine regression, the proposed algorithm in this paper provides more robust evaluation in terms of CPU time and accuracy than NLP and this is supported by computational experiments. Interestingly, it has been shown that the SVR significantly outperforms LSQ in terms of the accuracy while it can evaluate the cylindricity in a more robust fashion than NLP when the variance of the data points increases. The robust nature of the proposed algorithm is expected because it converts the original nonlinear problem with nonlinear constraints into other nonlinear problem with linear constraints. In addition, the proposed algorithm is programmed using Java Runtime Environment to provide users with a Web based open source environment. In a real-world setting, this would provide manufacturers with an algorithm that can be trusted to give the correct answer rather than making a good part rejected because of inaccurate computational results.     

On the efficiency of categorical combinators as a rewriting system

Categorical combinators form a formal system similar to Curry's combinatory logic. The original system was developed by Curien, inspired by the equivalence of the theories of typed λ-calculus and Cartesian closed categories, as shown by Lambek and Scott. A new system for categorical combinators was introduced by the author. This system uses a more compact notation for the code and needs a smaller set of rewriting rules. The aim of this paper is to analyse these two different rewriting systems for categorical combinators as a basis for implementation of applicative languages, and compare them with the classical approach due to Turner, using combinatory logic.     

Design and simulation of a parallel inference machine architecture for rule based systems

This paper presents an architecture of the inference machine for a rule based expert system. The paper, structured around the concept of “inference flow graphs”, is aimed at incorporating parallelism in antecedent matching to find out the firable rules as well as firing more than one rule simultaneously, whenever required. Through this architecture, the number of comparisons required during the antecedent matching phase, is significantly reduced. The flow of inferencing can also proceed in a pipelined manner resulting in faster inferences.