自动分析递归数据结构的归纳性质

本文提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为三个主要部分.首先,它将递归数据结构的归纳性质分为两个主要类别,并提出对应的处理模式,从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次,提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的：递归数据结构首先被分割为若干个互不相交的片段,然后这些片段以新的方式重新拼接在一起,形成一个新的数据结构.这个技术的重点在于如何将程序原有的性质保留下来,从而为后面的分析过程所使用.最后,提出了一种调用上下文敏感的程序摘要过程间分析方法.案例分析和实验结果表明我们的分析框架可以有效地分析递归数据结构的归纳性质,并生成对程序证明过程有用的断言.     

Recursive Program Optimization through Inductive Synthesis Proof Transformation

The research described in this paper involved developing transformation techniques that increase the efficiency of the original program, the source, by transforming its synthesis proof into one, the target, which yields a computationally more efficient algorithm. We describe a working proof transformation system that, by exploiting the duality between mathematical induction and recursion, employs the novel strategy of optimizing recursive programs by transforming inductive proofs. We compare and contrast this approach with the more traditional approaches to program transformation and highlight the benefits of proof transformation with regards to search, correctness, automatability, and generality.     

归纳定义与递归算法

归纳定义是定义某些概念时常用到的一种定义方法，但是，什么叫做“归纳定义”并没有严格的说法，本文从代数系统的观点出发，对归纳定义进行了严格的数学定义。递归算法是编程时经常使用的一种算法设计方法，其思想就是算法本身调用自己。本文对归纳定义与递归算法之间的联系进行了深入的讨论和研究，结论是：利用归纳定义所定义的概念一定可以利用递归算法进行判定；反之，由递归算法可以判定的概念一定能够进行归纳定义。     

Inductive Synthesis of an Automaton from Its Specification in the Logical Language \mathfrak{L}

An approach to the synthesis of an automaton specified by a formula of the logical language is proposed. This approach makes it possible to construct the automaton inductively, i.e., according to the structure of the formula, starting from automata corresponding to subformulas represented in the form of conjunction or disjunction of literals.     

Logical Equivalence for Subtyping Object and Recursive Types

Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first order ς-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence. U. de’Liguoro’s research was partially supported by project PRIN’05 prot. 2005015785_003.     

Recursive Learning Automata Approach to Markov Decision Processes

In this note, we present a sampling algorithm, called recursive automata sampling algorithm (RASA), for control of finite-horizon Markov decision processes (MDPs). By extending in a recursive manner Sastry's learning automata pursuit algorithm designed for solving nonsequential stochastic optimization problems, RASA returns an estimate of both the optimal action from a given state and the corresponding optimal value. Based on the finite-time analysis of the pursuit algorithm by Rajaraman and Sastry, we provide an analysis for the finite-time behavior of RASA. Specifically, for a given initial state, we derive the following probability bounds as a function of the number of samples: 1) a lower bound on the probability that RASA will sample the optimal action and 2) an upper bound on the probability that the deviation between the true optimal value and the RASA estimate exceeds a given error.     

Conjecture Synthesis for Inductive Theories

We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures ‘bottom-up’ from the available constants and free variables. The synthesis process is made tractable by only generating irreducible terms, which are then filtered through counter-example checking and passed to the automatic inductive prover IsaPlanner. The main technical contribution is the presentation of a constraint mechanism for synthesis. As theorems are discovered, this generates additional constraints on the synthesis process. We evaluate IsaCoSy as a tool for automatically generating the background theories one would expect in a mature proof assistant, such as the Isabelle system. The results show that IsaCoSy produces most, and sometimes all, of the theorems in the Isabelle libraries. The number of additional un-interesting theorems are small enough to be easily pruned by hand.     

逻辑马尔可夫决策编程和关系马尔可夫决策编程若干最新进展

逻辑马尔可夫决策过程和关系马尔可夫决策过程的引入,使得人们可能简洁地、陈述地表达复杂的马尔可夫决策过程。本文首先介绍有关逻辑马尔可夫决策过程和关系马尔可夫决策过程的概念,然后重点介绍它们与普通的马尔可夫决策过程根本不同的一些算法：①依赖于基本状态空间RL的转换法;②把Bellman方程推广到抽象状态空间的方法;③利用策略偏置空间寻求近似最优策略方法。最后对它们的研究现状进行总结及其对它们发展的一些展望。     

Real-Time Properties of Indirect Recursive Procedures

The purpose of this paper is to show that indirect recursive procedures can be used for implementing real-time applications without harm, if a few conditions are met. These conditions ensure that upper bounds for space and time requirements can be derived at compile time. Moreover they are simple enough such that many important recursive algorithms can be implemented. In addition, our approach allows for concentrating on essential properties of the parameter space during space and time analysis. This is done by morphisms that transfer important properties from the original parameter space to simpler ones, which results in simpler formulas of space and time estimates.     

A Note on Synthesis of Inductive Assertions

One of the principal impediments to widespread use of automated program verification methodology is due to the user burden of creating appropriate inductive assertions. In this paper, we investigate a class of programs for which such inductive assertions can be mechanically generated from Input-output specifications. This class of programs, called accumulating programs, are iterative realizations of problems in which the required output information is accumulated during successive passes over the input data structures. Obtaining invariant assertions for such programs is shown to be equivalent to the problem of generalizations of specifications to that over an extended closed data domain. For this purpose, a set of basis data elements are to be conceived of as generating the extended domain. An arbitary data element would thus be considered as uniquely decomposable into a sequence of basis elements. The structural relations between the components of a data element are used to extend program behavior and thus obtain the desired invariant.     

