A semantics for tracing declarative multi-paradigm programs

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 ion. 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. Categories and Subject Descriptors

• Type: Conference
• Year: 2004
• Where: PPDP
• Authors: Bernd Brassel, Michael Hanus, Frank Huch, Germán Vidal
• Keywords: Computations, Instrumented Operational Semantics, Operational Semantics, PPDP 2004