A pragmatic reconstruction of Lambda-Prolog

Catherine Belleannee (1) , Pascal Brisset (2) , Olivier Ridoux (3)

1 Dyliss - Dynamics, Logics and Inference for biological Systems and Sequences
2 ENAC - Ecole Nationale de l'Aviation Civile
3 LIS - Logical Information Systems

Lambda-Prolog is a logic programming language in which hereditary Harrop formulas generalize Horn formulas, and simply typed lambda-terms generalize Prolog terms. One may wonder if these extensions are simultaneously required, and if useful subsets of lambda-Prolog can be defined, at least for pedagogical purposes. We answer this question by exhibiting a network of necessity links between the new features of lambda-Prolog. The starting point of the network is the demand for programming by structural induction on lambda-terms, and the necessity links give a rationale for such a programming style.

Mots clés: quantifications; typing; prolog; logic programming; lambda calculus; types; induction

Domaines: Optimisation et contrôle [math.OC]

Catherine Belleannee, Pascal Brisset, Olivier Ridoux. A pragmatic reconstruction of Lambda-Prolog. Journal of Logic Programming, 1999, 41 (1), pp 67-102. ⟨10.1016/S0743-1066(98)10038-9⟩. ⟨hal-00934033⟩