Unintended failures during a computation are painful but frequent during software development. Failures due to external reasons (e.g., missing files, no permissions, etc.) can be caught by exception handlers. Programming failures, such as calling a partially defined operation with unintended arguments, are often not caught due to the assumption that the software is correct. This paper presents an approach to verify such assumptions. For this purpose, non-failure conditions for operations are inferred and then checked in all uses of partially defined operations. In the positive case, the absence of such failures is ensured. In the negative case, the programmer could adapt the program to handle possibly failing situations and check the program again. Our method is fully automatic and can be applied to larger declarative programs. The results of an implementation for functional logic Curry programs are presented.

Functional logic programming languages, such as Curry, integrate features of functional and logic paradigms, in particular, demand-driven deterministic evaluation from functional programming with non-deterministic search from logic programming. Though useful for programming, this combination can lead to unintended results and subtle bugs. To support programming with this powerful computation model, this paper proposes a method to detect unintended non-determinism at compile time. For this purpose, we propose determinism types to approximate the determinism behavior of functions and expressions. In contrast to standard types in strongly typed languages, determinism types do not restrict the set of admissible programs but support the programmer and programming tools in reasoning about functional logic programs, e.g., to enforce determinism in top-level I/O operations. We present the motivation behind this approach, discuss core concepts of functional logic programming and Curry, and outline methods to check for determinism through type-based analysis.

Abstract Logic programming is a flexible programming paradigm due to the use of predicates without a fixed data flow. To extend logic languages with the compact notation of functional programming, there are various proposals to map evaluable functions into predicates in order to stay in the logic programming framework. Since amalgamated functional logic languages offer flexible as well as efficient evaluation strategies, we propose an opposite approach in this paper. By mapping logic programs into functional logic programs with a transformation based on inferring functional dependencies, we develop a fully automatic transformation which keeps the flexibility of logic programming but can improve computations by reducing infinite search spaces to finite ones.

The declarative programming language Curry amalgamates demand-driven evaluation from functional programming with non-determinism from logic programming. In contrast to Prolog, the search strategy for non-deterministic computations is not fixed so that complete or parallel strategies are reasonable for Curry. In particular, a desirable option is a fair strategy which frees the programmer from considering the influence of the search strategy to the success of a computation. In this paper we describe an implementation with this property. Based on recent developments on operational models for functional logic programming, we present a new implementation which transforms Curry programs in several transformation steps into Go programs. By exploiting lightweight threads in the form of goroutines, we obtain a complete and fair implementation which automatically uses multi-processing to speed up non-deterministic computations. This has the effect that, in some cases, non-deterministic algorithms are more efficiently evaluated than deterministic ones.

Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre- and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking for the functional logic language Curry. Based on a formal model of contract checking for functional logic programming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, it can be omitted from dynamic checking. This method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution.

Failed computations are a frequent problem in software system development. Some failures have external reasons (e.g., missing files) that can be caught by exception handlers. Many other failures have internal reasons, such as calling a partially defined operation with unintended arguments. In order to avoid the latter kind of failures, one can try to analyze the program at compile time for potential occurrences of these failures at run time. In this paper we present an approach to verify the absence of such failures in functional logic programs. Since programming with failures is a typical technique in logic programming, we are not interested to abandon partially defined operations at all. Instead, we want to verify conditions which ensure that operations can be executed without running into a failure. For this purpose, we propose to annotate operations with non-fail conditions that are verified at compile time with an SMT solver. For successfully verified programs, it is ensured that computations never fail provided that the non-fail condition of the main operation is satisfied.

Abstract Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction in source programs, the language design can be simplified and the execution of programs can be optimized. As a consequence, we show that one kind of equational expressions is sufficient and unification is nothing else than an optimization of Boolean equality.

Abstract In functional logic programs, rules are applicable independently of textual order, i.e., any rule can potentially be used to evaluate an expression. This is similar to logic languages and contrary to functional languages, e.g., Haskell enforces a strict sequential interpretation of rules. However, in some situations it is convenient to express alternatives by means of compact default rules. Although default rules are often used in functional programs, the non-deterministic nature of functional logic programs does not allow to directly transfer this concept from functional to functional logic languages in a meaningful way. In this paper, we propose a new concept of default rules for Curry that supports a programming style similar to functional programming while preserving the core properties of functional logic programming, i.e., completeness, non-determinism, and logic-oriented use of functions. We discuss the basic concept and propose an implementation which exploits advanced features of functional logic languages.

