Home page


Conference Venue
12th Int'l Workshop on Functional and (Constraint) Logic Programming
Valencia, Spain, June 12-13, 2003


    Automatic Visualization of Recursion Trees: a Case Study on Generic Programming
    A. Cunha (Universidade do Minho, Braga, Portugal)

    Although the principles behind generic programming are already well understood, this style of programming is not widespread and examples of applications are rarely found in the literature. This paper addresses this shortage by presenting a new method, based on generic programming, to automatically visualize recursion trees of functions written in Haskell. Crucial to our solution is the fact that almost any function definition can be automatically factorized into the composition of a fold after an unfold of some intermediate data structure that models its recursion tree. By combining this technique with an existing tool for graphical debugging, and by extensively using Generic Haskell, we achieve a rather concise and elegant solution to this problem.

    Refined Definitional Trees and Prolog Implementations of Narrowing
    P. Julian-Iranzo (Universidad de Castilla-La Mancha, Ciudad Real,Spain)

    This paper describes how high level implementations of (need-ed) narrowing into Prolog can be improved by introducing a refined representation of definitional trees that handles properly the knowledge about the inductive positions of a pattern. We define some generic algorithms that allow us to transform a functional logic program into a set of Prolog clauses which incorporates some refinements that are obtained by ad hoc artifices in other similar implementations of functional logic languages. We also present and discuss the advantages of our proposal by means of some simple examples.

    Multiple Evaluation Strategies for the Multiparadigm Programming Language Brooks
    P. Hofstedt (Technische Universität Berlin, Germany)
    A. Metzner (Technische Universität Berlin, Germany)

    This paper presents the functional logic programming language Brooks which inherits from the languages Curry and BABEL, but allows the integration of different narrowing strategies. We describe briefly the abstract machine BEBAM as target for the compilation of Brooks programs together with key points of the translation process. Furthermore differences to other multiparadigm languages are discussed.

    Graphical Representations and Infinite Virtual Worlds in a Logic and Functional Programming Course
    J.E. Labra Gayo (University of Oviedo, Spain)

    The assignment scheme of our \emph{Logic and Functional Programming} course has adopted the generation of graphical representations, quadtrees and octrees to teach the different features of this kind of languages: higher order functions, lazy evaluation, polymorphism, logical variables, constraint satisfaction, etc. The use of standard XML vocabularies: SVG for graphics and X3D for virtual worlds enables to have numerous visualization tools. We consider that the incorporation of these exercises facilitates teaching and improves the motivation of students.

    A Narrowing-based Instantiation Rule for Rewriting-based Fold/Unfold Transformations
    G. Moreno (University of Castilla-La Mancha, Albacete, Spain)

    In this paper we show how to transfer some developments done in the field of functional-logic programming (FLP) to a pure functional setting (FP). More exactly, we propose a complete fold/unfold based transformation system for optimizing lazy functional programs. Our main contribution is the definition of a safe instantiation rule which is used to enable effective unfolding steps based on rewriting. Since instantiation has been traditionally considered problematic in FP, we take advantage of previous experiences in the more general setting of FLP where instantiation is naturally embedded into an unfolding rule based on narrowing. Inspired in the so called needed narrowing strategy, our instantiation rule inherits the best properties of this refinement of narrowing. Our proposal optimises previous approaches defined in the literature (that require more transformation effort) by anticipating bindings on unifiers used to instantiate a given program rule and by generating redexes at different positions on instantiated rules in order to enable subsequent unfolding steps. As a consequence, our correct/complete technique avoids redundant rules and preserve the natural structure of programs.

    A Demand Narrowing Calculus with Overlapping Definitional Trees
    R. del Vado Virseda (Universidad Complutense de Madrid, Spain)

    We propose a demand conditional narrowing calculus in which a variant of definitional trees is used to efficiently control the narrowing strategy. This calculus is sound and strongly complete w.r.t. Constructor-based ReWriting Logic (CRWL) semantics for a wide class of constructor-based conditional term rewriting systems. The calculus mantains the optimality properties of the needed narrowing strategy. Moreover, the treatment of strict equality as a primitive rather a defined function symbol, leads to an improved behaviour w.r.t. needed narrowing.

    Integrating Finite Domain Constraints and CLP with Sets
    A. Dal Palù (Università di Udine, Italy)
    A. Dovier (Università di Udine, Italy)
    E. Pontelli (New Mexico State University, USA)
    G. Rossi (Università di Parma, Italy)

    We propose a semantically well-founded combination of the constraint solvers used in the constraint programming languages CLP(SET) and CLP(FD). This work demonstrates that it is possible to provide efficient executions (through CLP(FD) solvers) while maintaining the expressive power and flexibility of the CLP(SET) language. We develop a combined constraint solver and we show how static analysis can help in organizing the distribution of constraints to the two constraint solvers.

    Functional Logic Programming with Failure and Built-in Equality
    F. López-Fraguas (Universidad Complutense de Madrid, Spain)
    J. Sánchez-Hernández (Universidad Complutense de Madrid, Spain)

    Constructive failure has been proposed recently as a programming construct useful for functional logic programming, playing a role similar to that of constructive negation in logic programming. On the other hand, almost any functional logic program requires the use of some kind of equality test between expressions. We face in this work in a rigorous way the interaction of failure and equality (even for non-ground expressions), which is a non trivial issue, requiring in particular the use of disequality conditions at the level of the operational mechanism of constructive failure. As an interesting side product, we develop a novel treatment of equality and disequality in functional logic programming, by giving them a functional status, which is better suited for practice than previous proposals.

    Towards Translating Embedded Curry to C
    M. Hanus (CAU Kiel, Germany)
    K. Höppner (CAU Kiel, Germany)
    F. Huch (CAU Kiel, Germany)

    This paper deals with a framework to program autonomous robots in the declarative multi-paradigm language Curry. Our goal is to apply a high-level declarative programming language for the programming of embedded systems. For this purpose, we use a specialization of Curry called Embedded Curry. We show the basic ideas of our framework and an implementation that translates Embedded Curry programs into C.

    A Monadic Semantics for Core Curry
    A. Tolmach (Portland State University, USA)
    S. Antoy (Portland State University, USA)

    We give a high-level operational semantics for the essential core of the Curry language, including higher-order functions, call-by-need evaluation, non-determinism, narrowing, and residuation. The semantics is structured in monadic style, and is presented in the form of an executable interpreter written in

    A Safe Relational Calculus for Functional Logic Deductive Databases
    J.M. Almendros-Jimenez (Universidad de Almeria, Spain)
    A. Becerra-Teron (Universidad de Almeria, Spain)

    In this paper, we present an extended relational calculus for expressing queries in functional-logic deductive databases. This calculus is based on first-order logic and handles relation predicates, equalities and inequalities over partially defined terms, and approximation equations. For the calculus formulas, we have studied syntactic conditions in order to ensure the domain independence property. Finally, we have studied its equivalence w.r.t. the original query language which is based on equality and inequality constraints.

    Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof
    N. Nishida (Nagoya University, Japan)
    M. Sakai (Nagoya University, Japan)
    T. Sakabe (Nagoya University, Japan)

    Term rewriting systems (TRSs) are extended by allowing to contain extra variables in their rewrite rules. We call the extended systems EV-TRSs. They are ill-natured since every one-step reduction by their rules with extra variables is infinitely branching and they are not terminating. To solve these problems, this paper extend narrowing on TRSs into that on EV-TRSs and show it simulates the reduction sequences of EV-TRSs as the sequences starting from ground terms. We prove the soundness of ground narrowing sequences for the reduction sequences of EV-TRSs. We prove the completeness for the case of right-linear EV-TRSs, and also for the case that no redex in terms substituted for extra variables is reduced in the reduction sequences. Moreover, we give a method to prove termination of EV-TRSs' simulation, extending the termination proof of TRSs using dependency pairs to that of narrowing starting from ground terms.

    Cost-Sensitive Debugging of Declarative Programs
    D. Ballis (Università di Udine, Italy)
    M. Falaschi (Università di Udine, Italy)
    C. Ferri (Universidad Politécnica de Valencia, Spain)
    J. Hernández-Orallo (Universidad Politécnica de Valencia, Spain)
    M.J. Ramírez (Universidad Politécnica de Valencia, Spain)

    Diagnosis methods in debugging aim at detecting bugs of a program, either by comparing it with a correct specification or by the help of an oracle (usually the user herself). Debugging techniques for declarative programs usually exploit the semantical properties of programs (and specifications) and generally try to detect one or more "buggy" rules. In this way, rules are split apart in an absolute way: either they are correct or not. However, in many situations, not every error has the same consequences, an issue that is ignored by classical debugging frameworks. In this paper, we generalise debugging by considering a cost function, i.e. a function that assigns different cost values to each kind of error and different benefit values to each kind of hit. The problem is now redefined as assigning a real-valued probability and cost to each rule, by considering each rule more or less "guilty" of the overall error and cost of the program. This makes possible to rank rules rather than only separate them between right and wrong. Our debugging method is also different from classical approaches in the way that it is probabilistic, i.e. we use a set of ground examples to approximate these rankings. However, by using a convenient cost function, the method is simple, effective and efficient; we are able to diagnose problems where specification and program differ in the auxiliary functions used or even in cases where there is no specification and we only have a set of positive and negative examples.

    Handling quantifiers in Relational Data Mining
    D. Lorenzo (Univ. Coruña, Spain)

    Relational data mining systems are able to mine regularities from data that is spread over multiple tables in a database. In these systems, both input data and the discovered regularities are represented using the syntax of Prolog. An interesting issue is to investigate whether these methods can be extended to find more expressive regularities where variabdles can be freely quantified. For this task several issues have to be studied concerning the search space to explore, the evaluation methods and the interestingness measures. From this study we implemented a simple learning system based on the system Claudien. We report on a reduced set of experiments to show the potential of the approach.

    Abstract Correction of Functional Programs
    M. Alpuente (Universidad Politécnica de Valencia, Spain)
    D. Ballis (Università di Udine, Italy)
    S. Escobar (Universidad Politécnica de Valencia, Spain)
    M. Falaschi (Università di Udine, Italy)
    S. Lucas (Universidad Politécnica de Valencia, Spain)

    Debussy is an (abstract) declarative diagnosis tool for functional programs which are written in OBJ style. The debugger does not require the user to either provide error symptoms in advance or answer any question concerning program correctness. In this paper, we develop a top-down inductive learner for repairing program bugs. Correct program rules are automatically synthesized from the examples which are generated as an outcome of the diagnoser.

    A Memoization Technique for Functional Logic Languages
    S. España (Universidad Politécnica de Valencia, Spain)
    V. Estruch (Universidad Politécnica de Valencia, Spain)

    Declarative multi-paradigm languages combine the main features of functional and logic programming, like laziness, logic variables and non-determinism. Pure functional and pure logic programming have for long time taken advantage of tabling or memoization schemes, which motivates the interest in adapting this technique to the integrated paradigm. In this work, we introduce an operational description of narrowing with memoization whose main aim is to provide the basis for a complete sequential implementation. Since the success of memoization critically depends on efficiently indexing terms and accessing the table, we study the adequacy of known term representation techniques. In this direction, we introduce a novel data structure for representing terms and show how to use this representation in our framework.

    Runtime Verification of Concurrent Haskell
    V. Stolz (RWTH Aachen, Germany)
    F. Huch (CAU of Kiel, Germany)

    In this article we use model checking techniques to debug Concurrent Haskell programs. LTL formulas specifying assertions or other properties are verified at runtime. If a formula cannot be satisfied, the debugger emits a warning and prints the path leading to the violation. It is possible to dynamically add formulas at runtime, giving a degree of flexibility which is not available in static verification of source code. We give a comprehensive example of using the new techniques to detect lock-reversal in Concurrent Haskell programs.

    Improving (Weakly) Outermost-Needed Narrowing: Natural Narrowing
    S. Escobar (Universidad Politécnica de Valencia, Spain)

    Different elaborated definitions of "demandness" have been proposed up to date to develop optimal rewriting strategies and enlarge the class of term rewriting systems (TRSs) allowing for optimal evaluation. Outermost-needed narrowing is a sound and complete optimal demand-driven strategy for the class of inductively sequential CSs which is defined as the functional logic counterpart of Huet and Lévy's strongly needed reduction. Its parallel extension (known as weakly) deals with non-inductively sequential CSs and it is defined as the functional logic counterpart of Sekar and Ramakrishnan parallel needed reduction. In this paper, we present natural narrowing, a suitable extension of (weakly) outermost-needed narrowing which is based on a refinement of the demandness notion associated to outermost-needed narrowing. Intuitively, natural narrowing always reduces or instantiates the most demanded position in a term. We formalize the strategy for left-linear CSs although, for the class of inductively sequential CSs, natural narrowing behaves even better than outermost-needed narrowing. Regarding inductively sequential CSs, we introduce a bigger class of systems called inductively sequential preserving where natural rewriting is optimal.

    Model Checking Erlang Programs -- LTL-Propositions and Abstract Interpretation
    F. Huch (CAU of Kiel, Germany)

    We present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. In previous work we defined a framework for the verification of Erlang programs using abstract interpretation and LTL model checking. The application of LTL model checking yields some problems in the verification of state propositions, because propositions are also abstracted in the framework. In dependence of the number of negations in front of state propositions in a formula they must be satisfied or refuted. We show how this can automatically be decided by means of the abstract domain. The approach is implemented as a prototype and we are able to prove properties like mutual exclusion or the absence of deadlocks and lifelocks for some Erlang programs.

    Towards a Mobile Haskell
    A.R. Du Bois (Heriot-Watt University, Edinburgh, UK)
    P. Trinder (Heriot-Watt University, Edinburgh, UK)
    H-W. Loidl (Ludwig-Maximilians-Universitat Muenchen, Germany)

    This paper proposes a set of communication primitives for Haskell, to be used in open distributed systems, i.e. systems where multiple executing programs can interact using a predefined protocol. Functions are first class citizens in a functional language, hence it would be natural transfer them between programs in a distributed system. However, existing distributed Haskell extensions are limited to closed systems or restrict the set of expressions that can be communicated. The former effectively prohibits large-scale distribution, whereas the latter sacrifices key abstraction constructs. A functional language that allows the communication of functions in an open system can be seen as a mobile computation language, hence we call our extension mHaskell (Mobile Haskell). We demonstrate how the proposed communication primitives can be used to implement more powerful abstractions, such as remote evaluation, and that common patterns of communication can be encoded as higher order functions or mobile skeletons. The design has been validated by constructing a prototype in Glasgow Distributed Haskell, and a compiled implementation is under construction.

    An Open System to Support Web-based Learning
    M. Hanus (CAU Kiel, Germany)
    F. Huch (CAU of Kiel, Germany)

    In this paper we present a system, called CurryWeb, to support web-based learning. Characteristic features of this system is openness and self-responsible use. Openness means that there is no strong distinction between instructors and students, i.e., every user can learn with the system or add new learning material to it. Self-responsible use means that every user is responsible for selecting the right material to obtain the desired knowledge. However, the system supports this selection process by structuring all learning material hierarchically and as a hypergraph whose nodes and edges are marked with educational objectives and educational units, respectively. The complete system is implemented with the declarative multi-paradigm language Curry. In this paper we describe how the various features of Curry support the high-level implementation of this system. This shows the appropriateness of declarative multi-paradigm languages for the implementation of complex web-based systems.

    Constructive Intensional Negation: A Practical Implementation
    S. Muñoz (Universidad Politécnica de Madrid, Spain)
    J. Mariño (Universidad Politécnica de Madrid, Spain)
    J.J. Moreno-Navarro (Universidad Politécnica de Madrid, Spain)

    Negation is arguably the most important feature of first order logic not present in Logic Programming (LP). While the integration of negation into LP has been actively studied from a semantic perspective, the negation capabilities in actual Prolog compilers are rather limited. One of the most promising techniques in the literature is intensional negation, following a transformational approach: for each positive predicate "p" its negative counterpart "intneg(p)" is generated. However, from the practical point of view intensional negation cannot be considered a successful approach because no implementation is given. The reson is that neither universally quantified goals can be computed nor many practical issues are addressed. In this paper, we describe our variant of the transformation of the intensional negation, called "Constructive Intensional Negation" providing some formal results as well as discussing a concrete implementation.


    A Web Oriented System for Equational Solving
    N. Kobayashi (University of Tsukuba, Japan)
    M. Marin (Austrian Academy of Sciences, Austria)
    T. Ida (University of Tsukuba, Japan)

    We describe a collaborative constraint functional logic programming system for web environments. The system is called Web CFLP, and is designed to solve systems of equations in theories presented by higher-order pattern rewrite systems by collaboration among equation solving services located on the web. Web CFLP is an extension of the system Open CFLP described in our previous work in order to deploy the system on the realistic web environment. We will discuss the architecture of Web CFLP and its language.

Last update May 2003 # sescobar@dsic.upv.es