Functional and Logic Programming

Frontmatter

Programming with Boolean Satisfaction

Abstract

In recent years, research on Boolean satisfiability (SAT) is generating remarkably powerful SAT solvers capable of handling larger and larger SAT instances. With the availability of progressively stronger SAT solvers, an accumulating number of applications have been developed which demonstrate that real world problems can often be solved by encoding them into SAT.

Tailgating the success of SAT technology are a variety of tools which can be applied to help specify and then compile problem instances to corresponding SAT instances. Typically, a constraint based modeling language is introduced and used to model instances. Then encoding techniques are applied to compile constraints to the language of an underlying solver such as SAT, SMT, or others.

In this talk I advocate the need for “optimizing compilers” for SAT encoding and present BEE (“Ben-Gurion University Equi-propagation Encoder”). Using BEE eases the encoding process and performs optimizations to simplify constraints prior to their encoding to CNF. I will describe these optimizations: equi-propagation, partial evaluation, and decomposition, and demonstrate their application. BEE is written in Prolog, and integrates directly with a SAT solver through a suitable Prolog interface, or else it outputs a DIMACS file.

Michael Codish

Automated Verification of Higher-Order Functional Programs

Abstract

Recently, motivated by the success of software model checkers for automated first-order program verification, researchers have proposed “model checkers” for automated verification of higher-order functional programs. Following the first-order methods, the higher-order verifiers employ a framework that separates control from data, allowing a smooth migration of tools and techniques such as predicate abstraction, CEGAR, SMT solving, and interpolation that have proven effective in first-order program verification. In this talk, we report on the state of the art in this emerging area of research, and discuss some future issues. In particular, we show that, in contrast to the automated methods for first-order programs, the current approaches lack relative completeness, and we present our ongoing research toward that end.

Tachio Terauchi

Dependently-Typed Programming in GHC

Abstract

Is Haskell a dependently-typed programming language?

The Glasgow Haskell Compiler (GHC) type-system extensions, such as Generalized Algebraic Datatypes (GADTs), multiparameter type classes and type families, give programmers the ability to encode domain-specific invariants in types. Clever functional programmers have used these features to enhance the reasoning capabilities of static type checking. But really, how far have we come?

In this talk, I will (attempt to) answer the question “Is it Dependent Types Yet?”, through examples, analysis and comparisons with modern full-spectrum dependently-typed languages, such as Agda and Coq. What sorts of dependently-typed programming can be done? What sorts of programming do these languages support that Haskell cannot? What should GHC learn from these languages, and conversely, what lessons can GHC offer in return?

Stephanie Weirich

Call-by-Value Solvability, Revisited

Abstract

In the call-by-value lambda-calculus solvable terms have been characterised by means of call-by-name reductions, which is disappointing and requires complex reasonings. We introduce the value-substitution lambda-calculus, a simple calculus borrowing ideas from Herbelin and Zimmerman’s call-by-value λ _CBV calculus and from Accattoli and Kesner’s substitution calculus λ _sub . In this new setting, we characterise solvable terms as those terms having normal form with respect to a suitable restriction of the rewriting relation.

Beniamino Accattoli, Luca Paolini

Compiling a Functional Logic Language: The Basic Scheme

Abstract

We present the design of a compiler for a functional logic programming language and discuss the compiler’s implementation. The source program is abstracted by a constructor based graph rewriting system obtained from a functional logic program after syntax desugaring, lambda lifting and similar transformations provided by a compiler’s front-end. This system is non-deterministic and requires a specialized normalization strategy. The target program consists of 3 procedures that execute graph replacements originating from either rewrite or pull-tab steps. These procedures are deterministic and easy to encode in an ordinary programming language. We describe the generation of the 3 procedures, discuss the correctness of our approach, highlight some key elements of an implementation, and benchmark the performance of a proof-of-concept. Our compilation scheme is elegant and simple enough to be presented in one page.

Sergio Antoy, Arthur Peters

Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts

Abstract

We systematically derive a classical call-by-need sequent calculus, which does not require an unbounded search for the standard redex, by using the unity of semantic artifacts proposed by Danvy et al. The calculus serves as an intermediate step toward the generation of an environment-based abstract machine. The resulting abstract machine is context-free, so that each step is parametric in all but one component. The context-free machine elegantly leads to an environment-based CPS transformation. This transformation is observationally different from a natural classical extension of the transformation of Okasaki et al., due to duplication of un-evaluated bindings.

Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin

Normal Form Bisimulations for Delimited-Control Operators

Abstract

We define a notion of normal form bisimilarity for the untyped call-by-value λ-calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.

