Narrowing was originally introduced to solve equational E-unification problems. It has also been recognized as a key mechanism to unify functional and logic programming. In both cases, narrowing supports equational reasoning and assumes confluent equations. The main goal of this work is to show that narrowing can be greatly generalized, so as to support a much wider range of applications, when it is performed with rewrite theories (Sigma,E,R), where (Sigma,E) is an equational theory, and R is a collection of rewrite rules with no restrictions. Such theories axiomatize concurrent systems, whose states are equivalence classes of terms modulo E, and whose transitions are specified by R. In this context, narrowing is generalized from an equational reasoning technique to a symbolic model checking technique for reachability analysis of a, typically infinite, concurrent system. We survey the foundations of this approach, suitable narrowing strategies, and various applications to security protocol verification, theorem proving, and programming languages.
Computing with failures is a typical programming technique in functional logic programs. However, there are also situations where a program should not fail (e.g., in a deterministic top-level computation) but the evaluation fails accidentally, e.g., due to missing pattern combinations in an operation defined by pattern matching. In this case the program developer is interested in the context of the failed program point in order to analyze the reason of the failure. Therefore, this paper discusses techniques for reporting failures and proposes a new one that has been integrated in a Prolog-based compiler for the declarative multi-paradigm language Curry. Our new technique supports separate compilation of modules, i.e., the compilation of modules has not take into account whether failures should be reported or not. The failure reporting is only considered in some linking code for modules. In contrast to previous approaches, the execution of programs in the failure reporting mode causes only a small overhead so that it can be also used in larger applications.
In this paper we propose applying the ideas of declarative debugging to the object-oriented language Java as an alternative to traditional trace debuggers used in imperative languages. The declarative debugger builds a suitable computation tree containing information about method invocations occurred during a wrong computation. The tree is then navigated, asking questions to the user in order to compare the intended semantics of each method with its actual behavior until a wrong method is found out. The technique has been implemented in an available prototype. We comment the several new issues that arise when using this debugging technique, traditionally applied to declarative languages, to a completely different paradigm and propose several possible improvements and lines of future work.
It is the basic credo of declarative programming that abstracting from certain aspects of program executions greatly improves the quality of the written code: Typical sources of errors are principally omitted, like issues of memory management, type errors and multiple allocation of variables. The program is much nearer to the \emph{logic} of the implemented algorithm than to its execution. This makes code much more readable, comprehensive and maintainable.
But on the other hand, abstracting from certain aspects of program executions greatly impairs the connection between the run-time system and the program. In many regards, what actually happens during program execution is totally obscure. In this paper we present an approach to enlighten the infamous run-time black box. The main idea is to trace a program's execution by side effects and then interpret these traces in the light of different evaluation strategies. Different views are then given on the resulting interpretation. This article introduces a framework in which the interpretations of such execution traces can be elegantly formulated using advanced programming techniques of functional logic languages.
Debugging by observing the evaluation of expressions and functions is a useful approach for finding bugs in lazy functional and functional logic programs. However, adding and removing observation annotations to a program is an effort making the use of this debugging technique in practice uncomfortable. Having tool support for managing observations is desirable. We developed a tool that provides this ability for programmers. Without annotating expressions in a program, the evaluation of functions, data structures and arbitrary subexpressions can be observed by selecting them from a tree-structure representing the whole program. Furthermore, the tool provides a step by step performing of observations where each observation is shown in a separated viewer. Beside searching bugs, the tool can be used to assist beginners in learning the non-deterministic behavior of lazy functional logic programs. To find a surrounding area that contains the failure, the tool can furthermore show the executed part of the program by marking the expressions that are activated during program execution.
Program slicing is a method for decomposing programs by analyzing their data and control flow. Slicing-based techniques have many applications in the field of software engineering (like program debugging, testing, code reuse, maintenance, etc). Slicing has been widely studied within the imperative programming paradigm, where it is often based on the so called program dependence graph, a data structure that makes explicit both the data and control dependences for each operation in a program. Unfortunately, the notion of "dependence" cannot be easily adapted to a functional context. In this work, we define a novel approach to static slicing (i.e., independent of a particular input data) for first-order functional programs which are represented by means of rewrite systems. For this purpose, we introduce an appropriate notion of dependence that can be used for computing program slices. Also, since the notion of static slice is generally undecidable, we introduce a complete approximation for computing static slices which is based on the construction of a term dependence graph, the counterpart of program dependence graphs.
Poly-controlled partial evaluation (PCPE) is a flexible approach for specializing logic programs, which has been recently proposed. It takes into account repertoires of global control and local control rules instead of a single, predetermined, combination. Thus, different global and local control rules can be assigned to different call patterns, obtaining results that are hybrid in the sense that they cannot be obtained using a single combination of control rules, as traditional partial evaluation does.
PCPE can be implemented as a search-based algorithm, producing sets of candidate specialized programs (many of them hybrid), instead of a single one. The quality of each of these programs is assessed through the use of different fitness functions, which can be resource aware, taking into account multiple factors such as run-time, memory consumption, and code size of the specialized programs, among others.
Although PCPE is an appealing approach, it suffers from an inherent blowup of its search space when implemented as a search-based algorithm. Thus, in order to be used in practice, and to deal with realistic programs, we must be able to prune its search space without losing the interesting solutions.
The contribution of this work is two-fold. On one hand we perform an experimental study on the heterogeneity of solutions obtained by search-based PCPE, showing that the solutions provided behave very differently when compared using a fitness function. Note that this is important since otherwise the cost of producing a large number of candidate specializations would not be justified.
The second contribution of this work is the introduction of a technique for pruning the search space of this approach. The proposed technique is easy to apply and produces a considerable reduction of the size of the search space, allowing PCPE to deal with a reasonable number of benchmark programs. Although pruning is done in a heuristic way, our experimental results suggest that our heuristic behaves well in practice, since the fitness value of the solutions obtained using pruning coincide with the fitness value of the solution obtained when no pruning is applied.
This paper presents the integration of the optimization known as dynamic cut within the functional-logic system Toy. The implementation automatically detects deterministic functions at compile time, and includes in the generated code the test for detecting at run time the computations that can actually be pruned. The outcome is a much better performance when executing deterministic functions including either or-branches in their definitional trees or extra variables in their conditions, with no serious overhead in the rest of the computations. The papers also proves the correctness of the criterion used for detecting deterministic functions w.r.t. the semantic calculus CRWL.
We show how the algebra of (binary) relations and the features of the integrated functional logic programming language Curry can be employed to solve problems on relational structures (like orders, graphs, and Petri nets) in a very high-level declarative style. The functional features of Curry are used to implement relation algebra and the logic features of the language are combined with BDD-based solving of Boolean constraints to obtain a fairly efficient implementation of a solver for relational specifications.
Programmers need mechanisms to store application specific data that persists multiple program runs. To accomplish this task, they usually have to deal with storage specific code to access files or relational databases. Functional logic programming provides a natural framework to transparent persistent storage through persistent predicates, i.e., predicates with externally stored facts.
We extend previous work on persistent predicates for Curry by lazy database access. Results of a database query are only read as much as they are demanded by the application program. We also present a type-oriented approach to convert between database and Curry values which is used to implement lazy access to persistent predicates based on a low level lazy database interface.
Expander2 is a flexible multi-purpose workbench for interactive rewriting, verification, constraint solving, flow graph analysis and other procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as two-dimensional structures ranging from trees and rooted graphs to a variety of pictorial representations that include tables, matrices, alignments, partitions, fractals and turtle systems. Proofs and computations performed with Expander2 follow the rules and the semantics of swinging types. Swinging types are based on many-sorted predicate logic and combine visible constructor-based types with hidden state-based types. The former come as initial term models, the latter as final models consisting of context interpretations. Relation symbols are interpreted as least or greatest solutions of their respective axioms. This paper presents an overview of Expander2 with particular emphasis on the system's prover capabilities. It is an adaptation of [ ] to the latest version of Expander2. In particular, proof rules tailor-made for transition rule specifications have been added to the system and are discussed and exemplified here for the first time.
Metaprogramming consists of writing programs that generate or manipulate other programs. Template Haskell is a recent extension of Haskell, currently implemented in the Glasgow Haskell Compiler, giving support to metaprogramming at compile time. Our aim is to apply these facilities in order to statically analyse programs and transform them at compile time. In this paper we use Template Haskell to implement an abstract interpretation based strictness analysis and a let-to-case transformation that uses the results of the analysis. This work shows the usefulness of the tool in order to incorporate new analyses and transformations into the compiler without modifying it.
The importance of temporal representation and reasoning is well known not only in the database community but also in the artificial intelligence one. Contextual Logic Programming (CxLP) is a simple and powerful language that extends logic programming with mechanisms for modularization. Recent work not only presented a revised specification of CxLP together with a new implementation for it but also explained how this language could be seen as a shift into the Object-Oriented Programming paradigm. In this paper we propose a temporal extension of such language called Temporal Contextual Logic Programming. Such extension follows a reified approach to the temporal qualification, that besides the acknowledge increased expressiveness allows us to capture the notion of time of the context. Together with the syntax of this language we also present its operational semantics and two application: management of workflows and vaccination plans.
The CFLP scheme for Constraint Functional Logic Programming has instances CFLP(D) corresponding to different constraint domains D. In this paper we propose an amalgamated sum construction for building coordination domains C, suitable to represent the cooperation between several constraint domains D1,...,Dn via a mediatorial domain M. Moreover, we present a cooperative goal solving calculus for CFLP(C) programming, based on lazy narrowing, invocation of solvers for the different domains Di involved in the coordination domain C, and projection operations for converting Di constraints into Dj constraints with the aid of mediatorial constraints (so-called bridges) supplied by M. Under natural correctness assumptions for the projection operations, the cooperative goal solving calculus can be proved fully sound w.r.t. the declarative semantics of CFLP(C). As a relevant concrete instance of our proposal, we consider the cooperation between Herbrand, real arithmetic and finite domain constraints.
Labelling is crucial in the performance of solving timetabling problems with constraint programming. Traditionally, labelling strategies are based on dynamic information about variables and their domains, and selecting variables and values to assign. However, the size of combinatorial problems is limited by these techniques. In this paper, we present a real problem solved with constraint programming using an explicit search based on the knowledge about the solution structure as an starting point for classical propagation and labelling techniques to find a feasible solution. For those problems in which solutions are close to the seed because of its structure, propagation and labelling can reach a first solution within a small response time. We apply our proposal to a real timetabling problem, and we tackle its implementation with two different languages, OPL and TOY, using the constraint programming paradigm over finite domains. OPL is a commercial, algebraic, and specific-purpose programming language, whereas TOY is a prototype of a general-purpose declarative programming language. We present the specification of the problem, its implementation with both languages, and a comparative performance analysis.
We describe the introduction of disequality constraints over algebraic data terms in Sloth, one implementation of the functional logic language Curry. This addition extends the standard definition of Curry in several ways. On one hand, we provide a disequality counterpart to the constraint equality operator (=:=). Secondly, boolean equality operators are also redefined to cope with constructive disequality information, which leads to a more symmetric design w.r.t. the existing one.
Semantically speaking, our implementation is very similar to previous proposals, although there are some novel aspects. One of them is that the implementation is partly based on an existing finite domain constraint solver, which provides a more efficient execution in some examples. There are also some issues regarding the interaction of our extension with the type and module systems that deserve some discussion.
Some benchmarks, an operational semantics minimally extending the one in the Curry draft, and a moderately detailed description of the implementation complete the paper.