D. Sands. Total Correctness by Local Improvement in Program Transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 221--232. ACM Press, 1995.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....(a subprogram of) the resulting program to be termiiatiig [5] In the Functional Programming Area Without pretending to be exhaustive, we want to mention a recent paper on the replacement operation for functional programs which, independently, follows sub stantially the same approach we do. In [86], Sands guarantees total correctness by requiring firstly the replacing expression to be equivalent to the replaced one and secondly by avoiding the introduction of a loop by requiring the replacing expression to be independent from the modified clause (corresponding to the method used in ....

....expression to be independent from the modified clause (corresponding to the method used in Theorem 7.2.14) or requiring the replacing expression to be an impi ovemeit over the replaced one. This clearly corresponds to the condition we give in Theorem 7.2.10. The underlying intuition given in [86] is that in this case, the evaluation of the repla cing expression converges faster than one of the replaced one, consequently, all evaluations will converge faster in the transformed program than in the original one and, parallelly, no dangerous loop may be introduced. Concluding remarks We ....

D. Sands. Total correctness by local improvement in program transformation. In Procccdigs of the 22d Aual ACM SIGPLAN-SIGACT Symposium o Prizciplcs of Programmizg Lazguagcs (POPL). ACM Press, January 1995. (To Appear).

....as the correctness foundation for data flow analysis of flowchart programs [11, 12, 31] and related research has demonstrated that a.i. can be applied to nonflowchart programs defined by denotational semantics [1, 6, 15, 20, 31, 35, 42, 51, 45, 46, 47] and structural operational semantics [13, 24, 56, 57, 58, 59, 66]. Model checking is another important applications area [8, 17, 18, 63, 64] In this paper, we survey abstract interpretation in the hierarchy of operational semantics: flowchart semantics, big step (natural) semantics, and small step semantics. We define it, explain how to do it, show how to ....

D. Sands. Total correctness by local improvement in program transformation. In Proc. 22nd Symp. on Principles of Prog. Languages, pages 221--232. ACM Press, 1995.

....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 above ....

D. Sands. Total Correctness by Local Improvement in Program Transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 221--232. ACM Press, 1995.

....correctness was guaranteed provided there the number of unfold steps is always greater than or equal to the number of fold steps, given certain conditions on the transformation. Also, Scherlis [Sch80] proposes a restriction on the use of the fold step that can guarantee total correctness. Sands [San95b] provides a general improvement theorem which can be used to guarantee correctness of higher order unfold fold based program transformation schemes. His theorem can also be used to verify that a particular transformation strictly improves the program. The generality of this system means that it ....

....to the 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 ....

D. Sands. Total correctness by local improvement in program transformation. In Symposium on Principles of Programming Languages, San Francisco, California, January 1995.

....the difficulty of understanding how to verify Burstall and Darlington s Fold Unfold transformations impeded mechanization. The total correctness of these transformations in the context of higher order functional languages was open for thirty years until Sands finally came up with a solution; see [68]. In the other approach, the goal was to have a large collection of easily mechanizable transformations specified as conditional rewriting rules; i.e. rewriting rules guaranteed to preserve correctness if conditions (limited to syntactically checkable program properties that implied semantic ....

Sands, D., Total correctness by local improvement in program transformation, pp. 221--232 in: Proceedings of the 22nd ACM Symposium on Principles of Programming Languages, January 1995.

....this problem of partial correctness. One is to suitably constrain the use of fold, for example as proposed by Kott [10] Another is to provide a separate proof of termination. Yet another is the tick algebra of Sands, which guarantees incremental improvement in performance to all transformations [17]. Besides the problem with correctness, unfold fold has a significant inconvenience in practice: a history must be kept of all versions of the program as it is being transformed (or the user must specify which versions to keep or throw away) This history is needed because a previous definition ....

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 221--232. ACM Press, 1995.

....problem of partial correctness. One is to suitably constrain the use of fold, for example as proposed by Kott [Kot85] Another is to provide a separate proof of termination. Yet another is the tick algebra of Sands, which guarantees incremental improvement in performance to all transformations [San95b]. Besides the problem with correctness, unfold fold has a significant inconvenience in practice: a history must be kept of all versions of the program as it is being transformed (or the user must specify which versions to keep or throw away) This history is essential because previous definitions ....

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 221--232. ACM Press, 1995.

....rules as well as the soundness of the strictness analysis. The former can be mirrored from the relevant work in program transformation, such as the work by Runciman for ensuring adherence to lazy semantics [RFJ89] and that by Sands to ensure total correctness of transformed programs [San95] Our strictness analysis can be considered as a simplified variant of disjunctive program analysis [Jen97] and its soundness can be proven in a similar spirit. We have so far described the mechanism for tupling functions with single recursion arguments. More work needs to be done for devising ....

David Sands. Total correctness by local improvement in program transformation. In 22nd ACM Principles of Programming Languages Conference, pages 221--232. ACM Press, January 1995.

....Next, we employ a programtransformation strategy to convert all unsafe consumers to equivalent safe ones. The transformation uses a fold unfold strategy, with generalization on expressions. We prove the termination of the transformation, and outline its total correctness using a result from Sands [San95]. The transformed functions are safe consumers of a special form, called the treeless consumer form, which has been shown to be desirable for deforestation [Chi94] and indirectly desirable for partial evaluation. Last, by arranging the function definitions according to their call graphs, we can ....

....to be obtained. A trivial violation of total correctness occurs when a function is folded against itself, as shown below: f x = x function definition Folding the right hand side of f against itself gives f x = f x The above fold step causes f to be transformed into a loop. Recently, Sands [San95] has shown that the total correctness issue can be related to improvement concerns. Informally, if a transformer can guarantee that its transformed expression e 0 is no less efficient than the original expression e (under, say, call by name semantics) then if e terminates yielding a weak ....

[Article contains additional citation context not shown here]

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the ACM SIGPLAN Symposium Principles of Programming Languages Conference, pages 221--232, New York, NY, January 1995. ACM Press.

....the output of deforestation should be semantically 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 ....

D. Sands. Total correctness by local improvement in program transformation. In Conference Record of the Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 221--232. ACM Press, 1995.

....of the conditions we presented. 8 Concluding Remarks For experts in transformations, the applicability conditions outlined in Theorem 13 are not fully surprising: similar concepts were rst employed in Logic Programming (for instance in [28, 4, 5, 7] and then applied to functional programs in [24, 25]. However, this is the rst time that they are applied to a concurrent context. To the best of our knowledge, this is the rst paper which treats the notion of replacement in a concurrent language. Acknowledgements We would like to thank the anonymous referees of LOPSTR and of APPIA GULP PRODE for ....

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, 1995.

....transformations preserve the exact semantics with the exception that unfolding by definition 16 and eliminating useless computations may make a non terminating computation terminate. Note that our transformations do not increase non termination as we do not use folding (which could be dangerous [77]) calls to incremental versions are only used to replace existing function calls. Our method also guarantees that the incremental program computes asymptotically at least as fast as computing from scratch using the original program, provided that the auxiliary information used, if any, can be ....

D. Sands. Total correctness by local improvement in program transformation. In Conference Record of the 22nd Annual ACM Symposium on Principles of Programming Languages. ACM, New York, Jan. 1995.

....the validity of the theorem. Lemma 5.2 (on equivalence) Every expression will be transformed to an equivalent expression if the higher order deforestation algorithm terminates. 2 Proof The proof of this lemma is similar to the proof of correctness of higher order deforestation given in [ 11 ] . 2 Lemma 5.3 (on higher order treeless form) Every expression in which each non linear variable is blazed at its binding occurrence and which contains only occurrences of functions with higher order treeless definitions will be transformed to a higher order treeless expression if the higher ....

....which contains only occurrences of functions with higher order treeless functions will be transformed without loss of efficiency if the higher order deforestation algorithm terminates. 2 Proof The proof of this lemma is similar to the proof of efficiency of higher order deforestation given in [ 11 ] . 2 Lemma 5.5 (on termination) The higher order deforestation algorithm will terminate for every expression which contains only occurrences of functions with higher order treeless definitions. 2 Proof In order to be able to prove that the higher order deforestation algorithm always ....

[Article contains additional citation context not shown here]

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the ACM Symposium on Principles of Programming Languages, January 1995.

....one would use to verify the correctness of a hand written cogen [20] It remains to be seen if these techniques scale up to more robust forms of partial evaluation that include sophisticated folding strategies. One approach might be to use Sand s calculus for sound fold unfold transformations [34]. The logic of Elf was not strong enough to encode the calculus soundness proof (see Theorem 2) More generally, the induction principles as required in the proofs of Theorems 1 and 3 could not be completely formalized. This manifested itself in the inabilty to mechanically guarantee the totality ....

David Sands. Total correctness by local improvement in program transformation. In Ron Cytron, editor, Proceedings of the Twenty-first Annual ACM Symposium on Principles of Programming Languages, pages 221--232, San Francisco, California, January 1995. ACM Press.

....the two compared nodes have labels that are disjoint terms. As for 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 ....

D. Sands. Total correctness by local improvement in program transformation. In 22nd Symposium on Principles of Programming Languages, pages 221--232. ACM Press, 1995.

....(a subprogram of) the resulting program to be terminating [1] In the Functional Programming Area Without pretending to be exhaustive, we want to mention a recent paper on the replacement operation for functional programs which, independently, follows substantially the same approach we do. In [36], Sands guarantees total correctness by requiring firstly the replacing expression to be equivalent to the replaced one and secondly by avoiding the introduction of a loop by ffl requiring the replacing expression to be independent from the modified clause (corresponding to the method used in ....

....expression to be independent from the modified clause (corresponding to the method used in Theorem 4.12) ffl or requiring the replacing expression to be an improvement over the replaced one. This clearly corresponds to the condition we give in Theorem 4.9. The underlying intuition given in [36] is that in this case, the evaluation of the replacing expression converges faster than one of the replaced one, consequently, all evaluations will converge faster in the transformed program than in the original one and, at the same time, no dangerous loop may be introduced. Concluding ....

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, January 1995.

....the output of deforestation should be semantically 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, ....

D. Sands. Total correctness by local improvement in program transformation. In Conference Record of the Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 221--232. ACM Press, 1995.

....of) the resulting program to be terminating [AB91] 6.2 In the Functional Programming Area Without pretending to be exhaustive, we want to mention a recent paper on the replacement operation for functional programs which, independently, follows substantially the same approach we do. In [San95] Sands guarantees total correctness by requiring, first, the replacing expression to be equivalent to the replaced one, and second, by avoiding the introduction of a loop by: ffl requiring the replacing expression to be independent from the modified clause (corresponding to the method used in ....

....of Functional and Logic Programming 1996 1 Etalle and Gabbrielli Correctness of the Replacement Operation xA ffl requiring the replacing expression to be an improvement over the replaced one. This clearly corresponds to the condition we give in Theorem 3. The underlying intuition given in [San95] is that in this case, the evaluation of the replacing expression converges faster than the evaluation of the replaced one, consequently, all evaluations will converge faster in the transformed program than in the original one and, at the same time, no dangerous loop may be introduced. 6.3 ....

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), New York, NY, January 1995. ACM Press.

.... gathered about which parts of the source program depend on known or unknown data) and a specialization phase (where constructs depending on known data are reduced away) 3,15] Recent work specifies the analysis phase using type systems [7] and the specialization phase using operational semantics [14,25,26]. The type system and operational semantics formalisms can be unified if one emphasizes their logical character: a type based analysis is a logic for deducing program properties, and an operational semantics is a logic for deducing computational steps or input output behaviour of programs. ....

.... scale up to (a) type based analyses that include conjunctive types, polymorphism, and more general forms of subtyping, and (b) more robust forms of partial evaluation that include sophisticated folding strategies (one approach might be to use Sand s calculus for sound fold unfold transformations [25]) Acknowledgements Thanks to Olivier Danvy for his encouragement and comments on various drafts, and to Frank Pfenning for several stimulating conversations and for providing easy access to his materials on Elf. Robert Gluck, Kristian Nielsen, David Sands, and other members of the DIKU TOPPS ....

David Sands. Total correctness by local improvement in program transformation. In Ron Cytron, editor, Proceedings of the Twenty-first Annual ACM Symposium on Principles of Programming Languages, pages 221--232, San Francisco, California, January 1995. ACM Press.

....As for preservation of operational 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 ....

D. Sands. Total correctness by local improvement in program transformation. In Conference Record of the Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 221--232. ACM Press, 1995.

....point because many transformations are cited as being instances of this class. 2 A Solution, in Principle To obtain total correctness without losing the local, stepwise character of program transformation, it is clear that a stronger condition than extensional equivalence is necessary. In [29] we presented such a condition, improvement. The Improvement Theorem states that if the local steps of a transformation are improvements, in a formal sense, then the transformation will be correct, and, a fortiori, will yield an improved program. The improvement relation is defined in terms of ....

....an improvement over another if in all program contexts it terminates at least as often, but never requires a greater number of function calls in order to do so. The method applies to call by name and call by value functional languages, including higher order functions and lazy data structures. In [29] the improvement theorem was used to design a method for restricting the unfold fold method, such that correctness and improvement are guaranteed. It is also claimed that the improvement theorem has practical value in proving the correctness without need for further restrictions of ....

[Article contains additional citation context not shown here]

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, January 1995.

....contribution of this paper is a proof of total correctness for Scherlis transformation rules in the context of a language with higherorder functions and lazy data structures. The proof itself is highly non trivial, and proved to be resilient to the techniques previously developed by the author [San94, San95b]. The basic tool for the technical development is a notion of weighted improvement: a relation which compares the relative efficiency of expressions, with respect to a given weight associated to each function definition. This is a generalisation of the notion of improvement used in [San94, ....

....[San94, San95b] The basic tool for the technical development is a notion of weighted improvement: a relation which compares the relative efficiency of expressions, with respect to a given weight associated to each function definition. This is a generalisation of the notion of improvement used in [San94, San95b], and is of independent interest. 2 Expression Procedure Transformation: An Example We introduce the rules of Scherlis transformation, in the context of a lazy higher order language, by means of a simple example. We begin with the function definitions given below: filter p xs Delta = case xs ....

[Article contains additional citation context not shown here]

D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, January 1995.

....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. (1995b). Total correctness by local improvement in program transformation.

No context found.

D. Sands. Total Correctness by Local Improvement in Program Transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 221--232. ACM Press, 1995.

No context found.

David Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 221--232. ACM Press, 1995.

No context found.

David Sands. Total correctness by local improvement in program transformation. In 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 176--234, New York, January 1995. ACM Press.

No context found.

Sands, D. 1995a. Total correctness by local improvement in program transformation. In 22nd ACM Symposium on Principles of Programming Languages, pages 221--232, ACM Press.

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.