Dariusz Biernacki, Sergueï Lenglet

Real-Time Persistent Queues and Deques with Logic Variables (Declarative Pearl)

Abstract

We present a Prolog implementation of real-time persistent queues and double-ended queues. Our implementation is inspired by Okasaki’s lazy-functional approach, but relies only on standard Prolog, comprising of the pure subset plus if-then-else constructs to efficiently implement guards and meta-calls for convenience. The resulting data structure is a nice demonstration of the fact that the use of logic variables to hold the outcome of an unfinished computation can sometimes give the same kind of elegant and compact solutions as lazy evaluation.

Gerlof Bouma

Declarative Debugging of Wrong and Missing Answers for SQL Views

Abstract

This paper presents a debugging technique for diagnosing errors in SQL views. The debugger allows the user to specify the error type, indicating if there is either a missing answer (a tuple was expected but it is not in the result) or a wrong answer (the result contains an unexpected tuple). This information is employed for slicing the associated queries, keeping only those parts that might be the cause of the error. The validity of the results produced by sliced queries is easier to determine, thus facilitating the location of the error. Although based on the ideas of declarative debugging, the proposed technique does not use computation trees explicitly. Instead, the logical relations among the nodes of the trees are represented by logical clauses that also contain the information extracted from the specific questions provided by the user. The atoms in the body of the clauses correspond to questions that the user must answer in order to detect an incorrect relation. The resulting logic program is executed by selecting at each step the unsolved atom that yields the simplest question, repeating the process until an erroneous relation is detected. Soundness and completeness results are provided. The theoretical ideas have been implemented in a working prototype included in the Datalog system DES.

Rafael Caballero, Yolanda García-Ruiz, Fernando Sáenz-Pérez

Improving the Performance of FD Constraint Solving in a CFLP System

Abstract

Constraint Functional Logic Programming (CFLP) integrates lazy narrowing with constraint solving. It provides a high modeling abstraction, but its solving performance can be penalized by lazy narrowing and solver interface surcharges. As for real-world problems most of the solving time is carried out by solver computations, the system performance can be improved by interfacing state-of-the-art external solvers with proven performance. In this work we depart from the CFLP system \(\mathcal{TOY(FD})\), implemented in SICStus Prolog and supporting Finite Domain (\(\mathcal{FD}\)) constraints by using its underlying Prolog \(\mathcal{FD}\) solver. We present a scheme describing how to interface an external CP(\(\mathcal{FD}\)) solver to \(\mathcal{TOY(FD})\), and easily adaptable to other Prolog CLP or CFLP systems. We prove the scheme to be generic enough by interfacing Gecode and ILOG solvers, and we analyze the new performance achieved.

Ignacio Castiñeiras, Fernando Sáenz-Pérez

A General Implementation Framework for Tabled CLP

Abstract

This paper describes a framework to combine tabling evaluation and constraint logic programming (TCLP). While this combination has been studied previously from a theoretical point of view and some implementations exist, they either suffer from a lack of efficiency, flexibility, or generality, or have inherent limitations with respect to the programs they can execute to completion (either with success or failure). Our framework addresses these issues directly, including the ability to check for answer / call entailment, which allows it to terminate in more cases than other approaches. The proposed framework is experimentally compared with existing solutions in order to provide evidence of the mentioned advantages.

Pablo Chico de Guzmán, Manuel Carro, Manuel V. Hermenegildo, Peter Stuckey

Extending the $\mathcal{TOY}$ System with the ECL i PS e Solver over Sets of Integers

Abstract

Starting from a computational model for the cooperation of constraint domains in the CFLP context (with lazy evaluation and higher-order functions), we present the theoretical basis for the coordination domain \(\mathcal{C}\) tailored to the cooperation of three pure domains: the domain of finite sets of integers (\(\mathcal{FS}\)), the finite domain of integers (\(\mathcal{FD}\)) and the Herbrand domain (\(\mathcal{H}\)). We also present the adaptation of the goal-solving calculus \(CCLNC{\mathcal C}\) (Cooperative Constraint Lazy Narrowing Calculus over \(\mathcal{C}\)) to this particular case, as well as soundness and limited completeness results. An implementation of this cooperation in the CFLP system \({\mathcal TOY}\) is presented. Our implementation is based on inter-process communication between \({\mathcal TOY}\) and the external solvers for sets of integers and finite domain of ECL ⁱ PS ^e .

Sonia Estévez-Martín, Jesús Correas Fernández, Fernando Sáenz-Pérez

Correct Looping Arrows from Cyclic Terms

