首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   9篇
  完全免费   1篇
  自动化技术   10篇
  2018年   1篇
  2014年   1篇
  2012年   1篇
  2011年   1篇
  2007年   1篇
  2001年   1篇
  1999年   2篇
  1996年   1篇
  1992年   1篇
排序方式: 共有10条查询结果,搜索用时 31 毫秒
1
1.
In the constructive setting, membership predicates over recursive types are inhabited by terms indexing the elements that satisfy the criteria for membership. In this paper, we motivate and explore this idea in the concrete setting of lists and trees. We show that the inhabitants of membership predicates are precisely the inhabitants of a generic shape type. We show that membership of x (of type T) in structure S, (xTS) can not, in general, index all parts of a structure S and we generalize to a form ρS where ρ is a predicate over S. Under this scheme, (λx.True)S is the set of all indexes into S, but we show that not all subsets of indexes are expressible by strictly local predicates. Accordingly, we extend our membership predicates to predicates that retain state “from above” as well as allow “looking below”. Predicates of this form are complete in the sense that they can express every subset of indexes in S. These ideas are motivated by experience programming in Nuprl's constructive type theory and examining the constructive content of mechanically checked formal proofs involving membership predicates.  相似文献
2.
The aim of this paper is to extend theConstructive Negation technique to the case ofCLP(SεT), a Constraint Logic Programming (CLP) language based on hereditarily (and hybrid) finite sets. The challenging aspects of the problem originate from the fact that the structure on whichCLP(SεT) is based is notadmissible closed, and this does not allow to reuse the results presented in the literature concerning the relationships betweenCLP and constructive negation. We propose a new constraint satisfaction algorithm, capable of correctly handling constructive negation for large classes ofCLP(SεT) programs; we also provide a syntactic characterization of such classes of programs. The resulting algorithm provides a novel constraint simplification procedure to handle constructive negation, suitable to theories where unification admits multiple most general unifiers. We also show, using a general result, that it is impossible to construct an interpreter forCLP(SεT) with constructive negation which is guaranteed to work for any arbitrary program; we identify classes of programs for which the implementation of the constructive negation technique is feasible. Agostino Dovier, Ph.D.: He is a researcher in the Department of Science and Technology at the University of Verona, Italy. He obtained his master degree in Computer Science from the University of Udine, Italy, in 1991 and his Ph.D. in Computer Science from the University of Pisa, Italy, in 1996. His research interests are in Programming Languages and Constraints over complex domains, such as Sets and Multisets. He has published over 20 research papers in International Journals and Conferences. He is teaching a course entitled “Special Languages and Techniques for Programming” at the University of Verona. Enrico Pontelli, Ph.D.: He is an Assistant Professor in the Department of Computer Science at the New Mexico State University. He obtained his Laurea degree from the University of Udine (Italy) in 1991, his Master degree from the University of Houston in 1992, and his Ph.D. degree from New Mexico State University in 1997. His research interests are in Programming Languages, Parallel Processing, and Constraint Programming. He has published over 50 papers and served on the program committees of different conferences. He is presently the Associate Director of the Laboratory for Logic, Databases, and Advanced Programming. Gianfranco Rossi, Ph.D.: He received his degree in Computer Science from the University of Pisa in 1979. From 1981 to 1983 he was employed at Intecs Co. System House in Pisa. From November 1983 to February 1989 he was a researcher at the Dipartimento di Informatica of the University of Turin. Since March 1989 he is an Associate Professor of Computer Science, currently with the University of Parma. He is the author of several papers dealing mainly with programming languages, in particular logic programming languages and Prolog, and extended unification algorithms. His current research interests are (logic) programming languages with sets and set unification algorithms.  相似文献
3.
Nested datatypes generalise regular datatypes in much the same way that context-free languages generalise regular ones. Although the categorical semantics of nested types turns out to be similar to the regular case, the fold functions are more limited because they can only describe natural transformations. Practical considerations therefore dictate the introduction of a generalised fold function in which this limitation can be overcome. In the paper we show how to construct generalised folds systematically for each nested datatype, and show that they possess a uniqueness property analogous to that of ordinary folds. As a consequence, generalised folds satisfy fusion properties similar to those developed for regular datatypes. Such properties form the core of an effective calculational theory of inductive datatypes. Received September 1998 / Accepted in revised form July 1999  相似文献
4.
We demonstrate that in the context of statically-typed purely-functional lambda calculi without recursion, unchecked exceptions (e.g., SML exceptions) can be strictly more powerful than call/cc. More precisely, we prove that a natural extension of the simply-typed lambda calculus with unchecked exceptions is strictly more powerful than all known sound extensions of Girard's F (a superset of the simply-typed lambda calculus) with call/cc.This result is established by showing that the first language is Turing complete while the later languages permit only a subset of the recursive functions to be written. We show that our natural extension of the simply-typed lambda calculus with unchecked exceptions is Turing complete by reducing the untyped lambda calculus to it by means of a novel method for simulating recursive types using unchecked-exception–returning functions. The result concerning extensions of F with call/cc stems from previous work of the author and Robert Harper.  相似文献
5.
Paramorphisms     
Catamorphisms are functions on an initial data type (an inductively defined domain) whose inductive definitional pattern mimics that of the type. These functions have powerful calculation properties by which inductive reasoning can be replaced by equational reasoning. This paper introduces a generalisation of catamorphisms, dubbed paramorphisms. Paramorphisms correspond to a larger class of inductive definition patterns; in fact, we show that any function defined on an initial type can be expressed as a paramorphism. In spite of this generality, it turns out that paramorphisms have calculation properties very similar to those of catamorphisms. In particular, we prove a Unique Extension Property and a Promotion Theorem for paramorphisms.  相似文献
6.
7.
介绍石油化工企业自动化仪表施工管理程序和施工管理方法,并指出设计、安装、调试要点.  相似文献
8.
介绍了欧姆龙PLC控制的酸性氧化还原电位水消毒水生成器的应用,主要介绍了控制原理、软件设计思想和程序结构,实际运行表明该控制系统是可行的。  相似文献
9.
在科学技术进一步日新月异的今天,网络应用编程作为一门理论实践结合非常紧密的课程,改革显得越加重要。文章总结了笔者六年教学的经验,从教材教辅建设、小班化和双语教学手段等多个方面探讨了教学改革过程中的收获、经验和教训。  相似文献
10.
刘斌斌  董威  王戟 《软件学报》2018,29(8):2180-2197
互联网、机器学习、人工智能等技术的迅速发展以及大量开源软件和开源社区的出现给软件工程的发展带来了新的机遇和挑战.目前在互联网上已经存在了数十亿行的各类程序代码,这些代码中存在着各种知识,尤其是众多已被广泛使用、高质量的软件代码,由此催生了利用大规模代码资源中蕴涵的众多知识进行智能化软件开发的新思路.它试图充分利用互联网中存在的代码资源、知识和群体智慧,以有效提高软件开发的效率和质量,其核心技术是程序搜索与构造,具有非常重要的理论与应用价值.目前该方向的研究工作主要集中在代码搜索、程序合成、代码推荐与补全、缺陷检测、代码风格改善、程序自动修复等方面.本文从以上几个方面对当前的主要研究工作进行综述,对具体的理论和技术途径进行梳理,并在最后总结了目前该领域研究过程中面临的挑战,给出了建议的研究方向.  相似文献
1
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号