lambda Prolog should not be seen as a mixture of functional and logic programming. While it is the case that lambda Prolog contains lambda-terms and such terms can be used to represent functional programs, the terms in lambda Prolog are simply typed and do not contain recursion or conditional. While it is possible to code up some functional computations using lambda Prolog's built-in beta-conversions, it would be hard to imagine doing general computations at that level.

One can imagine extending lambda Prolog in ways to allow for richer functional computations in terms. This would be done by enriching the equational nature of terms beyond the beta, eta-conversion rules it now has. One approach would be to add new constants with additional equations: for example, add constants to denote a fixed point constructor and a conditional and extend the equational nature of terms to include the natural equations for these constants. Another approach would be to allow new equations to be added via programs. In either case, the resulting systems would have rich and complicated unification problems in general, and would make the operational aspects of the language much more complicated then it is currently.

For example, consider the problem of finding a term F of type `int ->
int` that maps `1` to `2` and `2` to
`3`. Of course, there are an infinite number of computable
functions that satisfy these constraints. If you ask this question of
lambda Prolog, however,

?- (F 1) = 2, (F 2) = 3. no ?-the system will fail to find such a solution. The reason here is that the quanitification over

In fact, most of the programming that has been done in lambda Prolog has moved in the opposite direction of focusing on weaker equational aspects of lambda-terms. If the ``L-lambda restriction'' on free and bound variable occurrences is used, then only a weak subset of beta-conversion (called beta-0) is needed to capture the equality of lambda-terms. In that case, lambda Prolog will do unifications of only ``higher-order patterns'', which turns out to be decidable and has general unifiers. In that setting, lambda-terms are not used to represent general function as they are in functional programming language but certain kind of simple substitution operators.

Back to the FAQ / Home