A pragmatic reconstruction of lambda Prolog

lambda Prolog is a logic programming language in which hereditary Harrop fo rmulas generalize Horn formulas, and simply typed lambda-terms generalize P rolog terms. One may wonder if these extensions are simultaneously required , and if useful subsets of lambda Prolog can be defined, at least for pedag ogical purposes. We answer this question by exhibiting a network of necessi ty links between the new features of lambda Prolog. The starting point of t he network is the demand for programming by structural induction on lambda- terms, and the necessity links give a rationale for such a programming styl e. (C) 1999 Elsevier Science Inc. All rights reserved.