Abstract
In an earlier paper, one of the present authors presented a preliminary account of an equational logic called Pim. Pim is intended to function as a “transformational toolkit” to be used by compilers and analysis tools for imperative languages, and has been applied to such problems as program slicing, symbolic evaluation, conditional constant propagation, and dependence analysis. Pim consists of the untyped lambda calculus extended with an algebraic rewriting system that characterizes the behavior of lazy stores and generalized conditionals. A major question left open in the earlier paper was whether there existed a complete equational axiomatization of Pim's semantics. In this paper, we answer this question in the affirmative for Pim's core algebraic component, Pim t, under the assumption of certain reasonable restrictions on term formation. We systematically derive the complete Pim logic as the culmination of a sequence of increasingly powerful equational systems starting from a straightforward “interpreter” for closed Pim terms.
This work was supported in part by the European Communities under ESPRIT Basic Research Action 7166 (CONCUR II) and the Netherlands Organization for Scientific Research (NWO) under the Generic Tools for Program Analysis and Optimization project.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ammarguellat, Z. A control-flow normalization algorithm and its complexity. IEEE Transactions on Software Engineering 18, 3 (March 1992), 237–251.
Ballance, R. A., Maccabe, A. B., and Ottenstein, K. J. The program dependence Web: A representation supporting control-, data-, and demand-driven interpretation of imperative languages. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (White Plains, NY, June 1990), pp. 257–271.
Barendregt, H., van Eekelen, M., Glauert, J., Kennaway, J., Plasmeijer, M., and Sleep, M. Term graph rewriting. In Proc. PARLE Conference, Vol. II: Parallel Languages (Eindhoven, The Netherlands, 1987), vol. 259 of Lecture Notes in Computer Science, Springer-Verlag, pp. 141–158.
Bergstra, J., Dinesh, T., Field, J., and Heering, J. A complete transformational toolkit for compilers. Report CS-R9601, CWI, Amsterdam, January 1996; also Report RC 20342, IBM T.J. Watson Reseach Center, January 1996.
Bergstra,J., and Heering, J. Which data types have ω-complete initial algebra specifications? Theoretical Computer Science 124 (1994), 149–168.
Boehm, H.-J. Side effects and aliasing can have simple axiomatic descriptions. ACM Trans. on Programming Languages and Systems 7,4 (October 1985), 637–655.
Cartwright, R., and Felleisen, M. The semantics of program dependence. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (Portland, OR, June 1989), pp. 13–27.
Click, C. Global code motion, global value numbering. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (La Jolla, CA, June 1995), pp. 246–257. Published as ACM SIGPLAN Notices 30(6).
Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., and Zadeck, F. K. Efficiently computing static single assignment form and the control dependence graph. ACM Trans. on Programming Languages and Systems 13, 4 (October 1991), 451–490.
Dershowitz, N., and Jouannaud, J.-P. Rewrite systems. In Handbook of Theoretical Computer Science, Vol. B, Formal Models and Semantics, J. van Leeuwen, Ed. Elsevier/The MIT Press, 1990, pp. 243–320.
Felleisen, M., and Friedman, D. P. A syntactic theory of sequential state. Theoretical Computer Science 69 (1989), 243–287.
Ferrante, J., Ottenstein, K. J., and Warren, J. D. The program dependence graph and its use in optimization. ACM Trans. on Programming Languages and Systems 9, 3 (July 1987), 319–349.
Field, J. A simple rewriting semantics for realistic imperative programs and its application to program analysis. In Proc. ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (San Francisco, June 1992), pp. 98–107. Published as Yale University Technical Report YALEU/DCS/RR-909.
Field, J., Ramalingam, G., and Tip, F. Parametric program slicing. In Proc. Twenty-second ACM Symp. on Principles of Programming Languages (San Francisco, January 1995), pp. 379–392.
Fraus, U. Inductive theorem proving for algebraic specifications—TIP system user's manual. Tech. Rep. MIP 9401, University of Passau, 1994. The TIP system is available at URL: ftp://forwiss.uni-passau.de/pub/local/tip.
Garland, S., and Guttag, J. A Guide to LP, The Larch Prover. Tech. Rep. 82, Systems Research Center, DEC, Dec 1991.
Heering, J. Partial evaluation and ω-completeness of algebraic specifications. Theoretical Computer Science 43 (1986), 149–167.
Hoare, C., Hayes, I., Jifeng, H., Morgan, C., Roscoe, A., Sanders, J., Sorensen, I., Spivey, J., and Sufrin, B. Laws of programming. Communications of the ACM 30, 8 (August 1987), 672–686.
Jones, N., Gomard,C., and Sestoft, P. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.
Klop, J. Term rewriting systems. In Handbook of Logic in Computer Science, Vol. II, S. Abramsky, D. Gabbay, and T. Maibaum, Eds. Oxford University Press, 1992, pp. 1–116.
Lazrek, A., Lescanne, P., and Thiel, J.-J. Tools for proving inductive equalities, relative completeness, and ω-completeness. Information and Computation 84 (1990), 47–70.
Mason. I. A., and Talcott, C. Axiomatizing operational equivalence in the presence of side effects. In Proc. Fourth IEEE Symp. on Logic in Computer Science (Cambridge, MA, March 1989), pp. 284–293.
Meseguer, J., and Goguen, J. Initiality, induction and computability. In Algebraic Methods in Semantics, M. Nivat and J. Reynolds, Eds. Cambridge University Press, 1985, pp. 459–541.
Odersky, M., Rabin, D., and Hudak, P. Call by name, assignment, and the lambda calculus. In Proc. Twentieth ACM Symp. on Principles of Programming Languages (Charleston, SC, January 1993), pp. 43–56.
Swarup, V., Reddy, U., and Ireland, E. Assignments for applicative languages. In Proc. Fifth ACM Conf. on Functional Programming Languages and Computer Architecture (August 1991), vol. 523 of Lecture Notes in Computer Science, Springer-Verlag, pp. 192–214.
Weise, D., Crew, R., Ernst, M., and Steensgaard, B. Value dependence graphs: Representation without taxation. In Proc. Twenty-First ACM Symp. on Principles of Programming Languages (Portland, OR, January 1994), pp. 297–310.
Yang, W, Horwitz, S., and Reps, T. Detecting program components with equivalent behaviors. Tech. Rep. 840, University of Wiconsin-Madison, April 1989.
Yang, W., Horwitz, S., and Reps, T. A program integration algorithm that accommodates semantics-preserving transformations. In Proc. Fourth ACM SIGSOFT Symp.on Software Development Environments (Irvine, CA, December 1990),pp. 133–143.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bergstra, J.A., Dinesh, T.B., Field, J., Heering, J. (1996). A complete transformational toolkit for compilers. In: Nielson, H.R. (eds) Programming Languages and Systems — ESOP '96. ESOP 1996. Lecture Notes in Computer Science, vol 1058. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61055-3_31
Download citation
DOI: https://doi.org/10.1007/3-540-61055-3_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61055-7
Online ISBN: 978-3-540-49942-8
eBook Packages: Springer Book Archive