**The Structure of the System**
CFLP is a distributed software system for solving systems of equational goals in theories that can be represented as sets
of conditional rewrite rules over a term algebra whose signature is extended with external operators. The external operators
are used for expressing constraints over various domains. The system consists of three components:
- an interpreter based on a higher-order lazy narrowing calculus
**C**
- a cooperative constraint solver consisting of
- a scheduler which implements a strategy
**S** for solver cooperation
- various specialized constraint solvers
The general architecture of the system is depicted below.
**Figure ****1****. **The architecture of CFLP.
**The Interpreter**
The CFLP interpreter is designed to solve systems of equations between simply-typed -terms in theories axiomatized by finite sets of conditional rewrite rules of a certain kind, called *pattern rewrite rules*.
Roughly speaking, simply-typed -terms are analogous to the `Function` construct of *Mathematica*, modulo the following differences.
1. The keyword `Function` is replaced with the keyword . 2. Each such construct (which we will henceforth call a *-term*) should be well-typed, that is, a type can be inferred from the types of its base components (variables, constants, and function
symbols).
The current version of CFLP recognizes the following base types:
and the following constructed types:
For lists, we have adopted both the *Mathematica* notation `{` `}` to represent a list with elements , and the Prolog-like notation `[H|T]` to represent a list with head H and tail T.
The CFLP interpreter is based on a higher-order lazy narrowing calculus C for pattern rewrite systems [3] extended to handle also conditional pattern rewrite systems [4]. The underlying calculus essentially consists of the unification rules of higher-order patterns [5] and the lazy narrowing rules. Since the search space of such a calculus is extremely large, we have implemented a couple
of refinements with smaller search space for solutions, which are sound and complete for classes of functional logic programs
and of practical interest.
We have extended these calculi in two main directions: 1. the possibility to specify *constraints*, that is, equations that cannot be solved by narrowing, but for which specialized solvers are available; and 2. the possibility to specify explicit OR-parallelism.
The interpreter successively decomposes the goal toward an answer substitution by applying the inference steps of the underlying
lazy narrowing calculus. The only equations that cannot be solved in this way are the constraints. The constraints generated
upon derivations are collected and sent to be solved by specialized constraint solvers via the component called the *scheduler* (see Figure 1).
Note that the nondeterministic selection of a rewrite rule for a defined symbol and the explicit OR-formulas cause the initial
goal to be reduced to disjoint sets of constraints that can be solved in parallel. Thus, in the last illustrative example,
the reduction of the initial goal
involves the decomposition of the equation into simpler equations. The transformation step performed by our lazy narrowing calculus is
where X0, Y0 are new variables. In this step we have used the fresh variant
of the rewrite rule which defines f.
During step (2), an OR-subgoal is produced and as a result the initial goal is finally decomposed into two disjoint sets of
constraints. These sets of constraints are sent to be solved to the scheduler.
**The Scheduler**
The scheduler coordinates the process of solving the systems of constraints received from the interpreter. In order to solve
these sets of constraints, the constraint scheduler maintains a dynamic data structure called a *constraint tree*. The nodes of the constraint tree are pairs of the form where is a substitution and *cs* is a set of constraints.
Whenever a set of constraints *cs* is received from the interpreter, the scheduler adds a new son to the root of the constraint tree. Here stands for the empty substitution. The scheduler expands this tree by applying constraint-solving methods in parallel to
its leaf nodes.
A leaf node is expanded with respect to a method *m* as follows.
1. *cs* is decomposed into a set of constraints to which method *m* can be applied, and a set of other constraints. 2. is sent to be solved to a constraint solver which implements method *m*. We call such a solver an m-solver. 3. If the *m*-solver detects inconsistent, then the node is marked as inconsistent. Otherwise the *m*-solver returns if it cannot reduce , or it computes a finite sequence of pairs with the property that is a solution of *cs* if and only if there exists a solution of some , such that . 4. If the sequence is computed by the *m*-solver, then the nodes are added to the constraint tree as sons of the node .
A node is *final* if it cannot be reduced by any *m*-solver which is available.
The implementation of the scheduling algorithm is inspired by the work of Hong [6]. The scheduler can be regarded as a component parameterized with a list of constraint-solving methods. The scheduler implements a cooperation strategy S, which repeatedly applies the sequence of methods to the leaves of the constraint tree until they become either final or inconsistent. As soon as a final node is
generated, it is made accessible to the interpreter.
**The Constraint Solvers**
The constraint solvers are implementations of the constraint-solving methods specified to the scheduler through the list **M**. The current implementation of CFLP provides constraint solvers, which implement the following methods for solving constraints
over the domains of real and complex numbers.
These methods are tried in the order presented.
All solvers are implemented by separate *Mathematica* processes executing in parallel and communicating with the constraint scheduler via *MathLink* connections. There are two types of constraint solvers in CFLP.
1. Local constraint solvers that run as subsidiary *Mathematica* processes of the CFLP constraint scheduler. 2. Shared constraint solvers are started from outside a CFLP session and can be connected later to more CFLP schedulers,
which may run on a different machine.
The user can adjust the distributed constraint-solving component of the system by specifying the number of local constraint
solvers that are started at system initialization, and the remote machines on which to look for shared constraint solvers.
The communication mechanism between scheduler and constraint solvers is implemented completely in *MathLink* [7]. Therefore, CFLP is a platform-independent software system and can be used in heterogeneous networks.
Copyright © 2001 Wolfram Media, Inc. All rights reserved.[Article Index][Prev Page][Next Page] |