λ演算中的第二不动点定理*

作者研究λ演算中的第二不动点的性质．首先讨论关于第二不动点的3个命题之间的关系且证明了它们．然后为第二不动点组合子给以一个充分条件且作出一系列的第二不动点组合子．作者还提出和证明了多元第二不动点定理．     

有效的ν支持向量回归机的ν解路径算法

由Sch lkopf等人提出的v支持向量回归机具有通过参数控制支持向量和错误向量个数的优点,然而与标准的支持向量机相比,其形式更为复杂,迄今为止仍没有有效的算法计算v解路径.基于支持向量回归机的修改形式,提出了一种新的解路径算法,它能够追踪参数v对应的所有解,并通过理论分析和实验,说明了该算法能够尽可能地避免不可行的更新路径,并在有限步内拟合出所有的解路径.     

算子Fuzzy逻辑中的λ—蕴涵和λ—强蕴涵

在本文中,我们引进了算子模糊逻辑中的λ-蕴涵和λ-强蕴涵的概念,λ-逻辑结果和λ-弱逻辑结果的概念。证明了两子句的的λ-归结式是这两个子句的λ-逻辑结果,从而完成了λ-归结的完备性定理的证明。     

无线传感器网络中(ε,δ)-近似聚集算法

提出了一种基于Bernoulli抽样的近似聚集算法,以满足无线传感器网络(简称WSN)中用户给定的任意精度需求.同时,还提出了两种样本数据的自适应算法,分别用于处理用户的精确度需求以及网络中的感知数据发生变化的情况.理论分析及实验结果表明,所提出的算法在近似结果的精确度、能量开销等方面均优于已有的近似聚集算法.     

基于网络演算的簇树WSN性能上界分析

为保证WSN的服务质量(QoS),需精确求解其性能上界。对进入WSN节点的数据流进行漏桶管制,节点为数据流提供基于速率-延迟模型的服务保障,在已有簇状拓扑WSN性能模型研究基础上,利用确定性网络演算理论推导簇树WSN节点的有效带宽、缓冲区队列长度上界和数据流端到端延迟上界。     

具有模态词□φ=□1V□2φ且可靠与完备的公理系统

提出具有模态词□φ=□₁V□₂φ的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□₁与□₂是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=□₁V□₂φ;框架定义为三元组W,R₁,R₂,模型定义为四元组W,R₁,R₂,I;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果□₁的可达关系R₁等于□₂的可达关系R₂,那么该逻辑的公理化系统变成S5.     

基于流演算的多Agent请求/服务协作模型的研究

为了刻画多Agent环境中的交互特性,基于流演算理论和GoFlux语言,吸收了ConGolog语义,提出了CFlux语言。CFlux语言能有效地处理MAS中的For循环、并发、优先级并发、中断等操作,从而可以实现多Agent程序的并发交互执行。在此基础上,基于CFlux和一组通信动作提出一个请求/服务协作模型。最后,通过一个智能日程安排实例表明了上述理论。     

一种从面向对象Z规约到代码的精化演算方法

COOZ(complete object-oriented Z)的优势在于精确描述大型程序的规约.COOZ本身的结构 不支持精化演算,这限制了COOZ的应用能力,使COOZ难以作为完整的方法应用于软件的开发. 将精化演算引入COOZ,弥补了COOZ在设计和实现阶段的不足,同时也消除了规约与实现之间在 结构和表示方法上的完全分离,使程序开发在一个完整的框架下平滑进行.该文提出了基于CO OZ和精化演算的软件开发模型,通过实例讨论了数据精化和操作精化问题.在精化演算实现技 术方面构造了一种数据精化算子,提出一     

MDA中从PIM到PSM的模型转换

基于在MDA中PIM到PSM的模型转换实现,提出了用UML描述PIM的一种有效性补充(E-)LOTOS,试图达到在模型映射前实现对模型的有效逻辑验证;对模型转换的基础理论进行了探索,分析了目前在MDA中实现从PIM到PSM模型转换的主要途径和困难;最后展望了模型转换的实现前景。     

