检索结果-内蒙古大学图书馆

Information-gain computation in the FIFTH system

INTERNATIONAL JOURNAL OF APPROXIMATE REASONING 2019年第Feb.期105卷 386-395页

作者： Di Franco, Anthony Univ Calif Davis Dept Comp Sci Davis CA 95616 USA

Despite large incentives, correctness in software remains an elusive goal. declarative programming techniques, where algorithms are derived from a specification of the desired behavior, offer hope to address this problem, since there is a combinatorial reduction in complexity in programming in terms of specifications instead of algorithms, and arbitrary desired properties can be expressed and enforced in specifications directly. However, limitations on performance have prevented programming with declarative specifications from becoming a mainstream technique for general-purpose programming, because a strategy which is both efficient and fully general to derive algorithms from specifications does not yet exist. To address this bottleneck, I propose information-gain computation, a framework where an adaptive evaluation strategy is used to efficiently perform a search which derives algorithms that provide information about a query via the most efficient routes. Within this framework, opportunities to compress the search space present themselves, which suggest that information-theoretic bounds on the performance of such a system might be articulated and a system might be designed to achieve them. The computation of the information measures that are the basis of this strategy crucially depends on a probabilistic semantics for the relations represented by predicates, which may either already be present in a probabilistic logic language, or may be superimposed on a pure logic language. I describe a prototype implementation of FIFTH, a system that implements these techniques, and a preliminary empirical study of adaptive evaluation for a simple test program. In the test, the evaluation strategy adapts successfully to efficiently evaluate a query with pathological features that would prevent its evaluation by standard general-purpose strategies. (C) 2018 Elsevier Inc. All rights reserved.

关键词： declarative programming Probabilistic logic programming PROLOG Adaptive evaluation strategy Multi-armed bandits

来源：评论

学校读者我要写书评

暂无评论

Strongly sequential and inductively sequential term rewriting systems

引用

INFORMATION PROCESSING LETTERS 1998年第1期67卷 1-8页

作者： Hanus, M Lucas, S Middeldorp, A Rhein Westfal TH Aachen D-52056 Aachen Germany Univ Politecn Valencia DSIC E-46071 Valencia Spain Univ Tsukuba Inst Informat Sci & Elect Tsukuba Ibaraki 3058573 Japan

The concept of definitional tree by Antoy serves to introduce control information into the bare set of rules of a constructor-based term rewriting system (TRS). TRSs whose rules can be arranged into a definitional tree are called inductively sequential. By relying on the existence of such a definitional tree, an optimal rewriting strategy, the outermost-needed strategy, is defined. Optimality was proved with respect to the Huet-Levy theory of neededness. In this paper, we prove that strongly sequential and inductively sequential constructor-based TRSs coincide. We also show that outermost-needed rewriting only reduces strongly needed redexes. (C) 1998 Elsevier Science B.V.

关键词： programming languages definitional trees neededness strong sequentiality term rewriting declarative programming

来源：评论

学校读者我要写书评

暂无评论

First-Order Logic with Inductive Definitions for Model-Based Problem Solving

引用

AI MAGAZINE 2016年第3期37卷 69-80页

作者： Bruynooghe, Maurice Denecker, Marc Truszczynski, Mirosiaw Katholieke Univ Leuven Dept Comp Sci Leuven Belgium Declarat Languages & Artificial Intelligence Res Leuven Belgium Katholieke Univ Leuven Comp Sci Leuven Belgium Res Grp Knowledge Representat & Reasoning Leuven Belgium Univ Kentucky Comp Sci Lexington KY 40506 USA

In answer set programming (ASP), programs can be viewed as specifications of finite Herbrand structures. Other logics can be (and, in fact, were) used toward the same end and can be taken as the basis of declarative programming systems of similar functionality as ASP. We discuss here one such logic, the logic FO(ID), and its implementation IDP3. The choice is motivated by notable similarities between ASP and FO(ID), even if both approaches trace back to different origins.

关键词： declarative programming Problem Solving Stable model semantics Answer set programming First-order logic

来源：评论

学校读者我要写书评

暂无评论

Parallelism, concurrency and distribution in constraint handling rules: A survey

引用

THEORY AND PRACTICE OF LOGIC programming 2018年第5-6期18卷 759-805页

作者： Fruehwirth, Thom Ulm Univ Inst Software Engn & Programming Languages D-89069 Ulm Germany

