一类递归函数的多态类型

以上下文无关语言上的递归函数为基础的语言LFC(1anguage for context free recursive function)是一种形式规约语言,适于处理短语结构.LFC也是函数式语言,具有函数式语言的许多特点.LFC已经在形式规约获取系统SAQ(specification acquisition system)中实现,为其最初设计的类型系统不支持多态类型.引入类型变量和相应的类型检查方法,就可以将其类型系统扩充为多态类型系统.对多态类型系统实现中的一些问题也进行了讨论.在实现多态之后,LFC     

Garment中多态类型的Ideal模型

本文从Ideal的基本概念出发,研究了Ideal作为类型的语义模型所具有的性质.在类型的Ideal模型下,讨论了Garment中参数化多态类型和约束多态类型的语义.并在此基础上,证明了Garment中类型规则的语义可靠性.     

对象在类型系统λω×≤中的表示

类型系统是研究面向对象技术形式理论基础的重要工具 类型系统λω×≤ 是一个带高阶子类型关系的多态类型系统 ,对其性质和范畴论语义模型进行了研究 在此基础上 ,讨论了如何以类型系统λω× ≤ 为工具 ,研究对象、类、继承等面向对象技术的基本概念的形式语义 结合类POINT和CPOINT等例子 ,讨论了基于递归类型和基于存在类型的两种对象表示方法 ,并对它们的特点进行了总结与比较     

类型系统的λω×≤等式理论及其语义的合理性

类型系统在研究程序设计语言的理论基础方面起着十分重要的作用,特别地,带子类型的多态类型系统可刻画面向对象程序设计语言核心概念,如子类型、多态性等.为研究面向对象程序设计语言的形式理论基础,探讨了一个命名为类型系统λω×≤的带高阶子类型的多态类型系统,并利用插入子和fibration理论,引入λω×≤fibration作为该类型系统的语义模型.进一步,讨论了类型系统λω×≤的等式理论,特别是与受限全称量词有关的等式,并利用插入子的性质,证明了对于该等式理论,λω×≤fibration是合理的语义模型.     

Goedel语言类型系统

Goedel语言是一种说明性逻辑程序设计语言。该语言基于一阶逻辑，引入了一个多态多类的类型系统和多种新的语言成分，支持抽象数据类型和模块化程序设计等技术，语言本身也具有很强的说明性语义。详细介绍了Goedel语言的类型系统及其构造，对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论。     

Gdel语言类型系统

Gdel语言是一种说明性逻辑程序设计语言。该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义。详细介绍了Gdel语言的类型系统及其构造,对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论。     

Gödel语言类型系统

G(o)del语言是一种说明性逻辑程序设计语言.该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义.详细介绍了G(o)del语言的类型系统及其构造,对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论.     

G(o)del语言类型系统

G(o)del语言是一种说明性逻辑程序设计语言.该语言基于一阶逻辑,引入了一个多态多类的类型系统和多种新的语言成分,支持抽象数据类型和模块化程序设计等技术,语言本身也具有很强的说明性语义.详细介绍了G(o)del语言的类型系统及其构造,对在逻辑程序设计语言中引入类型系统的作用进行了一些深入的分析和讨论.     

多态π演算的互模拟等价关系及其公理化

类型系统在分布式系统理论中有着非常重要的作用。在为π演算引入多态类型系统后,需要对新的环境下进程的等价关系进行研究。在多态类型系统下,环境只能得知进程中通道的抽象类型,而无法得知通道的具体类型,此时环境的区分能力被削弱,所得到的互模拟关系更为粗糙。本文在以往文献研究的基础上给出了多态π演算互模拟的一个公理系统,并证明了公理系统的一致性和完备性。     

改进的流不敏感的类型限定词推断

类型限定词可以精化标准类型,提高类型系统的表达能力。流不敏感的类型限定词推断已被用于CQual架构,以提高C程序的质量。然而,类型转化会影响类型限定词推断的有效性。首先,展示了一种允许类型转化的程序语言和流不敏感的限定词推断系统;其次,提出了变量参与的限定词推断系统,引入了联合类型并给出约束求解算法;最后,证明了推断的正确性并展示了一些实例运行结果。     

结合限制的分隔模型及K-Means算法

将数据对象间的关联限制与K-means算法结合可以取得较好的效果,但由于划分是由K个中心决定的,每一类仅由一个中心决定,分隔的表示方法限制了算法效果的进一步提高.基于数据对象间的两类限制,定义了数据对象和集合间的两类关联,以及集合间的3类关联,在此基础上给出了结合限制的分隔模型.在模型中,基于集合间的正关联,多个子集中心可以用来表示同一类,使划分的表示可以更为灵活、精细.基于此模型,给出了相应的算法CKS(constrained K-meanswith subsets)来生成结合限制的分隔.对3个UCI数据集的实验结果显示:在准确率及健壮性上,CKS显著优于另一个结合关联限制的K-means类算法COP-K-means,与另一个代表性的算法CCL相比,也有相当优势;在时间代价上,CKS也有一定优势.     