Traced Categorical Interpretation in Haskell

Abstract

Arrows involving a loop operator provide an interesting programming methodology for looping computation. On the other hand, Haskell can define cyclic data structures by recursive definitions. This paper shows that there exists a common principle underlying both cyclic data and cyclic computations of arrow programs. We examine three concrete examples of constructing looping arrows from a syntactic structure called cyclic terms. Then we present a general pattern of constructing correct looping arrows, that is based on categorical semantics of loops and arrows, i.e. traced and Freyd categories.

Makoto Hamana

A Lambda Calculus for Gödel–Dummett Logic Capturing Waitfreedom

Abstract

We propose a typed lambda calculus based on Avron’s hypersequent calculus for Gödel–Dummett logic. This calculus turns out to model waitfree computation. Besides strong normalization and non-abortfullness, we give soundness and completeness of the calculus against the typed version of waitfree protocols. The calculus is not only proof theoretically interesting, but also valuable as a basis for distributed programming languages.

Yoichi Hirai

Iteratees

Abstract

Iteratee IO is a style of incremental input processing with precise resource control. The style encourages building input processors from a user-extensible set of primitives by chaining, layering, pairing and other modes of compositions. The programmer is still able, where needed, to precisely control look-ahead, the allocation of buffers, file descriptors and other resources. The style is especially suitable for processing of communication streams, large amount of data, and data undergone several levels of encoding such as pickling, compression, chunking, framing. It has been used for programming high-performance (HTTP) servers and web frameworks, in computational linguistics and financial trading.

We exposit programming with iteratees, contrasting them with Lazy IO and the Handle-based, |stdio|-like IO. We relate them to online parser combinators. We introduce a simple implementation as free monads, which lets us formally reason with iteratees. As an example, we validate several equational laws and use them to optimize iteratee programs. The simple implementation helps understand existing implementations of iteratees and derive new ones.

Oleg Kiselyov

Mutual Exclusion by Interpolation

Abstract

The question of what constraints must hold for a predicate to behave as a (partial) function, is key to understanding the behaviour of a logic program. It has been shown how this question can be answered by combining backward analysis, a form of analysis that propagates determinacy requirements against the control flow, with a component for deriving so-called mutual exclusion conditions. The latter infers conditions sufficient to ensure that if one clause yields an answer then another cannot. This paper addresses the challenge of how to compute these conditions by showing that this problem can be reformulated as that of vertex enumeration. Whilst directly applicable in logic programming, the method might well also find application in reasoning about type classes.

Jael Kriener, Andy King

Parallel Computation Skeletons with Premature Termination Property

Abstract

A parallel computation with early termination property is a special form of a parallel for loop. This paper devises a generic highlevel approach for such computation which is expressed as a scheme for algorithmic skeletons. We call this scheme map+reduce, in similarity with the map-reduce paradigm. The implementation is concise and relies heavily on laziness. Two case studies from computational number theory support our presentation.

Oleg Lobachev

Calculational Developments of New Parallel Algorithms for Size-Constrained Maximum-Sum Segment Problems

Abstract

Parallel algorithms for the one-dimensional and the two-dimensional size-constrained maximum-sum segment problems are proposed. The problem, which is a variant of the classic maximum-sum segment problem, is to locate the segment of the maximum total sum among those whose sizes are in a certain range, say, between l and u. It has several applications including pattern recognition, data mining, and DNA analyses, and the size requirement enables us to exclude trivial or useless results. Our parallel algorithms solve it in time O(n / n/p + log p) for one-dimensional arrays of length n and in time O(n ²(u–l) / p + log p) for n × n two-dimensional arrays on EREW PRAM that consists of p processors. It is worth noting that they achieve asymptotically optimal parallel speedups compared with the best known sequential algorithms that take O(n) and O(n ³) times for the one- and the two-dimensional cases, respectively. Our algorithms are correct by their construction: they are systematically derived from their specifications based on the Bird-Meertens formalism.

Akimasa Morihata

A Data Flow Language for Hybrid Query and Programming Languages

Abstract

In this paper, we present trix, which formalizes the data flow mechanisms used in low level descriptions of algorithms that implement data base as well as programming constructs. We show that the data flow formalism permits concise expression of physical data base operators and functional evaluation, and that the formalism permits unified reasoning about the equivalence of programs of each and all of these paradigms. Specifically, we present trix formally, illustrate how programming patterns (specifically queries) translate into trix, and use “data flow equivalence” equational reasoning to show some common optimizations correct. Finally we show how the use of trix as an intermediate language can improve performance for some standard benchmarks.

