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.