We present the design, implementation, and application of a system, called CASS, for the analysis of functional logic programs. The system is generic so that various kinds of analyses (e.g., groundness, non-determinism, demanded arguments) can be easily integrated. In order to analyze larger applications consisting of dozens or hundreds of modules, CASS supports a modular and incremental analysis of programs. Moreover, it can be used by different programming tools, like documentation generators, analysis environments, program optimizers, as well as Eclipse-based development environments. For this purpose, CASS can also be invoked as a server system to get a language-independent access to its functionality. CASS is completely implemented in the functional logic language Curry as a master/worker architecture to exploit parallel or distributed execution environments.

Abstract We describe a framework to support the implementation of web-based systems intended to manipulate data stored in relational databases. Since the conceptual model of a relational database is often specified as an entity-relationship (ER) model, we propose to use the ER model to generate a complete implementation in the declarative programming language Curry. This implementation contains operations to create and manipulate entities of the data model, supports authentication, authorization, session handling, and the composition of individual operations to user processes. Furthermore, the implementation ensures the consistency of the database w.r.t. the data dependencies specified in the ER model, i.e., updates initiated by the user cannot lead to an inconsistent state of the database. In order to generate a high-level declarative implementation that can be easily adapted to individual customer requirements, the framework exploits previous works on declarative database programming and web user interface construction in Curry.

Encapsulated search is a key feature of (functional) logic languages. It allows the programmer to access and process different results of a non-deterministic computation within a program. Unfortunately, due to advanced operational features (lazy evaluation, partial values, infinite structures), there is no straightforward definition of the semantics of encapsulated search in functional logic languages. As a consequence, various proposals and implementations are available but a rigorous definition covering all semantical aspects does not exist. In this paper, we analyze the requirements of encapsulated search in a functional logic language like Curry and provide a comprehensive definition that covers weak encapsulation, a modular form of encapsulation, as well as nested applications of search operators. We set up a denotational semantics that distinguishes non-termination and different levels of failures in a computation. The semantics is also the basis of a practical implementation of search operators in the functional logic language Curry.

Xtext is an open-source framework for implementing external, textual domain-specific languages (DSLs). So far, most DSLs implemented with Xtext and similar tools focus on structural aspects such as service specifications and entities. Because behavioral aspects are significantly more complicated to implement, they are often delegated to general-purpose programming languages. This approach introduces complex integration patterns and the DSL's high level of abstraction is compromised.

We propose a novel approach to encapsulate non-deterministic computations in functional logic programs. Our approach is based on set functions that return the set of all the results of a corresponding ordinary operation. A characteristic feature of our approach is the complete separation between a usually-non-deterministic operation and its possibly-non-deterministic arguments. This separation leads to the first provably order-independent approach to computing the set of values of non-deterministic expressions. The proof is provided within the framework of graph rewriting in constructor-based systems. We propose an abstract implementation of our approach and prove its independence of the order of evaluation. Our approach solves easily and naturally problems mishandled by current implementations of functional logic languages.

This paper presents a new program analysis framework to approximate call patterns and their results in functional logic computations. We consider programs containing nonstrict, nondeterministic operations in order to make the analysis applicable to modern functional logic languages like Curry or TOY. For this purpose, we present a new fixpoint characterization of functional logic computations w.r.t. a set of initial calls. We show how programs can be analyzed by approximating this fixpoint. The results of such an approximation have various applications, e.g., program optimization as well as verifying safety properties of programs

Designing debugging tools for lazy functional programming languages is a complex task which is often solved by expensive tracing of lazy computations. We present a new approach in which the information collected as a trace is reduced considerably (kilobytes instead of megabytes). The idea is to collect a kind of step information for a call-by-value interpreter, which can then efficiently reconstruct the computation for debugging/viewing tools, like declarative debugging. We show the correctness of the approach, discuss a proof-of-concept implementation with a declarative debugger as back end and present some benchmarks comparing our new approach with the Haskell debugger Hat.

