Imagining CLP (Lambda, alphabeta)
Résumé
We study under which conditions the domain of lambda-terms (Lambda) and the equality theory of the lambda-calculus (alphabeta) form the basis of a usable constraint logic programming language (CLP). The conditions are that the equality theory must contain axiom eta-gamma, and the formula language must depart from Horn clauses and accept universal quantifications and implications in goals. In short, gammaCLP(lambda gamma(alphabeta) must be close to lambdaProlog.