Constraint Handling Rules (CHR) is both an effective concurrent declarative programming language and a versatile computational logic formalism. In CHR, guarded reactive rules rewrite a multi-set of constraints. Concurrency is inherent, since rules can be applied to the constraints in parallel. In this comprehensive survey, we give an overview of the concurrent, parallel as well as distributed CHR semantics, standard and more exotic, that have been proposed over the years at various levels of refinement. These semantics range from the abstract to the concrete. They are related by formal soundness results. Their correctness is proven as a correspondence between parallel and sequential computations. On the more practical side, we present common concise example CHR programs that have been widely used in experiments and benchmarks. We review parallel and distributed CHR implementations in software as well as hardware. The experimental results obtained show a parallel speed-up for unmodified sequential CHR programs. The software implementations are available online for free download and we give the web links. Due to its high level of abstraction, the CHR formalism can also be used to implement and analyse models for concurrency. To this end, the Software Transaction Model, the Actor Model, Colored Petri Nets and the Join-Calculus have been faithfully encoded in CHR. Finally, we identify and discuss commonalities of the approaches surveyed and indicate what problems are left open for future research.

关键词： parallelism concurrency distribution constraint handling rules declarative programming concurrent constraint programming semantics rewriting concurrency models

来源：评论

学校读者我要写书评

暂无评论

Proving correctness and completeness of normal programs - a declarative approach

引用

THEORY AND PRACTICE OF LOGIC programming 2005年第6期5卷 669-711页

作者： Drabent, W Milkowska, M Polish Acad Sci Inst Comp Sci PL-01237 Warsaw Poland Linkoping Univ Dept Comp & Informat Sci S-58183 Linkoping Sweden Warsaw Univ Inst Informat PL-02097 Warsaw Poland

We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination;the latter includes nonfloundering. Only clean termination depends on the operational semantics, in particular on the selection rule. We show how to deal with correctness and completeness in a declarative way, treating programs only from the logical point of view. Specifications used in this approach are interpretations (or theories). We point out that specifications for correctness may differ from those for completeness, as usually there are answers which are neither considered erroneous nor required to be computed. We present proof methods for correctness and completeness for definite programs and generalize them to normal programs. For normal programs we use the 3-valued completion semantics;this is a standard semantics corresponding to negation as finite failure. The proof methods employ solely the classical 2-valued logic. We use a 2-valued characterization of the 3-valued completion semantics, which may be of separate interest. The method of proving correctness of definite programs is not new and can be traced back to the work of Clark in 1979. However a more complicated approach using operational semantics was proposed by some authors. We show that it is not stronger than the declarative one, as far as properties of program answers are concerned. For a corresponding operational approach to normal programs, we show that it is (strictly) weaker than our method. We also employ the ideas of this work to generalize a known method of proving termination of normal programs.

关键词： declarative programming negation in logic programming specifications program correctness and completeness termination teaching logic programming

来源：评论

学校读者我要写书评

暂无评论

PROGRAM PARTITION AND LOGIC PROGRAM ANALYSIS

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1995年第12期21卷 959-968页

作者： HAN, JL Department of Mathematics and Computing University of Southern Queensland Toowoomba Queensland 4350 Australia

A program partition Scheme for stratified programs introduced by Apt, Blair, and Walker is used to study efficient computation of logic programs. We consider three types of program partitions and their corresponding graph representations: 1) the natural partition, 2) stratified partitions;and 3) the reduced partition. The natural (program) partition consists of definitions of relations, each definition being a subprogram. Subprograms of a program partition may consist of several relations. A partition graph is introduced for a program partion, each node of which corresponds to a subprogram. The partition graph for a stratified partition is a directed acyclic graph (DAG). A stratified partition decomposes a program into modules. The stratified partition with the maximum number of modules is the reduced partition. The cost to achieve a reduced partition is linear in the program size, using well known graph algorithms. We introduce the modular interpretations, which are equivalent in semantics to the standard interpretation. The modular interpretations offer encapsulation and may reduce the computation cost for some modules significantly. The modular approach can play an important role in query optimization, efficient termination, programming design, and software engineering. We classify query types and answer types then discuss query optimization for some query types. Many efficient query processing strategies are applicable to restricted subclasses of programs. The program partition method allows us to select the most efficient strategy for each module. For example, if a module is a uniformly bounded recursion, then the module can be terminated efficiently. If a module defines the transitive closure, then efficient program transformations may be applied to this module.

关键词： declarative programming PROGRAM PARTITIONS SEMANTIC ANALYSIS LOGIC programming QUERY OPTIMIZATION DEDUCTIVE DATABASES PROGRAM VERIFICATIONS

来源：评论

学校读者我要写书评

暂无评论

COLAB - A HYBRID KNOWLEDGE REPRESENTATION AND COMPILATION LABORATORY

引用

ANNALS OF OPERATIONS RESEARCH 1995年第0期55卷 11-79页

作者： BOLEY, H HANSCHKE, P HINKELMANN, K MEYER, M DFKI KAISERSLAUTERNGERMANY