边赋权森林ω-路划分的O(n)算法

ω-路划分问题是路划分问题的一般化,它源于并行计算机系统、计算机网络与分布式控制系统等一类广播通信问题.设置最少的信息源节点,使得在指定的时间内将信息源节点所拥有的信息发送到其余节点,并且保证不同通信线路之间不得相交.从Hamilton路的NP-完全性不难看出,ω-路划分问题属于NP-完全问题.通过构造性证明技术,获得了边赋非负权路径、树和森林的ω-路划分问题的一些性质.分别提出了求解边赋非负权路径和边赋非负权树的ω-路划分问题的线性时间算法,讨论了算法的局部实现技术,详细地分析了这些算法的复杂度.以这两个算法为基础,提出了一个线性时间算法求解边赋非负权森林的ω-路划分问题.所提出的算法直观简明、操作容易,只需要较少的运行时间和较小的存储空间.     

Translating Braille into Chinese based on improved CBHG model

Transforming Mandarin Braille to Chinese text is a significant but less focused machine translation task. CBHG is a building block used in the Tacotron text-to-speech model. Since Mandarin Braille is constructed from the pronunciation of Chinese characters, CBHG can be used to perform Braille–Chinese translation. Unfortunately, only relying on the convolution blocks in CBHG cannot effectively extract the features of Braille sequences. Two ways are proposed to improve the CBHG model: CBHG-SE and CBHG-ECA. The two modules adaptively recalibrate channel-wise feature responses by explicitly modeling interdependencies between channels in CBHG. The quality of representations produced by the network can also be improved. Meanwhile, the network can learn to use global information to emphasize informative features and suppress less useful ones selectively. CBHG-ECA has stronger feature recalibration capabilities than CBHG-SE due to its more direct correspondence between channels and their weights. These two models can achieve 92.23 BLEU and 91.48 BLEU on the Braille–Chinese dataset, outperforming CBHG and other neural machine translation models.     

Expressing First-Order pi-Calculus in Higher-Order Calculus of Communicating Systems

In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order calculi (higher-order Calculus of Communicating Systems (CCS) and higher-orderπ-calculus, respectively) and the encoding from and to first-orderπ-calculus. However a fully abstract encoding of first-orderπ-calculus with higher-order CCS is not available up-tod...     

A Calculus for Reconfiguration: (Extended abstract)

We present a simple calculus, called R-calculus (for “reconfiguration”), intended to provide a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducing as basic terms of the calculus configurations, which are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a program running in the context of these components. The R-calculus has been originally developed as a formal model for programming-in-the large, where computations correspond to applications running in some context of software components, and operations at the meta-level correspond to the possibility of dynamically loading, updating or in general manipulat- ing these software components without stopping the application. However, the calculus can also encode programming-in-the-small issues, because configurations combine the features of lambda- abstractions (first-class functions), records, environments with mutually recursive definitions, and modules. We state confluence of the calculus and define a call-by-need strategy which leads to a generalization, including reconfiguration features, of call-by-need lambda-calculi.     

Taking Decisions Late: End-Based Choice Combined with Action Refinement

A choice in concurrent systems is usually taken by the starting of an action. We propose the alternative view that a choice is determined by the ending of actions as this alternative has relevant applications and interesting implications. The different points of view lead in particular to different refinement operators.We introduce a refinement operator on bundle event structures for the end-based view. The standard equivalences are not preserved by this refinement operator. Therefore, we also introduce and study new equivalences that are preserved by our refinement operator.     

A fully abstract semantics for value-passing CCS for trees

