FAQ: What features does lambda Prolog have?

What features does lambda Prolog have?

Polymorphic typing

lambda Prolog is a strongly typed language. Its typing was inspired by that of ML, but in details it is quite different. Variables are allowed in types, and this provides for generic polymorphism (as in, say, ML) and certain forms of ad hoc polymorphism (types can have significance at run-time).

All constants must be declared to be of a type, although various implementations may try to help the programmer infer those types. The Terzo system, for example, does not do type inference for constants (only for variables): it seems not to be a burden for programmers to explicitly type constants once per module. Such explicit declarations are a useful part of the documentation of a module.

Sound unification

Unification in lambda Prolog is sound: in particular, the occurs-check is made on first-order terms. In the presence of higher-order variables, the straightforward generalization for the occurs-check is not complete. As a result, lambda Prolog implements something called the ``rigid-path'' check: in the first-order case, this generalizes the occurs-check. This check does not lose completeness.

Implicational and universal quantified queries

Allowing implications and universal quantifiers in queries and the body of clauses is the essential logical difference between lambda Prolog and Prolog (apart from the orthogonal difference regarding quantification at higher-order types). When Horn clauses are generalized to allow such occurrences of these connectives, we have the class of formulas known as ``hereditary Harrop formulas''. These two connectives allow for hypothetical and generic queries, and they are responsible for producing the dynamic behaviour of lambda Prolog's runtime that is exploited for modular programming and abstract data types.

Modular programming

lambda Prolog code is organized into modules. Modules can incorporate other modules by accumulating or importing. The precise semantics of these module constructs are given by the underlying logic. In principle, these module directives can be removed so that a module always denotes a (possibly large) formula of intuitionistic logic.

Abstract data types

Using lambda Prolog's rich quantification, it is also possible to hide constants within a module. The local directive is used for this pursue. Such hiding can be used to support abstract data types.

Higher-order programming

Quantification over some predicate variables is allowed in lambda Prolog. Such quantification provides a simple and natural way to do higher-order programming: predicate expressions can be built and applied in much the same way that functional programming languages can build and apply functions. Some examples are available.

Simply-typed lambda-terms

The term structure of lambda Prolog is based on simply typed lambda-terms and not on the simpler first-order terms. As a result, lambda-abstractions can be used to represent bound variables in data items, a common situation in the implementation of meta-programming tasks, such as theorem provers, program transformers, and type checkers/inferers.

Unification of lambda-terms

Because lambda-terms are present, unification in lambda Prolog must unify them. To do that, a form of depth-first search applied to higher-order unification is implemented in a lambda Prolog interpreter. Since higher-order unification is undecidable, such an implementation is incomplete and simple example of unification can easily lead to a loop in the interpreter. Even when unifiers exist and can be found by the simple interpreter of the system, there may not be a simple most general unifier. Thus, an interpreter will need to backchain over choices of unifiers.

While these aspects of full higher-order unification are indeed complex and questionable elements of the core of a programming language, lots of experience with lambda Prolog code suggests that problematic unification problems do not often happen. In particular, a large percentage of unification programs generated by a wide range of examples produce unification problems contained in the L-lambda fragment of lambda Prolog: in this fragment, unification involves only higher-order patterns and these problems have properties similar to those of first-order unification. Furthermore, higher-order unification can often be reduced to this fragment via the introduction of some small logic programming to specify substitutions.

Back to the FAQ / Home