Knowledge bases for real-world domains such as mechanical engineering require expressive and efficient representation and processing tools. We pursue a declarative-compilative approach to knowledge engineering. While Horn logic (as implemented in PROLOG) is well-suited for representing relational clauses, other kinds of declarative knowledge call for hybrid extensions: functional dependencies and higher-order knowledge should be modeled directly. Forward (bottom-up) reasoning should be integrated with backward (top-down) reasoning. Constraint propagation should be used wherever possible instead of search-intensive resolution. Taxonomic knowledge should be classified into an intuitive subsumption hierarchy. Our LISP-based tools provide direct translators of these declarative representations into abstract machines such as an extended Warren Abstract Machine (WAM) and specialized inference engines that are interfaced to each other. More importantly, we provide source-to-source transformers between various knowledge types, both for user convenience and machine efficiency. These formalisms with their translators and transformers have been developed as part of COLAB, a compilation laboratory for studying what we call, respectively, 'vertical' and 'horizontal' compilation of knowledge, as well as for exploring the synergetic collaboration of the knowledge representation formalisms. A case study in the realm of mechanical engineering has been an important driving force behind the development of COLAB. It Will be used as the source of examples throughout the paper when discussing the enhanced formalisms, the hybrid representation architecture, and the compilers.

关键词： HYBRID KNOWLEDGE REPRESENTATION KNOWLEDGE COMPILATION declarative programming TAXONOMIC REASONING CONSTRAINT PROPAGATION RELATIONAL FUNCTIONAL COMPUTATION BOTTOM-UP DEDUCTION KNOWLEDGE-BASED SYSTEMS MECHANICAL ENGINEERING NC-programming

来源：评论

学校读者我要写书评

暂无评论

TOOLS OF THE TRADE The Importance of Being declarative

引用

IEEE SOFTWARE 2013年第1期30卷 90-91页

作者： Spinellis, Diomidis Athens Univ Econ & Business Dept Management Sci & Technol Athens Greece

A declarative programming style focuses on what you want your program to do rather than how to perform the task. By avoiding implementation details, well-written declarative code is easier to understand, modify, and maintain. The code you write in a declarative style is often so readable that you can share it with your project's domain experts. Furthermore, once you start working with declarative code, you can automatically process it to verify properties of its operation, generate test cases, or create parts of the system's documentation. Small choices, such as the naming of your methods and variables, matter. If you're coding an algorithm, have your code match the algorithm's published description. Other approaches to consider include table-driven programming, the implementation of a domain-specific language, or the use of task-specific libraries. When you have the choice, pick the highest level language you can afford and that's suitable for the task at hand. The Web extra at http://***/s4oWie6laq4 is an audio podcast of author Diomidis Spinellis discussing why well-written declarative code is easier to understand, modify, and maintain.

关键词： programming Documentation Encoding Domain Specific Languages Digital Audio Broadcasting Libraries Techniques declarative programming Abstraction Benefits

来源：评论

学校读者我要写书评

暂无评论

Puncalc: task-based parallelism and speculative reevaluation in spreadsheets

引用

JOURNAL OF SUPERCOMPUTING 2020年第7期76卷 4977-4997页

作者： Bock, Alexander Asp Biermann, Florian IT Univ Copenhagen Rued Langgaards Vej 7 DK-2300 Copenhagen S Denmark

Spreadsheets are commonly declarative, first-order functional programs and are used as organizational tools, for end-user development and for educational purposes. Spreadsheet end users are usually domain experts who use spreadsheets as their main computational model, but are seldom trained IT professionals who can leverage today's abundant multicore processors for spreadsheet computation. In this paper, we present an algorithm for automatic, parallel evaluation of spreadsheets targeting shared-memory multicore architectures, which lets end users transparently make use of their multicore processors. We evaluate our algorithm on a set of synthetic and real-world spreadsheets and obtain up to 16 times speedup on 48 cores.

关键词： Spreadsheets Parallelism Tasks Speculative declarative programming End-user programming

来源：评论

学校读者我要写书评

暂无评论

From Predicates to Programs: The Semantics of a Method Language

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第SPEC. ISS.期184卷 171-187页

作者： Faitelson, David Welch, James Davies, Jim Univ Oxford Comp Lab Wolfson BldgParks Rd Oxford OX1 3QD England

This paper explains how a declarative method language, based upon the formal notations of Z and B, can be used as a basis for automatic code generation. The language is used to describe the intended effect of operations, or methods, upon the components of an object model;each method is defined by a pair of predicates: a precondition, and a post-condition. Following the automatic incorporation of model invariants, including those arising from class associations, these predicates are extended-again, automatically-to address issues of consistency, definition, and dependency, before being translated into imperative programs. The result is a formal method for transforming object models into complete, working systems.

关键词： formal methods declarative programming object modelling weakest preconditions

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：