A semantics for tracing declarative multi-paradigm programs

ABSTRACT

We introduce the theoretical basis for tracing lazy functional logic computations in a declarative multi-paradigm language like Curry. Tracing computations is a difficult task due to the subtleties of the underlying operational semantics which combines laziness and non-determinism. In this work, we define an instrumented operational semantics that generates not only the computed values and bindings but also an appropriate data structure---a sort of redex trail---which can be used to trace computations at an adequate level of abstraction. In contrast to previous approaches, which rely solely on a transformation to instrument source programs, the formal definition of a tracing semantics improves the understanding of the tracing process. Furthermore, it allows us to formally prove the correctness of the computed trail. A prototype implementation of a tracer based on this semantics demonstrates the usefulness of our approach.

REFERENCES

• 1: E. Albert, M. Hanus, F. Huch, J. Oliver, and G. Vidal. Operational Semantics for Declarative Multi-Paradigm Languages. To appear in Journal of Symbolic Computation, 2004.
• 2: Sergio Antoy, Constructor-based conditional narrowing, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.199-206, September 05-07, 2001, Florence, Italy [doi>10.1145/773184.773205]
• 3: B. Braßel, O. Chitil, M. Hanus, and F. Huch. Observing Functional Logic Computations. In Proc. of the Sixth Int'l Symposium on Practical Aspects of Declarative Languages (PADL'04), pages 193--208. Springer LNCS 3057, 2004.
• 4: L. Byrd. Understanding the control flow of prolog programs. In Proc. of the Workshop on Logic Programming, Debrecen, 1980.
• 5: O. Chitil. A Semantics for Tracing. In 13th Int'l Workshop on Implementation of Functional Languages (IFL 2001), pages 249--254. Ericsson CSL, 2001.
• 6: Rachid Echahed , Jean-Christophe Janodet, Admissible graph rewriting and narrowing, Proceedings of the 1998 joint international conference and symposium on Logic programming, p.325-340, August 1998, Manchester, United Kingdom
• 7: A. Gill. Debugging Haskell by Observing Intermediate Data Structures. In Proc. of the 4th Haskell Workshop. University of Nottingham, 2000.
• 8: J.C. González-Moreno, M.T. Hortalá-González, F.J. López-Fraguas, and M. Rodríguez-Artalejo. An Approach to Declarative Programming based on a Rewriting Logic. Journal of Logic Programming, 40:47--87, 1999.
• 9: Michael Hanus, A unified computation model for functional and logic programming, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.80-93, January 15-17, 1997, Paris, France [doi>10.1145/263699.263710]
• 10: Michael Hanus , Christian Prehofer, Higher-order narrowing with definitional trees, Journal of Functional Programming, v.9 n.1, p.33-75, January 1999 [doi>10.1017/S0956796899003330]
• 11: M. Hanus (ed.). Curry: An Integrated Functional Logic Language. Available at: http://www.informatik.uni-kiel.de/~curry/.
• 12: John Launchbury, A natural semantics for lazy evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.144-154, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158618]
• 13: Francisco Javier López-Fraguas , Jaime Sánchez Hernández, TOY: A Multiparadigm Declarative System, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.244-247, July 02-04, 1999
• 14: H. Nilsson and P. Fritzson. Algorithmic debugging for lazy functional languages. Journal of Functional Programming, 4(3):337--370, 1994.
• 15: Henrik Nilsson , Jan Sparud, The Evaluation Dependence Tree as a Basis for Lazy FunctionalDebugging, Automated Software Engineering, v.4 n.2, p.121-150, April 1997 [doi>10.1023/A:1008681016679]
• 16: S. Peyton Jones, editor. Haskell 98 Language and Libraries : The Revised Report. Cambridge University Press, 2003.
• 17: Ehud Y. Shapiro, Algorithmic Program DeBugging, MIT Press, Cambridge, MA, 1983
• 18: Jan Sparud , Colin Runciman, Tracing Lazy Functional Computations Using Redex Trails, Proceedings of the9th International Symposium on Programming Languages: Implementations, Logics, and Programs: Including a Special Trach on Declarative Programming Languages in Education, p.291-308, September 03-05, 1997
• 19: M. Wallace, O. Chitil, T. Brehm, and C. Runciman. Multiple-View Tracing for Haskell: a New Hat. In Proc. of the 2001 ACM SIGPLAN Haskell Workshop. Universiteit Utrecht UU-CS-2001-23, 2001.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Languages, Theory

Keywords:
functional logic programming, semantics, tracing