Synthesizing recursive functional programs over algebraic data types from input-output examples remains challenging, largely due to the explosion of structurally distinct candidates during search. We present a synthesis approach for structurally recursive list/tree transformations based on a structure-element separation viewpoint: a structure transformation that determines output shape, and element computations that determine the values placed into that shape. Our method first infers structural relationships from examples that describe per-step output-size evolution along recursive calls and uses them to prune partial programs during top-down enumeration. For candidates that are structurally feasible, we apply a diamond function that converts the remaining element-level holes into small local program-by-example subproblems, which are then solved using symbolic execution and output alignment, enabling early acceptance or rejection without expanding unrelated global constructs. We implement the approach in an OCaml prototype synthesizer and evaluate it on a suite of list and tree benchmarks drawn from prior work. The results show that our method substantially reduces expensive example checking and improves synthesis performance on recursive list/tree transformation programs.

This paper studies a parsing method for strings containing placeholders, each of which may be later replaced by a string derived from the corresponding nonterminal symbol. Such a method potentially applies to parallel/distributed parsing, parsing for templates, modular syntax definitions, and so on. This paper investigates whether the introduction of the placeholder preserves the class of the grammar and proves the following two facts. First, the class of LR( k )grammars is preserved if k ≥ 1 and every nonterminal derives at least one nonempty string; hence, we can apply the standard LR parsing algorithm for parsing strings with placeholders. Second, the class of LR(0) is not. These results extend the preceding study for the LL(1) grammars.

Abstract The vertex-centric programming model is now widely used for processing large graphs. User-defined vertex programs are executed in parallel over every vertex of a graph, but the imperative and explicit message-passing style of existing systems makes defining a vertex program unintuitive and difficult. This article presents Fregel, a purely functional domain-specific language for processing large graphs and describes its model, design, and implementation. Fregel is a subset of Haskell, so Haskell tools can be used to test and debug Fregel programs. The vertex-centric computation is abstracted using compositional programming that uses second-order functions on graphs provided by Fregel. A Fregel program can be compiled into imperative programs for use in the Giraph and Pregel+ vertex-centric frameworks. Fregel’s functional nature without side effects enables various transformations and optimizations during the compilation process. Thus, the programmer is freed from the burden of program optimization, which is manually done for existing imperative systems. Experimental results for typical examples demonstrated that the compiled code can be executed with reasonable and promising performance.

Parallel reduction, which summarizes a given dataset, e.g., the total, average, and maximum, plays a crucial role in parallel programming. This paper presents a new approach, reverse engineering, to automatically discovering nontrivial parallel reductions in sequential programs. The body of the sequential reduction loop is regarded as a black box, and its input-output behaviors are sampled. If the behaviors correspond to a set of linear polynomials over a semiring, a divide-and-conquer parallel reduction is generated. Auxiliary reverse-engineering methods enable a long and nested loop body to be decomposed, which makes our parallelization scheme applicable to various types of reduction loops. This approach is not only simple and efficient but also agnostic to the details of the input program. Its potential is demonstrated through several use case scenarios. A proof-of-concept implementation successfully inferred linear polynomials for nearly all of the 74 benchmarks exhaustively collected from the literature. These characteristics and experimental results demonstrate the promise of the proposed approach, despite its inherent unsoundness.

Abstract Parallel reduction is a major component of parallel programming and widely used for summarisation and aggregation. It is not well understood, however, what sorts of non-trivial summarisations can be implemented as parallel reductions. This paper develops a calculus named λ AS , a simply typed lambda calculus with algebraic simplification. This calculus provides a foundation for studying a parallelisation of complex reductions by equational reasoning. Its key feature is δ abstraction. A δ abstraction is observationally equivalent to the standard λ abstraction, but its body is simplified before the arrival of its arguments using algebraic properties such as associativity and commutativity. In addition, the type system of λ AS guarantees that simplifications due to δ abstractions do not lead to serious overheads. The usefulness of λ AS is demonstrated on examples of developing complex parallel reductions, including those containing more than one reduction operator, loops with conditional jumps, prefix sum patterns and even tree manipulations.

Parallel reduction is a major component of parallel programming and widely used for summarization and aggregation. It is not well understood, however, what sorts of nontrivial summarizations can be implemented as parallel reductions. This paper develops a calculus named λ as , a simply typed lambda calculus with algebraic simplification. This calculus provides a foundation for studying parallelization of complex reductions by equational reasoning. Its key feature is δ abstraction. A δ abstraction is observationally equivalent to the standard λ abstraction, but its body is simplified before the arrival of its arguments by using algebraic properties such as associativity and commutativity. In addition, the type system of λ as guarantees that simplifications due to δ abstractions do not lead to serious overheads. The usefulness of λ as is demonstrated on examples of developing complex parallel reductions, including those containing more than one reduction operator, loops with jumps, prefix-sum patterns, and even tree manipulations.

The vertex-centric programming model, known as “think like a vertex”, is being used more and more to support various big graph processing methods through iterative supersteps that execute in parallel a user-defined vertex program over each vertex of a graph. However, the imperative and message-passing style of existing systems makes defining a vertex program unintuitive. In this paper, we show that one can benefit more from “Thinking like a vertex” by “Behaving like a function” rather than “Acting like a procedure” with full use of side effects and explicit control of message passing, state, and termination. We propose a functional approach to vertex-centric graph processing in which the computation at every vertex is abstracted as a higher-order function and present Fregel, a new domain-specific language. Fregel has clear functional semantics, supports declarative description of vertex computation, and can be automatically translated into Pregel, an emerging imperative-style distributed graph processing framework, and thereby achieve promising performance. Experimental results for several typical examples show the promise of this functional approach.

