We present a new declarative compilation of logicprograms with constraints into variable-free relational theories which are then executed by rewriting. this translation provides an algebraic formulation of the abstra...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
We present a new declarative compilation of logicprograms with constraints into variable-free relational theories which are then executed by rewriting. this translation provides an algebraic formulation of the abstract syntax of logicprograms. Management of logic variables, unification, and renaming apart is completely elided in favor of algebraic manipulation of variable-free relation expressions. We prove the translation is sound, and the rewriting system complete with respect to traditional SLD semantics.
We introduce negation to a symbolic-statistical modeling language PRISM and propose to eliminate negation by programtransformation called negation technique which is applicable to probabilistic logicprograms. We als...
详细信息
ISBN:
(纸本)3540266550
We introduce negation to a symbolic-statistical modeling language PRISM and propose to eliminate negation by programtransformation called negation technique which is applicable to probabilistic logicprograms. We also introduce finite PCFGs (probabilistic context free grammars) as PCFGs with finite constraints as part of generative modeling of stochastic HPSGs (head-driven phrase structure grammars). they are a subclass of log-linear models and allow exact computation of normalizing constants. We apply the negation technique to a PDCG (probabilistic definite clause grammar) program written in PRISM that describes a finite PCFG with a height constraint. the resulting program computes a normalizing constant for the finite PCFG in time linear in the given height. We also report on an experiment of parameter learning for a real grammar (ATR grammar) withthe height constraint. We have discovered that the height constraint does not necessarily lead to a significant decrease in parsing accuracy.
While there are well-understood methods for detecting loops whose iterations are independent and parallelizing them, there are comparatively fewer proposals that support parallel execution of a sequence of loops or ne...
详细信息
ISBN:
(纸本)9783642125911
While there are well-understood methods for detecting loops whose iterations are independent and parallelizing them, there are comparatively fewer proposals that support parallel execution of a sequence of loops or nested loops in the case where such loops have dependencies among them. this paper introduces a refined notion of independence, called eventual independence, that in its simplest form considers two loops, say loop, and loop, and captures the idea that for every i there exists k such that the i + 1-th iteration of loop, is independent from the j-th iteration of loop(1), for all j >= k. Eventual independence provides the foundation of a semantics-preserving programtransformation, called synchronized pipelining, that makes execution of consecutive or nested loops parallel, relying on a minimal number of synchronization events to ensure semantics preservation. the practical benefits of synchronized pipelining are demonstrated through experimental results on common algorithms such as sorting and Fourier transforms.
We present a generic scheme for the abstract debugging of functional logicprograms. We associate to programs a semantics based on a (continuous) immediate consequence operator. P[R], which models correctly the powerf...
详细信息
ISBN:
(纸本)9783642205507
We present a generic scheme for the abstract debugging of functional logicprograms. We associate to programs a semantics based on a (continuous) immediate consequence operator. P[R], which models correctly the powerful features of modern functional logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to provide error symptoms in advance and is applicable with partial specifications and even partial programs.
program correctness (in imperative and functional programming) splits in logicprogramming into correctness and completeness. Completeness means that a program produces all the answers required by its specification. L...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
program correctness (in imperative and functional programming) splits in logicprogramming into correctness and completeness. Completeness means that a program produces all the answers required by its specification. Little work has been devoted to reasoning about completeness. this paper presents a few sufficient conditions for completeness of definite programs. We also study preserving completeness under some cases of pruning of SLD-trees (e.g. due to using the cut). We treat logicprogramming as a declarative paradigm, abstracting from any operational semantics as far as possible. We argue that the proposed methods are simple enough to be applied, possibly at an informal level, in practical Prolog programming. We point out importance of approximate specifications.
Fault-tolerance is a crucial property in many systems. thus, mechanical verification of algorithms associated withsynthesis of fault-tolerant programs is desirable to ensure their correctness. In this paper, we prese...
详细信息
ISBN:
(纸本)3540266550
Fault-tolerance is a crucial property in many systems. thus, mechanical verification of algorithms associated withsynthesis of fault-tolerant programs is desirable to ensure their correctness. In this paper, we present the mechanized verification of algorithms that automate the addition of fault-tolerance to a given fault-intolerant program using the PVS theorem prover. By this verification, not only we prove the correctness of the synthesis algorithms, but also we guarantee that any program synthesized by these algorithms is correct by construction. Towards this end, we formally define a uniform framework for formal specification and verification of fault-tolerance that consists of abstract definitions for programs, specifications, faults, and levels of fault-tolerance, so that they are independent of platform and architecture. the essence of synthesis algorithms involves fixpoint calculations. Hence, we also develop a reusable library for fixpoint calculations on finite sets in PVS.
the need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear logic (CLL) for correct-by-construction...
详细信息
ISBN:
(纸本)9783030138387;9783030138370
the need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear logic (CLL) for correct-by-construction resource-based process composition, with guaranteed deadlock freedom, systematic resource accounting, and concurrent execution. We introduce algorithms to automate the necessary inference steps for binary compositions of processes in parallel, conditionally, and in sequence. We combine decision procedures and heuristics to achieve intuitive and practically useful compositions in an applied setting.
In recent work, the effectiveness of using declarative languages has been demonstrated for many problems in program analysis. Using a simple relational query language, like DATALOG, complex interprocedural analyses in...
详细信息
ISBN:
(纸本)9783642125911
In recent work, the effectiveness of using declarative languages has been demonstrated for many problems in program analysis. Using a simple relational query language, like DATALOG, complex interprocedural analyses involving dynamically created objects can be expressed in just a few lines. By exploiting the power of the Rewriting logic language MAUDE, we aim at transforming DATALOG programs into efficient rewrite systems that compute the same answers. A prototype has been implemented and applied to some real-world DATALOG-based analyses. Experimental results show that the performance of solving DATALOG queries in rewriting logic is comparable to state-of-the-art DATA LOG solvers.
In this paper we propose a novel semi-supervised active machine-learning method, based on two recursive higher-order functions that can inductively synthesize a functional computer program. based on properties formula...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
In this paper we propose a novel semi-supervised active machine-learning method, based on two recursive higher-order functions that can inductively synthesize a functional computer program. based on properties formulated using abstract algebra terms, the method uses two combined strategies: to reduce the dimensionality of the Boolean algebra where a target function lies and to combine known operations belonging to the algebra, using them as a basis to build a programthat emulates the target function. the method queries for data on specific points of the problem input space and build a programthat exactly fits the data. Applications of this method include all sorts of systems based on bitwise operations. Any functional computer program can be emulated using this approach. Combinatorial circuit design, model acquisition from sensor data, reverse engineering of existing computer programs are all fields where the proposed method can be useful.
We consider a new application condition of negative unfolding, which guarantees its safe use in unfold/fold transformation of stratified logicprograms. the new condition of negative unfolding is a natural one, since ...
详细信息
ISBN:
(纸本)9783642125911
We consider a new application condition of negative unfolding, which guarantees its safe use in unfold/fold transformation of stratified logicprograms. the new condition of negative unfolding is a natural one, since it is considered as a special case of replacement rule. the correctness of our unfold/fold transformation system in the sense of the perfect model semantics is proved. We then consider the coinductive proof rules proposed by Jaffar et al. We show that our unfold/fold transformation system, when used together with Lloyd-Topor transformation, can prove a proof problem which is provable by the coinductive proof rules by Jaffar et al. To this end, we propose a new replacement rule, called sowed replacement, which is not necessarily equivalence-preserving, but is essential to perform a reasoning step corresponding to coinduction.
暂无评论