We propose a framework to construct web-oriented user interfaces in a high-level way by exploiting declarative programming techniques. Such user interfaces are intended to manipulate complex data in a type-safe way, i.e., it is ensured that only typecorrect data is accepted by the interface, where types can be specified by standard types of a programming language as well as any computable predicate on the data. The interfaces are web based, i.e., the data can be manipulated with standard web browsers without any specific requirements on the client side. However, if the client's browser has JavaScript enabled, one could also check the correctness of the data on the client side providing immediate feedback to the user. In order to release the application programmer from the tedious details to interact with JavaScript, we propose an approach where the programmer must only provide a declarative description of the requirements of the user interface from which the necessary JavaScript programs and HTML forms are automatically generated. This approach leads to a very concise and maintainable implementation of web-based user interfaces. We demonstrate an implementation of this concept in the declarative multi-paradigm language Curry where the integrated functional and logic features are exploited to enable the high level of abstraction proposed in this paper.

This paper proposes a new technique for the high-level construction of type-safe web-oriented user interfaces. Our approach is useful to equip applications processing structured data with interfaces to manipulate these data in an efficient and maintainable way. The interfaces are web-based, i.e., the data can be manipulated with standard web browsers without any specific requirements on the client side. In order to support type-safe user interfaces, i.e., interfaces where users can only input type-correct data (types can be standard types of a programming language as well as any computable predicate on the data), we propose a set of type-oriented building blocks from which interfaces for more complex types can be easily constructed. This technique leads to a very concise and maintainable implementation of web-based user interfacesWe show an implementation of this concept in the declarative multi-paradigm language Curry. In particular, its integrated functional and logic features are exploited to enable the high level of abstraction proposed in this paper.

Many functional logic languages are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction mechanism of functional languages and the resolution principle of logic languages. Needed narrowing is an optimal evaluation strategy which constitutes the basis of modern (narrowing-based) lazy functional logic languages. In this work, we present the fundamentals of partial evaluation in such languages. We provide correctness results for partial evaluation based on needed narrowing and show that the nice properties of this strategy are essential for the specialization process. In particular, the structure of the original program is preserved by partial evaluation and, thus, the same evaluation strategy can be applied for the execution of specialized programs. This is in contrast to other partial evaluation schemes for lazy functional logic programs which may change the program structure in a negative way. Recent proposals for the partial evaluation of declarative multi-paradigm programs use (some form of) needed narrowing to perform computations at partial evaluation time. Therefore, our results constitute the basis for the correctness of such partial evaluators.

We introduce the theoretical basis for tracing lazy functional logic computations in a declarative multi-paradigm language like Curry. Tracing computations is a difficult task due to the subtleties of the underlying operational semantics which combines laziness and non-determinism. In this work, we define an instrumented operational semantics that generates not only the computed values and bindings but also an appropriate data structure---a sort of redex trail---which can be used to trace computations at an adequate level of abstraction. In contrast to previous approaches, which rely solely on a transformation to instrument source programs, the formal definition of a tracing semantics improves the understanding of the tracing process. Furthermore, it allows us to formally prove the correctness of the computed trail. A prototype implementation of a tracer based on this semantics demonstrates the usefulness of our approach.

An injective finite mapping is an abstraction common to many programs. We describe the design of an injective finite mapping and its implementation in Curry, a functional logic language. Curry supports the concurrent asynchronous execution of distinct portions of a program. This condition prevents passing from one portion to another a structure containing a partially constructed mapping to ensure that a new choice does not violate the injectivity condition. We present some motivating problems and we show fragments of programs that solve these problems using our design and implementation.

We present a new evaluation strategy for functional logic programs described by weakly orthogonal conditional term rewriting systems. Our notion of weakly orthogonal conditional rewrite system extends a notion of Bergstra and Klop and covers a large part of programs defined by conditional equations. Our strategy combines the flexibility of logic programming (computation of solutions for logic variables) with efficient evaluation methods from functional programming. In particular, it is the first known narrowing strategy for this class of programs that evaluates ground terms deterministically. This is achieved by a transformation of conditional term rewriting systems (CTRS) into unconditional ones which is sound and complete w.r.t. the semantics of the original CTRS. We show that the transformation preserves weak orthogonality for the terms of interest. This property allows us to apply a relatively efficient evaluation strategy for weakly orthogonal unconditional term rewriting systems (parallel narrowing) on the transformed programs.

