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

Information-gain computation in the FIFTH system

INTERNATIONAL JOURNAL OF APPROXIMATE REASONING 2019年 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

来源：评论

学校读者我要写书评

暂无评论

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 QLD 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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Correctness and Completeness of Logic Programs

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2016年第3期17卷 1–32页

作者： Drabent, Wlodzimierz Polish Acad Sci Inst Comp Sci Ul Jana Kazimierza 5 PL-01248 Warsaw Poland Linkoping Univ S-58183 Linkoping Sweden

We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method that should be well known but is often neglected. Also, we show how to prove completeness and correctness in the presence of SLD-tree pruning, and point out that approximate specifications simplify specifications and proofs. We compare the proof methods to declarative diagnosis (algorithmic debugging), showing that approximate specifications eliminate a major drawback of the latter. We argue that our proof methods reflect natural declarative thinking about programs, and that they can be used, formally or informally, in everyday programming.

关键词： Logic programming declarative programming program completeness program correctness specifications declarative diagnosis/algorithmic debugging

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

A GENTLE INTRODUCTION TO S-NET: TYPED STREAM PROCESSING AND declarative COORDINATION OF ASYNCHRONOUS COMPONENTS

引用

PARALLEL PROCESSING LETTERS 2008年第2期18卷 221-237页

作者： Grelck, Clemens Scholz, Sven-Bodo Shafarenko, Alex Univ Lubeck Inst Software Technol & Programming Languages Ratzeburger Allee 160 D-23538 Lubeck Germany Univ Hertfordshire Dept Comp Sci Hatfield AL10 9AB Herts England

We present the design of S-NET, a coordination language and component technology based on stream processing. S-NET achieves a near-complete separation between application code, written in a conventional programming language, and coordination code, written in S-NET itself. S-NET boxes integrate existing sequential code as stream-processing components into streaming networks, whose construction is based on algebraic formulae built out of four network combinators. Subtyping on the level of boxes and networks and a tailor-made inheritance mechanism achieve flexible software reuse.

关键词： Parallel programming models stream processing component models coordination declarative programming structural subtyping

来源：评论

学校读者我要写书评

暂无评论

COLAB - A HYBRID KNOWLEDGE REPRESENTATION AND COMPILATION LABORATORY

引用

ANNALS OF OPERATIONS RESEARCH 1995年第1期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

来源：评论

学校读者我要写书评

暂无评论

Axiomatization of a denotational semantics for first-order logic

引用

LOGIC JOURNAL OF THE IGPL 2004年第4期12卷 277-299页

作者： Vermeulen, C. F. M. Univ Auckland Dept Philosophy Auckland 1 New Zealand

An axiomatization is presented of the denotational semantics for first order language of Apt [1]. The goal is to obtain a rational reconstruction of the intuitions underlying this semantics. The axiomatization combines ideas about four valued logic with facts about substitutions. Soundness and completeness of the axiomatization are established. From the completeness proof a decision procedure is obtained that shows how four valued logic and order sensitivity of substitution together add up in a natural way to the denotational semantics for the language of first order logic as proposed by Apt.

关键词： declarative programming denotational semantics first order logic axiomatization

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：