We present two new algorithms which perform automatic parallelization via source-to-source transformations. the objective is to exploit goal-level, unrestricted independent and-parallelism. the proposed algorithms use...
详细信息
ISBN:
(纸本)9783540787686
We present two new algorithms which perform automatic parallelization via source-to-source transformations. the objective is to exploit goal-level, unrestricted independent and-parallelism. the proposed algorithms use as targets new parallel execution primitives which are simpler and more flexible than the well-known &/2 parallel operator. this makes it possible to generate better parallel expressions by exposing more potential parallelism among the literals of a clause than is possible with &/2. the difference between the two algorithms stems from whether the order of the solutions obtained is preserved or not. We also report on a preliminary evaluation of an implementation of our approach. We compare the performance obtained to that of previous annotation algorithms and show that relevant improvements can be obtained.
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number ...
详细信息
ISBN:
(纸本)3540266550
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem term enumeration,. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a proof enumeration problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. this in turn yields a proof enumeration algorithm.
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.
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.
It has often been observed that a point-free style of programming provides a more abstract view on programs. We aim to use the gain in abstraction to obtain a denotational semantics for functional logic languages in a...
详细信息
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.
A variable is local if it occurs in a clause body but not in its head. Local variables appear naturally in practical logicprogramming, but they complicate several aspects such as negation, compilation, memoization, s...
详细信息
ISBN:
(纸本)3540326545
A variable is local if it occurs in a clause body but not in its head. Local variables appear naturally in practical logicprogramming, but they complicate several aspects such as negation, compilation, memoization, static analysis, program approximation by neural networks etc. As a consequence, the absence of local variables yields better performance of several tools and is a prerequisite for many technical results. In this paper, we introduce an algorithm that eliminates local variables from a wide proper subclass of normal logicprograms. the proposed transformation preserves the Clark-Kunen semantics for normal logicprograms.
We present a method based on logicprogramtransformation, for verifying Computation Tree logic (CTL*) properties of finite state reactive systems. the finite state systems and the CTL* properties we want to verify, a...
详细信息
ISBN:
(纸本)9783642125911
We present a method based on logicprogramtransformation, for verifying Computation Tree logic (CTL*) properties of finite state reactive systems. the finite state systems and the CTL* properties we want to verify, are encoded as logicprograms on infinite lists. Our verification method consists of two steps. In the first step we transform the logicprogramthat encodes the given System and the given property, into a monadic w-program, that is, a stratified program defining nullary or unary predicates on infinite lists. this transformation is performed by applying unfold/fold rules that preserve the perfect model of the initial program. In the second step we verify the property of interest by using a proof method for monadic w-programs.
In very recent work, we introduced a non-termination preserving transformation from logicprograms with cut to definite logicprograms. While that approach allows us to prove termination of a large class of logic prog...
详细信息
ISBN:
(纸本)9783642205507
In very recent work, we introduced a non-termination preserving transformation from logicprograms with cut to definite logicprograms. While that approach allows us to prove termination of a large class of logicprograms with cut automatically, in several cases the transformation results in a non-terminating definite logicprogram. In this paper we extend the transformation such that logicprograms with cut are no longer transformed into definite logicprograms, but into dependency triple problems. By the implementation of our new method and extensive experiments, we empirically evaluate the practical benefit of our contributions.
programtransformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. this paper presents the first step towards developing program transf...
详细信息
ISBN:
(纸本)3540266550
programtransformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. this paper presents the first step towards developing programtransformation techniques for a concurrent constraint programming language where guarded rules rewrite and augment multi-sets of atomic formulae, called Constraint Handling Rules (CHR). We study the specialization of rules with regard to a given goal (query). We show the correctness of this programtransformation: Adding and removing specialized rules in a program does not change the program's operational semantics. Furthermore termination and confluence of the program are shown to be preserved.
暂无评论