Fundamenta Informaticae - Volume 69, issue 1-2

Authors: Pettorossi, Alberto | Proietti, Maurizio

Article Type: Other

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. v-vii, 2006

Authors: Chin, Wei-Ngan | Khoo, Siau-Cheng | Jones, Neil

Article Type: Research Article

Abstract: Redundant call elimination has been an important program optimisation process as it can produce super-linear speedup in optimised programs. In this paper, we investigate use of the tupling transformation in achieving this optimisation over a first-order functional language. Standard tupling technique, as described in [6], works excellently in a restricted variant of the language; namely, functions with single recursion argument. We provide a semantic understanding of call redundancy, upon which we construct an …analysis for handling the tupling of functions with multiple recursion arguments. The analysis provides a means to ensure termination of the tupling transformation. As the analysis is of polynomial complexity, it makes the tupling suitable as a step in compiler optimisation. Show more

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. 1-37, 2006

Authors: Hamilton, Geoff W.

Article Type: Research Article

Abstract: Deforestation is a well known transformation algorithmwhich can eliminate intermediate structures from functional programs. In previous work, we have shown how the deforestation algorithm can be extended to handle higher order programs. A higher order treeless form of expression was defined to ensure the termination of this algorithm. Our higher order algorithm was further extended by Seidl and Sørensen, and this extension was shown to remove some intermediate structures not removed by our algorithm (although our …original algorithm can also remove some intermedi-ate structures not removed by their technique). In this paper, we show how our original definition of higher order treeless form can be extended to allow the intermediate structures in the examples given by Seidl and Sørensen to be removed. We argue that, because our extended algorithm uses an easy to recognise treeless form, there is more transparency for the programmer in terms of the improvements which will be made. We prove that our new algorithm terminates, and we conjecture that it ensures that there is no efficiency loss, which we argue is essential for any optimisation. Show more

Keywords: deforestation, transformation, termination, efficiency

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. 39-61, 2006

Authors: Johann, Patricia | Voigtländer, Janis

Article Type: Research Article

Abstract: Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, standard parametricity results – including so-called free theorems – fail for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq. A folk theorem maintains that such results hold for a subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints …and algebraic datatypes even when seq is present provided the relations which appear in their derivations are required to be bottom-reflecting and admissible. In this paper we show that this folklore is incorrect, but that parametricity results can be recovered in the presence of seq by restricting attention to left-closed, total, and admissible relations instead. The key novelty of our approach is the asymmetry introduced by left-closedness, which leads to "inequational" versions of standard parametricity results together with preconditions guaranteeing their validity even when seq is present. We use these results to derive criteria ensuring that both equational and inequational versions of short cut fusion and related program transformations based on free theorems hold in the presence of seq Show more

Keywords: Haskell, control primitives, correctness proofs, denotational semantics, functional programming languages, logical relations, mixing strict and nonstrict evaluation, parametricity, polymorphism, program transformations, rank-2 types, short cut fusion, theorems for free

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. 63-102, 2006

Authors: Chen, Chiyan | Shi, Rui | Xi, Hongwei

Article Type: Research Article

Abstract: The notion of program transformation is ubiquitous in programming language studies on interpreters, compilers, partial evaluators, etc. In order to implement a program transformation, we need to choose a representation in the meta language, that is, the programming language in which we construct programs, for representing object programs, that is, the programs in the object language on which the program transformation is to be performed. In practice, most representations chosen for typed object programs are typeless …in the sense that the type of an object program cannot be reflected in the type of its representation. This is unsatisfactory as such typeless representations make it impossible to capture in the type system of the meta language various invariants in a program transformation that are related to the types of object programs. In this paper, we propose an approach to implementing program transformations that makes use of a first-order typeful program representation, where the type of an object program as well as the types of the free variables in the object program can be reflected in the type of the representation of the object program. We introduce some programming techniques needed to handle this typeful program representation, and then present an implementation of a CPS transform function where the relation between the type of an object program and that of its CPS transform is captured in the type system of DML. In a broader context, we claim to have taken a solid step along the line of research on constructing certifying compilers. Show more

Keywords: Typeful Program Transformation, Dependent Types, Applied Type System, ATS, Continuation Passing Style, CPS, Closure Conversion

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. 103-121, 2006

Authors: Bravenboer, Martin | van Dam, Arthur | Olmos, Karina | Visser, Eelco

Article Type: Research Article

Abstract: The applicability of term rewriting to program transformation is limited by the lack of control over rule application and by the context-free nature of rewrite rules. The first problem is addressed by languages supporting user-definable rewriting strategies. The second problem is addressed by the extension of rewriting strategies with scoped dynamic rewrite rules. Dynamic rules are defined at run-time and can access variables available from their definition context. Rules defined within a rule scope are automatically …retracted at the end of that scope. In this paper, we explore the design space of dynamic rules, and their application to transformation problems. The technique is formally defined by extending the operational semantics underlying the program transformation language Stratego, and illustrated by means of several program transformations in Stratego, including constant propagation, bound variable renaming, dead code elimination, function inlining, and function specialization. Show more

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. 123-178, 2006

Authors: King, Andy | Martin, Jonathan C.

Article Type: Research Article

Abstract: The objective of control generation in logic programming is to derive a computation rule for a program that is efficient and yet does not compromise programcorrectness. Progress in solving this fundamental problem in logic programming has been slow and, to date, only partial solutions have been proposed. Previously proposed schemes are either inefficient, incomplete (incorrect) or difficult to apply for programs consisting of many components (the scheme is not modular). This paper shows how the control …generation problem can be tackled by program transformation. The transformation relies on information about the depths of derivations to derive delay declarations which orchestrate the control. To prove correctness of the transformation, the notion of semi-delay recurrency is introduced, which generalises previous ideas in the termination literature for reasoning about logic programs with delay declarations. In contrast to previous work, semi-delay recurrency does not require an atom to be completely resolved before another is selected for reduction. This enhancement permits the transformation to introduce control which is flexible and relatively efficient. Show more

Keywords: logic programming, program transformation, control generation

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. 179-218, 2006

Authors: Rosenblueth, David A.

Article Type: Research Article

Abstract: A program-transformation system is determined by a repertoire of correctness-preserving rules, such as folding and unfolding. Normally, we would like the folding rule to be in some sense the inverse of the unfolding rule. Typically, however, the folding rule of logic program transformation systems is an inverse of a limited kind of unfolding. In many cases this limited kind of folding suffices. We argue, nevertheless, that it is both important and possible to extend such a …folding so as to be able to fold the clauses resulting from any unfolding of a positive literal. This extended folding rule allows us to derive some programs underivable by the existing version of this rule alone. In addition, our folding rule has applications to decompilation and reengineering, where we are interested in obtaining high-level program constructs from low-level program constructs. Moreover, we establish a connection between logic program transformation and inductive logic programming. This connection stems fromviewing our folding rule as a common extension of the existing multipleclause folding rule, on the one hand, and an operator devised in inductive logic programming, called "intra-construction",on the other hand. Hence, our folding rule can be regarded as a step towards incorporating inductive inference into logic program transformation. We prove correctness with respect to Dung and Kanchanasut's semantic kernel. Show more

Keywords: Logic program transformation, folding rule, most specific generalization, semantic kernel, decompilation, inductive logic programming

Citation: Fundamenta Informaticae, vol. 69, no. 1-2, pp. 219-249, 2006