函数式语言编译中多态类型的实现技术

函数式程度设计语言的重要特点之一是多态类型。它有很强的功能，是所有面向对象的程度设计语言实现多态性的重要机制之一。它的实现与基本数据类型和其它复合类型大不相同。本文给出实现多态类型的重要数据结构，通过剖析ＳＭＬ函数式程度设计语言编译程序中的类型推导过程，提示了多态类型的基本特征及其实现技术。     

Type-directed weaving of aspects for polymorphically typed functional languages

Incorporating aspect-oriented paradigm to a polymorphically typed functional language enables the declaration of type-scoped advice, in which the effect of an aspect can be harnessed by introducing possibly polymorphic type constraints to the aspect. The amalgamation of aspect orientation and functional programming enables quick behavioral adaption of functions, clear separation of concerns and expressive type-directed programming. However, proper static weaving of aspects in polymorphic languages with a type-erasure semantics remains a challenge. In this paper, we describe a type-directed static weaving strategy, as well as its implementation, that supports static type inference and static weaving of programs written in an aspect-oriented polymorphically typed functional language, AspectFun. We show examples of type-scoped advice, identify the challenges faced with compile-time weaving in the presence of type-scoped advice, and demonstrate how various advanced aspect features can be handled by our techniques. Finally, we prove the correctness of the static weaving strategy with respect to the operational semantics of AspectFun.     

Cutting Plane Method for Continuously Constrained Kernel-Based Regression

Incorporating constraints into the kernel-based regression is an effective means to improve regression performance. Nevertheless, in many applications, the constraints are continuous with respect to some parameters so that computational difficulties arise. Discretizing the constraints is a reasonable solution for these difficulties. However, in the context of kernel-based regression, most of existing works utilize the prior discretization strategy; this strategy suffers from a few inherent deficiencies: it cannot ensure that the regression result totally fulfills the original constraints and can hardly tackle high-dimensional problems. This paper proposes a cutting plane method (CPM) for constrained kernel-based regression problems and a relaxed CPM (R-CPM) for high-dimensional problems. The CPM discretizes the continuous constraints iteratively and ensures that the regression result strictly fulfills the original constraints. For high-dimensional problems, the R-CPM accepts a slight and controlled violation to attain a dimensional-independent computational complexity. The validity of the proposed methods is verified by numerical experiments.      

Suboptimal control of linear time-invariant systems subject to control structure constraints

A method is presented for designing controllers for linear time-invariant systems whose states are not all available or accessible for measurement and where the structure of the controller is constrained to be a linear time-invariant combination of the measurable states of the system. Two types of structure constraints are considered: 1) each control channel is constrained to be a linear, time-invariant combination of one set of measurable states; 2) each control channel is constrained to he a linear, time-invariant combination of different sets of measurable states. The control system, subject to these constraints is selected such that the resulting closed-loop system performs as "near" to some known optimal system as is possible, i.e., suboptimal. The nearness of the optimal system to the suboptimal system is defined in two ways and thus, two types of suboptimal controllers are found.     

Type checking and typability in domain-free lambda calculi

This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic lambda calculus, and (3) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with function and existential types. The first and the third results are proved by the second result and CPS translations that reduce those problems in the domain-free polymorphic lambda calculus to those in the domain-free lambda calculi with existential types. The key idea is the conservativity of the domain-free lambda calculi with existential types over the images of the translations.     

An Unboxed Operational Semantics for ML Polymorphism

We present an unboxed operational semantics for an ML-style polymorphic language. Different from the conventional formalisms, the proposed semantics accounts for actual representations of run-time objects of various types, and supports a refined notion of polymorphism that allows polymorphic functions to be applied directly to values of various different representations. In particular, polymorphic functions can receive multi-word constants such as floating-point numbers without requiring them to be boxed (i.e., heap allocated.) This semantics will serve as an alternative basis for implementing polymorphic languages. The development of the semantics is based on the technique of the type-inference-based compilation for polymorphic record operations [20]. We first develop a lower-level calculus, called a polymorphic unboxed calculus, that accounts for direct manipulation of unboxed values in a polymorphic language. This unboxed calculus supports efficient value binding through integer representation of variables. Different from de Bruijn indexes, our integer representation of a variable corresponds to the actual offset to the value in a run-time environment consisting of objects of various sizes. Polymorphism is supported through an abstraction mechanism over argument sizes. We then develop an algorithm that translates ML into the polymorphic unboxed calculus by using type information obtained through type inference. At the time of polymorphic let binding, the necessary size abstractions are inserted so that a polymorphic function is translated into a function that is polymorphic not only in the type of the argument but also in its size. The ML type system is shown to be sound with respect to the operational semantics realized by the translation.