We propose a fully abstract semantics for valuepassing CCS for trees (VCCTS) with the feature that processes are located at the vertices of a graph whose edges describe possible interaction capabilities. The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. We develop a theory of behavioral equivalences by introducing both weak barbed congruence and weak bisimilarity. In particular, we show that, on image-finite processes, weak barbed congruence coincides with weak bisimilarity. To illustrate potential applications and the powerful expressiveness of VCCTS, we formally compare VCCTS with some well-known models, e.g., dynamic pushdown networks, top-down tree automata and value-passing CCS.     

PPDDL一致性规划任务的有限域转换方法

给出了PPDDL一致性规划任务和有限域一致性规划任务的定义,扩展了非确定动作等相关语义,并在此基础上提出了一种将PPDDL表示的一致性规划任务转换为有限域表示的一致性规划任务的CFDR方法,实现了经典规划的FDR转换算法在一致性规划中的扩展。相比MCPT算法,主要改进了其中的合成不变量方法和任务生成方法,此外还增加了对于非确定动作效果的表示和处理。通过在标准的一致性规划域上的实验,证明了CFDR的适用性和有效性。     

A Calculus for Dynamic Reconfiguration with Low Priority Linking

Building on our previous work, we present a simple module calculus where execution steps of a module component can be interleaved with reconfiguration steps (that is, reductions at the module level), and where execution can partly control precedence between these reconfiguration steps. This is achieved by means of a low priority link operator which is only performed when a certain component, which has not been linked yet, is both available and really needed for execution to proceed, otherwise precedence is given to the outer operators. We illustrate the expressive power of this mechanism by a number of examples.We ensure soundness by combining a static type system, which prevents errors in applying module operators, and a dynamic check which raises a linkage error if the running program needs a component which cannot be provided by reconfiguration steps. In particular no linkage errors can be raised if all components are potentially available.     

Trace 演算

文章定义了基于踪迹(trace)的逻辑语言L_Trace,它是一阶线性时序逻辑语言的扩充,同时也是“对象演算”研究工作的基础.Trace演算所述的“对象”用来刻画具有内部状态和外部行为的动态实体,语法上由对象标记表示.对象标记Ω=(S,F,A,E)包含4个部分:数据类型S、函数F、属性A和动作E.Σ=(S,F)构成通常代数规范意义下的标记,可将动作看成一广义数据类型,从而得到标记Σ的动作扩充ΣE.对象标记的语义解释结构由关于标记ΣE的代数、映射和动作与踪迹的关系定义.ΣE-代数给出关于数据参数的解释;映射给出属性在动作踪迹中所取的值;而动作与踪迹的关系则给出执行一有限踪迹以后该动作是否允许执行.在定义了Trace演算的语法和语义之后,文章给出了Trace演算的公理系统及其可靠性证明.     

图像的平视化处理

摄像机拍摄图像时,会使物体在同一水平面上的边缘呈现曲线形状,给图像处理方法的实现和图像边缘位置的定位带来不便。这篇文章研究了把图像的曲线边缘变为直线边缘的图像平视化处理方法,推导了像素点和空间点的对应关系公式,陈述了图像平视化处理的思路,并对现场采集的图像进行了平视化处理。通过试验,这篇文章的平视化方法取得了较好的效果。     

Probabilistic Situation Calculus

In this article we propose a Probabilistic Situation Calculus logical language to represent and reason with knowledge about dynamic worlds in which actions have uncertain effects. Uncertain effects are modeled by dividing an action into two subparts: a deterministic (agent produced) input and a probabilistic reaction (produced by nature). We assume that the probabilities of the reactions have known distributions.Our logical language is an extension to Situation Calculae in the style proposed by Raymond Reiter. There are three aspects to this work. First, we extend the language in order to accommodate the necessary distinctions (e.g., the separation of actions into inputs and reactions). Second, we develop the notion of Randomly Reactive Automata in order to specify the semantics of our Probabilistic Situation Calculus. Finally, we develop a reasoning system in MATHEMATICA capable of performing temporal projection in the Probabilistic Situation Calculus.