Routing Properties of a Recursive Interconnection Network

In this paper, we consider a highly recursive interconnection network known as the fully connected cubic network (FCCN). By exploiting its recursive properties, we thoroughly analyze the performance of a simple routing algorithm for the FCCN. We show that at least 80% of the routes obtained from this simple algorithm are shortest paths, and this percentage increases further with the network size. Subsequently, we obtain the network diameter and average internodal distance, taking into account the communication locality that is exhibited in many parallel computations. The presence of the communication locality significantly reduces the average internodal distance.     

Recursive Approaches for Single Sample Path Based Markov Reward Processes

In this paper, two single sample path‐based recursive approaches for Markov decision problems are proposed. One is based on the simultaneous perturbation approach and can be applied to the general state problem, but its convergence rate is low. In this algorithm, the small perturbation on current parameters is necessary to get another sample path for comparison, but it may worsen the system. Hence, we introduce another approach, which directly estimates the gradient of the performance for optimization by “potential” theory. This algorithm, however, is limited to finite state space systems, but its convergence speed is higher than the first one. The estimate for gradient can be obtained by using the sample path with current parameters without any perturbation. This approach is more acceptable for practical applications.     

时变过程在线辨识的即时递推核学习方法研究

为了及时跟踪非线性化工过程的时变特性, 提出即时递推核学习 (Kernel learning, KL)的在线辨识方法. 针对待预测的新样本点, 采用即时学习 (Just-in-time kernel learning, JITL)策略, 通过构造累积相似度因子, 选择与其相似的样本集建立核学习辨识模型. 为避免传统即时学习对每个待预测点都重新建模的繁琐, 利用两个临近时刻相似样本集的异同点, 采用递推方法有效添加新样本, 并删减旧模型的样本, 以快速建立新即时模型. 通过一时变连续搅拌釜式反应过程的在线辨识, 表明了所提出方法在保证计算效率的同时, 较传统递推核学习方法提高了辨识的准确程度, 能更好地辨识时变过程.     

不同逻辑间翻译的逻辑性质

如果考虑逻辑间模型的翻译并且一个逻辑的模型类被翻译为另一个逻辑的模型类的真子类,那么可靠的(the soundness)和完备的(the completeness)翻译可以将不可满足的公式翻译为可满足的公式.针对上述问题,该文提出了语义忠实(the faithfulness)和语义满(the fullness)两条逻辑性质来确保可满足的公式翻译为可满足的公式,不可满足公式翻译为不可满足公式.该文例证了二阶逻辑在标准语义下到一阶逻辑的翻译是语义忠实的但不是语义满的,在Henkin语义下是语义忠实的和语义满的.     

Recursive coalgebras from comonads

The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this paper, we motivate the use of recursive coalgebras as a paradigm of structured recursion in programming semantics, list some basic facts about recursive coalgebras and, centrally, give new conditions for the recursiveness of a coalgebra based on comonads, comonad-coalgebras and distributive laws of functors over comonads. We also present an alternative construction using countable products instead of cofree comonads.     

基于逻辑框架LF的语义性质之验证

本文对基于类型理论逻辑框架（LF）的语义性质验证加以研究，针对函数式语言LAZY-PCF＋SHAR，利用计算机辅助推理方法和技术给出相应的形式化描述及相关性质证明，从而提倡严格的和计算机辅助的证明在语义性质验证方面的应用。同时，考察了LF以及其实现系统Plastic的能力。     

正反例归纳合成SQL查询程序

SQL是一种被广泛应用于操作关系数据库的编程语言, 很多用户(如数据分析人员和初级程序员等)由于缺少编程经验和SQL语法知识, 导致在编写SQL查询程序时会碰到各种困难. 当前, 使用程序合成方法根据<输入-输出>样例表自动生成相应的SQL查询程序, 吸引了越来越多人的关注. 所提ISST (正反例归纳合成)方法, 能够根据用户编辑的含有少量元组的<输入-输出>示例表自动合成满足用户期望的SQL查询程序. ISST方法包括5个主要阶段: 构建SQL查询程序草图、扩展工作表数据、划分正反例集合、归纳谓词和验证排序. 在PostgreSQL在线数据库上验证SQL查询程序, 并依据奥卡姆剃刀原则对已合成的SQL查询程序候选集打分排序. 使用Java语言实现了ISST方法, 并在包含28条样例的测试集上进行验证, ISST方法能正确合成其中的24条测试样例, 平均耗时2 s.     

针对递归函数的高级综合编译优化算法

为了消除高级综合中的递归函数调用,提出一种基于函数调用图(FCG)和分支决策的编译优化算法.首先在LLVM编译器架构下给出FCG的中间结构,将递归调用转换为非递归函数的嵌套调用,然后借助决策树的构造规则去除函数体中的分支判断及未调用的子支,最后采用子函数复用、资源预评估的方法控制实现电路的规模.实验结果表明,与内联展开算法RecursionHW相比,采用该算法综合后的逻辑单元数平均减少63％,时钟频率平均提高3.2倍,并且高级综合的总时长随递归深度的增大而呈指数级减少.