A theoretical framework for the declarative debugging of functional logic programs with lambda abstractions

In this paper, we extend the well-known Naish's declarative debugging scheme for diagnosing wrong computed answers in first-order lazy functional-logic programs to the higher-order setting of the simply typed λ-calculus, where programs are presented by conditional pattern rewrite systems. Our approach generalizes and combines declarative debugging techniques previously developed for less expressive declarative programming paradigms involving applicative rewrite rules instead of λ-abstractions and decidable higher-order unification. Debugging starts with the observation of a wrong computed answer which the user regards as incorrect w.r.t. an intended model that provides a declarative description of the program's semantics. Debugging proceeds by exploring an abridged proof tree built on a higher-order rewriting logic with λ-abstractions that provides a purely declarative view of the computation. Finally, debugging ends with the detection of a defined function rule in the program that is incorrect w.r.t. the intended model. We prove the logical correctness of the debugging method for any sound goal solving system whose computed answers are logical consequences of the program.