Kristoffer H. Rose, Lionel Villard, Naoto Sato

Coinductive Constraint Logic Programming

Abstract

Constraint logic programming (CLP) has been proposed as a declarative paradigm for merging constraint solving and logic programming. Recently, coinductive logic programming has been proposed as a powerful extension of logic programming for handling (rational) infinite objects and reasoning about their properties. Coinductive logic programming does not include constraints while CLP’s declarative semantics is given in terms of a least fixed-point (i.e., it is inductive) and cannot directly support reasoning about (rational) infinite objects and their properties. In this paper we combine constraint logic programming and coinduction to obtain co-constraint logic programming (co-CLP for brevity). We present the declarative semantics of co-CLP in terms of a greatest fixed-point and its operational semantics based on the coinductive hypothesis rule. We prove the equivalence of these two semantics for programs with rational terms.

Neda Saeedloei, Gopal Gupta

A Call-by-Name CPS Hierarchy

Abstract

The Continuation-Passing-Style (CPS) translation gives semantics to control operators such as exception and first-class continuations. By iterating this translation, Danvy and Filinski obtained a CPS hierarchy, and used it to specify a series of control operators, hierarchical (or layered) delimited-control operators.

We introduce a call-by-name variant of the CPS hierarchy. While most of the work on delimited-control operators is based on call-by-value calculi, call-by-name delimited-control operators are an active target of recent studies. Our strategy for developing such a hierarchy is to use the results for the call-by-value calculi as much as possible. The key tool is Hatcliff and Danvy’s factorization of Plotkin’s call-by-name CPS translation into a thunk translation and a call-by-value CPS translation. We show that a call-by-name CPS hierarchy can be obtained by naturally extending the factorization to the calculi with control operators, and then prove several properties for this hierarchy.

Asami Tanaka, Yukiyoshi Kameyama

Exact Flow Analysis by Higher-Order Model Checking

Abstract

We propose a novel control flow analysis for higher-order functional programs, based on a reduction to higher-order model checking. The distinguished features of our control flow analysis are that, unlike most of the control flow analyses like k-CFA, it is exact for simply-typed (λ)-calculus with recursion and finite base types, and that, unlike Mossin’s exact flow analysis, it is indeed runnable in practice, at least for small programs. Furthermore, under certain (arguably strong) assumptions, our control flow analysis runs in time cubic in the size of a program. We formalize the reduction of control flow analysis to higher-order model checking, prove the correctness, and report preliminary experiments.

Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi

Computing in Cantor’s Paradise with λ ZFC

Abstract

Applied mathematicians increasingly use computers to answer mathematical questions. We want to provide them domain-specific languages. The languages should have exact meanings and computational meanings. Some proof assistants can encode exact mathematics and extract programs, but formalizing the required theorems can take years.

As an alternative, we develop λ _ZFC, a lambda calculus that contains infinite sets as values, in which to express exact mathematics and gradually change infinite calculations to computable ones. We define it as a conservative extension of set theory, and prove that most contemporary theorems apply directly to λ _ZFC terms.

We demonstrate λ _ZFC’s expressiveness by coding up the real numbers, arithmetic and limits. We demonstrate that it makes deriving computational meaning easier by defining a monad in it for expressing limits, and using standard topological theorems to derive a computable replacement.

Neil Toronto, Jay McCarthy

The Finite Domain Constraint Solver of SWI-Prolog

Abstract

We present a new constraint solver over finite domains, freely available as library(clpfd) in SWI-Prolog. Our solver has several unique features, which we describe in this paper: Reasoning over arbitrarily large integers, always terminating propagation, and a domain-specific language that concisely expresses the full semantics of constraint reification. The library is entirely written in Prolog and can be easily ported to other Prolog systems that support attributed variables. The constraint solver is fast enough for teaching and research purposes and is already being used in courses at several universities in France, Germany, Italy, Austria and other countries.

Markus Triska

Explicit Binds: Effortless Efficiency with and without Trees

Abstract

We demonstrate a simple and robust program transformation technique that can improve asymptotic time complexity of data-manipulating programs (e.g., produce a linear-time list reversal function from the obvious quadratic one). In the version of the present paper, it applies to monadic inductive datatypes and can be stated in two flavors, through a datatype representation, with an explicit (“frozen”) bind constructor and a special associated defining clause for the fold function, and in a functional form (generalized Church numerals), with a special definition of the bind function in terms of the build constructor. The technique explicates, systematizes, combines and scales a number of ideas known from the literature, achieving a new level of generality.

Tarmo Uustalu

Backmatter