Equivalence of Two Formal Semantics for Functional Logic Programs 1

A distinctive feature of modern functional logic languages like Toy or Curry is the possibility of programming non-strict and non-deterministic functions with call-time choice semantics. For almost ten years the CRWL framework [J.C. González-Moreno, T. Hortalá-González, F. López-Fraguas, and M. Rodríguez-Artalejo. A rewriting logic for declarative programming. In Proc. European Symposium on Programming (ESOP'96), pages 156–172. Springer LNCS 1058, 1996, J.C. González-Moreno, T. Hortalá-González, F. López-Fraguas, and M. Rodríguez-Artalejo. An approach to declarative programming based on a rewriting logic. Journal of Logic Programming 40(1):47–87, 1999] has been the only formal setting covering all these semantic aspects. But recently [E. Albert, M. Hanus, F. Huch, J. Oliver, and G. Vidal. Operational semantics for declarative multi-paradigm languages. Journal of Symbolic Computation 40(1):795–829, 2005] an alternative proposal has appeared, focusing more on operational aspects. In this work we investigate the relation between both approaches, which is far from being obvious due to the wide gap between both descriptions, even at syntactical level.