D. Sands. Proving the Correctness of Recursion-Based Automatic Program Transformations. In P. Mosses, M. Nielsen, and M. Schwartzbach, editors, Sixth International Joint Conference on Theory and Practice of Software Development (TAPSOFT), LNCS 915, pages 681--695. Springer-Verlag, 1995.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....profiling heap space is much more complicated than those for time and stack space. In the rest of this section I review other proof methods to show safety of program transformations with respect to performance. David Sands studied time safety of transformations for call by name languages [16, 15]. In his study he extended applicative bisimulation and its context lemma to account execution time. Applicative bisimulation with the context lemma greatly simplifies safety proofs of many program transformations. As with the method of logical relations, it will be di#cult to extend this method ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science, 167(1&2):193--233, 1996.

....and static program monitoring. 1. INTRODUCTION A program transformation is a meaning preserving mapping de ned on a programming language [21] The program transformation methodology provides thinking tools for the development of programs from speci cations (such as the fold unfold transformation [24]) and program veri cation (such as temporal veri cation [9] The program transformation techniques provide mechanical tools for program optimization (such as cache optimization [12] call by name to call by value transformation [26] constant propagation [18] continuation passing style ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoret. Comput. Sci., 167(12):193233, 1996.

....role of such specifications in their work on the correctness of binding time analysis. Specializers have mostly been specified as symbolic interpreters in functional style [42] We note, however, a recent trend (including the present work) to use operational semantics for specifying specializers [1, 18, 33, 61, 62]. In fact, the first author has shown that by emphasizing the logical character of type based and operational semantics specifications, the correctness of a partial evaluator can be mechanically verified [35] Davies and Pfenning have developed a language for expressing staged computation based ....

David Sands. Proving the correctness of recursion-based automatic program transformations. In Peter Mosses, Mogens Nielsen, and Michael Schwartzbach, editors, Proceedings of TAPSOFT '95, number 915 in Lecture Notes in Computer Science, pages 681--695, Aarhus, Denmark, May 1995. 66

....new right hand sides are folded using existing equations in the program. The unfold fold rules can be deceptive; their application preserves the partial correctness of a program, but their use must be closely controlled in order to ensure the operational equivalence of the transformed program [San95b, San95c] Folding can alter the recursive structure of a program. Applying the folding step carelessly may result in a loss of termination in the resulting program; for example, consider folding the equation F (x) 42 to F (x) F (x) Restrictions for the application of the transformation rules ....

D. Sands. Proving the Correctness of Recursion-Based Automatic Program Transformations. In P. Mosses, M. Nielsen, and M. Schwartzbach, editors, Sixth International Joint Conference on Theory and Practice of Software Development (TAPSOFT), LNCS 915, pages 681--695. Springer-Verlag, 1995. BIBLIOGRAPHY 228

....basic deforestation algorithm to enable this partial evaluation style optimisation to take place. Sands provides some insight into proving the semantic correctness of unfold fold style transformations, and uses his method to prove that a higher order variant of deforestation is correct [San95b, San95a] 1.4.2 foldr build Deforestation Gill, Launchbury and Peyton Jones [GLJ93, Gil95] take an entirely different approach to deforestation. The motivation of their approach is to achieve deforestation through a minimum of effort, sacrificing some generality along the way. The technique is based ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. In P. Mosses, M. Nielsen, and M. Schwartzbach, editors, Sixth International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 915 of Lecture Notes in Computer Science, pages 681--695. Springer-Verlag, 1995.

....transformations additionally preserve or improve program performance. One program improves another if, for every binding of variables, it evaluates to the same answer in fewer steps. Sands has initiated a formal study of improvement for source to source transformation of sequential programs [30,29]. In this paper we study improvement for source to target transformation of parallel programs. Our source language is equipped with a natural parallel semantics, including a cost model, but lacks a direct parallel implementation. Our target is (almost) a subset of the source language that is ....

....# # #) is given by a costing function C, which is determined by the syntax of a term. We have: s # D t # # # w d implies s # D # t # #w d s # D t # w d implies s # D #C(s#D)t # # # #C(s#D)w d Our proof technique is similar to Sands use of the tick algebra [29]. We introduce ticks in the costed semantics in order to account for the costs introduced later by the transformations. There are differences, however; for example, our ticks depend on the nesting depth of iterators and conditionals. Unfortunately, a detailed discussion is beyond the scope of ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science, 167(10), Oct. 1996.

....equivalent to the input. That each step of the transformation rules for deforestation preserves call by need semantics is easily proved, but extending rigorously the proof to account for folding is more involved. A general technique due to Sands [41, 43] can be used to prove this for deforestation [40, 42]. As for non degradation in efficiency, the output of deforestation should be at least as efficient as the input. First, there is the problem of avoiding duplication of computation. Transformation can change a polynomial time program into an exponential time program. In Wadler s [55] Hamilton s ....

D. Sands. Proving the correctness of recursionbased automatic program transformations. Theoretical Computer Science, A(167), 1996.

....equivalent to the input. That each step of the transformation rules for deforestation preserves call by need semantics is easily proved, but extending rigorously the proof to account for folding is more involved. A general technique due to Sands [41, 43] can be used to prove this for deforestation [40, 42]. As for non degradation in efficiency, the output of deforestation should be at least as efficient as the input. First, there is the problem of avoiding duplication of computation. Transformation can change a polynomial time program into an exponential time program. In Wadler s [55] Hamilton s ....

D. Sands. Proving the correctness of recursionbased automatic program transformation. In P. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 681--695. Springer-Verlag, 1995.

....transformations additionally preserve or improve program performance. One program improves another if, for every binding of variables, it evaluates to the same answer in fewer steps. Sands has initiated a formal study of improvement for source to source transformation of sequential programs [30,29]. In this paper we study improvement for source to target transformation of parallel programs. Our source language is equipped with a natural parallel semantics, including a cost model, but lacks a direct parallel implementation. Our target is (almost) a subset of the source language that is ....

....costed evaluation (denoted 7 7 ) is given by a costing function C, which is determined by the syntax of a term. We have: s D t 7 7 w d implies s D 6 t 6w d s D t w d implies s D 6C(s D) t 7 7 6C(s D) w d Our proof technique is similar to Sands use of the tick algebra [29]. We introduce ticks in the costed semantics in order to account for the costs introduced later by the transformations. There are differences, however; for example, our ticks depend on the nesting depth of iterators and conditionals. Unfortunately, a detailed discussion is beyond the scope of ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science, 167(10), Oct. 1996.

....since it does not build the intermediate derivation trees any more. The partial correction of the transformation by folding unfolding is obvious. The total correction is not assured in general because some inopportune foldings can introduce cases of non termination. The Improvement Theorem in [19] can be extented to a method (the extended improved unfold fold method) presented in [20] which makes it possible to show the total correction of the method proposed in this paper. Dynamic slicing analyser The denition of the dynamic slicing analyser for the logic programming language is the ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. In Theory and Practice of Software Development, TAPSOFT'95. Springer-Verlag, 1995.

....proved for regular, covariant algebraic data types [Pit98] Nonetheless these limitations are mild, because nearly all types that appear in practise are regular and covariant. 7 Related Work Wadler [Wad90] coined the term deforestation. His method is based on fold unfold transformations; see [San96] for the first proof of correctness and a recent presentation of this approach. On the other hand, there are methods like short cut deforestation that abandon the treatment of generally recursive definitions in favour of some regular form of recursion. These methods use fusion laws based on ....

D. Sands. Proving the correctness of recursionbased automatic program transformations. Theoretical Computer Science, 167(1--2):193-- 233, October 1996.

....nature than the original formalism (cf. e.g. the intelligent compilers or the method to find procedural solutions for recursive function definition) For a long time, the necessity of proving the correctness of transformation strategies was neglected. Recently, this topic has been dicussed in [San95a, San95b]. There, he presents a tool for proving the correctness of existing transformation methods for higher order functional programs and a simple syntactic method for guiding and constraining the unfold fold method. In this paper we present a transformation strategy which eliminates primitive ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. In P. Mosses, M. Nielsen, and M. Schwartzbach, editors, Sixth International Joint Conference on Theory and Practice of Software Development (TAPSOFT), volume 915 of Lecture Notes in Computer Science, pages 681--695. Springer-Verlag, 1995.

....correctness, it is easily proved that each step of the transformation rules preserves normal order graph reduction semantics; extending rigorously the proof to account for folding is more involved. A general technique due to Sands [71] can be used to prove this for (positive) supercompilation, see [70]. 3.4 Discussion of the Algorithm A number of choices are left open or settled in an arbitrary way in our algorithm. First, our algorithm follows Turchin s generalization principle [89] which states that a generalization between two terms has a meaning only in the context of the computation ....

D. Sands. Proving the correctness of recursion-based automatic program transformation. In P. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, Theory and Practice of Software Development, vol. 915 of LNCS, pages 681--695. SpringerVerlag, 1995.

....role of such specifications in their work on the correctness of binding time analysis. Specializers have mostly been specified as symbolic interpreters in functional style [42] We note, however, a recent trend (including the present work) to use operational semantics for specifying specializers [1, 18, 33, 61, 62]. In fact, the first author has shown that by emphasizing the logical character of type based and operational semantics specifications, the correctness of a partial evaluator can be mechanically verified [35] Davies and Pfenning have developed a language for expressing staged computation based on ....

David Sands. Proving the correctness of recursion-based automatic program transformations. In Peter Mosses, Mogens Nielsen, and Michael Schwartzbach, editors, Proceedings of TAPSOFT '95, number 915 in Lecture Notes in Computer Science, pages 681--695, Aarhus, Denmark, May 1995.

....the program is typable in the HindleyMilner type system, but a more efficient and transparent approach is desirable. The first formulation of deforestation applicable directly to higher order programs is due to Marlow and Wadler [36] who leave open the question of guaranteeing termination. Sands [44,46] and Nielsen and S rensen [40] give other formulations of higher order deforestation, but are concerned with other problems than ensuring termination. The first direct solution to the termination problem for higher order deforestation is due to Hamilton [24] who presents a blazed higher order ....

....equivalent to the input. That each step of the transformation rules for deforestation preserves call by need semantics is easily proved, but extending rigorously the proof to account for folding is more involved. A technique due to Sands [45,47] can be used to prove this for deforestation [44,46]. It is beyond the scope of the present paper to explain this technique. As for non degradation in efficiency, the output of deforestation should be at least as efficient as the input. There are several aspects of this problem. First, transformation can change a polynomial time program into an ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science, A(167), 1996.

....the program is typable in the HindleyMilner type system, but a more efficient and transparent approach is desirable. The first formulation of deforestation applicable directly to higher order programs is due to Marlow and Wadler [36] who leave open the question of guaranteeing termination. Sands [44,46] and Nielsen and S rensen [40] give other formulations of higher order deforestation, but are concerned with other problems than ensuring termination. The first direct solution to the termination problem for higher order deforestation is due to Hamilton [24] who presents a blazed higher order ....

....equivalent to the input. That each step of the transformation rules for deforestation preserves call by need semantics is easily proved, but extending rigorously the proof to account for folding is more involved. A technique due to Sands [45,47] can be used to prove this for deforestation [44,46]. It is beyond the scope of the present paper to explain this technique. As for non degradation in efficiency, the output of deforestation should be at least as efficient as the input. There are several aspects of this problem. First, transformation can change a polynomial time program into an ....

D. Sands. Proving the correctness of recursion-based automatic program transformation. In P. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 681--695. Springer-Verlag, 1995.

....since it does not build the intermediate derivation trees any more. The partial correction of the transformation by folding unfolding is obvious. The total correction is not assured in general because some inopportune foldings can introduce cases of non termination. The Improvement Theorem in [20] can be extented to a method (the extended improved unfold fold method) presented in [21] which makes it possible to show the total correction of the method proposed in this paper. Dynamic slicing analyser The definition of the dynamic slicing analyser for the logic programming language is the ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. In TAPSOFT. Springer-Verlag, 1995.

....semantics, the output of deforestation should be equivalent to the input. That each step of deforestation preserves call by need semantics is easily proved, but extending the proof to account for folding is more involved. A general technique due to Sands [40, 42] can be used to prove this [39, 41]. As for non degradation in efficiency, the output of deforestation should be at least as efficient as the input. First, there is the problem of avoiding duplication of computation. Transformation can change a polynomial time program into an exponential time program. This can be avoided by ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science, A(167), 1996.

....semantics, the output of deforestation should be equivalent to the input. That each step of deforestation preserves call by need semantics is easily proved, but extending the proof to account for folding is more involved. A general technique due to Sands [40, 42] can be used to prove this [39, 41]. As for non degradation in efficiency, the output of deforestation should be at least as efficient as the input. First, there is the problem of avoiding duplication of computation. Transformation can change a polynomial time program into an exponential time program. This can be avoided by ....

D. Sands. Proving the correctness of recursion-based automatic program transformation. In P. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 681--695. Springer-Verlag, 1995.

....Improvement Theorem [San96b] The Improvement Theorem for a speci c higher order functional language has been used to develop a correctness preserving variant of unfoldfold transformations (in loc. cit. as well as to give the rst correctness proofs for some well known transformation methods [San96a] Functional (bi)simulations and Coinduction Operationally based proof principles of a more standard nature are also established for gdsos languages. We show that coinductive reasoning techniques based on bisimulation (# la [Abr90, How89, Pit99, Gor95] are sound for reasoning about the various ....

.... Improvement Theorem for this version of improvement provides a much simpler correctness proof than that presented in [San95a] Space does not permit an illustration of the utility of the Improvement Theorem in establishing the correctness of program transformations; we refer the reader to [San96b, San96a] for a number of substantial applications. 7.1 Open Improvement Induction The improvement induction principle is stated for closed expressions and contexts. Our proof extends to open expressions in two important special cases, according to how improvement behaves under the application of ....

D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science, A(167), October 1996. Preliminary version in TAPSOFT'95, LNCS 915.

....are intensional properties of a program properties of how the program computes, rather that what it computes. In this section we illustrate how improvement can be used as a tool for reasoning about the running time of lazy functional programs. Improvement Theory and its Applications 11 In Sands (1990) we introduced a simple set of nave time rules, derived directly from the operational semantics. These concern equations on hei, the time to evaluate expression e to (weak) head normal form, and hei N , the time to evaluate e to normal form. One of the principal limitations of the direct ....

Sands, D. (1996a). Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science A(167), xxx--xxx. To appear. Preliminary version in TAPSOFT'95, LNCS 915.

No context found.

D. Sands. Proving the Correctness of Recursion-Based Automatic Program Transformations. In P. Mosses, M. Nielsen, and M. Schwartzbach, editors, Sixth International Joint Conference on Theory and Practice of Software Development (TAPSOFT), LNCS 915, pages 681--695. Springer-Verlag, 1995.

No context found.

Sands, D. 1995b. Proving the correctness of recursion-based automatic program transformations.

No context found.

David Sands. Proving the correctness of recursion-based automatic program transformations. In Peter Mosses, Mogens Nielsen, and Michael Schwartzbach, editors, Proceedings of TAPSOFT '95, number 915 in Lecture Notes in Computer Science, pages 681--695, Aarhus, Denmark, May 1995.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.