=ADD=
=reftype=
14
=number=
00-28
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2000/00-28.ps.gz
=year=
2000
=month=
07
=author=
Marin; Mircea
=title=
Functional Logic Programming with Distributed Constraint Solving
=abstract=
The main goal of the thesis is the design of efficient calculi that can serve
as operational semantics of a higher-order functional logic programming
language with constraint solving capabilities.

The main advantages of higher-order logic versus first-order logic are
quantification over functions and predicates and its abstraction mechanism.
Higher-order programming is standard in functional programming
languages, and recent languages as $\lambda$-Prolog illustrate the practical
utility of higher-order logic programming. Currently, functional logic
programming is mainly restricted to first-order logic, although recent years
witnessed a growing interest to extend the operational principles of functional
logic programming to higher-order logic.

In this thesis we present various lazy narrowing calculi for higher-order
logic. We prove that our calculi satisfy essential properties, such as being
sound and complete, if the functional logic program satisfies certain restrictions.
In general, the restrictions investigated by us are widely accepted 
by the functional logic community, or are higher-order generalizations of
restrictions which are standard in first-order functional logic programming.

We claim that the calculi proposed in the thesis are better choices for an
operational semantics of higher-order functional logic programming than
what we found in the literature.

Secondly, in order to improve the solving capability of a higher-order
functional logic programming language, we aim at integrating the operational
principles of higher-order lazy narrowing and of concurrent constraint
solving.
Concurrent constraint solving is already recognized as a viable approach
to integrate the constraint solving capabilities of various constraint
solvers in a system that can solve problems that none of the single solvers
can handle alone.

We define a scheme CFLP(X, S, C) for constraint logic programming,
which describes the integration of a higher-order lazy narrowing calculus C
(the functional logic component) with the operational principle of a solver
cooperation over a constraint domain X. The solver cooperation is defined
by a collection of constraint solvers CS1, ..., CSn, which cooperate upon
solving a given problem in accordance with a strategy S.

Next, we describe an experimental system written in Mathematica,
which is the implementation of an instance of the scheme described by
us. The system is called CFLP, and it consists of a functional logic
interpreter running on one machine, and a distributed constraint solving
subsystem. The distributed constraint solving subsystem consists of a number
of constraint solvers running on possibly different machines and a special
component called constraint scheduler, vhich implements the strategy S to
coordinate the solver cooperation.

Finally, we illustrate the behaviour and utility of CFLP with several
example programs.
=keywords=
automated theorem proving
=sponsor=
The Theorema Project, the project "Distributed Constraint Solving for Functional Logic Programming" (AITEC Contract Res. Programme), Grant-in-Aid for Sci. Res. on Priority Areas, Grant-in-Aid for Sci. Res. (B) 10480053.