Back to the FAQ /
What features does lambda Prolog have?
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.
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.
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.
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.
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
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
Back to the FAQ /