arXiv subjects

Finn Teegen

Publications and source records attributed to Finn Teegen.

8 recordsLinked to original sources

arXiv2026

A Monadic Implementation of Functional Logic Programs

Functional logic languages are a high-level approach to programming by combining the most important declarative features. They abstract from small-step operational details so that programmers can concentrate on the logical aspects of an application. This is supported by appropriate evaluation strategies. Demand-driven evaluation from functional programming is amalgamated with non-determinism from logic programming so that solutions or values are computed whenever they exist. This frees the programmer from considering the influence of an operational strategy on the success of a computation, but it is a challenge to the language implementer. A non-deterministic demand-driven strategy might duplicate unevaluated choices of an expression, which could duplicate the computational effort. In recent implementations, this problem has been tackled by adding a kind of memoization of non-deterministic choices to the expression under evaluation. Since this has been implemented in imperative target languages, it was unclear whether this could also be supported in a functional programming environment like Haskell. This paper presents a solution to this challenge by transforming functional logic programs into a monadic representation. Although this transformation is not new, we present an implementation of the monadic interface which supports memoization in non-deterministic branches. Additionally, we include more advanced features of functional logic languages, namely functional patterns and encapsulated search, in our approach. By optimizing our implementation for purely functional computations with both a static and dynamic approach, we are able to achieve a promising performance that outperforms current compilers for Curry.

cs.PL↗

arXiv2020

Research Summary on Implementing Functional Patterns by Synthesizing Inverse Functions

In this research summary we present our recent work on implementing functional patterns with inverse functions in the lazy functional-logic programming language Curry. Our goal is the synthesis of the inverse of any given function in Curry itself. The setting of a functional-logic language especially allows the inversion of non-injective functions. In general, inverse computation is a non-trivial problem in lazy programming languages due to their non-strict semantics. We are so far able to directly derive the inverse function for a limited class of functions, namely those consisting of rules that do not involve both extra variables and non-linear right-hand sides. Because the synthesized definitions are based on standard code, known optimizations techniques can be applied to them. For all other functions we can still provide an inverse function by using non-strict unification.

cs.PL↗

arXiv2020

Memoized Pull-Tabbing for Functional Logic Programming

Pull-tabbing is an evaluation technique for functional logic programs which computes all non-deterministic results in a single graph structure. Pull-tab steps are local graph transformations to move non-deterministic choices towards the root of an expression. Pull-tabbing is independent of a search strategy so that different strategies (depth-first, breadth-first, parallel) can be used to extract the results of a computation. It has been used to compile functional logic languages into imperative or purely functional target languages. Pull-tab steps might duplicate choices in case of shared subexpressions. This could result in a dramatic increase of execution time compared to a backtracking implementation. In this paper we propose a refinement which avoids this efficiency problem while keeping all the good properties of pull-tabbing. We evaluate a first implementation of this improved technique in the Julia programming language.

cs.PL↗

arXiv2019

Adding Data to Curry

Functional logic languages can solve equations over user-defined data and functions. Thus, the definition of an appropriate meaning of equality has a long history in these languages, ranging from reflexive equality in early equational logic languages to strict equality in contemporary functional logic languages like Curry. With the introduction of type classes, where the equality operation "==" is overloaded and user-defined, the meaning became more complex. Moreover, logic variables appearing in equations require a different typing than pattern variables, since the latter might be instantiated with functional values or non-terminating operations. In this paper, we present a solution to these problems by introducing a new type class "Data" which is associated with specific algebraic data types, logic variables, and strict equality. We discuss the ideas of this class and its implications on various concepts of Curry, like unification, functional patterns, and program optimization.

cs.PL↗

arXiv2019

Structured Traversal of Search Trees in Constraint-logic Object-oriented Programming

