Declarative debugging of functional logic programs

Functional logic programming combines languages which integrate some of the best features of the classical declarative paradigms, namely functional and logic programming. Recent results show that the advantages of these styles can be efficiently and usefully combined into a single language. The operational semantics of integrated languages is usually based on narrowing, a combination of unification for parameter passing and reduction as evaluation mechanism which subsumes rewriting and SLD-resolution.; The debugging can be formulated in a declarative or procedural way. The main contribution of this thesis is the development of a declarative diagnosis method w.r.t. computed answers for functional logic programs. The conditions which we impose on the programs which we consider allow us to define a generic framework for declarative debugging which is parametric w.r.t. narrowing strategy. In particular, it both works for eager narrowing as well as for lazy narrowing. We associate a (continuous) immediate consequence operator to our programs which is parametric w.r.t. narrowing strategy $4$. We prove that, the answer substitutions computed by narrowing w.r.t. $4$ can be obtained by standard unification with the equations in the (fixpoint) semantics. We construct the operational semantics, $O4R$, and then we establish the relation between the fixpoint semantics and this operational semantics. Then we show that, given the intended specification of a program $I$, it is possible to check the correctness and completeness of $R$ by a single step of the immediate consequence operator. Then we present by approximating the intended specification of the success set. We use over and under specifications $I+$ and $I-$ to correctly over- (resp. under-) approximate the intended semantics. The basic methodology presented so far has been implemented by a prototype system BUGGY which includes a parser for a conditional functional logic language which can be executed by leftmost innermost narrowing, (innermost) basic narrowing, leftmost outermost narrowing and needed narrowing. Moreover, in the natural extending, then we present an algorithm for automatic program correction which is based on unfolding/folding and is able to automatically infer the correct rules from evidence.