A Semantics for Tracing Declarative Multi-Paradigm Programs

Bernd Brassel, Michael Hanus, Frank Huch, and Germán Vidal

6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2004), Verona (Italy).
ACM Press, pp. 179-190, 2004.

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. Preliminary experiments with a prototype implementation of a tracer based on the instrumented semantics demonstrates the usefulness of our approach.

Available: PDF BibTeX entry

Germán Vidal