Proving termination of, or generating efficient control for Constraint Handling Rules (CH R,) programs requires information about the kinds of constraints that can show up in the CHR constraint store. In contrast to L...
详细信息
ISBN:
(纸本)9783642125911
Proving termination of, or generating efficient control for Constraint Handling Rules (CH R,) programs requires information about the kinds of constraints that can show up in the CHR constraint store. In contrast to logicprogramming (LP), there are not many tools available for deriving such information for CHR. Hence, instead of building analyses for CHR from scratch, we define a, transformation from CHR to Prolog and reuse existing analysis tools for Prolog. the proposed transformation has been implemented and combined with Poly Types 1.3, a type analyser for Prolog, resulting in an accurate description of the types of CHR programs. Moreover, the transformation is not limited to type analysis. It can also be used to prove other properties of the constraints showing up in constraint stores, using tools for Prolog.
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.
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.
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.
We introduce negation into coinductive logicprogramming (co-LP) via what we term Coinductive SLDNF (co-SLDNF) resolution. We present declarative and operational semantics of co-SLDNF resolution and present their equi...
详细信息
ISBN:
(纸本)9783642125911
We introduce negation into coinductive logicprogramming (co-LP) via what we term Coinductive SLDNF (co-SLDNF) resolution. We present declarative and operational semantics of co-SLDNF resolution and present their equivalence under the restriction of rationality. Co-LP with co-SLDNF resolution provides a powerful, practical and efficient operational semantics for Fitting's Kripke-Kleene three-valued logic with restriction of rationality. Further, applications of co-SLDNF resolution are also discussed and illustrated where Co-SLDNF resolution allows one to develop elegant implementations of modal logics. Moreover it provides the capability of non-monotonic inference (e.g., predicate Answer Set programming) that can be used to develop novel and effective first-order modal non-monotonic inference engines.
We show how to combine the two most powerful approaches for automated termination analysis of logicprograms (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms...
详细信息
ISBN:
(纸本)9783642125911
We show how to combine the two most powerful approaches for automated termination analysis of logicprograms (LPs): the direct approach which operates directly on LPs and the transformational approach which transforms LPs to term rewrite systems (TRSs) and tries to prove termination of the resulting TRSs. To this end, we adapt the well-known dependency pair framework from TRSs to LPs. Withthe resulting method;one can combine arbitrary termination techniques for LPs in a completely modular way and one call use both direct and transformational techniques for different parts of the same LP.
Tracing program executions is a promising technique to find bugs in lazy functional logicprograms. In previous work we developed an extension of a heap based semantics for functional logic languages which generates a...
详细信息
ISBN:
(纸本)9783540714095
Tracing program executions is a promising technique to find bugs in lazy functional logicprograms. In previous work we developed an extension of a heap based semantics for functional logic languages which generates a trace reflecting the computation of the program. this extension was also prototypically implemented by instrumenting an interpreter for functional logicprograms. Since this interpreter is too restricted for real world applications, we developed a programtransformation which efficiently computes the trace by means of side effects during the computation. this paper presents our programtransformation.
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctne...
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctness of the programs they synthesise/transform, or rigorous, with strong theoretical foundations, but generating proof obligations which are difficult to satisfy.
Proofs-as-programs is an approach to programsynthesis involving the transformation of constructive proofs of specification requirements into functional programs. Various authors have adapted the proofs-as-programs to...
详细信息
ISBN:
(纸本)9783540787686
Proofs-as-programs is an approach to programsynthesis involving the transformation of constructive proofs of specification requirements into functional programs. Various authors have adapted the proofs-as-programs to other logics and programming paradigms. this paper presents an adaptation of proofs-as-programs for the synthesis of distributed program protocols with side-effect-free data views, from proofs in a constructive proof-system for Hennessy-Milner logic.
In this work, we devise an analysis that searches for semantically equivalent code fragments within a given logicprogram. the presence of duplicated code (or functionality) is a primary indication that the design of ...
详细信息
ISBN:
(纸本)3540266550
In this work, we devise an analysis that searches for semantically equivalent code fragments within a given logicprogram. the presence of duplicated code (or functionality) is a primary indication that the design of the program can be improved by performing a so-called refactoring transformation. Within the framework of our analysis, we formally characterize three situations of duplicated functionality and their associated refactorings: the extraction of a duplicated goal into a new predicate, the removal of equivalent predicates and the generalization of two predicates into a higher-order predicate. the resulting analysis detects in a completely automatic way what program fragments are suitable candidates for the considered refactoring transformations.
暂无评论