Search

Consider the puzzle: given a number, remove $k$ digits such that the resulting number is as large as possible. Various techniques were employed to derive a linear-time solution to the puzzle: predicate logic was used to justify the structure of a greedy algorithm, a dependently-typed proof assistant was used to give a constructive proof of the greedy condition, and equational reasoning was used to calculate the greedy step as well as the final, linear-time optimisation.

As part of the author's studies on equational reasoning for monadic programs, this report focus on non-determinism monad. We discuss what properties this monad should satisfy, what additional operators and notations can be introduced to facilitate equational reasoning about non-determinism, and put them to the test by proving a number of properties in our example problem inspired by the author's previous work on proving properties of Spark aggregation.

Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively less attention has been paid to reasoning about monadic programs. In this report we derive a backtracking algorithm for problem specifications that use a monadic unfold to generate possible solutions, which are filtered using a $\mathit{scanl}$-like predicate. We develop theorems that convert a variation of $\mathit{scanl}$ to a $\mathit{foldr}$ that uses the state monad, as well as theorems constructing hylomorphism. The algorithm is used to solve the $n$-queens puzzle, our running example. The aim is to develop theorems and patterns useful for the derivation of monadic programs, focusing on the intricate interaction between state and non-determinism.

Given a string of parentheses, the task is to find the longest consecutive segment that is balanced, in linear time. We find this problem interesting because it involves a combination of techniques: the usual approach for solving segment problems, and a theorem for constructing the inverse of a function -- through which we derive an instance of shift-reduce parsing.

Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregation. Since execution of parallel aggregation in Spark is inherently non-deterministic, a natural requirement for Spark programs is to give the same result for any execution on the same data set. We present PureSpark, an executable formal Haskell specification for Spark aggregate combinators. Our specification allows us to deduce the precise condition for deterministic outcomes from Spark aggregation. We report case studies analyzing deterministic outcomes and correctness of Spark programs., an extended version of a paper accepted at NETYS'17

"Technical Report No. TR-IIS-10-009", Problem statements often resort to superlatives such as in eg. “. . . the smallest such number”, “. . . the best approximation”, “. . . the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part). This paper introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution being sought. The framework encompasses re-factoring of results previously developed by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with.

In a lazy functional language, the standard encoding of recursion in DSLs uses the host language's recursion, so that DSL algorithms automatically use the host language's least fixpoints, even though many domains require algorithms to produce different fixpoints. In particular, this is the case for DSLs implemented as Applicative functors (structures with a notion of pure computations and function application).We propose a recursion primitive afix that models a recursive binder in a finally tagless HOAS encoding, but with a novel rank-2 type that allows us to specify and exploit the effectsvalues separation that characterises Applicative DSLs. Unlike related approaches for Monads and Arrows, we model effectful recursion, not value recursion. Using generic programming techniques, we define an aritygeneric version of the operator to model mutually recursive definitions. We recover intuitive user syntax with a form of shallow syntactic sugar: an alet construct that syntactically resembles the let construct, which we have implemented in the GHC Haskell compiler. We describe a proposed axiom for the afix operator. We demonstrate usefulness with examples from Applicative parser combinators and functional reactive programming. We show how higher-order recursive operators like many can be encoded without special library support, unlike previous approaches, and we demonstrate an implementation of the left recursion removal transform. Copyright © 2013 ACM. ispartof: pages:97-106 ispartof: PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013 pages:97-106 ispartof: Partial Evaluation and Program Manipulation (PEPM 2013) location:Rome, Italy date:21 Jan - 22 Jan 2013 status: published