The third list-homomorphism theorem states that if a function is both foldr and foldl, it has a divide-and-conquer parallel implementation as well. In this paper, we develop a theory for obtaining such parallelization theorems. The key is a new proof of the third list-homomorphism theorem based on shortcut deforestation. The proof implies that there exists a divide-and-conquer parallel program of the form of h(x 'merge' y) = h1 x odot h2 y, where h is the subject of parallelization, merge is the operation of integrating independent substructures, h1 and h2 are computations applied to substructures, possibly in parallel, and odot merges the results calculated for substructures, if (i) h can be specified by two certain forms of iterative programs, and (ii) merge can be implemented by a function of a certain polymorphic type. Therefore, when requirement (ii) is fulfilled, h has a divide-and-conquer implementation if h has two certain forms of implementations. We show that our approach is applicable to structure-consuming operations by catamorphisms (folds), structure-generating operations by anamorphisms (unfolds), and their generalizations called hylomorphisms.

Abstract Functional languages are suitable for transformational developments of programs. However, accumulative functions, or in particular tail-recursive functions, are known to be less suitable for manipulation. In this paper, we propose a program transformation named “IO swapping” that swaps call-time and return-time computations. It moves computations in accumulative parameters to results and thereby enables interesting transformations. We demonstrate effectiveness of IO swapping by several applications: deforestation, higher order removal, program inversion, and manipulation of circular programs.

Divide-and-conquer is an important technique in parallel programming. However, algebraic data structures do not fit divide-and-conquer parallelism. For example, the usual pointer-based implementation of lists cannot efficiently be divided at their middle, which prevents us from developing list-iterating divide-and-conquer parallel programs. Tree-iterating programs possibly face a similar problem, because trees might be ill-balanced and list-like shapes. This paper examines parallel programming based on balanced trees: we consider balanced-tree structures and develop recursive functions on them. By virtue of their balancing nature, either bottom-up or top-down recursive functions exploit divide-and-conquer parallelism. Our main contribution is to demonstrate the promise of this approach. We propose a way of systematically developing balanced trees from parallel algorithms, and then, we show that efficient parallel programs on them can be developed by equational reasoning powered by Reynolds' relational parametricity. We consider functions that operate either lists or binary trees, and show that our methods can uniformly deal with both cases. The developed parallel programs are purely functional, correct by construction, and sometimes even simpler than known algorithms.

The third list-homomorphism theorem says that a function is a list homomorphism if it can be described as an instance of both a foldr and a foldl. We prove a dual theorem for unfolds and generalise both theorems to trees: if a function generating a list can be described both as an unfoldr and an unfoldl, the list can be generated from the middle, and a function that processes or builds a tree both upwards and downwards may independently process/build a subtree and its one-hole context. The point-free, relational formalism helps to reveal the beautiful symmetry hidden in the theorem.

Parallel programs on lists have been intensively studied. It is well known that associativity provides a good characterization for divide-and-conquer parallel programs. In particular, the third homomorphism theorem is not only useful for systematic development of parallel programs on lists, but it is also suitable for automatic parallelization. The theorem states that if two sequential programs iterate the same list leftward and rightward, respectively, and compute the same value, then there exists a divide-and-conquer parallel program that computes the same value as the sequential programs.While there have been many studies on lists, few have been done for characterizing and developing of parallel programs on trees. Naive divide-and-conquer programs, which divide a tree at the root and compute independent subtrees in parallel, take time that is proportional to the height of the input tree and have poor scalability with respect to the number of processors when the input tree is ill-balanced.In this paper, we develop a method for systematically constructing scalable divide-and-conquer parallel programs on trees, in which two sequential programs lead to a scalable divide-andconquer parallel program. We focus on paths instead of trees so as to utilize rich results on lists and demonstrate that associativity provides good characterization for scalable divide-and-conquer parallel programs on trees. Moreover, we generalize the third homomorphism theorem from lists to trees.We demonstrate the effectiveness of our method with various examples. Our results, being generalizations of known results for lists, are generic in the sense that they work well for all polynomial data structures.

Divide-and-conquer algorithms are suitable for modern parallel machines, tending to have large amounts of inherent parallelism and working well with caches and deep memory hierarchies. Among others, list homomorphisms are a class of recursive functions on lists, which match very well with the divide-and-conquer paradigm. However, direct programming with list homomorphisms is a challenge for many programmers. In this paper, we propose and implement a novel systemthat can automatically derive cost-optimal list homomorphisms from a pair of sequential programs, based on the third homomorphism theorem. Our idea is to reduce extraction of list homomorphisms to derivation of weak right inverses. We show that a weak right inverse always exists and can be automatically generated from a wide class of sequential programs. We demonstrate our system with several nontrivial examples, including the maximum prefix sum problem, the prefix sum computation, the maximum segment sum problem, and the line-of-sight problem. The experimental results show practical efficiency of our automatic parallelization algorithm and good speedups of the generated parallel programs.