This paper describes an implementation of narrowing, an essential component of implementations of modern functional logic languages. These implementations rely on narrowing, in particular on some optimal narrowing strategies, to execute functional logic programs. We translate functional logic programs into imperative (Java) programs without an intermediate abstract machine. A central idea of our approach is the explicit representation and processing of narrowing computations as data objects. This enables the implementation of operationally complete strategies (i.e., without backtracking) or techniques for search control (e.g., encapsulated search). Thanks to the use of an intermediate and portable represen tation of programs, our implementation is general enough to be used as a common back end for a wide variety of functional logic languages.

Functional logic languages combine nondeterministic search facilities of logic languages with features of functional languages, e.g., monadic I/O to provide a declarative method to deal with I/O actions. Unfortunately, monadic I/O cannot be used in programs which split the computation due to nondeterministic reductions. This problem can be avoided if nondeterministic computations are encapsulated by search operators which are available, for instance, in the multi-paradigm language Curry. To support the programmer in identifying nondeterministic parts of a program, we develop a method based on a type and effect system that will find every possible source of nondeterminism. Additionally, such information can be exploited in compilers to optimize deterministically reducible parts of a program. 1. INTRODUCTION An important feature of logic languages is the ability to deal with nondeterministic computations to compute solutions for partially instantiated goals. This can lead to problems whe...

Functional logic languages combine the operational principles of the most important declarative programming paradigms, namely functional and logic programming. Inductively sequential programs admit the definition of optimal computation strategies and are the basis of several recent (lazy) functional logic languages. In this paper, we define a partial evaluator for inductively sequential functional logic programs. We prove strong correctness of this partial evaluator and show that the nice properties of inductively sequential programs carry over to the specialization process and the specialized programs. In particular, the structure of the programs is preserved by the specialization process. This is in contrast to other partial evaluation methods for functional logic programs which can destroy the original program structure. Finally, we present some experiments which highlight the practical advantages of our approach.

Functional logic languages with a sound and complete operational semantics are mainly based on an inference rule called narrowing. Narrowing extends functional evaluation by goal solving capabilities, as in logic programming. Due to the huge search space of simple narrowing, steadily improved narrowing strategies have been developed in the past. Needed narrowing is currently the best narrowing strategy for first-order functional logic programs due to its optimality properties wrt the length of derivations and the number of computed solutions. In this paper, we extend the needed narrowing strategy to higher-order functions and λ-terms as data structures. By the use of definitional trees, our strategy computes only independent solutions. Thus, it is the first calculus for higher-order functional logic programming which provides for such an optimality result. Since we allow higher-order logical variables denoting λ-terms, applications go beyond current functional and logic programming languages. We show soundness and completeness of our strategy with respect to LNT reductions, a particular form of higher-order reductions defined via definitional trees. A general completeness result is only provided for terminating rewrite systems due to the lack of an overall theory of higher-order reduction which is outside the scope of this paper.

We propose a new computation model which combines the operational principles of functional languages (reduction), logic languages (non-deterministic search for solutions), and integrated functional logic languages (residuation and narrowing). This computation model combines efficient evaluation principles of functional languages with the problem-solving capabilities of logic programming. Since the model allows the delay of function calls which are not sufficiently instantiated, it also supports a concurrent style of programming. We provide soundness and completeness results and show that known evaluation principles of functional logic languages are particular instances of this model. Thus, our model is a suitable basis for future declarative programming languages.

Narrowing is the operational principle of languages that integrate functional and logic programming. We propose a notion of a needed narrowing step that, for inductively sequential rewrite systems, extends the Huet and Le´vy notion of a needed reduction step. We define a strategy, based on this notion, that computes only needed narrowing steps. Our strategy is sound and complete for a large class of rewrite systems, is optimal w.r.t. the cost measure that counts the number of distinct steps of a derivation, computes only independent unifiers, and is efficiently implemented by pattern matching.