Fundamenta Informaticae - Volume 66, issue 4

Authors: Pettorossi, Alberto | Proietti, Maurizio

Article Type: Other

Citation: Fundamenta Informaticae, vol. 66, no. 4, pp. i-iii, 2005

Authors: Cunha, Alcino | Pinto, Jorge Sousa

Article Type: Research Article

Abstract: Functional programs are particularly well suited to formal manipulation by equational reasoning. In particular, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the introduction of accumulating parameters, can be implemented using calculation through the use of the fusion (or promotion) strategy. In this paper we revisit this transformation method, but, unlike most of the previous work on this subject, we adhere to a pure point-free calculus …that emphasizes the advantages of equational reasoning. We focus on the accumulation strategy initially proposed by Bird, where the transformed programs are seen as higher-order folds calculated systematically from a specification. The machinery of the calculus is expanded with higher-order point-free operators that simplify the calculations. A substantial number of examples (both classic and new) are fully developed, and we introduce several shortcut optimization rules that capture typical transformation patterns. Show more

Keywords: Functional Programming, Program Transformation, Program Calculation, Point-free Programming, Accumulation Strategy

Citation: Fundamenta Informaticae, vol. 66, no. 4, pp. 315-352, 2005

Authors: Gibbons, Jeremy | Hutton, Graham

Article Type: Research Article

Abstract: Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main methods for proving properties of corecursive programs: fixpoint induction, the approximation (or take) lemma, coinduction, and fusion.

Citation: Fundamenta Informaticae, vol. 66, no. 4, pp. 353-366, 2005

Authors: Glück, Robert | Kawabe, Masahiko

Article Type: Research Article

Abstract: We describe a method for automatic program inversion of first-order functional programs based on methods of LR(0) parsing. We formalize the transformation and illustrate it with several example programs. We approach one of the main problems of automatic program inversion - the elimination of nondeterminism - by viewing an inverse program as a context-free grammar. We apply LR-based parsing methods to turn a nondeterministic program into a deterministic program. This improves the efficiency of the inverse …programs and greatly expands the application range of our earlier method for program inversion. Show more

Keywords: program inversion, program transformation, LR parsing, functional programming

Citation: Fundamenta Informaticae, vol. 66, no. 4, pp. 367-395, 2005

Authors: Danvy, Olivier | Goldberg, Mayer

Article Type: Research Article

Abstract: We present a programming pattern where a recursive function defined over a data structure traverses another data structure at return time. The idea is that the recursive calls get us 'there' by traversing the first data structure and the returns get us 'back again' while traversing the second data structure. We name this programming pattern of traversing a data structure at call time and another data structure at return time "There And Back Again" (TABA). …The TABA pattern directly applies to computing symbolic convolutions and to multiplying polynomials. It also blends well with other programming patterns such as dynamic programming and traversing a list at double speed. We illustrate TABA and dynamic programming with Catalan numbers. We illustrate TABA and traversing a list at double speed with palindromes and we obtain a novel solution to this traditional exercise. Finally, through a variety of tree traversals, we show how to apply TABA to other data structures than lists. A TABA-based function written in direct style makes full use of an ALGOL-like control stack and needs no heap allocation. Conversely, in a TABA-based function written in continuation-passing style and recursively defined over a data structure (traversed at call time), the continuation acts as an iterator over a second data structure (traversed at return time). In general, the TABA pattern saves one from accumulating intermediate data structures at call time. Show more

Keywords: Recursive programming, continuations, defunctionalization, TABA

Citation: Fundamenta Informaticae, vol. 66, no. 4, pp. 397-413, 2005

Authors: Lisper, Bjórn

Article Type: Research Article

Abstract: We prove some new results about the correctness of transformations of nondeterministic programs. The reported work formalises the intuitive idea that two recursive programs ought to be equivalent, also in a nondeterministic setting, if they can be symbolically unfolded, through deterministic reductions, to the same, possibly infinite, term. In order to do this we develop two related semantics, based on computations modeled by reduction sequences, and argue that they are operationally meaningful. We then specialise …to the case of Combinatory Reduction Systems, which provides a suitable rewrite setting for higher order functional programs with nondeterministic constructs, e.g., stream or process primitives. In this setting we prove a theorem about equivalence of programs based on possibly infinite, deterministic unfoldings of programs converging to the same term. We then use the theorem to show a correctness criterion for unfold/fold-transformations of nondeterministic recursive programs. This criterion is similar to the well-known Tamaki-Sato correctness criterion for unfold/fold-transformations of logic programs. Show more

Citation: Fundamenta Informaticae, vol. 66, no. 4, pp. 415-439, 2005