Constructive Failure in Functional-Logic Programming: From Theory to Implementation1

Functional-logic programming amalgamates some of the main features of both functional and logic styles into a single paradigm. Nevertheless, negation is a widely investigated feature in logic programming that has not received much attention in such programming style. It is not difficult to incorporate some kind of negation as finite failure for ground goals, but we are interested in a constructive version able to deal with non-ground goals. With this aim, in previous works we have built a formal framework for checking (finite) failure of reduction. In this paper we adapt it for implementing a prototype for a functional-logic language with constructive failure as the natural counterpart to negation in logic programming.