In this paper, we propose an explicit, non-strict representation of search trees in constraint-logic object-oriented programming. Our search tree representation includes both the non-deterministic and deterministic behaviour during execution of an application. Introducing such a representation facilitates the use of various search strategies. In order to demonstrate the applicability of our approach, we incorporate explicit search trees into the virtual machine of the constraint-logic object-oriented programming language Muli. We then exemplarily implement three search algorithms that traverse the search tree on-demand: depth-first search, breadth-first search, and iterative deepening depth-first search. In particular, the last two strategies allow for a complete search, which is novel in constraint-logic object-oriented programming and highlights our main contribution. Finally, we compare the implemented strategies using several benchmarks.

cs.PL↗

arXiv2019

Implementing a Library for Probabilistic Programming using Non-strict Non-determinism

This paper presents PFLP, a library for probabilistic programming in the functional logic programming language Curry. It demonstrates how the concepts of a functional logic programming language support the implementation of a library for probabilistic programming. In fact, the paradigms of functional logic and probabilistic programming are closely connected. That is, language characteristics from one area exist in the other and vice versa. For example, the concepts of non-deterministic choice and call-time choice as known from functional logic programming are related to and coincide with stochastic memoization and probabilistic choice in probabilistic programming, respectively. We will further see that an implementation based on the concepts of functional logic programming can have benefits with respect to performance compared to a standard list-based implementation and can even compete with full-blown probabilistic programming languages, which we illustrate by several benchmarks. Under consideration in Theory and Practice of Logic Programming (TPLP).

cs.PL↗

arXiv2019

One Monad to Prove Them All

One Monad to Prove Them All is a modern fairy tale about curiosity and perseverance, two important properties of a successful PhD student. We follow the PhD student Mona on her adventure of proving properties about Haskell programs in the proof assistant Coq. On the one hand, as a PhD student in computer science Mona observes an increasing demand for correct software products. In particular, because of the large amount of existing software, verifying existing software products becomes more important. Verifying programs in the functional programming language Haskell is no exception. On the other hand, Mona is delighted to see that communities in the area of theorem proving are becoming popular. Thus, Mona sets out to learn more about the interactive theorem prover Coq and verifying Haskell programs in Coq. To prove properties about a Haskell function in Coq, Mona has to translate the function into Coq code. As Coq programs have to be total and Haskell programs are often not, Mona has to model partiality explicitly in Coq. In her quest for a solution Mona finds an ancient manuscript that explains how properties about Haskell functions can be proven in the proof assistant Agda by translating Haskell programs into monadic Agda programs. By instantiating the monadic program with a concrete monad instance the proof can be performed in either a total or a partial setting. Mona discovers that the proposed transformation does not work in Coq due to a restriction in the termination checker. In fact the transformation does not work in Agda anymore as well, as the termination checker in Agda has been improved. We follow Mona on an educational journey through the land of functional programming where she learns about concepts like free monads and containers as well as basics and restrictions of proof assistants like Coq. These concepts are well-known individually, but their interplay gives rise to a solution for Mona's problem based on the originally proposed monadic tranformation that has not been presented before. When Mona starts to test her approach by proving a statement about simple Haskell functions, she realizes that her approach has an additional advantage over the original idea in Agda. Mona's final solution not only works for a specific monad instance but even allows her to prove monad-generic properties. Instead of proving properties over and over again for specific monad instances she is able to prove properties that hold for all monads representable by a container-based instance of the free monad. In order to strengthen her confidence in the practicability of her approach, Mona evaluates her approach in a case study that compares two implementations for queues. In order to share the results with other functional programmers the fairy tale is available as a literate Coq file. If you are a citizen of the land of functional programming or are at least familiar with its customs, had a journey that involved reasoning about functional programs of your own, or are just a curious soul looking for the next story about monads and proofs, then this tale is for you.

cs.PL↗

arXiv2018

Synthesizing Set Functions

Set functions are a feature of functional logic programming to encapsulate all results of a non-deterministic computation in a single data structure. Given a function $f$ of a functional logic program written in Curry, we describe a technique to synthesize the definition of the set function of $f$. The definition produced by our technique is based on standard Curry constructs. Our approach is interesting for three reasons. It allows reasoning about set functions, it offers an implementation of set functions which can be added to any Curry system, and it has the potential of changing our thinking about the implementation of non-determinism, a notoriously difficult problem.

cs.PL↗