Nominalization,predication and type containment

In an attempt to accommodate natural language phenomena involving nominalization and self-application, various researchers in formal semantics have proposed abandoning the hierarchical type system which Montague inherited from Russell, in favour of more flexible type regimes. We briefly review the main extant proposals, and then develop a new approach, based semantically on Aczel's notion of Frege structure, which implements a version ofsubsumption polymorphism. Nominalization is achieved by virtue of the fact that the types of predicative and propositional complements are contained in the type of individuals. Russell's paradox is avoided by placing a type-constraint on lambda-abstraction, rather than by restricting comprehension.Kamareddine is grateful to the Department of Mathematics and Computing Science, Technical University of Eindhoven, for their financial support and hospitality during the academic year 1991–92.Klein's work has been carried out as part of the research programmes of the dyana project (BR 3175 and BR 6852), funded by CEC esprit Basic Research Division, and of the Human Communication Research Centre, supported by the UK Economic and Social Research Council.     

抽象算法C—T—ABS和ABSTRACT的理论推导与等价性证明

ＡＢＳＴＲＡＣＴ，Ｃ－Ｔ－ＡＢＳ是把λ表达式转换成ＳＫＩ表达式的抽象算法，是函数式语言实现的理论基础。本文从λ演算，ＳＫＩ演算的基本理论出发，对这两个算法进行了理论推导及功能的等价证明。展示了对一输入，Ｃ－Ｔ－ＡＢＳ能生成较优化的代码，并对它们生成代码的长度及归约效率进行了比较。     

A Polymorphic Environment Calculus and its Type-Inference Algorithm

The polymorphic environment calculus is a polymorphic lambda calculus which enables us to treat environments as first-class citizens. In the calculus, environments are formalized as explicit substitutions, and the substitutions are included in the set of terms of the calculus. First, we introduce an untyped environment calculus, and we present a semantics of the calculus as a translation into the lambda calculus. Second, we propose a polymorphic type system for the environment calculus based on Damas-Milner's ML-polymorphic type system. In ML, polymorphism is allowed only in let-expressions; in the polymorphic environment calculus, polymorphism is provided with environment compositions. We prove a subject-reduction theorem for the type system. Third, a type-inference algorithm is given to the polymorphic environment calculus, and we establish its soundness, termination, and principal-typing theorem.     

A fast neural net training algorithm and its application to speech classification

This paper describes a fast training algorithm for feedforward neural nets, as applied to a two-layer neural network to classify segments of speech as voiced, unvoiced, or silence. The speech classification method is based on five features computed for each speech segment and used as input to the network. The network weights are trained using a new fast training algorithm which minimizes the total least squares error between the actual output of the network and the corresponding desired output. The iterative training algorithm uses a quasi-Newtonian error-minimization method and employs a positive-definite approximation of the Hessian matrix to quickly converge to a locally optimal set of weights. Convergence is fast, with a local minimum typically reached within ten iterations; in terms of convergence speed, the algorithm compares favorably with other training techniques. When used for voiced-unvoiced-silence classification of speech frames, the network performance compares favorably with current approaches. Moreover, the approach used has the advantage of requiring no assumption of a particular probability distribution for the input features.     

Parallel implementations of Brunotte’s algorithm

In this paper the author make a comprehensive comparison of different parallelizations of a sequential number theoretic algorithm having large memory requirements. Brunotte’s algorithm is one of the currently known best methods for the decision of the canonical number system (or more generally shift radix system) property. Still, it can be very space-consuming in some cases. Pushing the algorithm to its limits may hopefully shed light on mathematical patterns that would otherwise not be discernible. The algorithm contains many n-dimensional vector operations and set operations like insert, find, clear, etc. The parallel algorithms encounter two difference kinds of concurrency problems. First, they need computationally intensive arithmetic vector operations, second, the set implementations require a huge amount of memory and general purpose processors. The algorithms described in this article are basically designed for two platforms. The first platform is a generic symmetric multiprocessing (SMP) architecture without any vector processor extension, the second is the Cell Broadband Engine. The SMP platforms have several general purpose processors in contrast with the Cell Broadband Engine where the processors have Synergistic vector processors.     

The particle swarm optimization algorithm: convergence analysis and parameter selection

The particle swarm optimization algorithm is analyzed using standard results from the dynamic system theory. Graphical parameter selection guidelines are derived. The exploration-exploitation tradeoff is discussed and illustrated. Examples of performance on benchmark functions superior to previously published results are given.     

决策树算法的系统实现与修剪优化

决策树是对分类问题进行深入分析的一种方法,在实际问题中,按算法生成的决策树往往复杂而庞大,令用户难以理解,这就告诉我们在重分类精确性的同时,也要加强对树修剪的研究,以一个决策树算法的程序实现为例,进一步讨论了对树进行修剪优化时可能涉及的问题,目的在于给决策树研究人员提供一个深入和清晰的简化技术视图。     

Hybrid multi-objective shape design optimization using Taguchi’s method and genetic algorithm

This research is based on a new hybrid approach, which deals with the improvement of shape optimization process. The objective is to contribute to the development of more efficient shape optimization approaches in an integrated optimal topology and shape optimization area with the help of genetic algorithms and robustness issues. An improved genetic algorithm is introduced to solve multi-objective shape design optimization problems. The specific issue of this research is to overcome the limitations caused by larger population of solutions in the pure multi-objective genetic algorithm. The combination of genetic algorithm with robust parameter design through a smaller population of individuals results in a solution that leads to better parameter values for design optimization problems. The effectiveness of the proposed hybrid approach is illustrated and evaluated with test problems taken from literature. It is also shown that the proposed approach can be used as first stage in other multi-objective genetic algorithms to enhance the performance of genetic algorithms. Finally, the shape optimization of a vehicle component is presented to illustrate how the present approach can be applied for solving multi-objective shape design optimization problems.     

On Euclid’s algorithm and elementary number theory

Algorithms can be used to prove and to discover new theorems. This paper shows how algorithmic skills in general, and the notion of invariance in particular, can be used to derive many results from Euclid’s algorithm. We illustrate how to use the algorithm as a verification interface (i.e., how to verify theorems) and as a construction interface (i.e., how to investigate and derive new theorems).The theorems that we verify are well-known and most of them are included in standard number-theory books. The new results concern distributivity properties of the greatest common divisor and a new algorithm for efficiently enumerating the positive rationals in two different ways. One way is known and is due to Moshe Newman. The second is new and corresponds to a deforestation of the Stern-Brocot tree of rationals. We show that both enumerations stem from the same simple algorithm. In this way, we construct a Stern-Brocot enumeration algorithm with the same time and space complexity as Newman’s algorithm. A short review of the original papers by Stern and Brocot is also included.     

A model for synchronous switching circuits and its theory of correctness

Following Bryant [2], an algorithm is given for translating a switching circuit design into a program that simulates its dynamic behavior. A theory of assertions based on Dijkstra [5] and UNITY [4] is then developed to formalize specifications of hardware circuit designs and to establish their correctness. Both combinational and sequential circuits are taken into account both in N-mos and C-mos; the latter turns out to be much simpler.Chaochen Zhou in on leave from the Software Institute, Academia Sinica