Infinite Unfolding and Transformations of Nondeterministic Programs

• Autorzy: Lisper B.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

logic programming; computer programming; functional programming languages; functional programming; programming languages

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 66, nr 4
• Strony: 415--439
• Opis fizyczny: Bibliogr. 51 poz.

Twórcy

autor

Lisper B.

• Dept.of Computer Science and Electronics Mälardalen University P.O.Box 883, SE-721 23 Västeräs, Sweden

Bibliografia

• [1] Abramsky, S.: The Lazy Lambda Calculus, in: Research Topics in Functional Programming (D. A. Turner, Ed.), The UT Year of Programming Series, chapter 4, Addison-Wesley, Reading, MA, 1989, 65–116.
• [2] Albert, E., Alpuente, M., Falaschi, M., Julián, P., Vidal, G.: Improving Control in Functional Logic Program Specialisation, Proc. 5th Int. Symposium on Static Analysis (G. Levi, Ed.), 1503, Springer-Verlag, Pisa, Italy, September 1998.
• [3] Alpuente, M., Falaschi, M., Julián, P., Vidal, G.: Specialization of lazy functional logic programs, Proc. 1997 ACM SIGPLAN symposium on Partial Evaluation and Semantics-based Program Manipulation, ACM, Amsterdam, The Netherlands, June 1997.
• [4] Alpuente, M., Falaschi, M., Vidal, G.: Narrowing-driven Partial Evaluation of Functional Logic Programs, Proc. 6th European Symposium on Programming (H. R. Nielson, Ed.), 1058, Springer-Verlag, Linköping, Sweden, April 1996.
• [5] Ariola, Z. M., Arvind: Properties of a First-Order Functional Language with Sharing, Theoret. Comput. Sci., 146, 1995, 69–108.
• [6] Ariola, Z. M., Felleisen, M.: The Call-by-need Lambda Calculus, J. Functional Programming, 7(3), May 1997, 265–301.
• [7] Arnold, A., Naudin, P., Nivat, M.: On Semantics of Nondeterministic Recursive Program Schemes, in: Algebraic Methods in Semantics (M. Nivat, J. C. Reynolds, Eds.), chapter 1, Cambridge University Press, 1985, 1–33.
• [8] Barendregt, H. P.: The Lambda Calculus – Its Syntax and Semantics, vol. 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1981.
• [9] Bertolino, M., Etalle, S., Palamidessi, C.: The Replacement Operation for CCP Programs, Proc. 9th Int. Workshop on Logic-Based Program Synthesis and Transformation (A. Bossi, Ed.), 1817, Springer-Verlag, Venice, Italy, September 1999.
• [10] Bossi, A., Cocco, N.: Preserving Universal termination through Unfold/fold, Proc. Fourth Int. Conf. on Algebraic and Logic Programming (G. Levi, M. Rodriguez-Artalejo, Eds.), 850, Springer-Verlag, 1994.
• [11] Bossi, A., Cocco, N.: Replacement can Preserve Termination, Proc. Int. Workshop on Logic-Based Program Synthesis and Transformation (J. Gallagher, Ed.), 1207, Springer-Verlag, 1996.
• [12] Bossi, A., Cocco, N., Etalle, S.: Transformation of Left-Terminating Programs, Proc. 9th Int. Workshop on Logic-Based Program Synthesis and Transformation (A. Bossi, Ed.), 1817, Springer-Verlag, Venice, Italy, September 1999.
• [13] Boudol, G.: Computational Semantics of Term Rewriting Systems, in: Algebraic Methods in Semantics (M. Nivat, J. C. Reynolds, Eds.), chapter 5, Cambridge University Press, 1985, 170–236.
• [14] Burstall, R. M., Darlington, J.: A transformation system for developing recursive programs, J. Assoc. Comput. Mach., 24(1), January 1977, 44–67.
• [15] Courcelle, B.: Infinite Trees in Normal Form and Recursive Equations Having a Unique Solution, Math. System. Theory, 13, 1979, 131–180.
• [16] Courcelle, B.: Equivalence and Transformations of Regular Systems, Theoret. Comput. Sci., 42, 1986, 1–122.
• [17] Courcelle, B.: Recursive Applicative Program Schemes, in: Handbook of Theoretical Computer Science (J. van Leeuwen, Ed.), chapter 9, Elsevier Science Publishers B. V., 1990, 459–492.
• [18] De Francesco, N., Santone, A.: A transformation system for concurrent processes, Acta Inform., 35(12), 1998, 1037–1073.
• [19] Etalle, S., Gabbrielli, M., Meo, M. C.: Transformations of CCP Programs, ACM Trans. Program. Lang. Syst., 23(3),May 2001.
• [20] Gengler, M., Martel, M.: Self-applicable partial evaluation for the pi-calculus, Proc. 1997 ACM SIGPLAN symposium on Partial Evaluation and Semantics-based Program Manipulation, ACM, Amsterdam, The Netherlands, June 1997.
• [21] Goguen, J. A., Thatcher, J. W., Wagner, E. G., Wright, J. B.: Initial Algebra Semantics and Continuous Algebras, J. Assoc. Comput. Mach., 24(1), January 1977, 68–95.
• [22] Hosoya, H., Kobayashi, N., Yonesawa, A.: Partial Evaluation Scheme for Concurrent Languages and its Correctness, Proc. Second International Euro-Par Conference (L. Bougé, P. Fraigniaud, A. Mignotte, Y. Robert, Eds.), 1123, Springer-Verlag, Lyon, France, August 1996.
• [23] Johnsson, T.: Lambda Lifting: Transforming Programs to Recursive Equations, Proc. Functional Programming Languages and Computer Architecture (J.-P. Jouannaud, Ed.), 201, Springer-Verlag, Berlin, Nancy, France, September 1985.
• [24] Kanamori, T., Fujita, H.: Unfold/fold Transformations of Logic Programs with Counters, Tech. Rep. ICOT TR-179, ICOT Research Center, Tokyo, Japan, 1986.
• [25] Kawamura, T., Kanamori, T.: Preservation of Stronger Equivalence in Unfold/fold Logic Program Transformation, Theoret. Comput. Sci., 73(1), 1990, 139–154.
• [26] Kennaway, R., Klop, J. W., Sleep, R., de Vries, F.-J.: Transfinite Reductions in Orthogonal Term Rewriting Systems, Information and Computation, 119(1),May 1995, 18–38.
• [27] Klop, J. W.: Combinatory Reduction Systems, Ph.D. Thesis, CWI, Amsterdam, 1980, Mathematical Centre Tracts Nr. 127.
• [28] Klop, J. W.: Term Rewriting Systems, in: Handbook of Logic in Computer Science, vol. 2 (S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, Eds.), chapter 1, Oxford University Press, Oxford, 1992, 1–116.
• [29] Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory Reduction Systems: Introduction and Survey, Theoret. Comput. Sci., 121, 1993, 279–308.
• [30] Kott, L.: Unfold/fold Program Transformations, in: Algebraic Methods in Semantics (M. Nivat, J. C. Reynolds, Eds.), chapter 12, Cambridge University Press, 1985, 411–434.
• [31] Kutzner, A., Schmidt-Schauß,M.: A Non-Deterministic Call-by-Need Lambda Calculus, Proc. International Conference on Functional Programming, ACM, Baltimore, MA, 1998.
• [32] Lévy, J.-J.: An Algebraic Interpretation of the λβK-calculus; and an application of a labeled λ-calculus, Theoret. Comput. Sci., 2(1), 1976, 97–114.
• [33] Lisper, B.: Computing in Unpredictable Environments: Semantics, Reduction Strategies, and Program Transformations, Theoret. Comput. Sci., 190(1), January 1998, 61–85.
• [34] Maraist, J., Odersky, M., Wadler, P.: The Call-by-need Lambda Calculus, J. Functional Programming, 8(3), May 1998, 275–317.
• [35] Marinescu, M., Goldberg, B.: Partial-evaluation techniques for concurrent programs, Proc. 1997 ACM SIGPLAN symposium on Partial Evaluation and Semantics-based Program Manipulation, ACM, Amsterdam, The Netherlands, June 1997.
• [36] McCarthy, J.: A basis for a mathematical theory of computations, in: Computer Programming and Formal Systems (P. Braffort, D. Hirschberg, Eds.), North-Holland, 1963, 33–70.
• [37] Moran, A. K.: Call-by-name, Call-by-need, and McCarthy’s Amb, Ph.D. Thesis, Department of Computing Science, Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden, September 1998.
• [38] Moran, A. K., Sands, D., Carlsson, M.: Erratic Fudgets: A Semantic Theory for an Embedded Coordination Language, Proc. Coordination’99, 1999.
• [39] Nivat, M.: On the Interpretation of Recursive Polyadic Program Schemes, Symposia Mathematica, 15, 1975, 255–281.
• [40] van Oostrom, V.: Private communication.
• [41] Proietti, M., Pettorossi, A.: Semantics Preserving Transformation Rules for Prolog, Proc. ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, New Haven, CT, June 1991.
• [42] Proietti, M., Pettorossi, A.: Transforming Inductive Definitions, Proc. the 16th Int. Conf. on Logic Programming (D. D. Schreye, Ed.), MIT Press, Las Cruces, New Mexico, November 1999.
• [43] Raoult, J.-C., Vuillemin, J.: Operational and Semantic Equivalence Between Recursive programs, J. Assoc. Comput. Mach., 27(4), October 1980, 772–796.
• [44] Sahlin, D.: Partial Evaluation of AKL, Proc. First International Workshop on Concurrent Constraint Programming, Cà Dolfin, Venice, May 1995.
• [45] Sands, D.: Total Correctness by Local Improvement in the Transformation of Functional Programs, ACM Trans. Program. Lang. Syst., 18(2), March 1996, 175–234.
• [46] Seki, H.: Unfold/fold Transformations of Stratified Programs, Theoret. Comput. Sci., 86(1), 1991, 107–139.
• [47] Seki, H.: Unfold/fold Transformations of General Programs for the Well-founded Semantics, J. Logic Program., 16(1), 1993, 5–23.
• [48] Søndergaard, H., Sestoft, P.: Referential Transparency, Definiteness and Unfoldability, Acta Informatica, 27, 1990, 505–517.
• [49] Tamaki, H., Sato, T.: Unfold/fold Transformations of Logic Programs, Proc. 2nd International Logic Programming Conference (S.-Ǻ. Tärnlund, Ed.), MIT Press, Uppsala, Sweden, 1984.
• [50] Ueda, K., Furukawa, K.: Transformation Rules for GHC Programs, Proceedings of the International Conference on Fifth Generation Computer Systems. Volume 2 (I. for New Generation Computer Technology (ICOT), Ed.), Springer Verlag, Berlin, FRG, November 28–December 2 1988, ISBN 3-540-19588-0.
• [51] Wadsworth, C. P.: The Relation Between Computational and Denotational Properties for Scott’s D∞-Models of the Lambda Calculus, SIAM J. Comput., 5(3), September 1976, 488–521.